# 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 ≪≫ α.

For completeness, we also define CategoryTheory.Iso.homCongr : (X ≅ X₁) → (Y ≅ Y₁) → (X ⟶ Y) ≃ (X₁ ⟶ Y₁), cf. Equiv.arrowCongr, and CategoryTheory.Iso.isoCongr : (f : X₁ ≅ X₂) → (g : Y₁ ≅ Y₂) → (X₁ ≅ Y₁) ≃ (X₂ ≅ Y₂).

def CategoryTheory.Iso.homCongr {C : Type u} {X : C} {Y : C} {X₁ : C} {Y₁ : C} (α : X X₁) (β : Y Y₁) :
(X Y) (X₁ Y₁)

If X is isomorphic to X₁ and Y is isomorphic to Y₁, then there is a natural bijection between X ⟶ Y and X₁ ⟶ Y₁. See also Equiv.arrowCongr.

Equations
• One or more equations did not get rendered due to their size.
Instances For
@[simp]
theorem CategoryTheory.Iso.homCongr_apply {C : Type u} {X : C} {Y : C} {X₁ : C} {Y₁ : C} (α : X X₁) (β : Y Y₁) (f : X Y) :
(α.homCongr β) f =
theorem CategoryTheory.Iso.homCongr_comp {C : Type u} {X : C} {Y : C} {Z : C} {X₁ : C} {Y₁ : C} {Z₁ : C} (α : X X₁) (β : Y Y₁) (γ : Z Z₁) (f : X Y) (g : Y Z) :
(α.homCongr γ) = CategoryTheory.CategoryStruct.comp ((α.homCongr β) f) ((β.homCongr γ) g)
theorem CategoryTheory.Iso.homCongr_refl {C : Type u} {X : C} {Y : C} (f : X Y) :
(.homCongr ) f = f
theorem CategoryTheory.Iso.homCongr_trans {C : Type u} {X₁ : C} {Y₁ : C} {X₂ : C} {Y₂ : C} {X₃ : C} {Y₃ : C} (α₁ : X₁ X₂) (β₁ : Y₁ Y₂) (α₂ : X₂ X₃) (β₂ : Y₂ Y₃) (f : X₁ Y₁) :
((α₁ ≪≫ α₂).homCongr (β₁ ≪≫ β₂)) f = ((α₁.homCongr β₁).trans (α₂.homCongr β₂)) f
@[simp]
theorem CategoryTheory.Iso.homCongr_symm {C : Type u} {X₁ : C} {Y₁ : C} {X₂ : C} {Y₂ : C} (α : X₁ X₂) (β : Y₁ Y₂) :
(α.homCongr β).symm = α.symm.homCongr β.symm
def CategoryTheory.Iso.isoCongr {C : Type u} {X₁ : C} {Y₁ : C} {X₂ : C} {Y₂ : C} (f : X₁ X₂) (g : Y₁ Y₂) :
(X₁ Y₁) (X₂ Y₂)

If X is isomorphic to X₁ and Y is isomorphic to Y₁, then there is a bijection between X ≅ Y and X₁ ≅ Y₁.

Equations
• f.isoCongr g = { toFun := fun (h : X₁ Y₁) => f.symm ≪≫ h ≪≫ g, invFun := fun (h : X₂ Y₂) => f ≪≫ h ≪≫ g.symm, left_inv := , right_inv := }
Instances For
def CategoryTheory.Iso.isoCongrLeft {C : Type u} {X₁ : C} {X₂ : C} {Y : C} (f : X₁ X₂) :
(X₁ Y) (X₂ Y)

If X₁ is isomorphic to X₂, then there is a bijection between X₁ ≅ Y and X₂ ≅ Y.

Equations
• f.isoCongrLeft = f.isoCongr
Instances For
def CategoryTheory.Iso.isoCongrRight {C : Type u} {X : C} {Y₁ : C} {Y₂ : C} (g : Y₁ Y₂) :
(X Y₁) (X Y₂)

If Y₁ is isomorphic to Y₂, then there is a bijection between X ≅ Y₁ and X ≅ Y₂.

Equations
• g.isoCongrRight = .isoCongr g
Instances For
def CategoryTheory.Iso.conj {C : Type u} {X : C} {Y : C} (α : X Y) :

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

