AutQuot C as an honest group, by quotienting

WeakStabilityCondition/StabilityCondition/Symmetry/Autoequivalence/Slicing/Strict.lean bought a MulAction by restricting to autoequivalences with strict inverses — isomorphisms of categories — which excludes Serre functors and spherical twists, i.e. the cases that actually matter downstream.

This file does the general thing instead: quotient triangulated auto-equivalences by natural isomorphism. AutQuot C is a genuine Group, and nothing is excluded — every triangulated auto-equivalence has a class in it.

Why the action descends

act_congr is the whole point, and it is short: if Φ⁻¹ ≅ Ψ⁻¹ then for every X, Φ⁻¹ X ≅ Ψ⁻¹ X, so s.P φ (Φ⁻¹ X) and s.P φ (Ψ⁻¹ X) are equivalent propositions — because a slicing's P is closed under isomorphism. propext then makes them equal, so the two slicings are equal on the nose and Slicing.ext finishes.

So closedUnderIso, an axiom of Slicing that looks like bookkeeping, is exactly what makes the quotient action well defined.

Why the forward functor is enough

The quotient relation asks only for Φ.functor ≅ Ψ.functor, as the usual definition of Aut(D) does. The chosen inverses are right adjoints to those functors. Transporting one adjunction across the given natural isomorphism and applying uniqueness of right adjoints gives Φ.inverse ≅ Ψ.inverse. Thus no extra choice of inverse isomorphism is part of the relation.

Scope

Slicings only. The action on stability conditions additionally needs K₀ functoriality, a class-map compatibility datum, and invariance of strict finite length under an equivalence of interval categories.

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

A triangulated auto-equivalence, bundled with its instances so that they travel with it.

• e : C ≌ C

  The underlying equivalence.

• fAdd : self.e.functor.Additive
• iAdd : self.e.inverse.Additive
• fCS : self.e.functor.CommShift ℤ
• iCS : self.e.inverse.CommShift ℤ
• fTri : self.e.functor.IsTriangulated
• iTri : self.e.inverse.IsTriangulated

def CategoryTheory.Triangulated.WeakStabilityCondition.StabilityCondition.GroupAction.TriEquiv.id {C : Type u} [Category.{w, u} C] [Limits.HasZeroObject C] [HasShift C ℤ] [Preadditive C] [∀ (n : ℤ), (shiftFunctor C n).Additive] [Pretriangulated C] : TriEquiv C

The identity auto-equivalence.

inferInstanceAs throughout: instance search will not unfold Equivalence.refl.functor to 𝟭 C on its own.

Equations

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

def CategoryTheory.Triangulated.WeakStabilityCondition.StabilityCondition.GroupAction.TriEquiv.comp {C : Type u} [Category.{w, u} C] [Limits.HasZeroObject C] [HasShift C ℤ] [Preadditive C] [∀ (n : ℤ), (shiftFunctor C n).Additive] [Pretriangulated C] (Φ Ψ : TriEquiv C) : TriEquiv C

Composition.

Equations

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

def CategoryTheory.Triangulated.WeakStabilityCondition.StabilityCondition.GroupAction.TriEquiv.symm {C : Type u} [Category.{w, u} C] [Limits.HasZeroObject C] [HasShift C ℤ] [Preadditive C] [∀ (n : ℤ), (shiftFunctor C n).Additive] [Pretriangulated C] (Φ : TriEquiv C) : TriEquiv C

Inverse: swap the two halves.

Equations

• Φ.symm = { e := Φ.e.symm, fAdd := ⋯, iAdd := ⋯, fCS := Φ.iCS, iCS := Φ.fCS, fTri := ⋯, iTri := ⋯ }

noncomputable def CategoryTheory.Triangulated.WeakStabilityCondition.StabilityCondition.GroupAction.TriEquiv.act {C : Type u} [Category.{w, u} C] [Limits.HasZeroObject C] [HasShift C ℤ] [Preadditive C] [∀ (n : ℤ), (shiftFunctor C n).Additive] [Pretriangulated C] (Φ : TriEquiv C) (s : Slicing C) : Slicing C

The induced map on slicings, (Φ • s).P φ X = s.P φ (Φ⁻¹ X).

Equations

• Φ.act s = s.mapEquiv Φ.e

@[simp]

theorem CategoryTheory.Triangulated.WeakStabilityCondition.StabilityCondition.GroupAction.TriEquiv.act_P {C : Type u} [Category.{w, u} C] [Limits.HasZeroObject C] [HasShift C ℤ] [Preadditive C] [∀ (n : ℤ), (shiftFunctor C n).Additive] [Pretriangulated C] (Φ : TriEquiv C) (s : Slicing C) (φ : ℝ) (X : C) : (Φ.act s).P φ X = s.P φ (Φ.e.inverse.obj X)

theorem CategoryTheory.Triangulated.WeakStabilityCondition.StabilityCondition.GroupAction.TriEquiv.act_id {C : Type u} [Category.{w, u} C] [Limits.HasZeroObject C] [HasShift C ℤ] [Preadditive C] [∀ (n : ℤ), (shiftFunctor C n).Additive] [Pretriangulated C] (s : Slicing C) : id.act s = s

