Strict autoequivalence groups acting on slicings

Aut(D) is not a group in Lean: C ≌ C under composition is associative only up to natural isomorphism, so it carries no Group instance and MulAction is not available. This file takes the cheap way out, deliberately: instead of quotienting to isomorphism classes, it asks for a group that maps into endofunctors strictly.

That works because functor composition in Lean is strictly associative — C ⥤ C is an honest monoid under ⋙. So StrictAut G C below is just a monoid homomorphism G → (C ⥤ C) whose functors are triangulated, and the resulting MulAction G (Slicing C) needs no coherence bookkeeping at all.

What this deliberately does NOT cover

map_one and map_mul are equalities of functors, so F g ⋙ F g⁻¹ = 𝟭 C on the nose: each F g is an isomorphism of categories, not merely an equivalence. Many autoequivalences one actually cares about — Serre functors, spherical twists — satisfy that only up to natural isomorphism, and are therefore out of scope here.

So this is a real restriction, not a reformulation. It buys a strict MulAction today at the cost of generality; the general Aut(D) action still wants the quotient. Do not cite this as "the Aut action is formalized". The stability-foundation ownership record notes this deliberate restriction.

What it does cover

Everything hard is already in WeakStabilityCondition/StabilityCondition/Symmetry/Autoequivalence/Slicing/Transport.lean — PostnikovTower.mapF, HNFiltration.mapF, Slicing.mapEquiv. This file only supplies the group packaging: StrictAut.equiv turns the strict data into an honest Equivalence (unit and counit are eqToIso, and the coherence field discharges automatically), and the MulAction laws are then two simps.

The MulAction is a def, not an instance — ρ is unrecoverable by instance search, so as an instance it was dead code. See mulActionSlicing's own docstring.

structure CategoryTheory.Triangulated.WeakStabilityCondition.StabilityCondition.GroupAction.StrictAut (G : Type u_1) [Group G] (C : Type u) [Category.{w, u} C] [Limits.HasZeroObject C] [HasShift C ℤ] [Preadditive C] [∀ (n : ℤ), (shiftFunctor C n).Additive] [Pretriangulated C] : Type (max (max u u_1) w)

A strict action of a group G on C by triangulated autoequivalences: a monoid hom into C ⥤ C, which is a strict monoid under ⋙.

map_mul is contravariant (F (g * h) = F h ⋙ F g) because ⋙ is diagrammatic order: (F h ⋙ F g).obj = F g ∘ F h.

• F : G → Functor C C

  The endofunctor attached to a group element.

• map_one : self.F 1 = Functor.id C

  The unit acts as the identity functor, on the nose.

• map_mul (g h : G) : self.F (g * h) = (self.F h).comp (self.F g)

  Multiplication is composition, on the nose.

• additive (g : G) : (self.F g).Additive

  Every F g is additive.

• commShift (g : G) : (self.F g).CommShift ℤ

  Every F g commutes with the shift. Unlike its neighbours this field is data, not a proof — Functor.CommShift carries the comparison isomorphism — which is why docBlame asks for a docstring here and not for the Prop-valued fields around it.

• triangulated (g : G) : (self.F g).IsTriangulated

  Every F g sends distinguished triangles to distinguished triangles.

theorem CategoryTheory.Triangulated.WeakStabilityCondition.StabilityCondition.GroupAction.StrictAut.comp_inv {C : Type u} [Category.{w, u} C] [Limits.HasZeroObject C] [HasShift C ℤ] [Preadditive C] [∀ (n : ℤ), (shiftFunctor C n).Additive] [Pretriangulated C] {G : Type u_1} [Group G] (ρ : StrictAut G C) (g : G) : (ρ.F g).comp (ρ.F g⁻¹) = Functor.id C

theorem CategoryTheory.Triangulated.WeakStabilityCondition.StabilityCondition.GroupAction.StrictAut.inv_comp {C : Type u} [Category.{w, u} C] [Limits.HasZeroObject C] [HasShift C ℤ] [Preadditive C] [∀ (n : ℤ), (shiftFunctor C n).Additive] [Pretriangulated C] {G : Type u_1} [Group G] (ρ : StrictAut G C) (g : G) : (ρ.F g⁻¹).comp (ρ.F g) = Functor.id C

theorem CategoryTheory.Triangulated.WeakStabilityCondition.StabilityCondition.GroupAction.StrictAut.obj_inv {C : Type u} [Category.{w, u} C] [Limits.HasZeroObject C] [HasShift C ℤ] [Preadditive C] [∀ (n : ℤ), (shiftFunctor C n).Additive] [Pretriangulated C] {G : Type u_1} [Group G] (ρ : StrictAut G C) (g : G) (X : C) : (ρ.F g⁻¹).obj ((ρ.F g).obj X) = X

theorem CategoryTheory.Triangulated.WeakStabilityCondition.StabilityCondition.GroupAction.StrictAut.obj_self {C : Type u} [Category.{w, u} C] [Limits.HasZeroObject C] [HasShift C ℤ] [Preadditive C] [∀ (n : ℤ), (shiftFunctor C n).Additive] [Pretriangulated C] {G : Type u_1} [Group G] (ρ : StrictAut G C) (g : G) (X : C) : (ρ.F g).obj ((ρ.F g⁻¹).obj X) = X

theorem CategoryTheory.Triangulated.WeakStabilityCondition.StabilityCondition.GroupAction.StrictAut.F_inv_one {C : Type u} [Category.{w, u} C] [Limits.HasZeroObject C] [HasShift C ℤ] [Preadditive C] [∀ (n : ℤ), (shiftFunctor C n).Additive] [Pretriangulated C] {G : Type u_1} [Group G] (ρ : StrictAut G C) : ρ.F 1⁻¹ = Functor.id C

