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} [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

α.hom_congr β = {to_fun := λ (f : X ⟶ Y), α.inv ≫ f ≫ β.hom, inv_fun := λ (f : X₁ ⟶ Y₁), α.hom ≫ f ≫ β.inv, left_inv := _, right_inv := _}

source

@[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

source

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

source

@[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

source

@[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

source

@[simp]

theorem category_theory.iso.hom_congr_symm {C : Type u} [category_theory.category C] {X₁ Y₁ X₂ Y₂ : C} (α : X₁ ≅ X₂) (β : Y₁ ≅ Y₂) :

(α.hom_congr β).symm = α.symm.hom_congr β.symm

source

def category_theory.iso.conj {C : Type u} [category_theory.category C] {X Y : C} (α : X ≅ Y) :

category_theory.End X ≃* category_theory.End Y

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

Equations

α.conj = {to_fun := (α.hom_congr α).to_fun, inv_fun := (α.hom_congr α).inv_fun, left_inv := _, right_inv := _, map_mul' := _}

source

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

source

@[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

source

@[simp]

theorem category_theory.iso.conj_id {C : Type u} [category_theory.category C] {X Y : C} (α : X ≅ Y) :

⇑(α.conj) (𝟙 X) = 𝟙 Y

source

@[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

source

@[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)

source

@[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

source

@[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

source

@[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

source

def category_theory.iso.conj_Aut {C : Type u} [category_theory.category C] {X Y : C} (α : X ≅ Y) :

category_theory.Aut X ≃* category_theory.Aut Y

conj defines a group isomorphisms between groups of automorphisms

Equations

α.conj_Aut = (category_theory.Aut.units_End_equiv_Aut X).symm.trans ((units.map_equiv α.conj).trans (category_theory.Aut.units_End_equiv_Aut Y))

source

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

source

@[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

source

@[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)

source

@[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

source

@[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) :

⇑(α.conj_Aut) (f ≪≫ g) = ⇑(α.conj_Aut) f ≪≫ ⇑(α.conj_Aut) g

source

@[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

source

@[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 : ℤ) :

⇑(α.conj_Aut) (f ^ n) = ⇑(α.conj_Aut) f ^ n

source

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)

source

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)

source

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)