doc-next-gen

Mathlib.CategoryTheory.HomCongr

Module docstring

{"# 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. "}

CategoryTheory.Iso.homCongr definition
{X Y X₁ Y₁ : C} (α : X ≅ X₁) (β : Y ≅ Y₁) : (X ⟶ Y) ≃ (X₁ ⟶ Y₁)
Full source 
/-- 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`. -/
@[simps]
def homCongr {X Y X₁ Y₁ : C} (α : X ≅ X₁) (β : Y ≅ Y₁) : (X ⟶ Y) ≃ (X₁ ⟶ Y₁) where
  toFun f := α.inv ≫ f ≫ β.hom
  invFun f := α.hom ≫ f ≫ β.inv
  left_inv f :=
    show α.hom ≫ (α.inv ≫ f ≫ β.hom) ≫ β.inv = f by
      rw [Category.assoc, Category.assoc, β.hom_inv_id, α.hom_inv_id_assoc, Category.comp_id]
  right_inv f :=
    show α.inv ≫ (α.hom ≫ f ≫ β.inv) ≫ β.hom = f by
      rw [Category.assoc, Category.assoc, β.inv_hom_id, α.inv_hom_id_assoc, Category.comp_id]
Bijection of morphism sets via isomorphisms
Informal description
Given isomorphisms $\alpha : X \cong X_1$ and $\beta : Y \cong Y_1$ in a category $\mathcal{C}$, there is a natural bijection between the morphism sets $\text{Hom}(X, Y)$ and $\text{Hom}(X_1, Y_1)$. The bijection is given by: - Forward direction: $f \mapsto \alpha^{-1} \circ f \circ \beta$ - Backward direction: $f \mapsto \alpha \circ f \circ \beta^{-1}$
CategoryTheory.Iso.homCongr_comp theorem
{X Y Z X₁ Y₁ Z₁ : C} (α : X ≅ X₁) (β : Y ≅ Y₁) (γ : Z ≅ Z₁) (f : X ⟶ Y) (g : Y ⟶ Z) : α.homCongr γ (f ≫ g) = α.homCongr β f ≫ β.homCongr γ g
Full source 
theorem homCongr_comp {X Y Z X₁ Y₁ Z₁ : C} (α : X ≅ X₁) (β : Y ≅ Y₁) (γ : Z ≅ Z₁) (f : X ⟶ Y)
    (g : Y ⟶ Z) : α.homCongr γ (f ≫ g) = α.homCongr β f ≫ β.homCongr γ g := by simp
Compatibility of `homCongr` with Morphism Composition
Informal description
Given isomorphisms $\alpha \colon X \cong X_1$, $\beta \colon Y \cong Y_1$, and $\gamma \colon Z \cong Z_1$ in a category $\mathcal{C}$, and morphisms $f \colon X \to Y$ and $g \colon Y \to Z$, the following equality holds: \[ \alpha.\text{homCongr}(\gamma)(f \circ g) = (\alpha.\text{homCongr}(\beta)(f)) \circ (\beta.\text{homCongr}(\gamma)(g)). \] Here, $\text{homCongr}$ denotes the bijection between morphism sets induced by the isomorphisms, and $\circ$ denotes composition of morphisms.
CategoryTheory.Iso.homCongr_refl theorem
{X Y : C} (f : X ⟶ Y) : (Iso.refl X).homCongr (Iso.refl Y) f = f
Full source 
theorem homCongr_refl {X Y : C} (f : X ⟶ Y) : (Iso.refl X).homCongr (Iso.refl Y) f = f := by simp
Identity Isomorphisms Induce Identity Bijection on Morphisms
Informal description
For any morphism $f \colon X \to Y$ in a category $\mathcal{C}$, the bijection $\text{homCongr}$ induced by the identity isomorphisms on $X$ and $Y$ maps $f$ to itself, i.e., $\text{homCongr}(\text{id}_X, \text{id}_Y)(f) = f$.
CategoryTheory.Iso.homCongr_trans theorem
{X₁ Y₁ X₂ Y₂ X₃ Y₃ : C} (α₁ : X₁ ≅ X₂) (β₁ : Y₁ ≅ Y₂) (α₂ : X₂ ≅ X₃) (β₂ : Y₂ ≅ Y₃) (f : X₁ ⟶ Y₁) : (α₁ ≪≫ α₂).homCongr (β₁ ≪≫ β₂) f = (α₁.homCongr β₁).trans (α₂.homCongr β₂) f
Full source 
theorem homCongr_trans {X₁ Y₁ X₂ Y₂ X₃ Y₃ : C} (α₁ : X₁ ≅ X₂) (β₁ : Y₁ ≅ Y₂) (α₂ : X₂ ≅ X₃)
    (β₂ : Y₂ ≅ Y₃) (f : X₁ ⟶ Y₁) :
    (α₁ ≪≫ α₂).homCongr (β₁ ≪≫ β₂) f = (α₁.homCongr β₁).trans (α₂.homCongr β₂) f := by simp
Compatibility of `homCongr` with Composition of Isomorphisms
Informal description
Given isomorphisms $\alpha_1 \colon X_1 \cong X_2$, $\beta_1 \colon Y_1 \cong Y_2$, $\alpha_2 \colon X_2 \cong X_3$, and $\beta_2 \colon Y_2 \cong Y_3$ in a category $\mathcal{C}$, and a morphism $f \colon X_1 \to Y_1$, the following equality holds: \[ (\alpha_1 \ggg \alpha_2).\text{homCongr}(\beta_1 \ggg \beta_2)(f) = (\alpha_1.\text{homCongr}(\beta_1)) \circ (\alpha_2.\text{homCongr}(\beta_2))(f). \] Here, $\ggg$ denotes the composition of isomorphisms, $\text{homCongr}$ is the bijection of morphism sets induced by isomorphisms, and $\circ$ denotes the composition of equivalences.
CategoryTheory.Iso.homCongr_symm theorem
{X₁ Y₁ X₂ Y₂ : C} (α : X₁ ≅ X₂) (β : Y₁ ≅ Y₂) : (α.homCongr β).symm = α.symm.homCongr β.symm
Full source 
@[simp]
theorem homCongr_symm {X₁ Y₁ X₂ Y₂ : C} (α : X₁ ≅ X₂) (β : Y₁ ≅ Y₂) :
    (α.homCongr β).symm = α.symm.homCongr β.symm :=
  rfl
Inverse of `homCongr` Equals `homCongr` of Inverses
Informal description
Given isomorphisms $\alpha \colon X_1 \cong X_2$ and $\beta \colon Y_1 \cong Y_2$ in a category $\mathcal{C}$, the inverse of the bijection $\text{homCongr}(\alpha, \beta) \colon \text{Hom}(X_1, Y_1) \simeq \text{Hom}(X_2, Y_2)$ is equal to the bijection $\text{homCongr}(\alpha^{-1}, \beta^{-1}) \colon \text{Hom}(X_2, Y_2) \simeq \text{Hom}(X_1, Y_1)$.
CategoryTheory.Iso.isoCongr definition
{X₁ Y₁ X₂ Y₂ : C} (f : X₁ ≅ X₂) (g : Y₁ ≅ Y₂) : (X₁ ≅ Y₁) ≃ (X₂ ≅ Y₂)
Full source 
/-- If `X` is isomorphic to `X₁` and `Y` is isomorphic to `Y₁`, then
there is a bijection between `X ≅ Y` and `X₁ ≅ Y₁`. -/
@[simps]
def isoCongr {X₁ Y₁ X₂ Y₂ : C} (f : X₁ ≅ X₂) (g : Y₁ ≅ Y₂) : (X₁ ≅ Y₁) ≃ (X₂ ≅ Y₂) where
  toFun h := f.symm.trans <| h.trans <| g
  invFun h := f.trans <| h.trans <| g.symm
  left_inv := by aesop_cat
  right_inv := by aesop_cat
Bijection of isomorphism sets induced by isomorphisms
Informal description
Given isomorphisms $f \colon X_1 \cong X_2$ and $g \colon Y_1 \cong Y_2$ in a category $\mathcal{C}$, there is a bijection between the sets of isomorphisms $\text{Iso}(X_1, Y_1)$ and $\text{Iso}(X_2, Y_2)$. The bijection maps an isomorphism $h \colon X_1 \cong Y_1$ to the composition $f^{-1} \circ h \circ g$, and its inverse maps $h' \colon X_2 \cong Y_2$ to the composition $f \circ h' \circ g^{-1}$.
CategoryTheory.Iso.isoCongrLeft definition
{X₁ X₂ Y : C} (f : X₁ ≅ X₂) : (X₁ ≅ Y) ≃ (X₂ ≅ Y)
Full source 
/-- If `X₁` is isomorphic to `X₂`, then there is a bijection between `X₁ ≅ Y` and `X₂ ≅ Y`. -/
def isoCongrLeft {X₁ X₂ Y : C} (f : X₁ ≅ X₂) : (X₁ ≅ Y) ≃ (X₂ ≅ Y) :=
  isoCongr f (Iso.refl _)
Bijection of isomorphism sets induced by an isomorphism on the left
Informal description
Given an isomorphism $f \colon X_1 \cong X_2$ in a category $\mathcal{C}$, there is a bijection between the sets of isomorphisms $\text{Iso}(X_1, Y)$ and $\text{Iso}(X_2, Y)$ for any object $Y$. The bijection maps an isomorphism $h \colon X_1 \cong Y$ to the composition $f^{-1} \circ h$, and its inverse maps $h' \colon X_2 \cong Y$ to the composition $f \circ h'$.
CategoryTheory.Iso.isoCongrRight definition
{X Y₁ Y₂ : C} (g : Y₁ ≅ Y₂) : (X ≅ Y₁) ≃ (X ≅ Y₂)
Full source 
/-- If `Y₁` is isomorphic to `Y₂`, then there is a bijection between `X ≅ Y₁` and `X ≅ Y₂`. -/
def isoCongrRight {X Y₁ Y₂ : C} (g : Y₁ ≅ Y₂) : (X ≅ Y₁) ≃ (X ≅ Y₂) :=
  isoCongr (Iso.refl _) g
Bijection of isomorphism sets induced by an isomorphism on the right
Informal description
Given an isomorphism $g \colon Y_1 \cong Y_2$ in a category $\mathcal{C}$, there is a bijection between the sets of isomorphisms $\text{Iso}(X, Y_1)$ and $\text{Iso}(X, Y_2)$ for any object $X$. The bijection maps an isomorphism $h \colon X \cong Y_1$ to the composition $h \circ g^{-1}$, and its inverse maps $h' \colon X \cong Y_2$ to the composition $h' \circ g$.
CategoryTheory.Functor.map_homCongr theorem
{X Y X₁ Y₁ : C} (α : X ≅ X₁) (β : Y ≅ Y₁) (f : X ⟶ Y) : F.map (Iso.homCongr α β f) = Iso.homCongr (F.mapIso α) (F.mapIso β) (F.map f)
Full source 
theorem map_homCongr {X Y X₁ Y₁ : C} (α : X ≅ X₁) (β : Y ≅ Y₁) (f : X ⟶ Y) :
    F.map (Iso.homCongr α β f) = Iso.homCongr (F.mapIso α) (F.mapIso β) (F.map f) := by simp
Functoriality of Morphism Conjugation under Isomorphisms
Informal description
Let $F : \mathcal{C} \to \mathcal{D}$ be a functor between categories, and let $\alpha : X \cong X_1$ and $\beta : Y \cong Y_1$ be isomorphisms in $\mathcal{C}$. For any morphism $f : X \to Y$, the functor $F$ maps the conjugated morphism $\alpha^{-1} \circ f \circ \beta$ to the conjugated morphism of $F(f)$ via the isomorphisms $F(\alpha)$ and $F(\beta)$. That is, \[ F(\alpha^{-1} \circ f \circ \beta) = F(\alpha)^{-1} \circ F(f) \circ F(\beta). \]
CategoryTheory.Functor.map_isoCongr theorem
{X Y X₁ Y₁ : C} (α : X ≅ X₁) (β : Y ≅ Y₁) (f : X ≅ Y) : F.mapIso (Iso.isoCongr α β f) = Iso.isoCongr (F.mapIso α) (F.mapIso β) (F.mapIso f)
Full source 
theorem map_isoCongr {X Y X₁ Y₁ : C} (α : X ≅ X₁) (β : Y ≅ Y₁) (f : X ≅ Y) :
    F.mapIso (Iso.isoCongr α β f) = Iso.isoCongr (F.mapIso α) (F.mapIso β) (F.mapIso f) := by
  ext
  simp
Functoriality of Isomorphism Conjugation: $F(\alpha^{-1} \circ f \circ \beta) = F(\alpha)^{-1} \circ F(f) \circ F(\beta)$
Informal description
Let $F \colon \mathcal{C} \to \mathcal{D}$ be a functor between categories, and let $\alpha \colon X \cong X_1$ and $\beta \colon Y \cong Y_1$ be isomorphisms in $\mathcal{C}$. For any isomorphism $f \colon X \cong Y$, the functor $F$ maps the isomorphism obtained via conjugation by $\alpha$ and $\beta$ (i.e., $\alpha^{-1} \circ f \circ \beta$) to the conjugation of $F(f)$ by $F(\alpha)$ and $F(\beta)$. That is, \[ F(\alpha^{-1} \circ f \circ \beta) = F(\alpha)^{-1} \circ F(f) \circ F(\beta). \]