Composing two transports

actStabAut transports a stability condition along one autoequivalence. This file proves that doing it twice is the same as doing it once along the composite — the associativity clause of a group action, without asserting that there is a group.

Two halves, and only one of them has content:

• the slicing half is definitional. Slicing.mapEquiv reindexes by Φ.inverse, and (Φ.trans Ψ).inverse is Ψ.inverse ⋙ Φ.inverse on the nose, so mapEquiv_trans is Slicing.ext applied to rfl;
• the charge half is where the composite lattice map appears. If Φ carries lam₁ and Ψ carries lam₂, then Φ.trans Ψ carries lam₁.comp lam₂ — note the order: hlam is stated for the quasi-inverse, and inverses reverse, so lam₁ is applied last.

Equivalence.trans and instance search

(Φ.trans Ψ).functor is reducibly Φ.functor ⋙ Ψ.functor, but instance search does not unfold Equivalence.trans to find it, so (Φ.trans Ψ).functor.Additive fails to synthesize. The six inferInstanceAs instances below supply what search cannot reach. They are stated once here and are what let mapEquiv (Φ.trans Ψ) be written at all.

What this file does not assert

• No new group and no new MulAction. This is one equation between two transports, stated for a bare lam : Λ →+ Λ. The bundled version already exists: GroupAction.AutPairQuot v (Stability/ClassMap.lean) is a group with a MulAction on WithClassMap C v, whose act_mul is this equation for pairs whose lam is invertible. This file is the strictly more general unbundled statement — a non-invertible lam still transports — and the kernel-tracking consumer (KernelAutoequivalence.actStab_trans) needs it in this form.
• Nothing about the composite of two stability conditions, which is not a thing; only about applying two transports in sequence.
• No claim that lam₁.comp lam₂ is the unique lattice map compatible with Φ.trans Ψ; uniqueness would need v surjective.

instance CategoryTheory.Triangulated.transFunctorAdditive {C : Type u} [Category.{u_1, u} C] [Preadditive C] (Φ Ψ : C ≌ C) [Φ.functor.Additive] [Ψ.functor.Additive] : (Φ.trans Ψ).functor.Additive

instance CategoryTheory.Triangulated.transInverseAdditive {C : Type u} [Category.{u_1, u} C] [Preadditive C] (Φ Ψ : C ≌ C) [Φ.inverse.Additive] [Ψ.inverse.Additive] : (Φ.trans Ψ).inverse.Additive

@[implicit_reducible]

instance CategoryTheory.Triangulated.transFunctorCommShift {C : Type u} [Category.{u_1, u} C] [HasShift C ℤ] (Φ Ψ : C ≌ C) [Φ.functor.CommShift ℤ] [Ψ.functor.CommShift ℤ] : (Φ.trans Ψ).functor.CommShift ℤ

Equations

• CategoryTheory.Triangulated.transFunctorCommShift Φ Ψ = { commShiftIso := CategoryTheory.Triangulated.transFunctorCommShift._aux_1 Φ Ψ, commShiftIso_zero := ⋯, commShiftIso_add := ⋯ }

@[implicit_reducible]

instance CategoryTheory.Triangulated.transInverseCommShift {C : Type u} [Category.{u_1, u} C] [HasShift C ℤ] (Φ Ψ : C ≌ C) [Φ.inverse.CommShift ℤ] [Ψ.inverse.CommShift ℤ] : (Φ.trans Ψ).inverse.CommShift ℤ

Equations

• CategoryTheory.Triangulated.transInverseCommShift Φ Ψ = { commShiftIso := CategoryTheory.Triangulated.transInverseCommShift._aux_1 Φ Ψ, commShiftIso_zero := ⋯, commShiftIso_add := ⋯ }

instance CategoryTheory.Triangulated.transFunctorIsTriangulated {C : Type u} [Category.{u_1, u} C] [Limits.HasZeroObject C] [HasShift C ℤ] [Preadditive C] [∀ (n : ℤ), (shiftFunctor C n).Additive] [Pretriangulated C] (Φ Ψ : C ≌ C) [Φ.functor.CommShift ℤ] [Ψ.functor.CommShift ℤ] [Φ.functor.IsTriangulated] [Ψ.functor.IsTriangulated] : (Φ.trans Ψ).functor.IsTriangulated

instance CategoryTheory.Triangulated.transInverseIsTriangulated {C : Type u} [Category.{u_1, u} C] [Limits.HasZeroObject C] [HasShift C ℤ] [Preadditive C] [∀ (n : ℤ), (shiftFunctor C n).Additive] [Pretriangulated C] (Φ Ψ : C ≌ C) [Φ.inverse.CommShift ℤ] [Ψ.inverse.CommShift ℤ] [Φ.inverse.IsTriangulated] [Ψ.inverse.IsTriangulated] : (Φ.trans Ψ).inverse.IsTriangulated

