The group of autoequivalence classes

The units of the monoid of natural isomorphism classes of endofunctors form a group. Its opposite uses functional composition as multiplication: the product of the classes of F and G is the class of G ⋙ F. Every self-equivalence defines an element, with its inverse functor representing the inverse element.

A group homomorphism into this group is an action by autoequivalences up to natural isomorphism; the Artin-group actions on homotopy and derived categories take values here. For underlying skeleton calculations, activate endofunctorMonoidalCategory locally, as in Mathlib.

Main definitions

• TauCeti.AutoequivalenceClass: the group of natural isomorphism classes of autoequivalences.
• CategoryTheory.Equivalence.toAutoequivalenceClass: the class of a self-equivalence.

Main results

• CategoryTheory.Equivalence.toAutoequivalenceClass_eq_iff: two self-equivalences have the same class exactly when their functors are naturally isomorphic.

@[reducible, inline]

abbrev TauCeti.AutoequivalenceClass (C : Type u) [CategoryTheory.Category.{v, u} C] : Type (max u v)

Autoequivalence classes, with multiplication in functional composition order.

def CategoryTheory.Equivalence.toAutoequivalenceClass {C : Type u} [Category.{v, u} C] (e : C ≌ C) : TauCeti.AutoequivalenceClass C

A self-equivalence determines its natural isomorphism class as a group element.

@[simp]

theorem CategoryTheory.Equivalence.toAutoequivalenceClass_val {C : Type u} [Category.{v, u} C] (e : C ≌ C) : ↑(MulOpposite.unop e.toAutoequivalenceClass) = toSkeleton e.functor

The forward functor represents the underlying endofunctor class.

@[simp]

theorem CategoryTheory.Equivalence.toAutoequivalenceClass_inv_val {C : Type u} [Category.{v, u} C] (e : C ≌ C) : ↑(MulOpposite.unop e.toAutoequivalenceClass)⁻¹ = toSkeleton e.inverse

The inverse functor represents the inverse unit component.

theorem CategoryTheory.Equivalence.toAutoequivalenceClass_eq_iff {C : Type u} [Category.{v, u} C] (e e' : C ≌ C) : e.toAutoequivalenceClass = e'.toAutoequivalenceClass ↔ Nonempty (e.functor ≅ e'.functor)

Two self-equivalences have the same class exactly when their functors are naturally isomorphic.

@[simp]

theorem CategoryTheory.Equivalence.toAutoequivalenceClass_refl {C : Type u} [Category.{v, u} C] : refl.toAutoequivalenceClass = 1

The identity equivalence represents the identity group element.

@[simp]

theorem CategoryTheory.Equivalence.toAutoequivalenceClass_symm {C : Type u} [Category.{v, u} C] (e : C ≌ C) : e.symm.toAutoequivalenceClass = e.toAutoequivalenceClass⁻¹

Taking the inverse equivalence gives the inverse group element.

@[simp]

theorem CategoryTheory.Equivalence.toAutoequivalenceClass_trans {C : Type u} [Category.{v, u} C] (e e' : C ≌ C) : (e.trans e').toAutoequivalenceClass = e'.toAutoequivalenceClass * e.toAutoequivalenceClass

Equivalence composition is reversed in functional-order multiplication.