The source central charge of Proposition 14.16

The phase-tilt implementation rotates a charge by the unit complex number exp (-pi * slopeCutPhase b * I). Proposition 14.16 is instead stated with the charge

Z_b = Z / (I - b).

These differ by the positive real factor 1 / sqrt (1 + b^2). This file proves that identity exactly and packages the resulting weak prestability condition with the source-facing charge, rather than merely an equivalent unit rotation.

noncomputable def CategoryTheory.Triangulated.WeakStabilityCondition.WeakPreStabilityCondition.sourceTiltScale (b : ℝ) : ℝ

The positive scale relating the source charge to the unit phase rotation.

Equations

• CategoryTheory.Triangulated.WeakStabilityCondition.WeakPreStabilityCondition.sourceTiltScale b = (√(1 + b ^ 2))⁻¹

theorem CategoryTheory.Triangulated.WeakStabilityCondition.WeakPreStabilityCondition.sourceTiltScale_pos (b : ℝ) : 0 < sourceTiltScale b

theorem CategoryTheory.Triangulated.WeakStabilityCondition.WeakPreStabilityCondition.sourceTilt_multiplier (b : ℝ) : (Complex.I - ↑b)⁻¹ = ↑(sourceTiltScale b) * Complex.exp (-(↑Real.pi * ↑(slopeCutPhase b)) * Complex.I)

The exact analytic normalization behind Proposition 14.16: 1 / (i-b) is a positive rescaling of the unit rotation through the phase corresponding to slope b.

noncomputable def CategoryTheory.Triangulated.WeakStabilityCondition.WeakPreStabilityCondition.sourceTiltRotation (b : ℝ) : ℂ →+ ℂ

Division by I-b, as an additive endomorphism of the complex plane.

Equations

• CategoryTheory.Triangulated.WeakStabilityCondition.WeakPreStabilityCondition.sourceTiltRotation b = { toFun := fun (z : ℂ) => z / (Complex.I - ↑b), map_zero' := ⋯, map_add' := ⋯ }

@[simp]

theorem CategoryTheory.Triangulated.WeakStabilityCondition.WeakPreStabilityCondition.sourceTiltRotation_apply (b : ℝ) (z : ℂ) : (sourceTiltRotation b) z = z / (Complex.I - ↑b)

theorem CategoryTheory.Triangulated.WeakStabilityCondition.WeakPreStabilityCondition.sourceTiltRotation_eq_scale_phaseTiltRotation (b : ℝ) (z : ℂ) : (sourceTiltRotation b) z = ↑(sourceTiltScale b) * (phaseTiltRotation (slopeCutPhase b)) z

Source division is the phase rotation followed by its positive real normalization.

noncomputable def CategoryTheory.Triangulated.WeakStabilityCondition.WeakPreStabilityCondition.sourceTiltLatticeCharge {C : Type u_1} [Category.{u_3, u_1} C] [Preadditive C] [Limits.HasZeroObject C] [HasShift C ℤ] [∀ (n : ℤ), (shiftFunctor C n).Additive] [Pretriangulated C] {V : Type u_2} [NormedAddCommGroup V] {v : K₀ C →+ V} (sigma : WeakPreStabilityCondition v) (b : ℝ) : V →+ ℂ

The lattice-level central charge Z/(I-b) from Proposition 14.16.

Equations

• sigma.sourceTiltLatticeCharge b = (CategoryTheory.Triangulated.WeakStabilityCondition.WeakPreStabilityCondition.sourceTiltRotation b).comp sigma.Z

@[simp]

theorem CategoryTheory.Triangulated.WeakStabilityCondition.WeakPreStabilityCondition.sourceTiltLatticeCharge_apply {C : Type u_1} [Category.{u_3, u_1} C] [Preadditive C] [Limits.HasZeroObject C] [HasShift C ℤ] [∀ (n : ℤ), (shiftFunctor C n).Additive] [Pretriangulated C] {V : Type u_2} [NormedAddCommGroup V] {v : K₀ C →+ V} (sigma : WeakPreStabilityCondition v) (b : ℝ) (x : V) : (sigma.sourceTiltLatticeCharge b) x = sigma.Z x / (Complex.I - ↑b)

