Saturated quotients of additive commutative groups

This file packages the algebraic construction shared by relative numerical Grothendieck groups and any other quotient in which the relation subgroup must first be saturated. It belongs in the algebra layer: neither the saturation nor its universal property depends on geometry or K-theory.

def AddSubgroup.saturation {A : Type u_1} [AddCommGroup A] (H : AddSubgroup A) : AddSubgroup A

The saturation of an additive subgroup: an element belongs when a nonzero natural multiple of it belongs to the original subgroup.

Equations

• H.saturation = { carrier := {x : A | ∃ (n : ℕ), n ≠ 0 ∧ n • x ∈ H}, add_mem' := ⋯, zero_mem' := ⋯, neg_mem' := ⋯ }

@[simp]

theorem AddSubgroup.mem_saturation {A : Type u_1} [AddCommGroup A] (H : AddSubgroup A) (x : A) : x ∈ H.saturation ↔ ∃ (n : ℕ), n ≠ 0 ∧ n • x ∈ H

theorem AddSubgroup.le_saturation {A : Type u_1} [AddCommGroup A] (H : AddSubgroup A) : H ≤ H.saturation

The original subgroup is contained in its saturation.

theorem AddSubgroup.saturation_le {A : Type u_1} [AddCommGroup A] {H K : AddSubgroup A} (hHK : H ≤ K) (hK : K.NSMulSaturated) : H.saturation ≤ K

The saturation is the least saturated subgroup containing the original subgroup.

theorem AddSubgroup.saturation_nsmulSaturated {A : Type u_1} [AddCommGroup A] (H : AddSubgroup A) : H.saturation.NSMulSaturated

Saturating a subgroup produces a saturated subgroup.

@[simp]

theorem AddSubgroup.saturation_eq_self {A : Type u_1} [AddCommGroup A] {H : AddSubgroup A} (hH : H.NSMulSaturated) : H.saturation = H

@[reducible, inline]

abbrev AddSubgroup.SaturatedQuotient {A : Type u_1} [AddCommGroup A] (H : AddSubgroup A) : Type u_1

The quotient by the saturation of a subgroup.

Equations

• H.SaturatedQuotient = (A ⧸ H.saturation)

theorem AddSubgroup.saturatedQuotient_isAddTorsionFree {A : Type u_1} [AddCommGroup A] (H : AddSubgroup A) : IsAddTorsionFree H.SaturatedQuotient

Quotienting by a saturated subgroup removes all additive torsion.

This is deliberately not a global instance: matching an arbitrary type against a quotient during unrelated typeclass searches is prohibitively expensive. Consumers can install it locally when needed.

def AddSubgroup.saturatedQuotientMk {A : Type u_1} [AddCommGroup A] (H : AddSubgroup A) : A →+ H.SaturatedQuotient

The canonical map to the saturated quotient.

Equations

• H.saturatedQuotientMk = QuotientAddGroup.mk' H.saturation

@[simp]

theorem AddSubgroup.saturatedQuotientMk_eq_zero_iff {A : Type u_1} [AddCommGroup A] (H : AddSubgroup A) (x : A) : H.saturatedQuotientMk x = 0 ↔ x ∈ H.saturation

def AddSubgroup.saturatedQuotientLift {A : Type u_1} {B : Type u_2} [AddCommGroup A] [AddCommGroup B] [IsAddTorsionFree B] (H : AddSubgroup A) (f : A →+ B) (hf : H ≤ f.ker) : H.SaturatedQuotient →+ B

A map to a torsion-free group which kills the original subgroup factors through the saturated quotient.

Equations

• H.saturatedQuotientLift f hf = QuotientAddGroup.lift H.saturation f ⋯

@[simp]

theorem AddSubgroup.saturatedQuotientLift_mk {A : Type u_1} {B : Type u_2} [AddCommGroup A] [AddCommGroup B] [IsAddTorsionFree B] (H : AddSubgroup A) (f : A →+ B) (hf : H ≤ f.ker) (x : A) : (H.saturatedQuotientLift f hf) (H.saturatedQuotientMk x) = f x

def AddSubgroup.saturatedQuotientMap {A : Type u_1} {B : Type u_2} [AddCommGroup A] [AddCommGroup B] (H : AddSubgroup A) (K : AddSubgroup B) (f : A →+ B) (hf : H ≤ comap f K) : H.SaturatedQuotient →+ K.SaturatedQuotient

An additive homomorphism carrying one relation subgroup into another induces a homomorphism of saturated quotients.

Equations

• H.saturatedQuotientMap K f hf = QuotientAddGroup.map H.saturation K.saturation f ⋯

@[simp]

theorem AddSubgroup.saturatedQuotientMap_mk {A : Type u_1} {B : Type u_2} [AddCommGroup A] [AddCommGroup B] (H : AddSubgroup A) (K : AddSubgroup B) (f : A →+ B) (hf : H ≤ comap f K) (x : A) : (H.saturatedQuotientMap K f hf) (H.saturatedQuotientMk x) = K.saturatedQuotientMk (f x)

theorem AddSubgroup.saturatedQuotientHom_ext {A : Type u_1} {B : Type u_2} [AddCommGroup A] [AddCommGroup B] {H : AddSubgroup A} {f g : H.SaturatedQuotient →+ B} (h : f.comp H.saturatedQuotientMk = g.comp H.saturatedQuotientMk) : f = g

Maps out of a saturated quotient are determined on representatives.

theorem AddSubgroup.saturatedQuotientHom_ext_iff {A : Type u_1} {B : Type u_2} [AddCommGroup A] [AddCommGroup B] {H : AddSubgroup A} {f g : H.SaturatedQuotient →+ B} : f = g ↔ f.comp H.saturatedQuotientMk = g.comp H.saturatedQuotientMk

@[simp]

theorem AddSubgroup.saturatedQuotientMap_id {A : Type u_1} [AddCommGroup A] (H : AddSubgroup A) : H.saturatedQuotientMap H (AddMonoidHom.id A) ⋯ = AddMonoidHom.id H.SaturatedQuotient

theorem AddSubgroup.saturatedQuotientMap_comp {A : Type u_1} {B : Type u_2} [AddCommGroup A] {C : Type u_3} [AddCommGroup B] [AddCommGroup C] (H : AddSubgroup A) (K : AddSubgroup B) (L : AddSubgroup C) (f : A →+ B) (g : B →+ C) (hf : H ≤ comap f K) (hg : K ≤ comap g L) : (K.saturatedQuotientMap L g hg).comp (H.saturatedQuotientMap K f hf) = H.saturatedQuotientMap L (g.comp f) ⋯

Saturated-quotient maps preserve composition.