Conjugate morphisms by isomorphisms #
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}
[category_theory.category C]
{X Y X₁ Y₁ : C}
(α : X ≅ X₁)
(β : Y ≅ 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
.
@[simp]
theorem
category_theory.iso.hom_congr_refl
{C : Type u}
[category_theory.category C]
{X Y : C}
(f : X ⟶ Y) :
⇑((category_theory.iso.refl X).hom_congr (category_theory.iso.refl Y)) f = f
An isomorphism between two objects defines a monoid isomorphism between their monoid of endomorphisms.
theorem
category_theory.iso.conj_apply
{C : Type u}
[category_theory.category C]
{X Y : C}
(α : X ≅ Y)
(f : category_theory.End X) :
@[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) :
@[simp]
theorem
category_theory.iso.conj_id
{C : Type u}
[category_theory.category C]
{X Y : C}
(α : X ≅ Y) :
@[simp]
theorem
category_theory.iso.refl_conj
{C : Type u}
[category_theory.category C]
{X : C}
(f : category_theory.End X) :
⇑((category_theory.iso.refl X).conj) f = f
@[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) :
@[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) :
@[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) :
@[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
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) :
@[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) :
@[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) :
@[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) :
@[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 : ℕ) :
@[simp]
theorem
category_theory.iso.conj_Aut_zpow
{C : Type u}
[category_theory.category C]
{X Y : C}
(α : X ≅ Y)
(f : category_theory.Aut X)
(n : ℤ) :
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) :
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) :