Transport of autoequivalence actions

An equivalence e : C ≌ D transports a self-equivalence F of C to e.symm.trans (F.trans e). On natural-isomorphism classes this is a group isomorphism, with functional composition as multiplication. Consequently any group action by autoequivalence classes transports along a supplied equivalence.

Equivalence.autoequivalenceClassCongr_eq_iff characterizes this transport by natural intertwining isomorphisms of the representing functors.

The construction uses Mathlib's Equivalence.congrLeft, Equivalence.congrRight and Equivalence.skeletonIsoCat.objEquiv on endofunctors, then Units.mapEquiv on their invertible classes. It applies in particular to braid actions on equivalent homotopy or derived categories; no choice of a Morita equivalence is implicit.

For ρ : H →* AutoequivalenceClass C, the transported action is e.autoequivalenceClassCongr.toMonoidHom.comp ρ. Mathlib's MulEquiv.monoidHomCongrRightEquiv packages this as an equivalence on actions.

noncomputable def CategoryTheory.Equivalence.endofunctorClassCongr {C : Type u₁} [Category.{v₁, u₁} C] {D : Type u₂} [Category.{v₂, u₂} D] (e : C ≌ D) : Skeleton (Functor C C) ≃* Skeleton (Functor D D)

Conjugation along a category equivalence identifies the monoids of natural-isomorphism classes of endofunctors.

@[simp]

theorem CategoryTheory.Equivalence.endofunctorClassCongr_toSkeleton {C : Type u₁} [Category.{v₁, u₁} C] {D : Type u₂} [Category.{v₂, u₂} D] (e : C ≌ D) (F : Functor C C) : e.endofunctorClassCongr (toSkeleton F) = toSkeleton ((e.inverse.comp F).comp e.functor)

Transport of an endofunctor class is represented by its conjugate functor.

@[simp]

theorem CategoryTheory.Equivalence.endofunctorClassCongr_refl {C : Type u₁} [Category.{v₁, u₁} C] : refl.endofunctorClassCongr = MulEquiv.refl (Skeleton (Functor C C))

Transport along the identity equivalence fixes every endofunctor class.

theorem CategoryTheory.Equivalence.endofunctorClassCongr_trans {C : Type u₁} [Category.{v₁, u₁} C] {D : Type u₂} [Category.{v₂, u₂} D] {E : Type u₃} [Category.{v₃, u₃} E] (e : C ≌ D) (f : D ≌ E) : (e.trans f).endofunctorClassCongr = e.endofunctorClassCongr.trans f.endofunctorClassCongr

Successive equivalences transport endofunctor classes successively.

theorem CategoryTheory.Equivalence.endofunctorClassCongr_symm {C : Type u₁} [Category.{v₁, u₁} C] {D : Type u₂} [Category.{v₂, u₂} D] (e : C ≌ D) : e.symm.endofunctorClassCongr = e.endofunctorClassCongr.symm

Reversing the supplied equivalence reverses transport of endofunctor classes.

noncomputable def CategoryTheory.Equivalence.autoequivalenceClassCongr {C : Type u₁} [Category.{v₁, u₁} C] {D : Type u₂} [Category.{v₂, u₂} D] (e : C ≌ D) : TauCeti.AutoequivalenceClass C ≃* TauCeti.AutoequivalenceClass D

Conjugation along an equivalence gives an isomorphism of groups of autoequivalence classes, in functional composition order.

@[simp]

theorem CategoryTheory.Equivalence.autoequivalenceClassCongr_val {C : Type u₁} [Category.{v₁, u₁} C] {D : Type u₂} [Category.{v₂, u₂} D] (e : C ≌ D) (x : TauCeti.AutoequivalenceClass C) : ↑(MulOpposite.unop (e.autoequivalenceClassCongr x)) = e.endofunctorClassCongr ↑(MulOpposite.unop x)

The underlying endofunctor class of a transported unit is its transported endofunctor class.

@[simp]

theorem CategoryTheory.Equivalence.autoequivalenceClassCongr_toAutoequivalenceClass {C : Type u₁} [Category.{v₁, u₁} C] {D : Type u₂} [Category.{v₂, u₂} D] (e : C ≌ D) (F : C ≌ C) : e.autoequivalenceClassCongr F.toAutoequivalenceClass = ((e.symm.trans F).trans e).toAutoequivalenceClass

Transport sends an explicit self-equivalence to its conjugate.

@[simp]

theorem CategoryTheory.Equivalence.autoequivalenceClassCongr_refl {C : Type u₁} [Category.{v₁, u₁} C] : refl.autoequivalenceClassCongr = MulEquiv.refl (TauCeti.AutoequivalenceClass C)

Transport along the identity equivalence fixes every autoequivalence class.

theorem CategoryTheory.Equivalence.autoequivalenceClassCongr_trans {C : Type u₁} [Category.{v₁, u₁} C] {D : Type u₂} [Category.{v₂, u₂} D] {E : Type u₃} [Category.{v₃, u₃} E] (e : C ≌ D) (f : D ≌ E) : (e.trans f).autoequivalenceClassCongr = e.autoequivalenceClassCongr.trans f.autoequivalenceClassCongr

Transport of autoequivalence classes is compatible with composition of the supplied equivalences.

theorem CategoryTheory.Equivalence.autoequivalenceClassCongr_symm {C : Type u₁} [Category.{v₁, u₁} C] {D : Type u₂} [Category.{v₂, u₂} D] (e : C ≌ D) : e.symm.autoequivalenceClassCongr = e.autoequivalenceClassCongr.symm

Reversing the supplied equivalence reverses transport of autoequivalence classes.

def CategoryTheory.Equivalence.transportedEndofunctorIso {C : Type u₁} [Category.{v₁, u₁} C] {D : Type u₂} [Category.{v₂, u₂} D] (e : C ≌ D) (F : Functor C C) : e.functor.comp ((e.inverse.comp F).comp e.functor) ≅ F.comp e.functor

The endofunctor transported across an equivalence intertwines with the original endofunctor across that equivalence.

@[simp]

theorem CategoryTheory.Equivalence.transportedEndofunctorIso_hom_app {C : Type u₁} [Category.{v₁, u₁} C] {D : Type u₂} [Category.{v₂, u₂} D] (e : C ≌ D) (F : Functor C C) (X : C) : (e.transportedEndofunctorIso F).hom.app X = e.functor.map (F.map (e.unitIso.inv.app X))

The intertwiner is induced by the inverse of the equivalence's unit.

@[simp]

theorem CategoryTheory.Equivalence.transportedEndofunctorIso_inv_app {C : Type u₁} [Category.{v₁, u₁} C] {D : Type u₂} [Category.{v₂, u₂} D] (e : C ≌ D) (F : Functor C C) (X : C) : (e.transportedEndofunctorIso F).inv.app X = e.functor.map (F.map (e.unitIso.hom.app X))

The inverse intertwiner is induced by the equivalence's unit.

theorem CategoryTheory.Equivalence.autoequivalenceClassCongr_eq_iff {C : Type u₁} [Category.{v₁, u₁} C] {D : Type u₂} [Category.{v₂, u₂} D] (e : C ≌ D) (F : C ≌ C) (F' : D ≌ D) : e.autoequivalenceClassCongr F.toAutoequivalenceClass = F'.toAutoequivalenceClass ↔ Nonempty (e.functor.comp F'.functor ≅ F.functor.comp e.functor)

A self-equivalence represents the transported class precisely when the supplied equivalence intertwines its functor with the original functor.