mathlib documentation

category_theory.eq_to_hom

def category_theory.eq_to_hom {C : Type u₁} [category_theory.category C] {X Y : C} (p : X = Y) :
X Y

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
@[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.congr_arg_mpr_hom_left {C : Type u₁} [category_theory.category C] {X Y Z : C} (p : X = Y) (q : Y Z) :

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 eq_to_hom.

It may be advisable to introduce any necessary eq_to_hom morphisms manually, rather than relying on this lemma firing.

@[simp]
theorem category_theory.congr_arg_mpr_hom_right {C : Type u₁} [category_theory.category C] {X Y Z : C} (p : X Y) (q : Z = Y) :

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 eq_to_hom.

It may be advisable to introduce any necessary eq_to_hom morphisms manually, rather than relying on this lemma firing.

def category_theory.eq_to_iso {C : Type u₁} [category_theory.category C] {X Y : C} (p : X = Y) :
X Y

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
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) (h_map : ∀ (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} (h_obj : ∀ (X : C), F.obj X = G.obj X) (h_map : ∀ (X Y : C) (f : X Y), F.map f == G.map f) :
F = G

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) :
F.obj X = G.obj X
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) :
@[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) :
theorem category_theory.nat_trans.congr {C : Type u₁} [category_theory.category C] {D : Type u₂} [category_theory.category D] {F G : C D} (α : F G) {X Y : C} (h : X = Y) :