Mathlib.CategoryTheory.EqToHom

CategoryTheory.eqToHom definition

{X Y : C} (p : X = Y) : X ⟶ Y

Full source

/-- An equality `X = Y` gives us a morphism `X ⟶ Y`.

It is typically better to use this, rather than rewriting by the equality then using `𝟙 _`
which usually leads to dependent type theory hell.
-/
def eqToHom {X Y : C} (p : X = Y) : X ⟶ Y := by rw [p]; exact 𝟙 _

Morphism from object equality

Informal description

Given an equality $p : X = Y$ between objects $X$ and $Y$ in a category $\mathcal{C}$, the function `eqToHom` constructs a morphism $X \to Y$ in $\mathcal{C}$. When $X$ and $Y$ are definitionally equal (i.e., $p$ is `rfl`), this morphism is the identity morphism on $X$.

CategoryTheory.eqToHom_refl theorem

(X : C) (p : X = X) : eqToHom p = 𝟙 X

Full source

@[simp]
theorem eqToHom_refl (X : C) (p : X = X) : eqToHom p = 𝟙 X :=
  rfl

Identity Morphism from Reflexive Equality

Informal description

For any object $X$ in a category $\mathcal{C}$ and any equality $p : X = X$, the morphism $\text{eqToHom}(p)$ is equal to the identity morphism $\text{id}_X$.

CategoryTheory.eqToHom_trans theorem

{X Y Z : C} (p : X = Y) (q : Y = Z) : eqToHom p ≫ eqToHom q = eqToHom (p.trans q)

Full source

@[reassoc (attr := simp)]
theorem eqToHom_trans {X Y Z : C} (p : X = Y) (q : Y = Z) :
    eqToHomeqToHom p ≫ eqToHom q = eqToHom (p.trans q) := by
  cases p
  cases q
  simp

Composition of Morphisms Induced by Object Equalities

Informal description

For any objects $X$, $Y$, and $Z$ in a category $\mathcal{C}$, given equalities $p : X = Y$ and $q : Y = Z$, the composition of the morphisms $\text{eqToHom}(p) : X \to Y$ and $\text{eqToHom}(q) : Y \to Z$ is equal to the morphism $\text{eqToHom}(p \cdot q) : X \to Z$ induced by the transitivity of the equalities.

CategoryTheory.eqToHom_heq_id_dom theorem

(X Y : C) (h : X = Y) : HEq (eqToHom h) (𝟙 X)

Full source

/-- `eqToHom h` is heterogeneously equal to the identity of its domain. -/
lemma eqToHom_heq_id_dom (X Y : C) (h : X = Y) : HEq (eqToHom h) (𝟙 X) := by
  subst h; rfl

Heterogeneous Equality of $\text{eqToHom}(h)$ with Identity Morphism on Domain

Informal description

For any objects $X$ and $Y$ in a category $\mathcal{C}$ and an equality $h : X = Y$, the morphism $\text{eqToHom}(h) : X \to Y$ is heterogeneously equal to the identity morphism $\text{id}_X : X \to X$.

CategoryTheory.eqToHom_heq_id_cod theorem

(X Y : C) (h : X = Y) : HEq (eqToHom h) (𝟙 Y)

Full source

/-- `eqToHom h` is heterogeneously equal to the identity of its codomain. -/
lemma eqToHom_heq_id_cod (X Y : C) (h : X = Y) : HEq (eqToHom h) (𝟙 Y) := by
  subst h; rfl

Heterogeneous equality of $\text{eqToHom}(h)$ with $\text{id}_Y$

Informal description

For any objects $X$ and $Y$ in a category $\mathcal{C}$ and an equality $h : X = Y$, the morphism $\text{eqToHom}(h) : X \to Y$ is heterogeneously equal to the identity morphism $\text{id}_Y$ on $Y$.