theorem CategoryTheory.Triangulated.WeakStabilityCondition.WeakPreStabilityCondition.sourceTiltLatticeCharge_eq_scale_phaseTiltLatticeCharge {C : Type u_1} [Category.{u_3, u_1} C] [Preadditive C] [Limits.HasZeroObject C] [HasShift C ℤ] [∀ (n : ℤ), (shiftFunctor C n).Additive] [Pretriangulated C] {V : Type u_2} [NormedAddCommGroup V] {v : K₀ C →+ V} (sigma : WeakPreStabilityCondition v) (b : ℝ) (x : V) : (sigma.sourceTiltLatticeCharge b) x = ↑(sourceTiltScale b) * (sigma.phaseTiltLatticeCharge (slopeCutPhase b)) x

noncomputable def CategoryTheory.Triangulated.WeakStabilityCondition.WeakPreStabilityCondition.sourceTiltCharge {C : Type u_1} [Category.{u_3, u_1} C] [Preadditive C] [Limits.HasZeroObject C] [HasShift C ℤ] [∀ (n : ℤ), (shiftFunctor C n).Additive] [Pretriangulated C] {V : Type u_2} [NormedAddCommGroup V] {v : K₀ C →+ V} (sigma : WeakPreStabilityCondition v) (b : ℝ) : K₀ C →+ ℂ

The source charge on the ambient Grothendieck group.

Equations

• sigma.sourceTiltCharge b = (CategoryTheory.Triangulated.WeakStabilityCondition.WeakPreStabilityCondition.sourceTiltRotation b).comp (sigma.Z.comp v)

@[simp]

theorem CategoryTheory.Triangulated.WeakStabilityCondition.WeakPreStabilityCondition.sourceTiltCharge_apply {C : Type u_1} [Category.{u_3, u_1} C] [Preadditive C] [Limits.HasZeroObject C] [HasShift C ℤ] [∀ (n : ℤ), (shiftFunctor C n).Additive] [Pretriangulated C] {V : Type u_2} [NormedAddCommGroup V] {v : K₀ C →+ V} (sigma : WeakPreStabilityCondition v) (b : ℝ) (E : C) : (sigma.sourceTiltCharge b) (K₀.of C E) = sigma.Z (v (K₀.of C E)) / (Complex.I - ↑b)

theorem CategoryTheory.Triangulated.WeakStabilityCondition.WeakPreStabilityCondition.sourceTiltCharge_eq_scale_phaseTiltCharge {C : Type u_1} [Category.{u_3, u_1} C] [Preadditive C] [Limits.HasZeroObject C] [HasShift C ℤ] [∀ (n : ℤ), (shiftFunctor C n).Additive] [Pretriangulated C] {V : Type u_2} [NormedAddCommGroup V] {v : K₀ C →+ V} (sigma : WeakPreStabilityCondition v) (b : ℝ) (E : C) : (sigma.sourceTiltCharge b) (K₀.of C E) = ↑(sourceTiltScale b) * (sigma.phaseTiltCharge (slopeCutPhase b)) (K₀.of C E)

noncomputable def CategoryTheory.Triangulated.WeakStabilityCondition.WeakPreStabilityCondition.sourceTiltWeakStabilityFunction {C : Type u_1} [Category.{u_3, u_1} C] [Preadditive C] [Limits.HasZeroObject C] [HasShift C ℤ] [∀ (n : ℤ), (shiftFunctor C n).Additive] [Pretriangulated C] [IsTriangulated C] {V : Type u_2} [NormedAddCommGroup V] {v : K₀ C →+ V} (sigma : WeakPreStabilityCondition v) (b : ℝ) : WeakStabilityFunction (sigma.slopeTorsionPair b).tilt

The weak stability function on the source tilted heart with the exact charge Z/(I-b).

Equations

• sigma.sourceTiltWeakStabilityFunction b = { Z := sigma.sourceTiltCharge b, nonzero_mem := ⋯ }

@[simp]

theorem CategoryTheory.Triangulated.WeakStabilityCondition.WeakPreStabilityCondition.sourceTiltWeakStabilityFunction_Z {C : Type u_1} [Category.{u_3, u_1} C] [Preadditive C] [Limits.HasZeroObject C] [HasShift C ℤ] [∀ (n : ℤ), (shiftFunctor C n).Additive] [Pretriangulated C] [IsTriangulated C] {V : Type u_2} [NormedAddCommGroup V] {v : K₀ C →+ V} (sigma : WeakPreStabilityCondition v) (b : ℝ) : (sigma.sourceTiltWeakStabilityFunction b).Z = sigma.sourceTiltCharge b

@[simp]

