# mathlib3documentation

category_theory.conj

# Conjugate morphisms by isomorphisms #

THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4.

An isomorphism α : X ≅ Y defines

• a monoid isomorphism conj : End X ≃* End Y by α.conj f = α.inv ≫ f ≫ α.hom;
• a group isomorphism conj_Aut : Aut X ≃* Aut Y by α.conj_Aut f = α.symm ≪≫ f ≪≫ α.

For completeness, we also define hom_congr : (X ≅ X₁) → (Y ≅ Y₁) → (X ⟶ Y) ≃ (X₁ ⟶ Y₁), cf. equiv.arrow_congr.

def category_theory.iso.hom_congr {C : Type u} {X Y X₁ 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.arrow_congr.

Equations
@[simp]
theorem category_theory.iso.hom_congr_apply {C : Type u} {X Y X₁ Y₁ : C} (α : X X₁) (β : Y Y₁) (f : X Y) :
(α.hom_congr β) f = α.inv f β.hom
theorem category_theory.iso.hom_congr_comp {C : Type u} {X Y Z X₁ Y₁ Z₁ : C} (α : X X₁) (β : Y Y₁) (γ : Z Z₁) (f : X Y) (g : Y Z) :
(α.hom_congr γ) (f g) = (α.hom_congr β) f (β.hom_congr γ) g
@[simp]
theorem category_theory.iso.hom_congr_refl {C : Type u} {X Y : C} (f : X Y) :
= f
@[simp]
theorem category_theory.iso.hom_congr_trans {C : Type u} {X₁ Y₁ X₂ Y₂ X₃ Y₃ : C} (α₁ : X₁ X₂) (β₁ : Y₁ Y₂) (α₂ : X₂ X₃) (β₂ : Y₂ Y₃) (f : X₁ Y₁) :
((α₁ ≪≫ α₂).hom_congr (β₁ ≪≫ β₂)) f = ((α₁.hom_congr β₁).trans (α₂.hom_congr β₂)) f
@[simp]
theorem category_theory.iso.hom_congr_symm {C : Type u} {X₁ Y₁ X₂ Y₂ : C} (α : X₁ X₂) (β : Y₁ Y₂) :
def category_theory.iso.conj {C : Type u} {X Y : C} (α : X Y) :

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

Equations
theorem category_theory.iso.conj_apply {C : Type u} {X Y : C} (α : X Y) (f : category_theory.End X) :
(α.conj) f = α.inv f α.hom
@[simp]
theorem category_theory.iso.conj_comp {C : Type u} {X Y : C} (α : X Y) (f g : category_theory.End X) :
(α.conj) (f g) = (α.conj) f (α.conj) g
@[simp]
theorem category_theory.iso.conj_id {C : Type u} {X Y : C} (α : X Y) :
(α.conj) (𝟙 X) = 𝟙 Y
@[simp]
theorem category_theory.iso.refl_conj {C : Type u} {X : C} (f : category_theory.End X) :
f = f
@[simp]
theorem category_theory.iso.trans_conj {C : Type u} {X Y : C} (α : X Y) {Z : C} (β : Y Z) (f : category_theory.End X) :
((α ≪≫ β).conj) f = (β.conj) ((α.conj) f)
@[simp]
theorem category_theory.iso.symm_self_conj {C : Type u} {X Y : C} (α : X Y) (f : category_theory.End X) :
(α.symm.conj) ((α.conj) f) = f
@[simp]
theorem category_theory.iso.self_symm_conj {C : Type u} {X Y : C} (α : X Y) (f : category_theory.End Y) :
(α.conj) ((α.symm.conj) f) = f
@[simp]
theorem category_theory.iso.conj_pow {C : Type u} {X Y : C} (α : X Y) (f : category_theory.End X) (n : ) :
(α.conj) (f ^ n) = (α.conj) f ^ n
def category_theory.iso.conj_Aut {C : Type u} {X Y : C} (α : X Y) :

conj defines a group isomorphisms between groups of automorphisms

Equations
theorem category_theory.iso.conj_Aut_apply {C : Type u} {X Y : C} (α : X Y) (f : category_theory.Aut X) :
(α.conj_Aut) f = α.symm ≪≫ f ≪≫ α
@[simp]
theorem category_theory.iso.conj_Aut_hom {C : Type u} {X Y : C} (α : X Y) (f : category_theory.Aut X) :
((α.conj_Aut) f).hom = (α.conj) f.hom
@[simp]
theorem category_theory.iso.trans_conj_Aut {C : Type u} {X Y : C} (α : X Y) {Z : C} (β : Y Z) (f : category_theory.Aut X) :
((α ≪≫ β).conj_Aut) f = (β.conj_Aut) ((α.conj_Aut) f)
@[simp]
theorem category_theory.iso.conj_Aut_mul {C : Type u} {X Y : C} (α : X Y) (f g : category_theory.Aut X) :
(α.conj_Aut) (f * g) = (α.conj_Aut) f * (α.conj_Aut) g
@[simp]
theorem category_theory.iso.conj_Aut_trans {C : Type u} {X Y : C} (α : X Y) (f g : category_theory.Aut X) :
@[simp]
theorem category_theory.iso.conj_Aut_pow {C : Type u} {X Y : C} (α : X Y) (f : category_theory.Aut X) (n : ) :
(α.conj_Aut) (f ^ n) = (α.conj_Aut) f ^ n
@[simp]
theorem category_theory.iso.conj_Aut_zpow {C : Type u} {X Y : C} (α : X Y) (f : category_theory.Aut X) (n : ) :
(α.conj_Aut) (f ^ n) = (α.conj_Aut) f ^ n
theorem category_theory.functor.map_hom_congr {C : Type u} {D : Type u₁} (F : C D) {X Y X₁ Y₁ : C} (α : X X₁) (β : Y Y₁) (f : X Y) :
F.map ((α.hom_congr β) f) = ((F.map_iso α).hom_congr (F.map_iso β)) (F.map f)
theorem category_theory.functor.map_conj {C : Type u} {D : Type u₁} (F : C D) {X Y : C} (α : X Y) (f : category_theory.End X) :
F.map ((α.conj) f) = ((F.map_iso α).conj) (F.map f)
theorem category_theory.functor.map_conj_Aut {C : Type u} {D : Type u₁} (F : C D) {X Y : C} (α : X Y) (f : category_theory.Aut X) :
F.map_iso ((α.conj_Aut) f) = ((F.map_iso α).conj_Aut) (F.map_iso f)