The class-map-compatible autoequivalence action

WeakStabilityCondition/StabilityCondition/Symmetry/Autoequivalence/Stability/Transport.lean produced actStabAut: a well-defined map on StabilityCondition.WithClassMap C v, and said so carefully, because the thing doing the acting was a pair (Φ, lam) and AutQuot groups the Φs alone.

This file bundles the pair and closes that gap. AutPairQuot v is a Group and it acts:

MulAction (AutPairQuot v) (StabilityCondition.WithClassMap C v)

The class-lattice datum has to be invertible, and that is not a detail

actStabAut asks only for lam : Λ →+ Λ, which is all a single application needs. A group needs lam⁻¹, and nothing produces one: v is an arbitrary additive map, so lam is genuinely extra input rather than something recovered from Φ. So the pair carries lam : Λ ≃+ Λ.

This is a real strengthening of the hypothesis, not repackaging. A Φ equipped with a non-invertible compatible lam still acts as a map — actStabAut is unchanged and still applies — but it is not a member of this group.

Where the inverse comes from is worth seeing, because it is the only step that uses Φ being an equivalence rather than merely a triangulated endofunctor: Φ.functor ⋙ Φ.inverse ≅ 𝟭 C via unitIso, and K₀.map_congr turns that natural isomorphism into an equality of maps on K₀. That is what lets compat be transported to Φ.symm.

What is quotiented, and what deliberately is not

Φ is taken modulo natural isomorphism, exactly as in AutQuot and for the same reason — TriEquiv.act_congr, resting on a slicing's closedUnderIso.

lam is not quotiented; the setoid asks for it on the nose. Two different lams can be compatible with the same Φ whenever v is not surjective, and they give genuinely different central charges σ.Z ∘ lam. Identifying them would make the action ill defined, so the relation is the conjunction and not a condition on Φ alone.

What this group is NOT

It is not Aut(D). It is not even a quotient or a subgroup of AutQuot C in any way proved here. The evident forgetful map AutPairQuot v → AutQuot C is neither shown injective (different lam over the same Φ) nor surjective (a Φ admitting no compatible lam at all has no preimage). Both statements are about v, and v is arbitrary. Say "the group of autoequivalences equipped with a compatible class-lattice automorphism", never "Aut(D) acts on stability conditions".

The Φ component uses the usual relation on autoequivalences: natural isomorphism of the forward functors. Natural isomorphism of the chosen inverses follows from uniqueness of right adjoints.

