mathlib documentation

category_theory.eq_to_hom

source
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
source
@[simp]
theorem category_theory.eq_to_hom_refl {C : Type u₁} [category_theory.category C] (X : C) (p : X = X) :
category_theory.eq_to_hom p = 𝟙 X

source
@[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') :
category_theory.eq_to_hom p ≫ category_theory.eq_to_hom q ≫ f' = category_theory.eq_to_hom _ ≫ f'

source
@[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) :
category_theory.eq_to_hom p ≫ category_theory.eq_to_hom q = category_theory.eq_to_hom _

source
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
source
@[simp]
theorem category_theory.eq_to_iso.hom {C : Type u₁} [category_theory.category C] {X Y : C} (p : X = Y) :
(category_theory.eq_to_iso p).hom = category_theory.eq_to_hom p

source
@[simp]
theorem category_theory.eq_to_iso.inv {C : Type u₁} [category_theory.category C] {X Y : C} (p : X = Y) :
(category_theory.eq_to_iso p).inv = category_theory.eq_to_hom _

source
@[simp]
theorem category_theory.eq_to_iso_refl {C : Type u₁} [category_theory.category C] {X : C} (p : X = X) :
category_theory.eq_to_iso p = category_theory.iso.refl X

source
@[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) :
category_theory.eq_to_iso p ≪≫ category_theory.eq_to_iso q = category_theory.eq_to_iso _

source
@[simp]
theorem category_theory.eq_to_hom_op {C : Type u₁} [category_theory.category C] {X Y : C} (h : X = Y) :
(category_theory.eq_to_hom h).op = category_theory.eq_to_hom _

source
@[simp]
theorem category_theory.eq_to_hom_unop {C : Type u₁} [category_theory.category C] {X Y : Cᵒᵖ} (h : X = Y) :
(category_theory.eq_to_hom h).unop = category_theory.eq_to_hom _

source
@[instance]
def category_theory.category_theory.is_iso {C : Type u₁} [category_theory.category C] {X Y : C} (h : X = Y) :
category_theory.is_iso (category_theory.eq_to_hom h)

Equations
source
@[simp]
theorem category_theory.inv_eq_to_hom {C : Type u₁} [category_theory.category C] {X Y : C} (h : X = Y) :
category_theory.is_iso.inv (category_theory.eq_to_hom h) = category_theory.eq_to_hom _

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

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

source
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

source
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 _

source
@[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) :
F.map (category_theory.eq_to_hom p) = category_theory.eq_to_hom _

source
@[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) :
F.map_iso (category_theory.eq_to_iso p) = category_theory.eq_to_iso _

source
@[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) :
(category_theory.eq_to_hom h).app X = category_theory.eq_to_hom _

source
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) :
α.app X = F.map (category_theory.eq_to_hom h) ≫ α.app Y ≫ G.map (category_theory.eq_to_hom _)