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} [CategoryTheory.Category.{v, u} C] {X : C} {Y : C} (α : X ≅ Y) : CategoryTheory.End X ≃* CategoryTheory.End Y

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

Equations

• α.conj = { toEquiv := α.homCongr α, map_mul' := ⋯ }

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

@[simp]

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

@[simp]

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

@[simp]

theorem CategoryTheory.Iso.refl_conj {C : Type u} [CategoryTheory.Category.{v, u} C] {X : C} (f : CategoryTheory.End X) : (CategoryTheory.Iso.refl X).conj f = f

@[simp]

theorem CategoryTheory.Iso.trans_conj {C : Type u} [CategoryTheory.Category.{v, u} C] {X : C} {Y : C} (α : X ≅ Y) {Z : C} (β : Y ≅ Z) (f : CategoryTheory.End X) : (α ≪≫ β).conj f = β.conj (α.conj f)

@[simp]

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

@[simp]

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

@[simp]

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

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

conj defines a group isomorphisms between groups of automorphisms

Equations

• α.conjAut = (CategoryTheory.Aut.unitsEndEquivAut X).symm.trans ((Units.mapEquiv α.conj).trans (CategoryTheory.Aut.unitsEndEquivAut Y))

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

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

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

theorem CategoryTheory.Functor.map_conj {C : Type u} [CategoryTheory.Category.{v, u} C] {D : Type u₁} [CategoryTheory.Category.{v₁, u₁} D] (F : CategoryTheory.Functor C D) {X : C} {Y : C} (α : X ≅ Y) (f : CategoryTheory.End X) : F.map (α.conj f) = (F.mapIso α).conj (F.map f)

theorem CategoryTheory.Functor.map_conjAut {C : Type u} [CategoryTheory.Category.{v, u} C] {D : Type u₁} [CategoryTheory.Category.{v₁, u₁} D] (F : CategoryTheory.Functor C D) {X : C} {Y : C} (α : X ≅ Y) (f : CategoryTheory.Aut X) : F.mapIso (α.conjAut f) = (F.mapIso α).conjAut (F.mapIso f)