mathlib documentation

category_theory.conj

Conjugate morphisms by isomorphisms

An isomorphism α : X ≅ Y defines

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} [category_theory.category C] {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} [category_theory.category C] {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} [category_theory.category C] {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_trans {C : Type u} [category_theory.category C] {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} [category_theory.category C] {X₁ Y₁ X₂ Y₂ : C} (α : X₁ X₂) (β : Y₁ 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} [category_theory.category C] {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} [category_theory.category C] {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} [category_theory.category C] {X Y : C} (α : X Y) :
(α.conj) (𝟙 X) = 𝟙 Y

@[simp]
theorem category_theory.iso.trans_conj {C : Type u} [category_theory.category C] {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} [category_theory.category C] {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} [category_theory.category C] {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} [category_theory.category C] {X Y : C} (α : X Y) (f : category_theory.End X) (n : ) :
(α.conj) (f ^ n) = (α.conj) f ^ n

conj defines a group isomorphisms between groups of automorphisms

Equations
theorem category_theory.iso.conj_Aut_apply {C : Type u} [category_theory.category C] {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} [category_theory.category C] {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} [category_theory.category C] {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} [category_theory.category C] {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} [category_theory.category C] {X Y : C} (α : X Y) (f g : category_theory.Aut X) :

@[simp]
theorem category_theory.iso.conj_Aut_pow {C : Type u} [category_theory.category C] {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_gpow {C : Type u} [category_theory.category C] {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} [category_theory.category C] {D : Type u₁} [category_theory.category D] (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} [category_theory.category C] {D : Type u₁} [category_theory.category D] (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} [category_theory.category C] {D : Type u₁} [category_theory.category D] (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)