CategoryTheory.conj_eqToHom_iff_heq theorem

 {W X Y Z : C} (f : W ⟶ X) (g : Y ⟶ Z) (h : W = Y) (h' : X = Z) : f = eqToHom h ≫ g ≫ eqToHom h'.symm ↔ HEq f g

Full source

/-- Two morphisms are conjugate via eqToHom if and only if they are heterogeneously equal.
Note this used to be in the Functor namespace, where it doesn't belong. -/
theorem conj_eqToHom_iff_heq {W X Y Z : C} (f : W ⟶ X) (g : Y ⟶ Z) (h : W = Y) (h' : X = Z) :
    f = eqToHom h ≫ g ≫ eqToHom h'.symm ↔ HEq f g := by
  cases h
  cases h'
  simp

Equivalence of Morphism Conjugation and Heterogeneous Equality via `eqToHom`

Informal description

For morphisms $f \colon W \to X$ and $g \colon Y \to Z$ in a category $\mathcal{C}$, and equalities $h \colon W = Y$ and $h' \colon X = Z$, the following are equivalent: 1. $f$ is equal to the composition $\text{eqToHom}(h) \circ g \circ \text{eqToHom}(h')^{-1}$. 2. $f$ and $g$ are heterogeneously equal (i.e., they are equal after accounting for the type differences induced by $h$ and $h'$).

CategoryTheory.conj_eqToHom_iff_heq' theorem

 {C} [Category C] {W X Y Z : C} (f : W ⟶ X) (g : Y ⟶ Z) (h : W = Y) (h' : Z = X) :
  f = eqToHom h ≫ g ≫ eqToHom h' ↔ HEq f g

Full source

theorem conj_eqToHom_iff_heq' {C} [Category C] {W X Y Z : C}
    (f : W ⟶ X) (g : Y ⟶ Z) (h : W = Y) (h' : Z = X) :
    f = eqToHom h ≫ g ≫ eqToHom h' ↔ HEq f g := conj_eqToHom_iff_heq _ _ _ h'.symm

Equivalence of Morphism Conjugation and Heterogeneous Equality via `eqToHom` (variant)

Informal description

For morphisms $f \colon W \to X$ and $g \colon Y \to Z$ in a category $\mathcal{C}$, and equalities $h \colon W = Y$ and $h' \colon Z = X$, the following are equivalent: 1. $f$ is equal to the composition $\text{eqToHom}(h) \circ g \circ \text{eqToHom}(h')$. 2. $f$ and $g$ are heterogeneously equal (i.e., they are equal after accounting for the type differences induced by $h$ and $h'$).

CategoryTheory.comp_eqToHom_iff theorem

{X Y Y' : C} (p : Y = Y') (f : X ⟶ Y) (g : X ⟶ Y') : f ≫ eqToHom p = g ↔ f = g ≫ eqToHom p.symm

Full source

theorem comp_eqToHom_iff {X Y Y' : C} (p : Y = Y') (f : X ⟶ Y) (g : X ⟶ Y') :
    f ≫ eqToHom pf ≫ eqToHom p = g ↔ f = g ≫ eqToHom p.symm :=
  { mp := fun h => h ▸ by simp
    mpr := fun h => by simp [eq_whisker h (eqToHom p)] }

Composition with `eqToHom` equivalence: $f \circ \text{eqToHom}(p) = g \leftrightarrow f = g \circ \text{eqToHom}(p^{-1})$

Informal description

For objects $X$, $Y$, and $Y'$ in a category $\mathcal{C}$, given an equality $p : Y = Y'$, morphisms $f : X \to Y$ and $g : X \to Y'$ satisfy $f \circ \text{eqToHom}(p) = g$ if and only if $f = g \circ \text{eqToHom}(p^{-1})$, where $p^{-1}$ is the inverse equality $Y' = Y$.

CategoryTheory.eqToHom_comp_iff theorem

{X X' Y : C} (p : X = X') (f : X ⟶ Y) (g : X' ⟶ Y) : eqToHom p ≫ g = f ↔ g = eqToHom p.symm ≫ f

Full source

theorem eqToHom_comp_iff {X X' Y : C} (p : X = X') (f : X ⟶ Y) (g : X' ⟶ Y) :
    eqToHomeqToHom p ≫ geqToHom p ≫ g = f ↔ g = eqToHom p.symm ≫ f :=
  { mp := fun h => h ▸ by simp
    mpr := fun h => h ▸ by simp [whisker_eq _ h] }

Composition with `eqToHom` equivalence: $\text{eqToHom}(p) \circ g = f \leftrightarrow g = \text{eqToHom}(p^{-1}) \circ f$

Informal description

For objects $X$, $X'$, and $Y$ in a category $\mathcal{C}$, given an equality $p : X = X'$, morphisms $f : X \to Y$ and $g : X' \to Y$ satisfy $\text{eqToHom}(p) \circ g = f$ if and only if $g = \text{eqToHom}(p^{-1}) \circ f$, where $p^{-1}$ is the inverse equality $X' = X$.

CategoryTheory.eqToHom_comp_heq theorem

{C} [Category C] {W X Y : C} (f : Y ⟶ X) (h : W = Y) : HEq (eqToHom h ≫ f) f

Full source

theorem eqToHom_comp_heq {C} [Category C] {W X Y : C}
    (f : Y ⟶ X) (h : W = Y) : HEq (eqToHomeqToHom h ≫ f) f := by
  rw [← conj_eqToHom_iff_heq _ _ h rfl, eqToHom_refl, Category.comp_id]

Heterogeneous equality of $\text{eqToHom}(h) \circ f$ and $f$

Informal description

For any morphism $f \colon Y \to X$ in a category $\mathcal{C}$ and any equality $h \colon W = Y$ between objects, the composition $\text{eqToHom}(h) \circ f$ is heterogeneously equal to $f$.

CategoryTheory.eqToHom_comp_heq_iff theorem

{C} [Category C] {W X Y Z Z' : C} (f : Y ⟶ X) (g : Z ⟶ Z') (h : W = Y) : HEq (eqToHom h ≫ f) g ↔ HEq f g

Full source

@[simp] theorem eqToHom_comp_heq_iff {C} [Category C] {W X Y Z Z' : C}
    (f : Y ⟶ X) (g : Z ⟶ Z') (h : W = Y) :
    HEqHEq (eqToHom h ≫ f) g ↔ HEq f g :=
  ⟨(eqToHom_comp_heq ..).symm.trans, (eqToHom_comp_heq ..).trans⟩

Heterogeneous Equality Condition for Composition with `eqToHom`

Informal description

For objects $W, X, Y, Z, Z'$ in a category $\mathcal{C}$, given a morphism $f \colon Y \to X$, a morphism $g \colon Z \to Z'$, and an equality $h \colon W = Y$, the composition $\text{eqToHom}(h) \circ f$ is heterogeneously equal to $g$ if and only if $f$ is heterogeneously equal to $g$.

CategoryTheory.heq_eqToHom_comp_iff theorem

{C} [Category C] {W X Y Z Z' : C} (f : Y ⟶ X) (g : Z ⟶ Z') (h : W = Y) : HEq g (eqToHom h ≫ f) ↔ HEq g f

Full source

@[simp] theorem heq_eqToHom_comp_iff {C} [Category C] {W X Y Z Z' : C}
    (f : Y ⟶ X) (g : Z ⟶ Z') (h : W = Y) :
    HEqHEq g (eqToHom h ≫ f) ↔ HEq g f :=
  ⟨(·.trans (eqToHom_comp_heq ..)), (·.trans (eqToHom_comp_heq ..).symm)⟩

Heterogeneous Equality of Morphisms via `eqToHom` Composition

Informal description

For any morphisms $f \colon Y \to X$ and $g \colon Z \to Z'$ in a category $\mathcal{C}$, and any equality $h \colon W = Y$ between objects, the heterogeneous equality $g \approx \text{eqToHom}(h) \circ f$ holds if and only if $g \approx f$.

CategoryTheory.comp_eqToHom_heq theorem

{C} [Category C] {X Y Z : C} (f : X ⟶ Y) (h : Y = Z) : HEq (f ≫ eqToHom h) f

Full source

theorem comp_eqToHom_heq {C} [Category C] {X Y Z : C}
    (f : X ⟶ Y) (h : Y = Z) : HEq (f ≫ eqToHom h) f := by
  rw [← conj_eqToHom_iff_heq' _ _ rfl h, eqToHom_refl, Category.id_comp]

Heterogeneous Equality of Composition with `eqToHom`

Informal description

For any morphism $f \colon X \to Y$ in a category $\mathcal{C}$ and any equality $h \colon Y = Z$, the composition $f \circ \text{eqToHom}(h)$ is heterogeneously equal to $f$.

CategoryTheory.comp_eqToHom_heq_iff theorem

{C} [Category C] {W X Y Z Z' : C} (f : X ⟶ Y) (g : Z ⟶ Z') (h : Y = W) : HEq (f ≫ eqToHom h) g ↔ HEq f g

Full source

@[simp] theorem comp_eqToHom_heq_iff {C} [Category C] {W X Y Z Z' : C}
    (f : X ⟶ Y) (g : Z ⟶ Z') (h : Y = W) :
    HEqHEq (f ≫ eqToHom h) g ↔ HEq f g :=
  ⟨(comp_eqToHom_heq ..).symm.trans, (comp_eqToHom_heq ..).trans⟩

Heterogeneous Equality of Composition with `eqToHom` Morphism

Informal description

Let $\mathcal{C}$ be a category, and let $X, Y, W, Z, Z'$ be objects in $\mathcal{C}$. Given morphisms $f \colon X \to Y$ and $g \colon Z \to Z'$, and an equality $h \colon Y = W$, the composition $f \circ \text{eqToHom}(h)$ is heterogeneously equal to $g$ if and only if $f$ is heterogeneously equal to $g$.

CategoryTheory.heq_comp_eqToHom_iff theorem

{C} [Category C] {W X Y Z Z' : C} (f : X ⟶ Y) (g : Z ⟶ Z') (h : Y = W) : HEq g (f ≫ eqToHom h) ↔ HEq g f

Full source

@[simp] theorem heq_comp_eqToHom_iff {C} [Category C] {W X Y Z Z' : C}
    (f : X ⟶ Y) (g : Z ⟶ Z') (h : Y = W) :
    HEqHEq g (f ≫ eqToHom h) ↔ HEq g f :=
  ⟨(·.trans (comp_eqToHom_heq ..)), (·.trans (comp_eqToHom_heq ..).symm)⟩

Heterogeneous Equality of Composition with `eqToHom` Morphism (Symmetric Form)

Informal description

Let $\mathcal{C}$ be a category, and let $X, Y, W, Z, Z'$ be objects in $\mathcal{C}$. Given morphisms $f \colon X \to Y$ and $g \colon Z \to Z'$, and an equality $h \colon Y = W$, the composition $f \circ \text{eqToHom}(h)$ is heterogeneously equal to $g$ if and only if $g$ is heterogeneously equal to $f$.

CategoryTheory.heq_comp theorem

 {C} [Category C] {X Y Z X' Y' Z' : C} {f : X ⟶ Y} {g : Y ⟶ Z} {f' : X' ⟶ Y'} {g' : Y' ⟶ Z'} (eq1 : X = X')
  (eq2 : Y = Y') (eq3 : Z = Z') (H1 : HEq f f') (H2 : HEq g g') : HEq (f ≫ g) (f' ≫ g')

Full source

theorem heq_comp {C} [Category C] {X Y Z X' Y' Z' : C}
    {f : X ⟶ Y} {g : Y ⟶ Z} {f' : X' ⟶ Y'} {g' : Y' ⟶ Z'}
    (eq1 : X = X') (eq2 : Y = Y') (eq3 : Z = Z')
    (H1 : HEq f f') (H2 : HEq g g') :
    HEq (f ≫ g) (f' ≫ g') := by
  cases eq1; cases eq2; cases eq3; cases H1; cases H2; rfl

Heterogeneous Equality of Compositions under Object Equality

Informal description

Let $\mathcal{C}$ be a category, and let $X, Y, Z, X', Y', Z'$ be objects in $\mathcal{C}$. Given morphisms $f \colon X \to Y$, $g \colon Y \to Z$, $f' \colon X' \to Y'$, and $g' \colon Y' \to Z'$, along with equalities $X = X'$, $Y = Y'$, and $Z = Z'$, if $f$ is heterogeneously equal to $f'$ and $g$ is heterogeneously equal to $g'$, then the composition $f \circ g$ is heterogeneously equal to $f' \circ g'$.

CategoryTheory.eqToHom_naturality theorem

 {f g : β → C} (z : ∀ b, f b ⟶ g b) {j j' : β} (w : j = j') : z j ≫ eqToHom (by simp [w]) = eqToHom (by simp [w]) ≫ z j'

Full source

/-- We can push `eqToHom` to the left through families of morphisms. -/
-- The simpNF linter incorrectly claims that this will never apply.
-- It seems the side condition `w` is not applied by `simpNF`.
-- https://github.com/leanprover-community/mathlib4/issues/5049
@[reassoc (attr := simp, nolint simpNF)]
theorem eqToHom_naturality {f g : β → C} (z : ∀ b, f b ⟶ g b) {j j' : β} (w : j = j') :
    z j ≫ eqToHom (by simp [w]) = eqToHomeqToHom (by simp [w]) ≫ z j' := by
  cases w
  simp

Naturality of Morphisms Induced by Index Equality in a Category

Informal description

Let $\mathcal{C}$ be a category, and let $f, g \colon \beta \to \mathcal{C}$ be families of objects in $\mathcal{C}$ indexed by a type $\beta$. Given a family of morphisms $z \colon \forall b, f(b) \to g(b)$ and an equality $w \colon j = j'$ between indices $j, j' \in \beta$, the following diagram commutes: $$ z(j) \circ \text{eqToHom}(w) = \text{eqToHom}(w) \circ z(j') $$ where $\text{eqToHom}(w)$ is the morphism induced by the equality $w$ (applied componentwise to the families $f$ and $g$).

CategoryTheory.eqToHom_iso_hom_naturality theorem

 {f g : β → C} (z : ∀ b, f b ≅ g b) {j j' : β} (w : j = j') :
  (z j).hom ≫ eqToHom (by simp [w]) = eqToHom (by simp [w]) ≫ (z j').hom

Full source

/-- A variant on `eqToHom_naturality` that helps Lean identify the families `f` and `g`. -/
-- The simpNF linter incorrectly claims that this will never apply.
-- It seems the side condition `w` is not applied by `simpNF`.
-- https://github.com/leanprover-community/mathlib4/issues/5049
@[reassoc (attr := simp, nolint simpNF)]
theorem eqToHom_iso_hom_naturality {f g : β → C} (z : ∀ b, f b ≅ g b) {j j' : β} (w : j = j') :
    (z j).hom ≫ eqToHom (by simp [w]) = eqToHomeqToHom (by simp [w]) ≫ (z j').hom := by
  cases w
  simp

Naturality of Isomorphism Homomorphisms with Respect to Index Equality

Informal description

Let $\mathcal{C}$ be a category, and let $f, g \colon \beta \to \mathcal{C}$ be families of objects indexed by a type $\beta$. Given a family of isomorphisms $z_b \colon f(b) \cong g(b)$ for each $b \in \beta$ and an equality $w \colon j = j'$ between indices $j, j' \in \beta$, the following diagram commutes: $$ (z_j)_\text{hom} \circ \text{eqToHom}(w) = \text{eqToHom}(w) \circ (z_{j'})_\text{hom} $$ where $\text{eqToHom}(w)$ is the morphism induced by the equality $w$ (applied componentwise to the families $f$ and $g$).

CategoryTheory.eqToHom_iso_inv_naturality theorem

 {f g : β → C} (z : ∀ b, f b ≅ g b) {j j' : β} (w : j = j') :
  (z j).inv ≫ eqToHom (by simp [w]) = eqToHom (by simp [w]) ≫ (z j').inv

Full source

/-- A variant on `eqToHom_naturality` that helps Lean identify the families `f` and `g`. -/
-- The simpNF linter incorrectly claims that this will never apply.
-- It seems the side condition `w` is not applied by `simpNF`.
-- https://github.com/leanprover-community/mathlib4/issues/5049
@[reassoc (attr := simp, nolint simpNF)]
theorem eqToHom_iso_inv_naturality {f g : β → C} (z : ∀ b, f b ≅ g b) {j j' : β} (w : j = j') :
    (z j).inv ≫ eqToHom (by simp [w]) = eqToHomeqToHom (by simp [w]) ≫ (z j').inv := by
  cases w
  simp

Naturality of Inverse Isomorphisms with Respect to Index Equality

Informal description

Let $\mathcal{C}$ be a category, and let $f, g \colon \beta \to \mathcal{C}$ be families of objects in $\mathcal{C}$ indexed by a type $\beta$. Given a family of isomorphisms $z \colon \forall b, f(b) \cong g(b)$ and an equality $w \colon j = j'$ between indices $j, j' \in \beta$, the following diagram commutes for the inverse morphisms: $$ (z(j))^{-1} \circ \text{eqToHom}(w) = \text{eqToHom}(w) \circ (z(j'))^{-1} $$ where $\text{eqToHom}(w)$ is the morphism induced by the equality $w$ (applied componentwise to the families $f$ and $g$).

CategoryTheory.congrArg_cast_hom_left theorem

{X Y Z : C} (p : X = Y) (q : Y ⟶ Z) : cast (congrArg (fun W : C => W ⟶ Z) p.symm) q = eqToHom p ≫ q

Full source

/-- Reducible form of congrArg_mpr_hom_left -/
@[simp]
theorem congrArg_cast_hom_left {X Y Z : C} (p : X = Y) (q : Y ⟶ Z) :
    cast (congrArg (fun W : C => W ⟶ Z) p.symm) q = eqToHomeqToHom p ≫ q := by
  cases p
  simp

Cast of Morphism Along Object Equality Equals Composition with eqToHom

Informal description

For objects $X, Y, Z$ in a category $\mathcal{C}$, given an equality $p : X = Y$ and a morphism $q : Y \to Z$, the cast of $q$ along the equality of hom-sets induced by $p$ is equal to the composition of the morphism $\text{eqToHom}(p) : X \to Y$ with $q$.

CategoryTheory.congrArg_mpr_hom_left theorem

{X Y Z : C} (p : X = Y) (q : Y ⟶ Z) : (congrArg (fun W : C => W ⟶ Z) p).mpr q = eqToHom p ≫ q

Full source

/-- If we (perhaps unintentionally) perform equational rewriting on
the source object of a morphism,
we can replace the resulting `_.mpr f` term by a composition with an `eqToHom`.

It may be advisable to introduce any necessary `eqToHom` morphisms manually,
rather than relying on this lemma firing.
-/
theorem congrArg_mpr_hom_left {X Y Z : C} (p : X = Y) (q : Y ⟶ Z) :
    (congrArg (fun W : C => W ⟶ Z) p).mpr q = eqToHomeqToHom p ≫ q := by
  cases p
  simp

Rewriting Source of Morphism via Equality is Composition with `eqToHom`

Informal description

For objects $X, Y, Z$ in a category $\mathcal{C}$, given an equality $p : X = Y$ and a morphism $q : Y \to Z$, the morphism obtained by rewriting the source of $q$ along $p$ (via `congrArg`) is equal to the composition of the morphism `eqToHom p : X → Y` with $q$.

CategoryTheory.congrArg_cast_hom_right theorem

{X Y Z : C} (p : X ⟶ Y) (q : Z = Y) : cast (congrArg (fun W : C => X ⟶ W) q.symm) p = p ≫ eqToHom q.symm

Full source

/-- Reducible form of `congrArg_mpr_hom_right` -/
@[simp]
theorem congrArg_cast_hom_right {X Y Z : C} (p : X ⟶ Y) (q : Z = Y) :
    cast (congrArg (fun W : C => X ⟶ W) q.symm) p = p ≫ eqToHom q.symm := by
  cases q
  simp

Compatibility of cast with composition via eqToHom

Informal description

Let $\mathcal{C}$ be a category, $X, Y, Z$ objects in $\mathcal{C}$, $p : X \to Y$ a morphism, and $q : Z = Y$ an equality between objects. Then the cast of $p$ along the equality $\text{congrArg} (fun W \Rightarrow X \to W) q.symm$ is equal to the composition $p \circ \text{eqToHom} q.symm$.

CategoryTheory.congrArg_mpr_hom_right theorem

{X Y Z : C} (p : X ⟶ Y) (q : Z = Y) : (congrArg (fun W : C => X ⟶ W) q).mpr p = p ≫ eqToHom q.symm

Full source

/-- If we (perhaps unintentionally) perform equational rewriting on
the target object of a morphism,
we can replace the resulting `_.mpr f` term by a composition with an `eqToHom`.

It may be advisable to introduce any necessary `eqToHom` morphisms manually,
rather than relying on this lemma firing.
-/
theorem congrArg_mpr_hom_right {X Y Z : C} (p : X ⟶ Y) (q : Z = Y) :
    (congrArg (fun W : C => X ⟶ W) q).mpr p = p ≫ eqToHom q.symm := by
  cases q
  simp

Rewriting Target of Morphism via Equality of Objects

Informal description

For any morphism $p \colon X \to Y$ in a category $\mathcal{C}$ and any equality $q \colon Z = Y$ between objects, the morphism obtained by rewriting the target of $p$ using $q$ is equal to the composition of $p$ with the inverse of the morphism induced by $q$, i.e., $$(\text{congrArg}\, (\lambda W \colon \mathcal{C}, X \to W)\, q).\text{mpr}\, p = p \circ \text{eqToHom}\, q^{-1}.$$

CategoryTheory.eqToIso definition

{X Y : C} (p : X = Y) : X ≅ Y

Full source

/-- An equality `X = Y` gives us an isomorphism `X ≅ Y`.

It is typically better to use this, rather than rewriting by the equality then using `Iso.refl _`
which usually leads to dependent type theory hell.
-/
def eqToIso {X Y : C} (p : X = Y) : X ≅ Y :=
  ⟨eqToHom p, eqToHom p.symm, by simp, by simp⟩

Isomorphism from object equality

Informal description

Given an equality $p : X = Y$ between objects $X$ and $Y$ in a category $\mathcal{C}$, the function `eqToIso` constructs an isomorphism $X \cong Y$ in $\mathcal{C}$. The isomorphism consists of the morphism $X \to Y$ induced by $p$ and its inverse $Y \to X$ induced by the symmetry of $p$. When $X$ and $Y$ are definitionally equal (i.e., $p$ is `rfl`), this isomorphism is the identity isomorphism on $X$.

CategoryTheory.eqToIso.hom theorem

{X Y : C} (p : X = Y) : (eqToIso p).hom = eqToHom p

Full source

@[simp]
theorem eqToIso.hom {X Y : C} (p : X = Y) : (eqToIso p).hom = eqToHom p :=
  rfl

Homomorphism Component of Isomorphism from Object Equality Equals Morphism from Equality

Informal description

For any equality $p : X = Y$ between objects $X$ and $Y$ in a category $\mathcal{C}$, the homomorphism component of the isomorphism $\text{eqToIso}(p) : X \cong Y$ is equal to the morphism $\text{eqToHom}(p) : X \to Y$ induced by $p$.

CategoryTheory.eqToIso.inv theorem

{X Y : C} (p : X = Y) : (eqToIso p).inv = eqToHom p.symm

Full source

@[simp]
theorem eqToIso.inv {X Y : C} (p : X = Y) : (eqToIso p).inv = eqToHom p.symm :=
  rfl

Inverse of Isomorphism from Object Equality Equals Morphism from Symmetric Equality

Informal description

For any equality $p : X = Y$ between objects $X$ and $Y$ in a category $\mathcal{C}$, the inverse morphism of the isomorphism $\text{eqToIso}(p) : X \cong Y$ is equal to the morphism $\text{eqToHom}(p^{-1}) : Y \to X$ induced by the symmetric equality $p^{-1} : Y = X$.

CategoryTheory.eqToIso_refl theorem

{X : C} (p : X = X) : eqToIso p = Iso.refl X

Full source

@[simp]
theorem eqToIso_refl {X : C} (p : X = X) : eqToIso p = Iso.refl X :=
  rfl

Identity Isomorphism from Reflexive Equality

Informal description

For any object $X$ in a category $\mathcal{C}$ and equality $p : X = X$, the isomorphism $\text{eqToIso}(p)$ is equal to the identity isomorphism $\text{Iso.refl}(X)$.

CategoryTheory.eqToIso_trans theorem

{X Y Z : C} (p : X = Y) (q : Y = Z) : eqToIso p ≪≫ eqToIso q = eqToIso (p.trans q)

Full source

@[simp]
theorem eqToIso_trans {X Y Z : C} (p : X = Y) (q : Y = Z) :
    eqToIsoeqToIso p ≪≫ eqToIso q = eqToIso (p.trans q) := by ext; simp

Composition of Isomorphisms Induced by Object Equalities

Informal description

For any objects $X$, $Y$, and $Z$ in a category $\mathcal{C}$, given equalities $p : X = Y$ and $q : Y = Z$, the composition of the isomorphisms $\text{eqToIso}(p) : X \cong Y$ and $\text{eqToIso}(q) : Y \cong Z$ is equal to the isomorphism $\text{eqToIso}(p \cdot q) : X \cong Z$ induced by the transitivity of the equalities.

CategoryTheory.eqToHom_op theorem

{X Y : C} (h : X = Y) : (eqToHom h).op = eqToHom (congr_arg op h.symm)

Full source

@[simp]
theorem eqToHom_op {X Y : C} (h : X = Y) : (eqToHom h).op = eqToHom (congr_arg op h.symm) := by
  cases h
  rfl

Opposite of Equality-Induced Morphism Equals Morphism Induced by Opposite Equality

Informal description

For any objects $X$ and $Y$ in a category $\mathcal{C}$ and an equality $h : X = Y$, the opposite morphism of the morphism induced by $h$ (i.e., $(eqToHom\ h).op$) is equal to the morphism induced by the equality of opposite objects $op\ Y = op\ X$ (i.e., $eqToHom\ (congr\_arg\ op\ h.symm)$).

CategoryTheory.eqToHom_unop theorem

{X Y : Cᵒᵖ} (h : X = Y) : (eqToHom h).unop = eqToHom (congr_arg unop h.symm)

Full source

@[simp]
theorem eqToHom_unop {X Y : Cᵒᵖ} (h : X = Y) :
    (eqToHom h).unop = eqToHom (congr_arg unop h.symm) := by
  cases h
  rfl

Unopposite of Equality-Induced Morphism in Opposite Category

Informal description

For any objects $X$ and $Y$ in the opposite category $\mathcal{C}^\mathrm{op}$ and an equality $h : X = Y$, the unopposite of the morphism $\mathrm{eqToHom}(h) : X \to Y$ is equal to the morphism $\mathrm{eqToHom}(\mathrm{unop}(h^\mathrm{symm})) : \mathrm{unop}(Y) \to \mathrm{unop}(X)$ in the original category $\mathcal{C}$.

CategoryTheory.instIsIsoEqToHom instance

{X Y : C} (h : X = Y) : IsIso (eqToHom h)

Full source

instance {X Y : C} (h : X = Y) : IsIso (eqToHom h) :=
  (eqToIso h).isIso_hom

Morphism Induced by Object Equality is an Isomorphism

Informal description

For any objects $X$ and $Y$ in a category $\mathcal{C}$ and an equality $h : X = Y$, the morphism $\mathrm{eqToHom}(h) : X \to Y$ is an isomorphism.

CategoryTheory.inv_eqToHom theorem

{X Y : C} (h : X = Y) : inv (eqToHom h) = eqToHom h.symm

Full source

@[simp]
theorem inv_eqToHom {X Y : C} (h : X = Y) : inv (eqToHom h) = eqToHom h.symm := by
  aesop_cat

Inverse of Equality-Induced Isomorphism is Reverse Equality Morphism

Informal description

For any objects $X$ and $Y$ in a category $\mathcal{C}$ and an equality $h : X = Y$, the inverse of the isomorphism $\mathrm{eqToHom}(h) : X \to Y$ is equal to the morphism $\mathrm{eqToHom}(h^\mathrm{symm}) : Y \to X$ induced by the reverse equality $h^\mathrm{symm} : Y = X$.

CategoryTheory.Functor.ext_of_iso theorem

{F G : C ⥤ D} (e : F ≅ G) (hobj : ∀ X, F.obj X = G.obj X) (happ : ∀ X, e.hom.app X = eqToHom (hobj X)) : F = G

Full source

lemma ext_of_iso {F G : C ⥤ D} (e : F ≅ G) (hobj : ∀ X, F.obj X = G.obj X)
    (happ : ∀ X, e.hom.app X = eqToHom (hobj X)) : F = G :=
  Functor.ext hobj (fun X Y f => by
    rw [← cancel_mono (e.hom.app Y), e.hom.naturality f, happ, happ, Category.assoc,
    Category.assoc, eqToHom_trans, eqToHom_refl, Category.comp_id])

Functor Equality via Natural Isomorphism and Object Equality

Informal description

Given two functors $F, G \colon \mathcal{C} \to \mathcal{D}$ and a natural isomorphism $e \colon F \cong G$, if for every object $X$ in $\mathcal{C}$ we have $F(X) = G(X)$ and the component $e.hom.app X$ of the natural isomorphism equals the morphism $\text{eqToHom}(F(X) = G(X))$ induced by this equality, then $F = G$.

CategoryTheory.Functor.hext theorem

{F G : C ⥤ D} (h_obj : ∀ X, F.obj X = G.obj X) (h_map : ∀ (X Y) (f : X ⟶ Y), HEq (F.map f) (G.map f)) : F = G

Full source

/-- Proving equality between functors using heterogeneous equality. -/
theorem hext {F G : C ⥤ D} (h_obj : ∀ X, F.obj X = G.obj X)
    (h_map : ∀ (X Y) (f : X ⟶ Y), HEq (F.map f) (G.map f)) : F = G :=
  Functor.ext h_obj fun _ _ f => (conj_eqToHom_iff_heq _ _ (h_obj _) (h_obj _)).2 <| h_map _ _ f

Heterogeneous Equality Implies Functor Equality

Informal description

For any two functors $F, G \colon \mathcal{C} \to \mathcal{D}$, if for every object $X$ in $\mathcal{C}$ we have $F(X) = G(X)$, and for every pair of objects $X, Y$ and every morphism $f \colon X \to Y$ the morphisms $F(f)$ and $G(f)$ are heterogeneously equal, then $F = G$.

CategoryTheory.Functor.congr_obj theorem

{F G : C ⥤ D} (h : F = G) (X) : F.obj X = G.obj X

Full source

theorem congr_obj {F G : C ⥤ D} (h : F = G) (X) : F.obj X = G.obj X := by rw [h]

Equality of Functors Implies Equality on Objects

Informal description

For any two functors $F$ and $G$ between categories $C$ and $D$, if $F = G$, then for every object $X$ in $C$, the objects $F(X)$ and $G(X)$ are equal in $D$.

CategoryTheory.Functor.congr_hom theorem

 {F G : C ⥤ D} (h : F = G) {X Y} (f : X ⟶ Y) :
  F.map f = eqToHom (congr_obj h X) ≫ G.map f ≫ eqToHom (congr_obj h Y).symm

Full source

@[reassoc]
theorem congr_hom {F G : C ⥤ D} (h : F = G) {X Y} (f : X ⟶ Y) :
    F.map f = eqToHomeqToHom (congr_obj h X) ≫ G.map f ≫ eqToHom (congr_obj h Y).symm := by
  subst h; simp

Functor Equality Induces Morphism Equality via $\text{eqToHom}$

Informal description

Let $F$ and $G$ be functors from category $\mathcal{C}$ to category $\mathcal{D}$, and suppose $F = G$. For any objects $X, Y$ in $\mathcal{C}$ and any morphism $f : X \to Y$, the image of $f$ under $F$ is equal to the composition: \[ F(f) = \text{eqToHom}(F(X) = G(X)) \circ G(f) \circ \text{eqToHom}(G(Y) = F(Y)) \] where $\text{eqToHom}$ constructs a morphism from an equality between objects.

CategoryTheory.Functor.congr_inv_of_congr_hom theorem

 (F G : C ⥤ D) {X Y : C} (e : X ≅ Y) (hX : F.obj X = G.obj X) (hY : F.obj Y = G.obj Y)
  (h₂ : F.map e.hom = eqToHom (by rw [hX]) ≫ G.map e.hom ≫ eqToHom (by rw [hY])) :
  F.map e.inv = eqToHom (by rw [hY]) ≫ G.map e.inv ≫ eqToHom (by rw [hX])

Full source

theorem congr_inv_of_congr_hom (F G : C ⥤ D) {X Y : C} (e : X ≅ Y) (hX : F.obj X = G.obj X)
    (hY : F.obj Y = G.obj Y)
    (h₂ : F.map e.hom = eqToHomeqToHom (by rw [hX]) ≫ G.map e.hom ≫ eqToHom (by rw [hY])) :
    F.map e.inv = eqToHomeqToHom (by rw [hY]) ≫ G.map e.inv ≫ eqToHom (by rw [hX]) := by
  simp only [← IsIso.Iso.inv_hom e, Functor.map_inv, h₂, IsIso.inv_comp, inv_eqToHom,
    Category.assoc]

Functorial Consistency of Inverse Morphisms under Object Equality

Informal description

Let $F$ and $G$ be functors from category $\mathcal{C}$ to category $\mathcal{D}$, and let $e \colon X \cong Y$ be an isomorphism in $\mathcal{C}$. Suppose we have: 1. Object equalities $h_X \colon F(X) = G(X)$ and $h_Y \colon F(Y) = G(Y)$, and 2. A morphism equality showing that $F(e_{\text{hom}})$ equals the composition: \[ \text{eqToHom}(h_X) \circ G(e_{\text{hom}}) \circ \text{eqToHom}(h_Y^{-1}) \] Then the image of the inverse morphism satisfies: \[ F(e_{\text{inv}}) = \text{eqToHom}(h_Y) \circ G(e_{\text{inv}}) \circ \text{eqToHom}(h_X^{-1}) \]

CategoryTheory.Functor.map_comp_heq theorem

 (hx : F.obj X = G.obj X) (hy : F.obj Y = G.obj Y) (hz : F.obj Z = G.obj Z) (hf : HEq (F.map f) (G.map f))
  (hg : HEq (F.map g) (G.map g)) : HEq (F.map (f ≫ g)) (G.map (f ≫ g))

Full source

theorem map_comp_heq (hx : F.obj X = G.obj X) (hy : F.obj Y = G.obj Y) (hz : F.obj Z = G.obj Z)
    (hf : HEq (F.map f) (G.map f)) (hg : HEq (F.map g) (G.map g)) :
    HEq (F.map (f ≫ g)) (G.map (f ≫ g)) := by
  rw [F.map_comp, G.map_comp]
  congr

Heterogeneous Equality of Functor Images for Compositions

Informal description

Let $F, G : C \to D$ be functors between categories $C$ and $D$, and let $X, Y, Z$ be objects in $C$. Suppose we have: 1. Equalities $hx : F(X) = G(X)$, $hy : F(Y) = G(Y)$, and $hz : F(Z) = G(Z)$, 2. Heterogeneous equalities $hf : F(f) \cong G(f)$ and $hg : F(g) \cong G(g)$ for morphisms $f : X \to Y$ and $g : Y \to Z$. Then there is a heterogeneous equality $F(f \circ g) \cong G(f \circ g)$ between the images of the composition under $F$ and $G$.

CategoryTheory.Functor.map_comp_heq' theorem

 (hobj : ∀ X : C, F.obj X = G.obj X) (hmap : ∀ {X Y} (f : X ⟶ Y), HEq (F.map f) (G.map f)) :
  HEq (F.map (f ≫ g)) (G.map (f ≫ g))

Full source

theorem map_comp_heq' (hobj : ∀ X : C, F.obj X = G.obj X)
    (hmap : ∀ {X Y} (f : X ⟶ Y), HEq (F.map f) (G.map f)) :
    HEq (F.map (f ≫ g)) (G.map (f ≫ g)) := by
  rw [Functor.hext hobj fun _ _ => hmap]

Heterogeneous Equality of Functor Compositions under Object-wise Equality

Informal description

Let $F, G \colon \mathcal{C} \to \mathcal{D}$ be functors between categories $\mathcal{C}$ and $\mathcal{D}$. Suppose that: 1. For every object $X$ in $\mathcal{C}$, we have $F(X) = G(X)$, and 2. For every pair of objects $X, Y$ in $\mathcal{C}$ and every morphism $f \colon X \to Y$, the morphisms $F(f)$ and $G(f)$ are heterogeneously equal. Then for any composable morphisms $f \colon X \to Y$ and $g \colon Y \to Z$ in $\mathcal{C}$, the morphisms $F(f \circ g)$ and $G(f \circ g)$ are heterogeneously equal.

CategoryTheory.Functor.precomp_map_heq theorem

 (H : E ⥤ C) (hmap : ∀ {X Y} (f : X ⟶ Y), HEq (F.map f) (G.map f)) {X Y : E} (f : X ⟶ Y) :
  HEq ((H ⋙ F).map f) ((H ⋙ G).map f)

Full source

theorem precomp_map_heq (H : E ⥤ C) (hmap : ∀ {X Y} (f : X ⟶ Y), HEq (F.map f) (G.map f)) {X Y : E}
    (f : X ⟶ Y) : HEq ((H ⋙ F).map f) ((H ⋙ G).map f) :=
  hmap _

Heterogeneous equality of precomposed functors' actions on morphisms

Informal description

Let $F, G : C \to D$ be functors, $H : E \to C$ another functor, and suppose that for all objects $X, Y$ in $C$ and morphisms $f : X \to Y$, we have a heterogeneous equality $\mathrm{HEq}(F(f), G(f))$. Then for any objects $X, Y$ in $E$ and morphism $f : X \to Y$, we have the heterogeneous equality $\mathrm{HEq}((H \circ F)(f), (H \circ G)(f))$.

CategoryTheory.Functor.postcomp_map_heq theorem

 (H : D ⥤ E) (hx : F.obj X = G.obj X) (hy : F.obj Y = G.obj Y) (hmap : HEq (F.map f) (G.map f)) :
  HEq ((F ⋙ H).map f) ((G ⋙ H).map f)

Full source

theorem postcomp_map_heq (H : D ⥤ E) (hx : F.obj X = G.obj X) (hy : F.obj Y = G.obj Y)
    (hmap : HEq (F.map f) (G.map f)) : HEq ((F ⋙ H).map f) ((G ⋙ H).map f) := by
  dsimp
  congr

Heterogeneous Equality of Postcomposed Functor Maps under Object Equality

Informal description

Let $F, G : C \to D$ be functors, $H : D \to E$ be another functor, and $f : X \to Y$ be a morphism in $C$. If $F(X) = G(X)$, $F(Y) = G(Y)$, and $F(f)$ is heterogeneously equal to $G(f)$, then the morphisms $(F \circ H)(f)$ and $(G \circ H)(f)$ are heterogeneously equal.

CategoryTheory.Functor.postcomp_map_heq' theorem

 (H : D ⥤ E) (hobj : ∀ X : C, F.obj X = G.obj X) (hmap : ∀ {X Y} (f : X ⟶ Y), HEq (F.map f) (G.map f)) :
  HEq ((F ⋙ H).map f) ((G ⋙ H).map f)

Full source

theorem postcomp_map_heq' (H : D ⥤ E) (hobj : ∀ X : C, F.obj X = G.obj X)
    (hmap : ∀ {X Y} (f : X ⟶ Y), HEq (F.map f) (G.map f)) :
    HEq ((F ⋙ H).map f) ((G ⋙ H).map f) := by rw [Functor.hext hobj fun _ _ => hmap]

Heterogeneous Equality of Postcomposed Functor Maps under Object-wise Equality

Informal description

Let $F, G \colon \mathcal{C} \to \mathcal{D}$ and $H \colon \mathcal{D} \to \mathcal{E}$ be functors. If for every object $X$ in $\mathcal{C}$ we have $F(X) = G(X)$, and for every pair of objects $X, Y$ and every morphism $f \colon X \to Y$ the morphisms $F(f)$ and $G(f)$ are heterogeneously equal, then for any morphism $f \colon X \to Y$ in $\mathcal{C}$, the morphisms $(F \circ H)(f)$ and $(G \circ H)(f)$ are heterogeneously equal.

CategoryTheory.Functor.hcongr_hom theorem

{F G : C ⥤ D} (h : F = G) {X Y} (f : X ⟶ Y) : HEq (F.map f) (G.map f)

Full source

theorem hcongr_hom {F G : C ⥤ D} (h : F = G) {X Y} (f : X ⟶ Y) : HEq (F.map f) (G.map f) := by
  rw [h]

Heterogeneous Equality of Functor Maps under Functor Equality

Informal description

For any two functors $F, G \colon C \to D$ that are equal (i.e., $F = G$), and for any morphism $f \colon X \to Y$ in $C$, the morphisms $F.map f$ and $G.map f$ are heterogeneously equal (denoted as $\text{HEq}$).

CategoryTheory.eqToHom_map theorem

(F : C ⥤ D) {X Y : C} (p : X = Y) : F.map (eqToHom p) = eqToHom (congr_arg F.obj p)

Full source

/-- This is not always a good idea as a `@[simp]` lemma,
as we lose the ability to use results that interact with `F`,
e.g. the naturality of a natural transformation.

In some files it may be appropriate to use `attribute [local simp] eqToHom_map`, however.
-/
theorem eqToHom_map (F : C ⥤ D) {X Y : C} (p : X = Y) :
    F.map (eqToHom p) = eqToHom (congr_arg F.obj p) := by cases p; simp

Functoriality of `eqToHom` under Functor Application

Informal description

Let $F \colon \mathcal{C} \to \mathcal{D}$ be a functor between categories $\mathcal{C}$ and $\mathcal{D}$. For any objects $X, Y \in \mathcal{C}$ and an equality $p \colon X = Y$, the functor $F$ maps the morphism $\text{eqToHom}(p) \colon X \to Y$ to the morphism $\text{eqToHom}(\text{congr\_arg} F.obj\, p) \colon F(X) \to F(Y)$. In other words, $F(\text{eqToHom}(p)) = \text{eqToHom}(F(X) = F(Y))$.

CategoryTheory.eqToHom_map_comp theorem

 (F : C ⥤ D) {X Y Z : C} (p : X = Y) (q : Y = Z) : F.map (eqToHom p) ≫ F.map (eqToHom q) = F.map (eqToHom <| p.trans q)

Full source

@[reassoc (attr := simp)]
theorem eqToHom_map_comp (F : C ⥤ D) {X Y Z : C} (p : X = Y) (q : Y = Z) :
    F.map (eqToHom p) ≫ F.map (eqToHom q) = F.map (eqToHom <| p.trans q) := by aesop_cat

Functoriality of Composition of Equality-Induced Morphisms

Informal description

Let $F \colon \mathcal{C} \to \mathcal{D}$ be a functor between categories $\mathcal{C}$ and $\mathcal{D}$. For any objects $X, Y, Z \in \mathcal{C}$ and equalities $p \colon X = Y$ and $q \colon Y = Z$, the composition of the images under $F$ of the morphisms induced by $p$ and $q$ equals the image under $F$ of the morphism induced by the transitivity of $p$ and $q$. That is, $$ F(\text{eqToHom}(p)) \circ F(\text{eqToHom}(q)) = F(\text{eqToHom}(p \cdot q)). $$

CategoryTheory.eqToIso_map theorem

(F : C ⥤ D) {X Y : C} (p : X = Y) : F.mapIso (eqToIso p) = eqToIso (congr_arg F.obj p)

Full source

/-- See the note on `eqToHom_map` regarding using this as a `simp` lemma.
-/
theorem eqToIso_map (F : C ⥤ D) {X Y : C} (p : X = Y) :
    F.mapIso (eqToIso p) = eqToIso (congr_arg F.obj p) := by ext; cases p; simp

Functoriality of Isomorphism from Object Equality: $F(\text{eqToIso}(p)) = \text{eqToIso}(F(X) = F(Y))$

Informal description

Let $F \colon \mathcal{C} \to \mathcal{D}$ be a functor between categories $\mathcal{C}$ and $\mathcal{D}$. For any objects $X, Y \in \mathcal{C}$ and an equality $p \colon X = Y$, the image under $F$ of the isomorphism $\text{eqToIso}(p) \colon X \cong Y$ equals the isomorphism $\text{eqToIso}(F(X) = F(Y))$ in $\mathcal{D}$ induced by the equality of objects $F(X) = F(Y)$.

CategoryTheory.eqToIso_map_trans theorem

 (F : C ⥤ D) {X Y Z : C} (p : X = Y) (q : Y = Z) :
  F.mapIso (eqToIso p) ≪≫ F.mapIso (eqToIso q) = F.mapIso (eqToIso <| p.trans q)

Full source

@[simp]
theorem eqToIso_map_trans (F : C ⥤ D) {X Y Z : C} (p : X = Y) (q : Y = Z) :
    F.mapIso (eqToIso p) ≪≫ F.mapIso (eqToIso q) = F.mapIso (eqToIso <| p.trans q) := by aesop_cat

Functoriality of Composition of Equality-Induced Isomorphisms: $F(\text{eqToIso}(p)) \ggg F(\text{eqToIso}(q)) = F(\text{eqToIso}(p \cdot q))$

Informal description

Let $F \colon \mathcal{C} \to \mathcal{D}$ be a functor between categories $\mathcal{C}$ and $\mathcal{D}$. For any objects $X, Y, Z \in \mathcal{C}$ and equalities $p \colon X = Y$ and $q \colon Y = Z$, the composition of the isomorphisms $F(\text{eqToIso}(p)) \colon F(X) \cong F(Y)$ and $F(\text{eqToIso}(q)) \colon F(Y) \cong F(Z)$ equals the isomorphism $F(\text{eqToIso}(p \cdot q)) \colon F(X) \cong F(Z)$, where $p \cdot q$ denotes the transitivity of $p$ and $q$. That is, $$ F(\text{eqToIso}(p)) \ggg F(\text{eqToIso}(q)) = F(\text{eqToIso}(p \cdot q)). $$

CategoryTheory.eqToHom_app theorem

{F G : C ⥤ D} (h : F = G) (X : C) : (eqToHom h : F ⟶ G).app X = eqToHom (Functor.congr_obj h X)

Full source

@[simp]
theorem eqToHom_app {F G : C ⥤ D} (h : F = G) (X : C) :
    (eqToHom h : F ⟶ G).app X = eqToHom (Functor.congr_obj h X) := by subst h; rfl

Component Equality of Natural Transformation from Functor Equality

Informal description

For any two functors $F$ and $G$ between categories $\mathcal{C}$ and $\mathcal{D}$, if $h : F = G$ is an equality between the functors, then for every object $X$ in $\mathcal{C}$, the component of the natural transformation $\text{eqToHom}\, h$ at $X$ is equal to the morphism $\text{eqToHom}\, (F.obj X = G.obj X)$ induced by the equality of objects $F.obj X = G.obj X$.

CategoryTheory.NatTrans.congr theorem

 {F G : C ⥤ D} (α : F ⟶ G) {X Y : C} (h : X = Y) : α.app X = F.map (eqToHom h) ≫ α.app Y ≫ G.map (eqToHom h.symm)

Full source

theorem NatTrans.congr {F G : C ⥤ D} (α : F ⟶ G) {X Y : C} (h : X = Y) :
    α.app X = F.map (eqToHom h) ≫ α.app Y ≫ G.map (eqToHom h.symm) := by
  rw [α.naturality_assoc]
  simp [eqToHom_map]

Naturality Condition for Components under Object Equality

Informal description

Let $F, G \colon \mathcal{C} \to \mathcal{D}$ be functors between categories $\mathcal{C}$ and $\mathcal{D}$, and let $\alpha \colon F \to G$ be a natural transformation. For any objects $X, Y \in \mathcal{C}$ and an equality $h \colon X = Y$, the component of $\alpha$ at $X$ satisfies: \[ \alpha_X = F(\text{eqToHom}(h)) \circ \alpha_Y \circ G(\text{eqToHom}(h^{-1})) \] where $\text{eqToHom}(h) \colon X \to Y$ is the morphism induced by the equality $h$, and $h^{-1}$ denotes the inverse equality $Y = X$.

CategoryTheory.dcongr_arg theorem

 {ι : Type*} {F G : ι → C} (α : ∀ i, F i ⟶ G i) {i j : ι} (h : i = j) :
  α i = eqToHom (congr_arg F h) ≫ α j ≫ eqToHom (congr_arg G h.symm)

Full source

theorem dcongr_arg {ι : Type*} {F G : ι → C} (α : ∀ i, F i ⟶ G i) {i j : ι} (h : i = j) :
    α i = eqToHomeqToHom (congr_arg F h) ≫ α j ≫ eqToHom (congr_arg G h.symm) := by
  subst h
  simp

Naturality of Morphism Families under Index Equality

Informal description

Let $\iota$ be a type, and let $F, G \colon \iota \to C$ be families of objects in a category $\mathcal{C}$. Given a family of morphisms $\alpha \colon \forall i, F i \to G i$ and an equality $h \colon i = j$ between indices $i, j \in \iota$, we have the equality: \[ \alpha_i = \text{eqToHom}(\text{congr\_arg}\, F\, h) \circ \alpha_j \circ \text{eqToHom}(\text{congr\_arg}\, G\, h^{-1}) \] where $\text{eqToHom}$ constructs a morphism from an equality of objects, and $\text{congr\_arg}$ applies the equality to the families $F$ and $G$.

CategoryTheory.Equivalence.induced definition

{T : Type*} (e : T ≃ D) : InducedCategory D e ≌ D

Full source

/-- If `T ≃ D` is a bijection and `D` is a category, then
`InducedCategory D e` is equivalent to `D`. -/
@[simps]
def Equivalence.induced {T : Type*} (e : T ≃ D) :
    InducedCategoryInducedCategory D e ≌ D where
  functor := inducedFunctor e
  inverse :=
    { obj := e.symm
      map {X Y} f := show e (e.symm X) ⟶ e (e.symm Y) from
        eqToHomeqToHom (e.apply_symm_apply X) ≫ f ≫
          eqToHom (e.apply_symm_apply Y).symm
      map_comp {X Y Z} f g := by
        dsimp
        rw [Category.assoc]
        erw [Category.assoc]
        rw [Category.assoc, eqToHom_trans_assoc, eqToHom_refl, Category.id_comp] }
  unitIso := NatIso.ofComponents (fun _ ↦ eqToIso (by simp)) (fun {X Y} f ↦ by
    dsimp
    erw [eqToHom_trans_assoc _ (by simp), eqToHom_refl, Category.id_comp]
    rfl )
  counitIso := NatIso.ofComponents (fun _ ↦ eqToIso (by simp))
  functor_unitIso_comp X := eqToHom_trans (by simp) (by simp)

Equivalence between Induced Category and Original Category via Bijection

Informal description

Given a bijection $e \colon T \simeq D$ where $D$ is a category, the induced category $\text{InducedCategory}\, D\, e$ is equivalent to $D$. The equivalence is constructed as follows: - The functor from $\text{InducedCategory}\, D\, e$ to $D$ is the induced functor $e$. - The inverse functor from $D$ to $\text{InducedCategory}\, D\, e$ is given by $e^{-1}$ on objects, and for morphisms $f \colon X \to Y$ in $D$, the corresponding morphism is constructed using $\text{eqToHom}$ applied to the equalities $e(e^{-1}(X)) = X$ and $e(e^{-1}(Y)) = Y$. - The unit and counit natural isomorphisms are constructed using $\text{eqToIso}$ applied to appropriate equalities, and they satisfy the required triangle identities.