Equations
• α.conj = let __src := α.homCongr α; { toEquiv := __src, map_mul' := }
Instances For
theorem CategoryTheory.Iso.conj_apply {C : Type u} {X : C} {Y : C} (α : X Y) (f : ) :
α.conj f =
@[simp]
theorem CategoryTheory.Iso.conj_comp {C : Type u} {X : C} {Y : C} (α : X Y) (f : ) (g : ) :
α.conj = CategoryTheory.CategoryStruct.comp (α.conj f) (α.conj g)
@[simp]
theorem CategoryTheory.Iso.conj_id {C : Type u} {X : C} {Y : C} (α : X Y) :
@[simp]
theorem CategoryTheory.Iso.refl_conj {C : Type u} {X : C} (f : ) :
.conj f = f
@[simp]
theorem CategoryTheory.Iso.trans_conj {C : Type u} {X : C} {Y : C} (α : X Y) {Z : C} (β : Y Z) (f : ) :
(α ≪≫ β).conj f = β.conj (α.conj f)
@[simp]
theorem CategoryTheory.Iso.symm_self_conj {C : Type u} {X : C} {Y : C} (α : X Y) (f : ) :
α.symm.conj (α.conj f) = f
@[simp]
theorem CategoryTheory.Iso.self_symm_conj {C : Type u} {X : C} {Y : C} (α : X Y) (f : ) :
α.conj (α.symm.conj f) = f
theorem CategoryTheory.Iso.conj_pow {C : Type u} {X : C} {Y : C} (α : X Y) (f : ) (n : ) :
α.conj (f ^ n) = α.conj f ^ n
def CategoryTheory.Iso.conjAut {C : Type u} {X : C} {Y : C} (α : X Y) :

conj defines a group isomorphisms between groups of automorphisms

Equations
Instances For
theorem CategoryTheory.Iso.conjAut_apply {C : Type u} {X : C} {Y : C} (α : X Y) (f : ) :
α.conjAut f = α.symm ≪≫ f ≪≫ α
@[simp]
theorem CategoryTheory.Iso.conjAut_hom {C : Type u} {X : C} {Y : C} (α : X Y) (f : ) :
(α.conjAut f).hom = α.conj f.hom
@[simp]
theorem CategoryTheory.Iso.trans_conjAut {C : Type u} {X : C} {Y : C} (α : X Y) {Z : C} (β : Y Z) (f : ) :
(α ≪≫ β).conjAut f = β.conjAut (α.conjAut f)
theorem CategoryTheory.Iso.conjAut_mul {C : Type u} {X : C} {Y : C} (α : X Y) (f : ) (g : ) :
α.conjAut (f * g) = α.conjAut f * α.conjAut g
@[simp]
theorem CategoryTheory.Iso.conjAut_trans {C : Type u} {X : C} {Y : C} (α : X Y) (f : ) (g : ) :
α.conjAut (f ≪≫ g) = α.conjAut f ≪≫ α.conjAut g
theorem CategoryTheory.Iso.conjAut_pow {C : Type u} {X : C} {Y : C} (α : X Y) (f : ) (n : ) :
α.conjAut (f ^ n) = α.conjAut f ^ n
theorem CategoryTheory.Iso.conjAut_zpow {C : Type u} {X : C} {Y : C} (α : X Y) (f : ) (n : ) :
α.conjAut (f ^ n) = α.conjAut f ^ n
theorem CategoryTheory.Functor.map_homCongr {C : Type u} {D : Type u₁} [] (F : ) {X : C} {Y : C} {X₁ : C} {Y₁ : C} (α : X X₁) (β : Y Y₁) (f : X Y) :
F.map ((α.homCongr β) f) = ((F.mapIso α).homCongr (F.mapIso β)) (F.map f)
theorem CategoryTheory.Functor.map_conj {C : Type u} {D : Type u₁} [] (F : ) {X : C} {Y : C} (α : X Y) (f : ) :
F.map (α.conj f) = (F.mapIso α).conj (F.map f)
theorem CategoryTheory.Functor.map_conjAut {C : Type u} {D : Type u₁} [] (F : ) {X : C} {Y : C} (α : X Y) (f : ) :
F.mapIso (α.conjAut f) = (F.mapIso α).conjAut (F.mapIso f)