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.

def CategoryTheory.Iso.homCongr {C : Type u} [CategoryTheory.Category.{v, u} C] {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.

@[simp]

theorem CategoryTheory.Iso.homCongr_apply {C : Type u} [CategoryTheory.Category.{v, u} C] {X : C} {Y : C} {X₁ : C} {Y₁ : C} (α : X ≅ X₁) (β : Y ≅ Y₁) (f : X ⟶ Y) : (CategoryTheory.Iso.homCongr α β) f = CategoryTheory.CategoryStruct.comp α.inv (CategoryTheory.CategoryStruct.comp f β.hom)

theorem CategoryTheory.Iso.homCongr_comp {C : Type u} [CategoryTheory.Category.{v, u} C] {X : C} {Y : C} {Z : C} {X₁ : C} {Y₁ : C} {Z₁ : C} (α : X ≅ X₁) (β : Y ≅ Y₁) (γ : Z ≅ Z₁) (f : X ⟶ Y) (g : Y ⟶ Z) : (CategoryTheory.Iso.homCongr α γ) (CategoryTheory.CategoryStruct.comp f g) = CategoryTheory.CategoryStruct.comp ((CategoryTheory.Iso.homCongr α β) f) ((CategoryTheory.Iso.homCongr β γ) g)

theorem CategoryTheory.Iso.homCongr_refl {C : Type u} [CategoryTheory.Category.{v, u} C] {X : C} {Y : C} (f : X ⟶ Y) : (CategoryTheory.Iso.homCongr (CategoryTheory.Iso.refl X) (CategoryTheory.Iso.refl Y)) f = f

theorem CategoryTheory.Iso.homCongr_trans {C : Type u} [CategoryTheory.Category.{v, u} C] {X₁ : C} {Y₁ : C} {X₂ : C} {Y₂ : C} {X₃ : C} {Y₃ : C} (α₁ : X₁ ≅ X₂) (β₁ : Y₁ ≅ Y₂) (α₂ : X₂ ≅ X₃) (β₂ : Y₂ ≅ Y₃) (f : X₁ ⟶ Y₁) : (CategoryTheory.Iso.homCongr (α₁ ≪≫ α₂) (β₁ ≪≫ β₂)) f = ((CategoryTheory.Iso.homCongr α₁ β₁).trans (CategoryTheory.Iso.homCongr α₂ β₂)) f

@[simp]

theorem CategoryTheory.Iso.homCongr_symm {C : Type u} [CategoryTheory.Category.{v, u} C] {X₁ : C} {Y₁ : C} {X₂ : C} {Y₂ : C} (α : X₁ ≅ X₂) (β : Y₁ ≅ Y₂) : (CategoryTheory.Iso.homCongr α β).symm = CategoryTheory.Iso.homCongr α.symm β.symm

def CategoryTheory.Iso.conj {C : Type u} [CategoryTheory.Category.{v, u} C] {X : C} {Y : C} (α : X ≅ Y) : CategoryTheory.End X ≃* CategoryTheory.End Y

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

Equations

• One or more equations did not get rendered due to their size.

theorem CategoryTheory.Iso.conj_apply {C : Type u} [CategoryTheory.Category.{v, u} C] {X : C} {Y : C} (α : X ≅ Y) (f : CategoryTheory.End X) : (CategoryTheory.Iso.conj α) f = CategoryTheory.CategoryStruct.comp α.inv (CategoryTheory.CategoryStruct.comp f α.hom)

@[simp]

theorem CategoryTheory.Iso.conj_comp {C : Type u} [CategoryTheory.Category.{v, u} C] {X : C} {Y : C} (α : X ≅ Y) (f : CategoryTheory.End X) (g : CategoryTheory.End X) : (CategoryTheory.Iso.conj α) (CategoryTheory.CategoryStruct.comp f g) = CategoryTheory.CategoryStruct.comp ((CategoryTheory.Iso.conj α) f) ((CategoryTheory.Iso.conj α) g)

@[simp]

theorem CategoryTheory.Iso.conj_id {C : Type u} [CategoryTheory.Category.{v, u} C] {X : C} {Y : C} (α : X ≅ Y) : (CategoryTheory.Iso.conj α) (CategoryTheory.CategoryStruct.id X) = CategoryTheory.CategoryStruct.id Y

@[simp]

theorem CategoryTheory.Iso.refl_conj {C : Type u} [CategoryTheory.Category.{v, u} C] {X : C} (f : CategoryTheory.End X) : (CategoryTheory.Iso.conj (CategoryTheory.Iso.refl X)) f = f

@[simp]

theorem CategoryTheory.Iso.trans_conj {C : Type u} [CategoryTheory.Category.{v, u} C] {X : C} {Y : C} (α : X ≅ Y) {Z : C} (β : Y ≅ Z) (f : CategoryTheory.End X) : (CategoryTheory.Iso.conj (α ≪≫ β)) f = (CategoryTheory.Iso.conj β) ((CategoryTheory.Iso.conj α) f)

@[simp]

theorem CategoryTheory.Iso.symm_self_conj {C : Type u} [CategoryTheory.Category.{v, u} C] {X : C} {Y : C} (α : X ≅ Y) (f : CategoryTheory.End X) : (CategoryTheory.Iso.conj α.symm) ((CategoryTheory.Iso.conj α) f) = f

@[simp]

theorem CategoryTheory.Iso.self_symm_conj {C : Type u} [CategoryTheory.Category.{v, u} C] {X : C} {Y : C} (α : X ≅ Y) (f : CategoryTheory.End Y) : (CategoryTheory.Iso.conj α) ((CategoryTheory.Iso.conj α.symm) f) = f

theorem CategoryTheory.Iso.conj_pow {C : Type u} [CategoryTheory.Category.{v, u} C] {X : C} {Y : C} (α : X ≅ Y) (f : CategoryTheory.End X) (n : ℕ) : (CategoryTheory.Iso.conj α) (f ^ n) = (CategoryTheory.Iso.conj α) f ^ n

def CategoryTheory.Iso.conjAut {C : Type u} [CategoryTheory.Category.{v, u} C] {X : C} {Y : C} (α : X ≅ Y) : CategoryTheory.Aut X ≃* CategoryTheory.Aut Y

conj defines a group isomorphisms between groups of automorphisms

Equations

• One or more equations did not get rendered due to their size.

theorem CategoryTheory.Iso.conjAut_apply {C : Type u} [CategoryTheory.Category.{v, u} C] {X : C} {Y : C} (α : X ≅ Y) (f : CategoryTheory.Aut X) : (CategoryTheory.Iso.conjAut α) f = α.symm ≪≫ f ≪≫ α

@[simp]

theorem CategoryTheory.Iso.conjAut_hom {C : Type u} [CategoryTheory.Category.{v, u} C] {X : C} {Y : C} (α : X ≅ Y) (f : CategoryTheory.Aut X) : ((CategoryTheory.Iso.conjAut α) f).hom = (CategoryTheory.Iso.conj α) f.hom

@[simp]

theorem CategoryTheory.Iso.trans_conjAut {C : Type u} [CategoryTheory.Category.{v, u} C] {X : C} {Y : C} (α : X ≅ Y) {Z : C} (β : Y ≅ Z) (f : CategoryTheory.Aut X) : (CategoryTheory.Iso.conjAut (α ≪≫ β)) f = (CategoryTheory.Iso.conjAut β) ((CategoryTheory.Iso.conjAut α) f)

theorem CategoryTheory.Iso.conjAut_mul {C : Type u} [CategoryTheory.Category.{v, u} C] {X : C} {Y : C} (α : X ≅ Y) (f : CategoryTheory.Aut X) (g : CategoryTheory.Aut X) : (CategoryTheory.Iso.conjAut α) (f * g) = (CategoryTheory.Iso.conjAut α) f * (CategoryTheory.Iso.conjAut α) g

@[simp]

theorem CategoryTheory.Iso.conjAut_trans {C : Type u} [CategoryTheory.Category.{v, u} C] {X : C} {Y : C} (α : X ≅ Y) (f : CategoryTheory.Aut X) (g : CategoryTheory.Aut X) : (CategoryTheory.Iso.conjAut α) (f ≪≫ g) = (CategoryTheory.Iso.conjAut α) f ≪≫ (CategoryTheory.Iso.conjAut α) g

theorem CategoryTheory.Iso.conjAut_pow {C : Type u} [CategoryTheory.Category.{v, u} C] {X : C} {Y : C} (α : X ≅ Y) (f : CategoryTheory.Aut X) (n : ℕ) : (CategoryTheory.Iso.conjAut α) (f ^ n) = (CategoryTheory.Iso.conjAut α) f ^ n

theorem CategoryTheory.Iso.conjAut_zpow {C : Type u} [CategoryTheory.Category.{v, u} C] {X : C} {Y : C} (α : X ≅ Y) (f : CategoryTheory.Aut X) (n : ℤ) : (CategoryTheory.Iso.conjAut α) (f ^ n) = (CategoryTheory.Iso.conjAut α) f ^ n

theorem CategoryTheory.Functor.map_homCongr {C : Type u} [CategoryTheory.Category.{v, u} C] {D : Type u₁} [CategoryTheory.Category.{v₁, u₁} D] (F : CategoryTheory.Functor C D) {X : C} {Y : C} {X₁ : C} {Y₁ : C} (α : X ≅ X₁) (β : Y ≅ Y₁) (f : X ⟶ Y) : F.toPrefunctor.map ((CategoryTheory.Iso.homCongr α β) f) = (CategoryTheory.Iso.homCongr (F.mapIso α) (F.mapIso β)) (F.toPrefunctor.map f)

theorem CategoryTheory.Functor.map_conj {C : Type u} [CategoryTheory.Category.{v, u} C] {D : Type u₁} [CategoryTheory.Category.{v₁, u₁} D] (F : CategoryTheory.Functor C D) {X : C} {Y : C} (α : X ≅ Y) (f : CategoryTheory.End X) : F.toPrefunctor.map ((CategoryTheory.Iso.conj α) f) = (CategoryTheory.Iso.conj (F.mapIso α)) (F.toPrefunctor.map f)

theorem CategoryTheory.Functor.map_conjAut {C : Type u} [CategoryTheory.Category.{v, u} C] {D : Type u₁} [CategoryTheory.Category.{v₁, u₁} D] (F : CategoryTheory.Functor C D) {X : C} {Y : C} (α : X ≅ Y) (f : CategoryTheory.Aut X) : F.mapIso ((CategoryTheory.Iso.conjAut α) f) = (CategoryTheory.Iso.conjAut (F.mapIso α)) (F.mapIso f)