Conjugate morphisms by isomorphisms

We define CategoryTheory.Iso.homCongr : (X ≅ X₁) → (Y ≅ Y₁) → (X ⟶ Y) ≃ (X₁ ⟶ Y₁), cf. Equiv.arrowCongr, and CategoryTheory.Iso.isoCongr : (f : X₁ ≅ X₂) → (g : Y₁ ≅ Y₂) → (X₁ ≅ Y₁) ≃ (X₂ ≅ Y₂).

As corollaries, 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 ≪≫ α which can be found in CategoryTheory.Conj.

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) : (α.homCongr β) f = CategoryTheory.CategoryStruct.comp α.inv (CategoryTheory.CategoryStruct.comp f β.hom)

@[simp]

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

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) : (α.homCongr γ) (CategoryTheory.CategoryStruct.comp f g) = CategoryTheory.CategoryStruct.comp ((α.homCongr β) f) ((β.homCongr γ) g)

theorem CategoryTheory.Iso.homCongr_refl {C : Type u} [CategoryTheory.Category.{v, u} C] {X : C} {Y : C} (f : X ⟶ Y) : ((CategoryTheory.Iso.refl X).homCongr (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₁) : ((α₁ ≪≫ α₂).homCongr (β₁ ≪≫ β₂)) f = ((α₁.homCongr β₁).trans (α₂.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₂) : (α.homCongr β).symm = α.symm.homCongr β.symm

def CategoryTheory.Iso.isoCongr {C : Type u} [CategoryTheory.Category.{v, u} C] {X₁ : C} {Y₁ : C} {X₂ : C} {Y₂ : C} (f : X₁ ≅ X₂) (g : Y₁ ≅ Y₂) : (X₁ ≅ Y₁) ≃ (X₂ ≅ Y₂)

If X is isomorphic to X₁ and Y is isomorphic to Y₁, then there is a bijection between X ≅ Y and X₁ ≅ Y₁.

Equations

• f.isoCongr g = { toFun := fun (h : X₁ ≅ Y₁) => f.symm ≪≫ h ≪≫ g, invFun := fun (h : X₂ ≅ Y₂) => f ≪≫ h ≪≫ g.symm, left_inv := ⋯, right_inv := ⋯ }

@[simp]

theorem CategoryTheory.Iso.isoCongr_symm_apply {C : Type u} [CategoryTheory.Category.{v, u} C] {X₁ : C} {Y₁ : C} {X₂ : C} {Y₂ : C} (f : X₁ ≅ X₂) (g : Y₁ ≅ Y₂) (h : X₂ ≅ Y₂) : (f.isoCongr g).symm h = f ≪≫ h ≪≫ g.symm

@[simp]

theorem CategoryTheory.Iso.isoCongr_apply {C : Type u} [CategoryTheory.Category.{v, u} C] {X₁ : C} {Y₁ : C} {X₂ : C} {Y₂ : C} (f : X₁ ≅ X₂) (g : Y₁ ≅ Y₂) (h : X₁ ≅ Y₁) : (f.isoCongr g) h = f.symm ≪≫ h ≪≫ g

def CategoryTheory.Iso.isoCongrLeft {C : Type u} [CategoryTheory.Category.{v, u} C] {X₁ : C} {X₂ : C} {Y : C} (f : X₁ ≅ X₂) : (X₁ ≅ Y) ≃ (X₂ ≅ Y)

If X₁ is isomorphic to X₂, then there is a bijection between X₁ ≅ Y and X₂ ≅ Y.

Equations

• f.isoCongrLeft = f.isoCongr (CategoryTheory.Iso.refl Y)

def CategoryTheory.Iso.isoCongrRight {C : Type u} [CategoryTheory.Category.{v, u} C] {X : C} {Y₁ : C} {Y₂ : C} (g : Y₁ ≅ Y₂) : (X ≅ Y₁) ≃ (X ≅ Y₂)

If Y₁ is isomorphic to Y₂, then there is a bijection between X ≅ Y₁ and X ≅ Y₂.

Equations

• g.isoCongrRight = (CategoryTheory.Iso.refl X).isoCongr g

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.map ((α.homCongr β) f) = ((F.mapIso α).homCongr (F.mapIso β)) (F.map f)

theorem CategoryTheory.Functor.map_isoCongr {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.mapIso ((α.isoCongr β) f) = ((F.mapIso α).isoCongr (F.mapIso β)) (F.mapIso f)