Conjugate morphisms by isomorphisms

An isomorphism α : X ≅ Y defines

• a monoid isomorphism CategoryTheory.Iso.conj : End X ≃* End Y by α.conj f = α.inv ≫ f ≫ α.hom;
• a group isomorphism CategoryTheory.Iso.conjAut : Aut X ≃* Aut Y by α.conjAut f = α.symm ≪≫ f ≪≫ α using CategoryTheory.Iso.homCongr : (X ≅ X₁) → (Y ≅ Y₁) → (X ⟶ Y) ≃ (X₁ ⟶ Y₁) and CategoryTheory.Iso.isoCongr : (f : X₁ ≅ X₂) → (g : Y₁ ≅ Y₂) → (X₁ ≅ Y₁) ≃ (X₂ ≅ Y₂) which are defined in CategoryTheory.HomCongr.

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

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

theorem CategoryTheory.Iso.conj_apply {C : Type u} [Category.{v, u} C] {X Y : C} (α : X ≅ Y) (f : End X) : α.conj f = CategoryStruct.comp α.inv (CategoryStruct.comp f α.hom)

@[simp]

theorem CategoryTheory.Iso.conj_comp {C : Type u} [Category.{v, u} C] {X Y : C} (α : X ≅ Y) (f g : End X) : α.conj (CategoryStruct.comp f g) = CategoryStruct.comp (α.conj f) (α.conj g)

@[simp]

theorem CategoryTheory.Iso.conj_id {C : Type u} [Category.{v, u} C] {X Y : C} (α : X ≅ Y) : α.conj (CategoryStruct.id X) = CategoryStruct.id Y

@[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 : ℕ) : α.conj (f ^ n) = α.conj f ^ n

def CategoryTheory.Iso.conjAut {C : Type u} [Category.{v, u} C] {X Y : C} (α : X ≅ Y) : Aut X ≃* Aut Y

conj defines a group isomorphism between groups of automorphisms

theorem CategoryTheory.Iso.conjAut_apply {C : Type u} [Category.{v, u} C] {X Y : C} (α : X ≅ Y) (f : Aut X) : α.conjAut f = α.symm ≪≫ f ≪≫ α

@[simp]

theorem CategoryTheory.Iso.conjAut_hom {C : Type u} [Category.{v, u} C] {X Y : C} (α : X ≅ Y) (f : Aut X) : (α.conjAut f).hom = α.conj f.hom

@[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) : (α ≪≫ β).conjAut f = β.conjAut (α.conjAut f)

@[simp]

theorem CategoryTheory.Iso.conjAut_mul {C : Type u} [Category.{v, u} C] {X Y : C} (α : X ≅ Y) (f g : Aut X) : α.conjAut (f * g) = α.conjAut f * α.conjAut g

@[simp]

theorem CategoryTheory.Iso.conjAut_trans {C : Type u} [Category.{v, u} C] {X Y : C} (α : X ≅ Y) (f g : Aut X) : α.conjAut (f ≪≫ g) = α.conjAut f ≪≫ α.conjAut g

@[simp]

theorem CategoryTheory.Iso.conjAut_pow {C : Type u} [Category.{v, u} C] {X Y : C} (α : X ≅ Y) (f : Aut X) (n : ℕ) : α.conjAut (f ^ n) = α.conjAut f ^ n

@[simp]

theorem CategoryTheory.Iso.conjAut_zpow {C : Type u} [Category.{v, u} C] {X Y : C} (α : X ≅ Y) (f : Aut X) (n : ℤ) : α.conjAut (f ^ n) = α.conjAut f ^ 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)