Uniform support after killing zero-charge classes

Definition 21.9 of arXiv:1902.08184v4 first quotients the class lattice by the saturated subgroup generated by zero-charge heart classes. Definition 21.15 then places its quadratic form on the resulting real quotient. This file models the real-linear part of that construction.

The quotient is genuine: the form has domain V ⧸ V₀, the charge is the canonical lift through Submodule.mkQ, and the selected semistable classes are mapped into that quotient. In particular, no condition is imposed on a pullback form along V₀.mkQ; such a pullback necessarily vanishes on V₀ and therefore cannot be negative definite on the original kernel.

def CategoryTheory.Triangulated.WeakStabilityCondition.Support.quotientCharge {V : Type u_2} {W : Type u_3} [NormedAddCommGroup V] [NormedSpace ℝ V] [NormedAddCommGroup W] [NormedSpace ℝ W] (V₀ : Submodule ℝ V) (Z : V →ₗ[ℝ] W) (hV₀ : V₀ ≤ Z.ker) : V ⧸ V₀ →ₗ[ℝ] W

The charge induced on a quotient by a subspace contained in its kernel.

Equations

• CategoryTheory.Triangulated.WeakStabilityCondition.Support.quotientCharge V₀ Z hV₀ = V₀.liftQ Z hV₀

theorem CategoryTheory.Triangulated.WeakStabilityCondition.Support.quotientCharge_mkQ {V : Type u_2} {W : Type u_3} [NormedAddCommGroup V] [NormedSpace ℝ V] [NormedAddCommGroup W] [NormedSpace ℝ W] (V₀ : Submodule ℝ V) (Z : V →ₗ[ℝ] W) (hV₀ : V₀ ≤ Z.ker) (x : V) : (quotientCharge V₀ Z hV₀) (V₀.mkQ x) = Z x

def CategoryTheory.Triangulated.WeakStabilityCondition.Support.quotientFamilyLocus {I : Type u_1} {V : Type u_2} [NormedAddCommGroup V] [NormedSpace ℝ V] (V₀ : Submodule ℝ V) (S : I → Set V) : I → Set (V ⧸ V₀)

The image in the quotient of each selected locus.

Equations

• CategoryTheory.Triangulated.WeakStabilityCondition.Support.quotientFamilyLocus V₀ S i = ⇑V₀.mkQ '' S i

def CategoryTheory.Triangulated.WeakStabilityCondition.Support.HasUniformQuadraticSupportPropertyModulo {I : Type u_1} {V : Type u_2} {W : Type u_3} [NormedAddCommGroup V] [NormedSpace ℝ V] [FiniteDimensional ℝ V] [NormedAddCommGroup W] [NormedSpace ℝ W] (V₀ : Submodule ℝ V) (Z : V →ₗ[ℝ] W) (hV₀ : V₀ ≤ Z.ker) (S : I → Set V) : Prop

Uniform genuine quadratic support on the quotient V ⧸ V₀.

The proof hV₀ is part of the input so the charge is definitionally the canonical quotient charge.

Equations

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

theorem CategoryTheory.Triangulated.WeakStabilityCondition.Support.hasUniformQuadraticSupportPropertyModulo_iff {I : Type u_1} {V : Type u_2} {W : Type u_3} [NormedAddCommGroup V] [NormedSpace ℝ V] [FiniteDimensional ℝ V] [NormedAddCommGroup W] [NormedSpace ℝ W] (V₀ : Submodule ℝ V) (Z : V →ₗ[ℝ] W) (hV₀ : V₀ ≤ Z.ker) (S : I → Set V) : HasUniformQuadraticSupportPropertyModulo V₀ Z hV₀ S ↔ ∃ (Q : QuadraticForm ℝ (V ⧸ V₀)), (∀ (i : I), ∀ x ∈ S i, 0 ≤ Q (V₀.mkQ x)) ∧ ∀ (y : V ⧸ V₀), (quotientCharge V₀ Z hV₀) y = 0 → y ≠ 0 → Q y < 0

Unfolded source-facing form of quotient support: one quadratic form on the quotient, nonnegative on every mapped selected class, and negative definite on the kernel of the descended charge.

theorem CategoryTheory.Triangulated.WeakStabilityCondition.Support.HasUniformQuadraticSupportPropertyModulo.fiber {I : Type u_1} {V : Type u_2} {W : Type u_3} [NormedAddCommGroup V] [NormedSpace ℝ V] [FiniteDimensional ℝ V] [NormedAddCommGroup W] [NormedSpace ℝ W] {V₀ : Submodule ℝ V} {Z : V →ₗ[ℝ] W} {hV₀ : V₀ ≤ Z.ker} {S : I → Set V} (h : HasUniformQuadraticSupportPropertyModulo V₀ Z hV₀ S) (i : I) : HasQuadraticSupportProperty (quotientCharge V₀ Z hV₀) (⇑V₀.mkQ '' S i)

Quotient support supplies genuine quadratic support on each individual fiber locus.

theorem CategoryTheory.Triangulated.WeakStabilityCondition.Support.HasUniformQuadraticSupportPropertyModulo.hasSupportProperty {I : Type u_1} {V : Type u_2} {W : Type u_3} [NormedAddCommGroup V] [NormedSpace ℝ V] [FiniteDimensional ℝ V] [NormedAddCommGroup W] [NormedSpace ℝ W] {V₀ : Submodule ℝ V} {Z : V →ₗ[ℝ] W} {hV₀ : V₀ ≤ Z.ker} {S : I → Set V} (h : HasUniformQuadraticSupportPropertyModulo V₀ Z hV₀ S) (i : I) : HasSupportProperty (quotientCharge V₀ Z hV₀) (⇑V₀.mkQ '' S i)

Hence every quotient fiber locus satisfies the norm formulation of the support property as well.

theorem CategoryTheory.Triangulated.WeakStabilityCondition.Support.mkQ_eq_zero_of_mem {V : Type u_2} [NormedAddCommGroup V] [NormedSpace ℝ V] (V₀ : Submodule ℝ V) {x : V} (hx : x ∈ V₀) : V₀.mkQ x = 0

Every class in the killed subspace maps to zero in the quotient.

theorem CategoryTheory.Triangulated.WeakStabilityCondition.Support.HasQuadraticSupportProperty.constant_modulo {V : Type u_2} {W : Type u_3} [NormedAddCommGroup V] [NormedSpace ℝ V] [FiniteDimensional ℝ V] [NormedAddCommGroup W] [NormedSpace ℝ W] (V₀ : Submodule ℝ V) (Z : V →ₗ[ℝ] W) (hV₀ : V₀ ≤ Z.ker) {S : Set V} (h : HasQuadraticSupportProperty (quotientCharge V₀ Z hV₀) (⇑V₀.mkQ '' S)) (I : Type u_4) : HasUniformQuadraticSupportPropertyModulo V₀ Z hV₀ fun (x : I) => S

A constant selected locus gives a constant quotient-supported family.