structure CategoryTheory.Triangulated.WeakStabilityCondition.StabilityCondition.GroupAction.AutPair {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 →+ Λ) : Type (max (max u u') w)

A triangulated auto-equivalence together with the class-lattice automorphism that carries it, and the compatibility tying them to v.

lam is an ≃+ rather than a →+ because this is going to be a group; see the module docstring.

• Φ : TriEquiv C

  The auto-equivalence, with its instances travelling alongside.

• lam : Λ ≃+ Λ

  The induced automorphism of the class lattice. Extra data, not recovered from Φ, because v is arbitrary.

• compat (x : K₀ C) : v ((K₀.map self.Φ.e.inverse) x) = self.lam (v x)

  v ∘ K₀(Φ⁻¹) = lam ∘ v.

def CategoryTheory.Triangulated.WeakStabilityCondition.StabilityCondition.GroupAction.AutPair.id {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 →+ Λ) : AutPair v

The identity pair.

Equations

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

def CategoryTheory.Triangulated.WeakStabilityCondition.StabilityCondition.GroupAction.AutPair.mul {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 →+ Λ} (a b : AutPair v) : AutPair v

mul a b is a * b: it acts by b first, matching (a * b) • σ = a • (b • σ).

Both components reverse, and they must reverse together — the Φs compose contravariantly through Equivalence.trans while the lams compose covariantly through AddEquiv.trans, and it is the two together that make compat survive.

Equations

• a.mul b = { Φ := b.Φ.comp a.Φ, lam := a.lam.trans b.lam, compat := ⋯ }

def CategoryTheory.Triangulated.WeakStabilityCondition.StabilityCondition.GroupAction.AutPair.inv {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 →+ Λ} (a : AutPair v) : AutPair v

The inverse pair.

The only step in this file that uses Φ being an equivalence: unitIso gives Φ.functor ⋙ Φ.inverse ≅ 𝟭 C, and K₀.map_congr promotes that natural isomorphism to an equality of maps on K₀. Without it there is no way to move compat across to Φ⁻¹.

Equations

• a.inv = { Φ := a.Φ.symm, lam := a.lam.symm, compat := ⋯ }

@[implicit_reducible]

instance CategoryTheory.Triangulated.WeakStabilityCondition.StabilityCondition.GroupAction.AutPair.setoid {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 →+ Λ) : Setoid (AutPair v)

Isomorphism of pairs: the auto-equivalences are naturally isomorphic, and the class-lattice automorphisms are equal.

lam on the nose, deliberately — see the module docstring.

Equations

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

The action

noncomputable def CategoryTheory.Triangulated.WeakStabilityCondition.StabilityCondition.GroupAction.AutPair.act {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 →+ Λ} (a : AutPair v) (σ : StabilityCondition.WithClassMap C v) : StabilityCondition.WithClassMap C v

The action of a pair, which is actStabAut with the datum bundled.

Equations

• a.act σ = CategoryTheory.Triangulated.actStabAut a.Φ.e v a.lam.toAddMonoidHom ⋯ σ

@[simp]

theorem CategoryTheory.Triangulated.WeakStabilityCondition.StabilityCondition.GroupAction.AutPair.act_slicing {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 →+ Λ} (a : AutPair v) (σ : StabilityCondition.WithClassMap C v) : (a.act σ).slicing = σ.slicing.mapEquiv a.Φ.e

@[simp]

theorem CategoryTheory.Triangulated.WeakStabilityCondition.StabilityCondition.GroupAction.AutPair.act_Z {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 →+ Λ} (a : AutPair v) (σ : StabilityCondition.WithClassMap C v) (x : Λ) : (a.act σ).Z x = σ.Z (a.lam x)

theorem CategoryTheory.Triangulated.WeakStabilityCondition.StabilityCondition.GroupAction.AutPair.act_id {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) : (id v).act σ = σ

theorem CategoryTheory.Triangulated.WeakStabilityCondition.StabilityCondition.GroupAction.AutPair.act_mul {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 →+ Λ} (a b : AutPair v) (σ : StabilityCondition.WithClassMap C v) : (a.mul b).act σ = a.act (b.act σ)

theorem CategoryTheory.Triangulated.WeakStabilityCondition.StabilityCondition.GroupAction.AutPair.act_congr {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 →+ Λ} {a b : AutPair v} (h : a ≈ b) (σ : StabilityCondition.WithClassMap C v) : a.act σ = b.act σ

Descent. Isomorphic pairs act identically.

The slicing half is TriEquiv.act_congr; the charge half is immediate, because the setoid fixed lam on the nose rather than up to anything.

def CategoryTheory.Triangulated.WeakStabilityCondition.StabilityCondition.GroupAction.AutPairQuot {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 →+ Λ) : Type (max (max u u') w)

Autoequivalences carrying a compatible class-lattice automorphism, modulo natural isomorphism of the auto-equivalence.

Not Aut(D) — see the module docstring before citing it as such.

Equations

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

@[implicit_reducible]

instance CategoryTheory.Triangulated.WeakStabilityCondition.StabilityCondition.GroupAction.AutPairQuot.group {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 →+ Λ} : Group (AutPairQuot v)

Equations

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

def CategoryTheory.Triangulated.WeakStabilityCondition.StabilityCondition.GroupAction.AutPairQuot.mk {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 →+ Λ} (a : AutPair v) : AutPairQuot v

The class of a pair. Explicit return type for the same reason as AutQuot.mk: AutPairQuot is a plain def, so a bare _root_.Quotient.mk leaves • unable to find its instance.

Equations

• CategoryTheory.Triangulated.WeakStabilityCondition.StabilityCondition.GroupAction.AutPairQuot.mk a = ⟦a⟧

@[implicit_reducible]

noncomputable instance CategoryTheory.Triangulated.WeakStabilityCondition.StabilityCondition.GroupAction.AutPairQuot.mulAction {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 →+ Λ} : MulAction (AutPairQuot v) (StabilityCondition.WithClassMap C v)

The Aut half of §8, as a group action.

This is the statement WeakStabilityCondition/StabilityCondition/Symmetry/Autoequivalence/Stability/Transport.lean could not make.

Equations

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

@[simp]

theorem CategoryTheory.Triangulated.WeakStabilityCondition.StabilityCondition.GroupAction.AutPairQuot.mk_smul_slicing {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 →+ Λ} (a : AutPair v) (σ : StabilityCondition.WithClassMap C v) : (mk a • σ).slicing = σ.slicing.mapEquiv a.Φ.e

@[simp]

theorem CategoryTheory.Triangulated.WeakStabilityCondition.StabilityCondition.GroupAction.AutPairQuot.mk_smul_Z {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 →+ Λ} (a : AutPair v) (σ : StabilityCondition.WithClassMap C v) (x : Λ) : (mk a • σ).Z x = σ.Z (a.lam x)

def CategoryTheory.Triangulated.WeakStabilityCondition.StabilityCondition.GroupAction.AutPairQuot.toAutQuot {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 →+ Λ} : AutPairQuot v →* AutQuot C

The Φ component, forgetting the class-lattice datum.

A group homomorphism, and neither injective nor surjective in general — both failures are about v. Recorded as a MonoidHom because it is useful, not because it identifies this group with AutQuot C.

Equations

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