Documentation

Mathlib.CategoryTheory.Conj

Conjugate morphisms by isomorphisms #

An isomorphism α : X ≅ Y defines

def CategoryTheory.Iso.conj {C : Type u} [Category.{v, u} C] {X Y : C} (α : X Y) :

An isomorphism between two objects defines a monoid isomorphism between their monoid of endomorphisms.

Equations
Instances For
    @[simp]
    theorem CategoryTheory.Iso.conj_comp {C : Type u} [Category.{v, u} C] {X Y : C} (α : X Y) (f g : End X) :
    @[simp]
    theorem CategoryTheory.Iso.refl_conj {C : Type u} [Category.{v, u} C] {X : C} (f : End X) :
    (refl X).conj f = f
    @[simp]
    theorem CategoryTheory.Iso.trans_conj {C : Type u} [Category.{v, u} C] {X Y : C} (α : X Y) {Z : C} (β : Y Z) (f : End X) :
    (α ≪≫ β).conj f = β.conj (α.conj f)
    @[simp]
    theorem CategoryTheory.Iso.symm_self_conj {C : Type u} [Category.{v, u} C] {X Y : C} (α : X Y) (f : End X) :
    α.symm.conj (α.conj f) = f
    @[simp]
    theorem CategoryTheory.Iso.self_symm_conj {C : Type u} [Category.{v, u} C] {X Y : C} (α : X Y) (f : End Y) :
    α.conj (α.symm.conj f) = f
    @[simp]
    theorem CategoryTheory.Iso.conj_pow {C : Type u} [Category.{v, u} C] {X Y : C} (α : X Y) (f : End X) (n : ) :
    def CategoryTheory.Iso.conjAut {C : Type u} [Category.{v, u} C] {X Y : C} (α : X Y) :

    conj defines a group isomorphisms between groups of automorphisms

    Equations
    Instances For
      @[simp]
      theorem CategoryTheory.Iso.conjAut_hom {C : Type u} [Category.{v, u} C] {X Y : C} (α : X Y) (f : Aut X) :
      @[simp]
      theorem CategoryTheory.Iso.trans_conjAut {C : Type u} [Category.{v, u} C] {X Y : C} (α : X Y) {Z : C} (β : Y Z) (f : Aut X) :
      @[simp]
      theorem CategoryTheory.Iso.conjAut_mul {C : Type u} [Category.{v, u} C] {X Y : C} (α : X Y) (f g : Aut X) :
      @[simp]
      theorem CategoryTheory.Iso.conjAut_trans {C : Type u} [Category.{v, u} C] {X Y : C} (α : X Y) (f g : Aut X) :
      @[simp]
      theorem CategoryTheory.Iso.conjAut_pow {C : Type u} [Category.{v, u} C] {X Y : C} (α : X Y) (f : Aut X) (n : ) :
      @[simp]
      theorem CategoryTheory.Iso.conjAut_zpow {C : Type u} [Category.{v, u} C] {X Y : C} (α : X Y) (f : Aut X) (n : ) :
      theorem CategoryTheory.Functor.map_conj {C : Type u} [Category.{v, u} C] {D : Type u₁} [Category.{v₁, u₁} D] (F : Functor C D) {X Y : C} (α : X Y) (f : End X) :
      F.map (α.conj f) = (F.mapIso α).conj (F.map f)
      theorem CategoryTheory.Functor.map_conjAut {C : Type u} [Category.{v, u} C] {D : Type u₁} [Category.{v₁, u₁} D] (F : Functor C D) {X Y : C} (α : X Y) (f : Aut X) :
      F.mapIso (α.conjAut f) = (F.mapIso α).conjAut (F.mapIso f)