theorem CategoryTheory.Triangulated.Slicing.mapEquiv_trans {C : Type u} [Category.{u_1, u} C] [Limits.HasZeroObject C] [HasShift C ℤ] [Preadditive C] [∀ (n : ℤ), (shiftFunctor C n).Additive] [Pretriangulated C] (Φ Ψ : C ≌ C) [Φ.functor.Additive] [Φ.inverse.Additive] [Ψ.functor.Additive] [Ψ.inverse.Additive] [Φ.functor.CommShift ℤ] [Φ.inverse.CommShift ℤ] [Ψ.functor.CommShift ℤ] [Ψ.inverse.CommShift ℤ] [Φ.functor.IsTriangulated] [Φ.inverse.IsTriangulated] [Ψ.functor.IsTriangulated] [Ψ.inverse.IsTriangulated] (s : Slicing C) : (s.mapEquiv Φ).mapEquiv Ψ = s.mapEquiv (Φ.trans Ψ)

Reindexing twice is reindexing along the composite.

Definitional: mapEquiv reindexes by Φ.inverse, and (Φ.trans Ψ).inverse is Ψ.inverse ⋙ Φ.inverse on the nose. The bundled counterpart is TriEquiv.act_comp (Slicing/Quotient.lean) — the same Slicing.ext-on-rfl argument for a TriEquiv instead of a bare Equivalence.

Pin note: "on the nose" is Mathlib's literal inverse := f.inverse ⋙ e.inverse in the definition of Equivalence.trans. If a Mathlib bump redefines Equivalence.trans, this rfl — and KernelAutoequivalence.actStab_trans behind it — is the first thing to break. Re-check here if the pin moves.

theorem CategoryTheory.Triangulated.hlam_trans {C : Type u} [Category.{u_1, u} C] [Limits.HasZeroObject C] [HasShift C ℤ] [Preadditive C] [∀ (n : ℤ), (shiftFunctor C n).Additive] [Pretriangulated C] {Λ : Type u'} [AddCommGroup Λ] (v : K₀ C →+ Λ) (Φ Ψ : C ≌ C) [Φ.inverse.Additive] [Ψ.inverse.Additive] [Φ.inverse.CommShift ℤ] [Ψ.inverse.CommShift ℤ] [Φ.inverse.IsTriangulated] [Ψ.inverse.IsTriangulated] {lam₁ lam₂ : Λ →+ Λ} (h₁ : ∀ (x : K₀ C), v ((K₀.map Φ.inverse) x) = lam₁ (v x)) (h₂ : ∀ (x : K₀ C), v ((K₀.map Ψ.inverse) x) = lam₂ (v x)) (x : K₀ C) : v ((K₀.map (Φ.trans Ψ).inverse) x) = (lam₁.comp lam₂) (v x)

The composite carries the composite lattice map.

The order is the one the quasi-inverse forces: (Φ.trans Ψ).inverse is Ψ.inverse ⋙ Φ.inverse, so lam₂ acts first and lam₁ last.

theorem CategoryTheory.Triangulated.actStabAut_trans {C : Type u} [Category.{u_1, u} C] [Limits.HasZeroObject C] [HasShift C ℤ] [Preadditive C] [∀ (n : ℤ), (shiftFunctor C n).Additive] [Pretriangulated C] [IsTriangulated C] {Λ : Type u'} [AddCommGroup Λ] (v : K₀ C →+ Λ) (Φ Ψ : C ≌ C) [Φ.functor.Additive] [Φ.inverse.Additive] [Ψ.functor.Additive] [Ψ.inverse.Additive] [Φ.functor.CommShift ℤ] [Φ.inverse.CommShift ℤ] [Ψ.functor.CommShift ℤ] [Ψ.inverse.CommShift ℤ] [Φ.functor.IsTriangulated] [Φ.inverse.IsTriangulated] [Ψ.functor.IsTriangulated] [Ψ.inverse.IsTriangulated] {lam₁ lam₂ : Λ →+ Λ} (h₁ : ∀ (x : K₀ C), v ((K₀.map Φ.inverse) x) = lam₁ (v x)) (h₂ : ∀ (x : K₀ C), v ((K₀.map Ψ.inverse) x) = lam₂ (v x)) (σ : StabilityCondition.WithClassMap C v) : actStabAut Ψ v lam₂ h₂ (actStabAut Φ v lam₁ h₁ σ) = actStabAut (Φ.trans Ψ) v (lam₁.comp lam₂) ⋯ σ

Transporting twice is transporting once along the composite.

The associativity clause of an action, stated as a single equation. The lattice map of the composite is lam₁.comp lam₂, supplied by hlam_trans, so no new hypothesis enters.