theorem CategoryTheory.Triangulated.WeakStabilityCondition.WeakPreStabilityCondition.sourceTiltWeakStabilityFunction_charge {C : Type u_1} [Category.{u_3, u_1} C] [Preadditive C] [Limits.HasZeroObject C] [HasShift C ℤ] [∀ (n : ℤ), (shiftFunctor C n).Additive] [Pretriangulated C] [IsTriangulated C] {V : Type u_2} [NormedAddCommGroup V] {v : K₀ C →+ V} (sigma : WeakPreStabilityCondition v) (b : ℝ) (E : C) : (sigma.sourceTiltWeakStabilityFunction b).charge E = sigma.Z (v (K₀.of C E)) / (Complex.I - ↑b)

theorem CategoryTheory.Triangulated.WeakStabilityCondition.WeakPreStabilityCondition.sourceTiltWeakStabilityFunction_charge_eq_scale_phaseTilt {C : Type u_1} [Category.{u_3, u_1} C] [Preadditive C] [Limits.HasZeroObject C] [HasShift C ℤ] [∀ (n : ℤ), (shiftFunctor C n).Additive] [Pretriangulated C] [IsTriangulated C] {V : Type u_2} [NormedAddCommGroup V] {v : K₀ C →+ V} (sigma : WeakPreStabilityCondition v) (b : ℝ) (E : C) : (sigma.sourceTiltWeakStabilityFunction b).charge E = ↑(sourceTiltScale b) * (sigma.phaseTiltWeakStabilityFunction (slopeCutPhase b) ⋯ ⋯).charge E

theorem CategoryTheory.Triangulated.WeakStabilityCondition.WeakPreStabilityCondition.sourceTiltWeakStabilityFunction_slope_eq_phaseTilt {C : Type u_1} [Category.{u_3, u_1} C] [Preadditive C] [Limits.HasZeroObject C] [HasShift C ℤ] [∀ (n : ℤ), (shiftFunctor C n).Additive] [Pretriangulated C] [IsTriangulated C] {V : Type u_2} [NormedAddCommGroup V] {v : K₀ C →+ V} (sigma : WeakPreStabilityCondition v) (b : ℝ) (E : C) : (sigma.sourceTiltWeakStabilityFunction b).slope E = (sigma.phaseTiltWeakStabilityFunction (slopeCutPhase b) ⋯ ⋯).slope E

theorem CategoryTheory.Triangulated.WeakStabilityCondition.WeakPreStabilityCondition.sourceTiltWeakStabilityFunction_isSemistable_iff_phaseTilt {C : Type u_1} [Category.{u_3, u_1} C] [Preadditive C] [Limits.HasZeroObject C] [HasShift C ℤ] [∀ (n : ℤ), (shiftFunctor C n).Additive] [Pretriangulated C] [IsTriangulated C] {V : Type u_2} [NormedAddCommGroup V] {v : K₀ C →+ V} (sigma : WeakPreStabilityCondition v) (b : ℝ) (E : C) : (sigma.sourceTiltWeakStabilityFunction b).IsSemistable E ↔ (sigma.phaseTiltWeakStabilityFunction (slopeCutPhase b) ⋯ ⋯).IsSemistable E

theorem CategoryTheory.Triangulated.WeakStabilityCondition.WeakPreStabilityCondition.sourceTiltWeakStabilityFunction_isStable_iff_phaseTilt {C : Type u_1} [Category.{u_3, u_1} C] [Preadditive C] [Limits.HasZeroObject C] [HasShift C ℤ] [∀ (n : ℤ), (shiftFunctor C n).Additive] [Pretriangulated C] [IsTriangulated C] {V : Type u_2} [NormedAddCommGroup V] {v : K₀ C →+ V} (sigma : WeakPreStabilityCondition v) (b : ℝ) (E : C) : (sigma.sourceTiltWeakStabilityFunction b).IsStable E ↔ (sigma.phaseTiltWeakStabilityFunction (slopeCutPhase b) ⋯ ⋯).IsStable E

theorem CategoryTheory.Triangulated.WeakStabilityCondition.WeakPreStabilityCondition.sourceTiltWeakStabilityFunction_zeroCharge_iff {C : Type u_1} [Category.{u_3, u_1} C] [Preadditive C] [Limits.HasZeroObject C] [HasShift C ℤ] [∀ (n : ℤ), (shiftFunctor C n).Additive] [Pretriangulated C] [IsTriangulated C] {V : Type u_2} [NormedAddCommGroup V] {v : K₀ C →+ V} (sigma : WeakPreStabilityCondition v) (b : ℝ) (E : C) : (sigma.sourceTiltWeakStabilityFunction b).zeroCharge E ↔ (sigma.phaseTiltWeakStabilityFunction (slopeCutPhase b) ⋯ ⋯).zeroCharge E

