Elementary transport of Harder--Narasimhan mass

This file owns the mass bookkeeping that does not mention a distinguished triangle: the charge-norm bound, behaviour of mass under the shift by ±1, invariance under a lifted rotation of the GL⁺(2, ℝ) action, and the mass of a filtration extended by one appended factor.

These are the arithmetic inputs to the triangle comparisons; keeping them apart from the heart bridge lets them be imported without the heart-equivalence machinery.

theorem CategoryTheory.Triangulated.norm_charge_le_stabilityMass_toReal {C : Type u} [Category.{w, u} C] [Limits.HasZeroObject C] [HasShift C ℤ] [Preadditive C] [∀ (n : ℤ), (shiftFunctor C n).Additive] [Pretriangulated C] [IsTriangulated C] {Λ : Type u'} [AddCommGroup Λ] {v : K₀ C →+ Λ} (σ : StabilityCondition.WithClassMap C v) (E : C) : ‖σ.charge E‖ ≤ (stabilityMass σ E).toReal

The norm of the total charge is at most the sum of the norms of the Harder--Narasimhan factor charges.

theorem CategoryTheory.Triangulated.HNFiltration.mass_shift_one {C : Type u} [Category.{w, u} C] [Limits.HasZeroObject C] [HasShift C ℤ] [Preadditive C] [∀ (n : ℤ), (shiftFunctor C n).Additive] [Pretriangulated C] {Λ : Type u'} [AddCommGroup Λ] {v : K₀ C →+ Λ} (σ : StabilityCondition.WithClassMap C v) {E : C} (F : HNFiltration C σ.slicing.P E) : mass σ (shift C σ.slicing F 1) = mass σ F

Shifting an HN filtration by one does not change its mass.

@[simp]

theorem CategoryTheory.Triangulated.stabilityMass_shift_one {C : Type u} [Category.{w, u} C] [Limits.HasZeroObject C] [HasShift C ℤ] [Preadditive C] [∀ (n : ℤ), (shiftFunctor C n).Additive] [Pretriangulated C] [IsTriangulated C] {Λ : Type u'} [AddCommGroup Λ] {v : K₀ C →+ Λ} (σ : StabilityCondition.WithClassMap C v) (E : C) : stabilityMass σ ((shiftFunctor C 1).obj E) = stabilityMass σ E

Shifting an object by one does not change its HN mass.

theorem CategoryTheory.Triangulated.HNFiltration.mass_shift_neg_one {C : Type u} [Category.{w, u} C] [Limits.HasZeroObject C] [HasShift C ℤ] [Preadditive C] [∀ (n : ℤ), (shiftFunctor C n).Additive] [Pretriangulated C] {Λ : Type u'} [AddCommGroup Λ] {v : K₀ C →+ Λ} (σ : StabilityCondition.WithClassMap C v) {E : C} (F : HNFiltration C σ.slicing.P E) : mass σ (shift C σ.slicing F (-1)) = mass σ F

Shifting an HN filtration by minus one does not change its mass.

@[simp]

theorem CategoryTheory.Triangulated.stabilityMass_shift_neg_one {C : Type u} [Category.{w, u} C] [Limits.HasZeroObject C] [HasShift C ℤ] [Preadditive C] [∀ (n : ℤ), (shiftFunctor C n).Additive] [Pretriangulated C] [IsTriangulated C] {Λ : Type u'} [AddCommGroup Λ] {v : K₀ C →+ Λ} (σ : StabilityCondition.WithClassMap C v) (E : C) : stabilityMass σ ((shiftFunctor C (-1)).obj E) = stabilityMass σ E

Shifting an object by minus one does not change its HN mass.

Invariance under lifted rotations

theorem CategoryTheory.Triangulated.actC_rotationGLPos (θ : ℝ) (z : ℂ) : (WeakStabilityCondition.StabilityCondition.GroupAction.actC (WeakStabilityCondition.StabilityCondition.GroupAction.rotationGLPos θ)) z = WeakStabilityCondition.StabilityCondition.GroupAction.cexpI (Real.pi * θ) * z

A rotation matrix acts on the complex plane by multiplication by the unit complex number with the corresponding angle.

theorem CategoryTheory.Triangulated.norm_actC_rotationGLPos (θ : ℝ) (z : ℂ) : ‖(WeakStabilityCondition.StabilityCondition.GroupAction.actC (WeakStabilityCondition.StabilityCondition.GroupAction.rotationGLPos θ)) z‖ = ‖z‖

Rotations preserve the complex norm used in each HN mass summand.

def CategoryTheory.Triangulated.HNFiltration.rotateStability {C : Type u} [Category.{w, u} C] [Limits.HasZeroObject C] [HasShift C ℤ] [Preadditive C] [∀ (n : ℤ), (shiftFunctor C n).Additive] [Pretriangulated C] [IsTriangulated C] {Λ : Type u'} [AddCommGroup Λ] {v : K₀ C →+ Λ} (σ : StabilityCondition.WithClassMap C v) {θ : ℝ} {E : C} (F : HNFiltration C σ.slicing.P E) : HNFiltration C (WeakStabilityCondition.StabilityCondition.GroupAction.liftedRotation θ • σ).slicing.P E

Relabel an HN filtration after acting on its stability condition by a lifted rotation. The tower is unchanged and every phase is translated by θ.

Equations

• CategoryTheory.Triangulated.HNFiltration.rotateStability σ F = { toPostnikovTower := F.toPostnikovTower, φ := fun (i : Fin F.n) => F.φ i + θ, hφ := ⋯, semistable := ⋯ }

def CategoryTheory.Triangulated.HNFiltration.unrotateStability {C : Type u} [Category.{w, u} C] [Limits.HasZeroObject C] [HasShift C ℤ] [Preadditive C] [∀ (n : ℤ), (shiftFunctor C n).Additive] [Pretriangulated C] [IsTriangulated C] {Λ : Type u'} [AddCommGroup Λ] {v : K₀ C →+ Λ} (σ : StabilityCondition.WithClassMap C v) {θ : ℝ} {E : C} (F : HNFiltration C (WeakStabilityCondition.StabilityCondition.GroupAction.liftedRotation θ • σ).slicing.P E) : HNFiltration C σ.slicing.P E

Undo the phase relabelling of an HN filtration for a rotated stability condition.

Equations

• CategoryTheory.Triangulated.HNFiltration.unrotateStability σ F = { toPostnikovTower := F.toPostnikovTower, φ := fun (i : Fin F.n) => F.φ i - θ, hφ := ⋯, semistable := ⋯ }

theorem CategoryTheory.Triangulated.HNFiltration.mass_rotateStability {C : Type u} [Category.{w, u} C] [Limits.HasZeroObject C] [HasShift C ℤ] [Preadditive C] [∀ (n : ℤ), (shiftFunctor C n).Additive] [Pretriangulated C] [IsTriangulated C] {Λ : Type u'} [AddCommGroup Λ] {v : K₀ C →+ Λ} (σ : StabilityCondition.WithClassMap C v) {θ : ℝ} {E : C} (F : HNFiltration C σ.slicing.P E) : mass (WeakStabilityCondition.StabilityCondition.GroupAction.liftedRotation θ • σ) (rotateStability σ F) = mass σ F

Relabelling an HN filtration by a lifted rotation preserves its finite mass sum.

theorem CategoryTheory.Triangulated.HNFiltration.mass_unrotateStability {C : Type u} [Category.{w, u} C] [Limits.HasZeroObject C] [HasShift C ℤ] [Preadditive C] [∀ (n : ℤ), (shiftFunctor C n).Additive] [Pretriangulated C] [IsTriangulated C] {Λ : Type u'} [AddCommGroup Λ] {v : K₀ C →+ Λ} (σ : StabilityCondition.WithClassMap C v) {θ : ℝ} {E : C} (F : HNFiltration C (WeakStabilityCondition.StabilityCondition.GroupAction.liftedRotation θ • σ).slicing.P E) : mass σ (unrotateStability σ F) = mass (WeakStabilityCondition.StabilityCondition.GroupAction.liftedRotation θ • σ) F

Undoing a lifted rotation also preserves the finite HN mass sum.

@[simp]

theorem CategoryTheory.Triangulated.stabilityMass_liftedRotation {C : Type u} [Category.{w, u} C] [Limits.HasZeroObject C] [HasShift C ℤ] [Preadditive C] [∀ (n : ℤ), (shiftFunctor C n).Additive] [Pretriangulated C] [IsTriangulated C] {Λ : Type u'} [AddCommGroup Λ] {v : K₀ C →+ Λ} (σ : StabilityCondition.WithClassMap C v) (θ : ℝ) (E : C) : stabilityMass (WeakStabilityCondition.StabilityCondition.GroupAction.liftedRotation θ • σ) E = stabilityMass σ E

Acting on a stability condition by a pure lifted rotation leaves the HN mass of every object unchanged.

Exact mass splitting across a phase cutoff

theorem CategoryTheory.Triangulated.HNFiltration.mass_appendFactor {C : Type u} [Category.{w, u} C] [Limits.HasZeroObject C] [HasShift C ℤ] [Preadditive C] [∀ (n : ℤ), (shiftFunctor C n).Additive] [Pretriangulated C] {Λ : Type u'} [AddCommGroup Λ] {v : K₀ C →+ Λ} (σ : StabilityCondition.WithClassMap C v) {X E : C} (GX : HNFiltration C σ.slicing.P X) (T : Pretriangulated.Triangle C) (hT : T ∈ Pretriangulated.distinguishedTriangles) (eT₁ : T.obj₁ ≅ X) (eT₂ : T.obj₂ ≅ E) (ψ : ℝ) (hψ : σ.slicing.P ψ T.obj₃) (hψ_lt : ∀ (j : Fin GX.n), ψ < GX.φ j) : mass σ (appendFactor C GX T hT eT₁ eT₂ ψ hψ hψ_lt) = mass σ GX + ENNReal.ofReal ‖σ.charge T.obj₃‖

Appending one strictly lower semistable factor to an HN filtration adds exactly the norm of that factor's charge to the finite mass.

theorem CategoryTheory.Triangulated.stabilityMass_toReal_appendFactor {C : Type u} [Category.{w, u} C] [Limits.HasZeroObject C] [HasShift C ℤ] [Preadditive C] [∀ (n : ℤ), (shiftFunctor C n).Additive] [Pretriangulated C] [IsTriangulated C] {Λ : Type u'} [AddCommGroup Λ] {v : K₀ C →+ Λ} (σ : StabilityCondition.WithClassMap C v) {X E : C} (GX : HNFiltration C σ.slicing.P X) (T : Pretriangulated.Triangle C) (hT : T ∈ Pretriangulated.distinguishedTriangles) (eT₁ : T.obj₁ ≅ X) (eT₂ : T.obj₂ ≅ E) (ψ : ℝ) (hψ : σ.slicing.P ψ T.obj₃) (hψ_lt : ∀ (j : Fin GX.n), ψ < GX.φ j) : (stabilityMass σ E).toReal = (stabilityMass σ X).toReal + ‖σ.charge T.obj₃‖

Real-valued ambient form of HNFiltration.mass_appendFactor.