mathlib documentation

category_theory.eq_to_hom

def category_theory.eq_to_hom {C : Type uā‚} [category_theory.category C] {X Y : C} :
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') :

def category_theory.eq_to_iso {C : Type uā‚} [category_theory.category C] {X Y : C} :
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
@[simp]

@[simp]

@[simp]

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} :
(āˆ€ (X : C), F.obj X = G.obj X) ā†’ (āˆ€ (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) :