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.

@[implicit_reducible]

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

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

Equations

• α.conj = { toEquiv := CategoryTheory.End.homEquiv.trans ((α.homCongr α).trans CategoryTheory.End.homEquiv.symm), map_mul' := ⋯ }

@[simp]

theorem CategoryTheory.Iso.conj_symm_apply_asHom {C : Type u_1} [Category.{v_1, u_1} C] {X Y : C} (α : X ≅ Y) (a✝ : End Y) : (α.conj.symm a✝).asHom = CategoryStruct.comp α.hom (CategoryStruct.comp a✝.asHom α.inv)

@[simp]

theorem CategoryTheory.Iso.conj_apply_asHom {C : Type u_1} [Category.{v_1, u_1} C] {X Y : C} (α : X ≅ Y) (a✝ : End X) : (α.conj a✝).asHom = CategoryStruct.comp α.inv (CategoryStruct.comp a✝.asHom α.hom)

@[deprecated CategoryTheory.Iso.conj_apply_asHom (since := "2026-09-12")]

theorem CategoryTheory.Iso.conj_apply {C : Type u_1} [Category.{v_1, u_1} C] {X Y : C} (α : X ≅ Y) (a✝ : End X) : (α.conj a✝).asHom = CategoryStruct.comp α.inv (CategoryStruct.comp a✝.asHom α.hom)

Alias of CategoryTheory.Iso.conj_apply_asHom.

@[deprecated "use map_mul" (since := "2026-09-12")]

theorem CategoryTheory.Iso.conj_comp {C : Type u_1} [Category.{v_1, u_1} C] {X Y : C} (α : X ≅ Y) (f g : End X) : α.conj (f * g) = α.conj f * α.conj g

@[deprecated "use map_one" (since := "2026-09-12")]

theorem CategoryTheory.Iso.conj_id {C : Type u_1} [Category.{v_1, u_1} C] {X Y : C} (α : X ≅ Y) : α.conj 1 = 1

@[simp]

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

@[simp]

theorem CategoryTheory.Iso.trans_conj {C : Type u_1} [Category.{v_1, u_1} 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_1} [Category.{v_1, u_1} C] {X Y : C} (α : X ≅ Y) (f : End X) : α.symm.conj (α.conj f) = f

@[simp]

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

@[simp]

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

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

conj defines a group isomorphism 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_1} [Category.{v_1, u_1} C] {X Y : C} (α : X ≅ Y) (f : Aut X) : (α.conjAut f).asIso = α.symm ≪≫ f.asIso ≪≫ α

@[simp]

theorem CategoryTheory.Iso.conjAut_hom {C : Type u_1} [Category.{v_1, u_1} C] {X Y : C} (α : X ≅ Y) (f : Aut X) : (α.conjAut f).asIso.hom = (α.conj (Aut.toEnd f)).asHom

@[simp]

theorem CategoryTheory.Iso.trans_conjAut {C : Type u_1} [Category.{v_1, u_1} 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_1} [Category.{v_1, u_1} 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_1} [Category.{v_1, u_1} C] {X Y : C} (α : X ≅ Y) (f g : X ≅ X) : (α.conjAut { asIso := f ≪≫ g }).asIso = (α.conjAut { asIso := f }).asIso ≪≫ (α.conjAut { asIso := g }).asIso

@[simp]

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

theorem CategoryTheory.Functor.map_conj {C : Type u_1} [Category.{v_1, u_1} C] {D : Type u_2} [Category.{v_2, u_2} D] (F : Functor C D) {X Y : C} (α : X ≅ Y) (f : End X) : F.map (α.conj f).asHom = ((F.mapIso α).conj ((mapEnd X F) f)).asHom

theorem CategoryTheory.Functor.map_conjAut {C : Type u_1} [Category.{v_1, u_1} C] {D : Type u_2} [Category.{v_2, u_2} D] (F : Functor C D) {X Y : C} (α : X ≅ Y) (f : Aut X) : F.mapIso (α.conjAut f).asIso = ((F.mapIso α).conjAut ((mapAut X F) f)).asIso