Comparing the integral and real zero-charge quotients

Definition 21.9 of arXiv:1902.08184v4 forms a free abelian quotient by the saturated subgroup generated by zero-charge classes. Definition 21.15(4) puts the uniform quadratic form on a real quotient. This file supplies the previously missing comparison map between those two constructions.

The comparison is canonical once the integral classes are realized in the real vector space and the chosen generators land in the killed subspace. It is not automatically an equivalence: the equivalence constructor below requires a proof that the scalar-extended comparison is bijective.

def CategoryTheory.Triangulated.WeakStabilityCondition.Support.ZeroChargeLattice.quotientToRealQuotient {Λ : Type u_1} {V : Type u_2} [AddCommGroup Λ] [AddCommGroup V] [Module ℝ V] (S : Set Λ) (ι : Λ →+ V) (V₀ : Submodule ℝ V) (hS : ∀ x ∈ S, ι x ∈ V₀) : Quotient S →+ V ⧸ V₀

The map from the saturated integral quotient to the real quotient.

The hypothesis says exactly that every chosen zero-charge generator is killed by the real quotient. Saturation then makes the map descend because a real vector space is torsion-free as an additive group.

Equations

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

@[simp]

theorem CategoryTheory.Triangulated.WeakStabilityCondition.Support.ZeroChargeLattice.quotientToRealQuotient_quotientClass {Λ : Type u_1} {V : Type u_2} [AddCommGroup Λ] [AddCommGroup V] [Module ℝ V] (S : Set Λ) (ι : Λ →+ V) (V₀ : Submodule ℝ V) (hS : ∀ x ∈ S, ι x ∈ V₀) (x : Λ) : (quotientToRealQuotient S ι V₀ hS) ((quotientClass S) x) = V₀.mkQ (ι x)

The integral comparison sends the class of x to its realized class in the real quotient.

@[reducible, inline]

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

Scalar extension of the saturated integral quotient to ℝ.

The scalar factor is placed first so Mathlib's canonical left-module structure makes this tensor product an ℝ-module without any auxiliary choice.

Equations

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

def CategoryTheory.Triangulated.WeakStabilityCondition.Support.ZeroChargeLattice.scalarExtensionComparison {Λ : Type u_1} {V : Type u_2} [AddCommGroup Λ] [AddCommGroup V] [Module ℝ V] (S : Set Λ) (ι : Λ →+ V) (V₀ : Submodule ℝ V) (hS : ∀ x ∈ S, ι x ∈ V₀) : RealScalarExtension S →ₗ[ℝ] V ⧸ V₀

The canonical real-linear comparison from the scalar-extended integral quotient to the real quotient.

Equations

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

@[simp]

theorem CategoryTheory.Triangulated.WeakStabilityCondition.Support.ZeroChargeLattice.scalarExtensionComparison_tmul {Λ : Type u_1} {V : Type u_2} [AddCommGroup Λ] [AddCommGroup V] [Module ℝ V] (S : Set Λ) (ι : Λ →+ V) (V₀ : Submodule ℝ V) (hS : ∀ x ∈ S, ι x ∈ V₀) (r : ℝ) (x : Quotient S) : (scalarExtensionComparison S ι V₀ hS) (r ⊗ₜ[ℤ] x) = r • (quotientToRealQuotient S ι V₀ hS) x

Formula for the scalar-extension comparison on pure tensors.

@[simp]

theorem CategoryTheory.Triangulated.WeakStabilityCondition.Support.ZeroChargeLattice.scalarExtensionComparison_quotientClass {Λ : Type u_1} {V : Type u_2} [AddCommGroup Λ] [AddCommGroup V] [Module ℝ V] (S : Set Λ) (ι : Λ →+ V) (V₀ : Submodule ℝ V) (hS : ∀ x ∈ S, ι x ∈ V₀) (r : ℝ) (x : Λ) : (scalarExtensionComparison S ι V₀ hS) (r ⊗ₜ[ℤ] (quotientClass S) x) = r • V₀.mkQ (ι x)

On a scalar-extended original class, the comparison is the expected real multiple of its image in the quotient.

theorem CategoryTheory.Triangulated.WeakStabilityCondition.Support.ZeroChargeLattice.exists_scalarExtensionEquiv_iff {Λ : Type u_1} {V : Type u_2} [AddCommGroup Λ] [AddCommGroup V] [Module ℝ V] (S : Set Λ) (ι : Λ →+ V) (V₀ : Submodule ℝ V) (hS : ∀ x ∈ S, ι x ∈ V₀) : (∃ (e : RealScalarExtension S ≃ₗ[ℝ] V ⧸ V₀), ↑e = scalarExtensionComparison S ι V₀ hS) ↔ Function.Bijective ⇑(scalarExtensionComparison S ι V₀ hS)

A real-linear equivalence exists with the canonical comparison as its underlying map exactly when that comparison is bijective. This records the missing comparison hypothesis explicitly instead of treating it as automatic.

noncomputable def CategoryTheory.Triangulated.WeakStabilityCondition.Support.ZeroChargeLattice.scalarExtensionEquiv {Λ : Type u_1} {V : Type u_2} [AddCommGroup Λ] [AddCommGroup V] [Module ℝ V] (S : Set Λ) (ι : Λ →+ V) (V₀ : Submodule ℝ V) (hS : ∀ x ∈ S, ι x ∈ V₀) (hbij : Function.Bijective ⇑(scalarExtensionComparison S ι V₀ hS)) : RealScalarExtension S ≃ₗ[ℝ] V ⧸ V₀

Upgrade the canonical comparison to a linear equivalence when its bijectivity has been proved in the geometric or numerical model at hand.

Equations

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

@[simp]

theorem CategoryTheory.Triangulated.WeakStabilityCondition.Support.ZeroChargeLattice.scalarExtensionEquiv_apply {Λ : Type u_1} {V : Type u_2} [AddCommGroup Λ] [AddCommGroup V] [Module ℝ V] (S : Set Λ) (ι : Λ →+ V) (V₀ : Submodule ℝ V) (hS : ∀ x ∈ S, ι x ∈ V₀) (hbij : Function.Bijective ⇑(scalarExtensionComparison S ι V₀ hS)) (x : RealScalarExtension S) : (scalarExtensionEquiv S ι V₀ hS hbij) x = (scalarExtensionComparison S ι V₀ hS) x