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.
Equations
- category_theory.eq_to_hom p = _.mpr (𝟙 Y)
@[simp]
theorem
category_theory.eq_to_hom_refl
{C : Type u}
[category_theory.category C]
(X : C)
(p : X = X) :
@[simp]
theorem
category_theory.eq_to_hom_trans_assoc
{C : Type u}
[category_theory.category C]
{X Y Z : C}
(p : X = Y)
(q : Y = Z)
{X' : C}
(f' : Z ⟶ X') :
@[simp]
theorem
category_theory.eq_to_hom_trans
{C : Type u}
[category_theory.category C]
{X Y Z : C}
(p : X = Y)
(q : Y = Z) :
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 iso.refl _
which usually leads to dependent type theory hell.
Equations
- category_theory.eq_to_iso p = {hom := category_theory.eq_to_hom p, inv := category_theory.eq_to_hom _, hom_inv_id' := _, inv_hom_id' := _}
@[simp]
theorem
category_theory.eq_to_iso.hom
{C : Type u}
[category_theory.category C]
{X Y : C}
(p : X = Y) :
@[simp]
theorem
category_theory.eq_to_iso.inv
{C : Type u}
[category_theory.category C]
{X Y : C}
(p : X = Y) :
@[simp]
theorem
category_theory.eq_to_iso_refl
{C : Type u}
[category_theory.category C]
(X : C)
(p : X = X) :
@[simp]
theorem
category_theory.eq_to_iso_trans
{C : Type u}
[category_theory.category C]
{X Y Z : C}
(p : X = Y)
(q : Y = Z) :
@[simp]
theorem
category_theory.eq_to_hom_op
{C : Type u}
[category_theory.category C]
(X Y : C)
(h : X = Y) :
theorem
category_theory.functor.ext
{C : Type u}
[category_theory.category C]
{D : Type u'}
[category_theory.category D]
{F G : C ⥤ D}
(h_obj : ∀ (X : C), F.obj X = G.obj X) :
(∀ (X Y : C) (f : X ⟶ Y), F.map f = category_theory.eq_to_hom _ ≫ G.map f ≫ category_theory.eq_to_hom _) → F = G
Proving equality between functors. This isn't an extensionality lemma, because usually you don't really want to do this.
theorem
category_theory.functor.hext
{C : Type u}
[category_theory.category C]
{D : Type u'}
[category_theory.category D]
{F G : C ⥤ D} :
Proving equality between functors using heterogeneous equality.
theorem
category_theory.functor.congr_obj
{C : Type u}
[category_theory.category C]
{D : Type u'}
[category_theory.category D]
{F G : C ⥤ D}
(h : F = G)
(X : C) :
theorem
category_theory.functor.congr_hom
{C : Type u}
[category_theory.category C]
{D : Type u'}
[category_theory.category D]
{F G : C ⥤ D}
(h : F = G)
{X Y : C}
(f : X ⟶ Y) :
F.map f = category_theory.eq_to_hom _ ≫ G.map f ≫ category_theory.eq_to_hom _
@[simp]
theorem
category_theory.eq_to_hom_map
{C : Type u}
[category_theory.category C]
{D : Type u'}
[category_theory.category D]
(F : C ⥤ D)
{X Y : C}
(p : X = Y) :
@[simp]
theorem
category_theory.eq_to_iso_map
{C : Type u}
[category_theory.category C]
{D : Type u'}
[category_theory.category D]
(F : C ⥤ D)
{X Y : C}
(p : X = Y) :
@[simp]
theorem
category_theory.eq_to_hom_app
{C : Type u}
[category_theory.category C]
{D : Type u'}
[category_theory.category D]
{F G : C ⥤ D}
(h : F = G)
(X : C) :