The saturated zero-charge subgroup

Definition 21.9 of arXiv:1902.08184v4 uses the saturated subgroup generated by all zero-charge classes before passing to the quotient lattice. This file constructs that subgroup for an arbitrary set of classes and proves its universal property. It also descends any charge that vanishes on the generators.

Freeness of the quotient is not inferred merely from the words "lattice": it requires the usual finite-free hypotheses on the original integral group. The declarations here isolate the saturation and descent statements that do not require those additional hypotheses.

def CategoryTheory.Triangulated.WeakStabilityCondition.Support.ZeroChargeLattice.IsSaturated {Λ : Type u_1} [AddCommGroup Λ] (H : AddSubgroup Λ) : Prop

A subgroup is saturated when membership of a nonzero natural multiple forces membership of the original element.

Equations

• CategoryTheory.Triangulated.WeakStabilityCondition.Support.ZeroChargeLattice.IsSaturated H = ∀ ⦃n : ℕ⦄ ⦃x : Λ⦄, n • x ∈ H → n = 0 ∨ x ∈ H

def CategoryTheory.Triangulated.WeakStabilityCondition.Support.ZeroChargeLattice.saturatedClosure {Λ : Type u_1} [AddCommGroup Λ] (S : Set Λ) : AddSubgroup Λ

The smallest saturated subgroup containing a set of classes.

Equations

• One or more equations did not get rendered due to their size.

theorem CategoryTheory.Triangulated.WeakStabilityCondition.Support.ZeroChargeLattice.subset_saturatedClosure {Λ : Type u_1} [AddCommGroup Λ] (S : Set Λ) : S ⊆ ↑(saturatedClosure S)

The saturated closure contains every generator.

theorem CategoryTheory.Triangulated.WeakStabilityCondition.Support.ZeroChargeLattice.isSaturated_saturatedClosure {Λ : Type u_1} [AddCommGroup Λ] (S : Set Λ) : IsSaturated (saturatedClosure S)

The saturated closure is saturated.

theorem CategoryTheory.Triangulated.WeakStabilityCondition.Support.ZeroChargeLattice.saturatedClosure_le {Λ : Type u_1} [AddCommGroup Λ] {S : Set Λ} {H : AddSubgroup Λ} (hS : S ⊆ ↑H) (hH : IsSaturated H) : saturatedClosure S ≤ H

Universal property of the saturated closure.

theorem CategoryTheory.Triangulated.WeakStabilityCondition.Support.ZeroChargeLattice.neg_mem_saturatedClosure_iff {Λ : Type u_1} [AddCommGroup Λ] (S : Set Λ) (x : Λ) : -x ∈ saturatedClosure S ↔ x ∈ saturatedClosure S

Membership in the saturated closure is invariant under negation.

@[reducible, inline]

abbrev CategoryTheory.Triangulated.WeakStabilityCondition.Support.ZeroChargeLattice.Quotient {Λ : Type u_1} [AddCommGroup Λ] (S : Set Λ) : Type u_1

The integral quotient by the saturated zero-charge subgroup.

Equations

• CategoryTheory.Triangulated.WeakStabilityCondition.Support.ZeroChargeLattice.Quotient S = (Λ ⧸ CategoryTheory.Triangulated.WeakStabilityCondition.Support.ZeroChargeLattice.saturatedClosure S)

def CategoryTheory.Triangulated.WeakStabilityCondition.Support.ZeroChargeLattice.quotientClass {Λ : Type u_1} [AddCommGroup Λ] (S : Set Λ) : Λ →+ Quotient S

The canonical class in the zero-charge quotient.

Equations

• One or more equations did not get rendered due to their size.

@[simp]

theorem CategoryTheory.Triangulated.WeakStabilityCondition.Support.ZeroChargeLattice.quotientClass_eq_zero_iff {Λ : Type u_1} [AddCommGroup Λ] (S : Set Λ) (x : Λ) : (quotientClass S) x = 0 ↔ x ∈ saturatedClosure S

theorem CategoryTheory.Triangulated.WeakStabilityCondition.Support.ZeroChargeLattice.quotient_isAddTorsionFree {Λ : Type u_1} [AddCommGroup Λ] (S : Set Λ) : IsAddTorsionFree (Quotient S)

Saturation is exactly what makes the additive quotient torsion-free.

theorem CategoryTheory.Triangulated.WeakStabilityCondition.Support.ZeroChargeLattice.quotient_moduleFinite {Λ : Type u_1} [AddCommGroup Λ] [Module.Finite ℤ Λ] (S : Set Λ) : Module.Finite ℤ (Quotient S)

A quotient of a finite integral module is finite as an integral module.

theorem CategoryTheory.Triangulated.WeakStabilityCondition.Support.ZeroChargeLattice.quotient_moduleFree {Λ : Type u_1} [AddCommGroup Λ] [Module.Finite ℤ Λ] (S : Set Λ) : Module.Free ℤ (Quotient S)

Under the finite-generation hypothesis expected of a lattice, the saturated quotient is a free abelian group, as asserted in Definition 21.9.

theorem CategoryTheory.Triangulated.WeakStabilityCondition.Support.ZeroChargeLattice.saturatedClosure_le_ker {Λ : Type u_1} {Γ : Type u_2} [AddCommGroup Λ] [AddCommGroup Γ] [IsAddTorsionFree Γ] (S : Set Λ) (Z : Λ →+ Γ) (hS : ∀ x ∈ S, Z x = 0) : saturatedClosure S ≤ Z.ker

A charge into a torsion-free group that vanishes on the generators also vanishes on their saturated closure.

def CategoryTheory.Triangulated.WeakStabilityCondition.Support.ZeroChargeLattice.quotientCharge {Λ : Type u_1} {Γ : Type u_2} [AddCommGroup Λ] [AddCommGroup Γ] [IsAddTorsionFree Γ] (S : Set Λ) (Z : Λ →+ Γ) (hS : ∀ x ∈ S, Z x = 0) : Quotient S →+ Γ

The charge induced on the quotient by the saturated zero-charge subgroup.

Equations

• One or more equations did not get rendered due to their size.

@[simp]

theorem CategoryTheory.Triangulated.WeakStabilityCondition.Support.ZeroChargeLattice.quotientCharge_quotientClass {Λ : Type u_1} {Γ : Type u_2} [AddCommGroup Λ] [AddCommGroup Γ] [IsAddTorsionFree Γ] (S : Set Λ) (Z : Λ →+ Γ) (hS : ∀ x ∈ S, Z x = 0) (x : Λ) : (quotientCharge S Z hS) ((quotientClass S) x) = Z x