theorem CategoryTheory.Triangulated.WeakStabilityCondition.StabilityCondition.GroupAction.StrictAut.F_inv_mul {C : Type u} [Category.{w, u} C] [Limits.HasZeroObject C] [HasShift C ℤ] [Preadditive C] [∀ (n : ℤ), (shiftFunctor C n).Additive] [Pretriangulated C] {G : Type u_1} [Group G] (ρ : StrictAut G C) (g h : G) : ρ.F (g * h)⁻¹ = (ρ.F g⁻¹).comp (ρ.F h⁻¹)

noncomputable def CategoryTheory.Triangulated.WeakStabilityCondition.StabilityCondition.GroupAction.StrictAut.equiv {C : Type u} [Category.{w, u} C] [Limits.HasZeroObject C] [HasShift C ℤ] [Preadditive C] [∀ (n : ℤ), (shiftFunctor C n).Additive] [Pretriangulated C] {G : Type u_1} [Group G] (ρ : StrictAut G C) (g : G) : C ≌ C

Each ρ.F g is an equivalence, with ρ.F g⁻¹ as a strict inverse.

Unit and counit are eqToIso; Equivalence.mk's coherence field discharges automatically.

Equations

• ρ.equiv g = CategoryTheory.Equivalence.mk (ρ.F g) (ρ.F g⁻¹) (CategoryTheory.eqToIso ⋯) (CategoryTheory.eqToIso ⋯)

@[simp]

theorem CategoryTheory.Triangulated.WeakStabilityCondition.StabilityCondition.GroupAction.StrictAut.equiv_functor {C : Type u} [Category.{w, u} C] [Limits.HasZeroObject C] [HasShift C ℤ] [Preadditive C] [∀ (n : ℤ), (shiftFunctor C n).Additive] [Pretriangulated C] {G : Type u_1} [Group G] (ρ : StrictAut G C) (g : G) : (ρ.equiv g).functor = ρ.F g

@[simp]

theorem CategoryTheory.Triangulated.WeakStabilityCondition.StabilityCondition.GroupAction.StrictAut.equiv_inverse {C : Type u} [Category.{w, u} C] [Limits.HasZeroObject C] [HasShift C ℤ] [Preadditive C] [∀ (n : ℤ), (shiftFunctor C n).Additive] [Pretriangulated C] {G : Type u_1} [Group G] (ρ : StrictAut G C) (g : G) : (ρ.equiv g).inverse = ρ.F g⁻¹

noncomputable def CategoryTheory.Triangulated.WeakStabilityCondition.StabilityCondition.GroupAction.StrictAut.actSlicing {C : Type u} [Category.{w, u} C] [Limits.HasZeroObject C] [HasShift C ℤ] [Preadditive C] [∀ (n : ℤ), (shiftFunctor C n).Additive] [Pretriangulated C] {G : Type u_1} [Group G] (ρ : StrictAut G C) (g : G) (s : Slicing C) : Slicing C

g acts on a slicing by moving objects: (g • s).P φ X = s.P φ (g⁻¹ X).

Dual to relabel, which moves phases and fixes objects. The letIs must state each instance at the (ρ.equiv g).functor form — instance search will not unfold it to ρ.F g — and must be letI, not haveI, because Functor.IsTriangulated depends on the CommShift instance and an opaque haveI breaks the match.

Equations

• ρ.actSlicing g s = s.mapEquiv (ρ.equiv g)

@[simp]

theorem CategoryTheory.Triangulated.WeakStabilityCondition.StabilityCondition.GroupAction.StrictAut.actSlicing_P {C : Type u} [Category.{w, u} C] [Limits.HasZeroObject C] [HasShift C ℤ] [Preadditive C] [∀ (n : ℤ), (shiftFunctor C n).Additive] [Pretriangulated C] {G : Type u_1} [Group G] (ρ : StrictAut G C) (g : G) (s : Slicing C) (φ : ℝ) (X : C) : (ρ.actSlicing g s).P φ X = s.P φ ((ρ.F g⁻¹).obj X)

@[reducible]

noncomputable def CategoryTheory.Triangulated.WeakStabilityCondition.StabilityCondition.GroupAction.StrictAut.mulActionSlicing {C : Type u} [Category.{w, u} C] [Limits.HasZeroObject C] [HasShift C ℤ] [Preadditive C] [∀ (n : ℤ), (shiftFunctor C n).Additive] [Pretriangulated C] {G : Type u_1} [Group G] (ρ : StrictAut G C) : MulAction G (Slicing C)

A strict group of triangulated autoequivalences acts on slicings.

A def, not an instance, and that is forced rather than stylistic. ρ is explicit data appearing neither in the return type MulAction G (Slicing C) nor in any instance-implicit argument, so instance search has nothing to infer it from: as an instance this was unreachable and could never have fired — the impossibleInstance linter's finding, and a real defect, not a style nit.

It would also be the wrong thing to register globally even if it worked, since the head MulAction G (Slicing C) claims every group acts on the slicings of every pretriangulated category, for whatever ρ search happened to pick.

Bring it into scope at the use site with letI := ρ.mulActionSlicing. For an action • can find on its own, use AutQuot (WeakStabilityCondition/StabilityCondition/Symmetry/Autoequivalence/Slicing/Quotient.lean), where the acting object is the group.

@[reducible] because Lean requires it of any def whose type is a class — Mathlib's reducible-non-instance convention, and what makes the letI above transparent to later instance search.

Equations

• ρ.mulActionSlicing = { smul := ρ.actSlicing, mul_smul := ⋯, one_smul := ⋯ }