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} [Category.{v, u} 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.arrowCongr.

@[simp]

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

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

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

theorem CategoryTheory.Iso.homCongr_trans {C : Type u} [Category.{v, u} C] {X₁ Y₁ X₂ Y₂ X₃ 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} [Category.{v, u} C] {X₁ Y₁ X₂ Y₂ : C} (α : X₁ ≅ X₂) (β : Y₁ ≅ Y₂) : (α.homCongr β).symm = α.symm.homCongr β.symm

def CategoryTheory.Iso.isoCongr {C : Type u} [Category.{v, u} C] {X₁ Y₁ X₂ 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₁.

@[simp]

theorem CategoryTheory.Iso.isoCongr_symm_apply {C : Type u} [Category.{v, u} C] {X₁ Y₁ X₂ 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} [Category.{v, u} C] {X₁ Y₁ X₂ 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} [Category.{v, u} C] {X₁ X₂ 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.

def CategoryTheory.Iso.isoCongrRight {C : Type u} [Category.{v, u} C] {X Y₁ 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₂.

theorem CategoryTheory.Functor.map_homCongr {C : Type u} [Category.{v, u} C] {D : Type u₁} [Category.{v₁, u₁} D] (F : Functor C D) {X Y X₁ 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} [Category.{v, u} C] {D : Type u₁} [Category.{v₁, u₁} D] (F : Functor C D) {X Y X₁ Y₁ : C} (α : X ≅ X₁) (β : Y ≅ Y₁) (f : X ≅ Y) : F.mapIso ((α.isoCongr β) f) = ((F.mapIso α).isoCongr (F.mapIso β)) (F.mapIso f)