theorem CategoryTheory.Triangulated.WeakStabilityCondition.WeakPreStabilityCondition.sourceTiltWeakStabilityFunction_ambientPhasePredicate_eq_phaseTilt {C : Type u_1} [Category.{u_3, u_1} C] [Preadditive C] [Limits.HasZeroObject C] [HasShift C ℤ] [∀ (n : ℤ), (shiftFunctor C n).Additive] [Pretriangulated C] [IsTriangulated C] {V : Type u_2} [NormedAddCommGroup V] {v : K₀ C →+ V} (sigma : WeakPreStabilityCondition v) (b : ℝ) : (sigma.sourceTiltWeakStabilityFunction b).ambientPhasePredicate = (sigma.phaseTiltWeakStabilityFunction (slopeCutPhase b) ⋯ ⋯).ambientPhasePredicate

Positive rescaling preserves the integer-normalized ambient phase family, not just heart semistability.

noncomputable def CategoryTheory.Triangulated.WeakStabilityCondition.WeakPreStabilityCondition.sourceTiltWeakPreStabilityConditionOfTiltingProperty {C : Type u_1} [Category.{u_3, u_1} C] [Preadditive C] [Limits.HasZeroObject C] [HasShift C ℤ] [∀ (n : ℤ), (shiftFunctor C n).Additive] [Pretriangulated C] [IsTriangulated C] {V : Type u_2} [NormedAddCommGroup V] {v : K₀ C →+ V} (sigma : WeakPreStabilityCondition v) (b : ℝ) (htilt : sigma.TiltingProperty) : WeakPreStabilityCondition v

The weak upper tilt with the exact source charge Z/(I-b). Its slicing is unchanged from the phase-tilt construction because the two charges differ by a positive real scale.

Equations

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

@[simp]

theorem CategoryTheory.Triangulated.WeakStabilityCondition.WeakPreStabilityCondition.sourceTiltWeakPreStabilityConditionOfTiltingProperty_Z {C : Type u_1} [Category.{u_3, u_1} C] [Preadditive C] [Limits.HasZeroObject C] [HasShift C ℤ] [∀ (n : ℤ), (shiftFunctor C n).Additive] [Pretriangulated C] [IsTriangulated C] {V : Type u_2} [NormedAddCommGroup V] {v : K₀ C →+ V} (sigma : WeakPreStabilityCondition v) (b : ℝ) (htilt : sigma.TiltingProperty) : (sigma.sourceTiltWeakPreStabilityConditionOfTiltingProperty b htilt).Z = sigma.sourceTiltLatticeCharge b

@[simp]

theorem CategoryTheory.Triangulated.WeakStabilityCondition.WeakPreStabilityCondition.sourceTiltWeakPreStabilityConditionOfTiltingProperty_P {C : Type u_1} [Category.{u_3, u_1} C] [Preadditive C] [Limits.HasZeroObject C] [HasShift C ℤ] [∀ (n : ℤ), (shiftFunctor C n).Additive] [Pretriangulated C] [IsTriangulated C] {V : Type u_2} [NormedAddCommGroup V] {v : K₀ C →+ V} (sigma : WeakPreStabilityCondition v) (b : ℝ) (htilt : sigma.TiltingProperty) : (sigma.sourceTiltWeakPreStabilityConditionOfTiltingProperty b htilt).slicing.P = (sigma.phaseTiltWeakStabilityFunction (slopeCutPhase b) ⋯ ⋯).ambientPhasePredicate

theorem CategoryTheory.Triangulated.WeakStabilityCondition.WeakPreStabilityCondition.sourceTiltWeakPreStabilityConditionOfTiltingProperty_P_source {C : Type u_1} [Category.{u_3, u_1} C] [Preadditive C] [Limits.HasZeroObject C] [HasShift C ℤ] [∀ (n : ℤ), (shiftFunctor C n).Additive] [Pretriangulated C] [IsTriangulated C] {V : Type u_2} [NormedAddCommGroup V] {v : K₀ C →+ V} (sigma : WeakPreStabilityCondition v) (b : ℝ) (htilt : sigma.TiltingProperty) : (sigma.sourceTiltWeakPreStabilityConditionOfTiltingProperty b htilt).slicing.P = (sigma.sourceTiltWeakStabilityFunction b).ambientPhasePredicate

The slicing of the exact source-normalized weak condition is the ambient phase family of its exact tilted heart function.