theorem CategoryTheory.Triangulated.WeakStabilityCondition.StabilityCondition.GroupAction.TriEquiv.act_comp {C : Type u} [Category.{w, u} C] [Limits.HasZeroObject C] [HasShift C ℤ] [Preadditive C] [∀ (n : ℤ), (shiftFunctor C n).Additive] [Pretriangulated C] (Φ Ψ : TriEquiv C) (s : Slicing C) : (Φ.comp Ψ).act s = Ψ.act (Φ.act s)

def CategoryTheory.Triangulated.WeakStabilityCondition.StabilityCondition.GroupAction.TriEquiv.inverseIsoOfFunctorIso {C : Type u} [Category.{w, u} C] [Limits.HasZeroObject C] [HasShift C ℤ] [Preadditive C] [∀ (n : ℤ), (shiftFunctor C n).Additive] [Pretriangulated C] {Φ Ψ : TriEquiv C} (h : Φ.e.functor ≅ Ψ.e.functor) : Φ.e.inverse ≅ Ψ.e.inverse

Naturally isomorphic equivalences have naturally isomorphic chosen inverses, by uniqueness of right adjoints.

Equations

• CategoryTheory.Triangulated.WeakStabilityCondition.StabilityCondition.GroupAction.TriEquiv.inverseIsoOfFunctorIso h = Φ.e.toAdjunction.rightAdjointUniq (Ψ.e.toAdjunction.ofNatIsoLeft h.symm)

theorem CategoryTheory.Triangulated.WeakStabilityCondition.StabilityCondition.GroupAction.TriEquiv.act_congr {C : Type u} [Category.{w, u} C] [Limits.HasZeroObject C] [HasShift C ℤ] [Preadditive C] [∀ (n : ℤ), (shiftFunctor C n).Additive] [Pretriangulated C] {Φ Ψ : TriEquiv C} (h : Φ.e.functor ≅ Ψ.e.functor) (s : Slicing C) : Φ.act s = Ψ.act s

Descent. Naturally isomorphic auto-equivalences act identically — not merely up to isomorphism of slicings, but equally, because Slicing.P is closed under isomorphism and propext upgrades the resulting Iff to Eq.

@[implicit_reducible]

instance CategoryTheory.Triangulated.WeakStabilityCondition.StabilityCondition.GroupAction.TriEquiv.setoid {C : Type u} [Category.{w, u} C] [Limits.HasZeroObject C] [HasShift C ℤ] [Preadditive C] [∀ (n : ℤ), (shiftFunctor C n).Additive] [Pretriangulated C] : Setoid (TriEquiv C)

Isomorphism of triangulated auto-equivalences, expressed by a natural isomorphism of their forward functors.

Equations

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

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

AutQuot C: triangulated auto-equivalences modulo natural isomorphism.

This is NOT the paper's Aut(D) and must not be named as it. TriEquiv.setoid quotients by a bare natural isomorphism of the underlying functors, leaving the CommShift datum unconstrained, so AutQuot C is a priori COARSER than exact autoequivalences modulo isomorphism of exact functors. Coarser makes the action theorem stronger, not weaker -- but it is a different group.

Unlike StrictAut, this excludes nothing.

Equations

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

@[implicit_reducible]

instance CategoryTheory.Triangulated.WeakStabilityCondition.StabilityCondition.GroupAction.AutQuot.group {C : Type u} [Category.{w, u} C] [Limits.HasZeroObject C] [HasShift C ℤ] [Preadditive C] [∀ (n : ℤ), (shiftFunctor C n).Additive] [Pretriangulated C] : Group (AutQuot C)

a * b composes b first, matching (a * b) • s = a • (b • s).

Equations

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

@[implicit_reducible]

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

AutQuot C acts on slicings. Well defined by TriEquiv.act_congr.

Equations

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

def CategoryTheory.Triangulated.WeakStabilityCondition.StabilityCondition.GroupAction.AutQuot.mk {C : Type u} [Category.{w, u} C] [Limits.HasZeroObject C] [HasShift C ℤ] [Preadditive C] [∀ (n : ℤ), (shiftFunctor C n).Additive] [Pretriangulated C] (Φ : TriEquiv C) : AutQuot C

The class of an auto-equivalence. Stated with an explicit AutQuot C return type: AutQuot is a plain def, so a bare _root_.Quotient.mk does not carry enough type information for • to find its instance.

Equations

• CategoryTheory.Triangulated.WeakStabilityCondition.StabilityCondition.GroupAction.AutQuot.mk Φ = ⟦Φ⟧

@[simp]

theorem CategoryTheory.Triangulated.WeakStabilityCondition.StabilityCondition.GroupAction.AutQuot.mk_smul_P {C : Type u} [Category.{w, u} C] [Limits.HasZeroObject C] [HasShift C ℤ] [Preadditive C] [∀ (n : ℤ), (shiftFunctor C n).Additive] [Pretriangulated C] (Φ : TriEquiv C) (s : Slicing C) (φ : ℝ) (X : C) : (mk Φ • s).P φ X = s.P φ (Φ.e.inverse.obj X)