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, and CategoryTheory.Iso.isoCongr : (f : X₁ ≅ X₂) → (g : Y₁ ≅ Y₂) → (X₁ ≅ Y₁) ≃ (X₂ ≅ Y₂).

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)

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 := ⋯ }

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

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

• α.conj = let __src := α.homCongr α; { toEquiv := __src, map_mul' := ⋯ }

theorem CategoryTheory.Iso.conj_apply {C : Type u} [CategoryTheory.Category.{v, u} C] {X : C} {Y : C} (α : X ≅ Y) (f : CategoryTheory.End X) : α.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) : α.conj (CategoryTheory.CategoryStruct.comp f g) = CategoryTheory.CategoryStruct.comp (α.conj f) (α.conj g)

@[simp]

theorem CategoryTheory.Iso.conj_id {C : Type u} [CategoryTheory.Category.{v, u} C] {X : C} {Y : C} (α : X ≅ Y) : α.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.refl X).conj 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) : (α ≪≫ β).conj f = β.conj (α.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) : α.symm.conj (α.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) : α.conj (α.symm.conj 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 : ℕ) : α.conj (f ^ n) = α.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

• α.conjAut = (CategoryTheory.Aut.unitsEndEquivAut X).symm.trans ((Units.mapEquiv α.conj).trans (CategoryTheory.Aut.unitsEndEquivAut Y))

theorem CategoryTheory.Iso.conjAut_apply {C : Type u} [CategoryTheory.Category.{v, u} C] {X : C} {Y : C} (α : X ≅ Y) (f : CategoryTheory.Aut X) : α.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) : (α.conjAut f).hom = α.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) : (α ≪≫ β).conjAut f = β.conjAut (α.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) : α.conjAut (f * g) = α.conjAut f * α.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) : α.conjAut (f ≪≫ g) = α.conjAut f ≪≫ α.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 : ℕ) : α.conjAut (f ^ n) = α.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 : ℤ) : α.conjAut (f ^ n) = α.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.map ((α.homCongr β) f) = ((F.mapIso α).homCongr (F.mapIso β)) (F.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.map (α.conj f) = (F.mapIso α).conj (F.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 (α.conjAut f) = (F.mapIso α).conjAut (F.mapIso f)