mathlib3 documentation

category_theory.eq_to_hom

Morphisms from equations between objects. #

THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4.

When working categorically, sometimes one encounters an equation h : X = Y between objects.

Your initial aversion to this is natural and appropriate: you're in for some trouble, and if there is another way to approach the problem that won't rely on this equality, it may be worth pursuing.

You have two options:

Use the equality h as one normally would in Lean (e.g. using rw and subst). This may immediately cause difficulties, because in category theory everything is dependently typed, and equations between objects quickly lead to nasty goals with eq.rec.
Promote h to a morphism using eq_to_hom h : X ⟶ Y, or eq_to_iso h : X ≅ Y.

This file introduces various simp lemmas which in favourable circumstances result in the various eq_to_hom morphisms to drop out at the appropriate moment!

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

category_theory.eq_to_hom p = _.mpr (𝟙 Y)

Instances for category_theory.eq_to_hom

category_theory.eq_to_hom.is_iso

@[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

@[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'

@[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 _

theorem category_theory.comp_eq_to_hom_iff {C : Type u₁} [category_theory.category C] {X Y Y' : C} (p : Y = Y') (f : X ⟶ Y) (g : X ⟶ Y') :

f ≫ category_theory.eq_to_hom p = g ↔ f = g ≫ category_theory.eq_to_hom _

theorem category_theory.eq_to_hom_comp_iff {C : Type u₁} [category_theory.category C] {X X' Y : C} (p : X = X') (f : X ⟶ Y) (g : X' ⟶ Y) :

category_theory.eq_to_hom p ≫ g = f ↔ g = category_theory.eq_to_hom _ ≫ f

@[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) :

_.mpr q = category_theory.eq_to_hom p ≫ q

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) :

_.mpr p = p ≫ category_theory.eq_to_hom _

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

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) :

(category_theory.eq_to_iso p).hom = category_theory.eq_to_hom p

@[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 _

@[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

@[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 _

@[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 _

@[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 _

@[protected, instance]

def category_theory.eq_to_hom.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)

@[simp]

theorem category_theory.inv_eq_to_hom {C : Type u₁} [category_theory.category C] {X Y : C} (h : X = Y) :

category_theory.inv (category_theory.eq_to_hom h) = category_theory.eq_to_hom _

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.conj_eq_to_hom_iff_heq {C : Type u₁} [category_theory.category C] {W X Y Z : C} (f : W ⟶ X) (g : Y ⟶ Z) (h : W = Y) (h' : X = Z) :

f = category_theory.eq_to_hom h ≫ g ≫ category_theory.eq_to_hom _ ↔ f == g

Two morphisms are conjugate via eq_to_hom if and only if they are heterogeneously equal.

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) :

F.map f = category_theory.eq_to_hom _ ≫ G.map f ≫ category_theory.eq_to_hom _

theorem category_theory.functor.congr_inv_of_congr_hom {C : Type u₁} [category_theory.category C] {D : Type u₂} [category_theory.category D] (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 = category_theory.eq_to_hom _ ≫ G.map e.hom ≫ category_theory.eq_to_hom _) :

F.map e.inv = category_theory.eq_to_hom _ ≫ G.map e.inv ≫ category_theory.eq_to_hom _

theorem category_theory.functor.congr_map {C : Type u₁} [category_theory.category C] {D : Type u₂} [category_theory.category D] (F : C ⥤ D) {X Y : C} {f g : X ⟶ Y} (h : f = g) :

F.map f = F.map g

theorem category_theory.functor.map_comp_heq {C : Type u₁} [category_theory.category C] {D : Type u₂} [category_theory.category D] {F G : C ⥤ D} {X Y Z : C} {f : X ⟶ Y} {g : Y ⟶ Z} (hx : F.obj X = G.obj X) (hy : F.obj Y = G.obj Y) (hz : F.obj Z = G.obj Z) (hf : F.map f == G.map f) (hg : F.map g == G.map g) :

F.map (f ≫ g) == G.map (f ≫ g)

theorem category_theory.functor.map_comp_heq' {C : Type u₁} [category_theory.category C] {D : Type u₂} [category_theory.category D] {F G : C ⥤ D} {X Y Z : C} {f : X ⟶ Y} {g : Y ⟶ Z} (hobj : ∀ (X : C), F.obj X = G.obj X) (hmap : ∀ {X Y : C} (f : X ⟶ Y), F.map f == G.map f) :

F.map (f ≫ g) == G.map (f ≫ g)

theorem category_theory.functor.precomp_map_heq {C : Type u₁} [category_theory.category C] {D : Type u₂} [category_theory.category D] {E : Type u₃} [category_theory.category E] {F G : C ⥤ D} (H : E ⥤ C) (hmap : ∀ {X Y : C} (f : X ⟶ Y), F.map f == G.map f) {X Y : E} (f : X ⟶ Y) :

(H ⋙ F).map f == (H ⋙ G).map f

theorem category_theory.functor.postcomp_map_heq {C : Type u₁} [category_theory.category C] {D : Type u₂} [category_theory.category D] {E : Type u₃} [category_theory.category E] {F G : C ⥤ D} {X Y : C} {f : X ⟶ Y} (H : D ⥤ E) (hx : F.obj X = G.obj X) (hy : F.obj Y = G.obj Y) (hmap : F.map f == G.map f) :

(F ⋙ H).map f == (G ⋙ H).map f

theorem category_theory.functor.postcomp_map_heq' {C : Type u₁} [category_theory.category C] {D : Type u₂} [category_theory.category D] {E : Type u₃} [category_theory.category E] {F G : C ⥤ D} {X Y : C} {f : X ⟶ Y} (H : D ⥤ E) (hobj : ∀ (X : C), F.obj X = G.obj X) (hmap : ∀ {X Y : C} (f : X ⟶ Y), F.map f == G.map f) :

(F ⋙ H).map f == (G ⋙ H).map f

theorem category_theory.functor.hcongr_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 == G.map f

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 _

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 local attribute [simp] eq_to_hom_map, however.

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 _

See the note on eq_to_hom_map regarding using this as a simp lemma.

@[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 _

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

theorem category_theory.eq_conj_eq_to_hom {C : Type u₁} [category_theory.category C] {X Y : C} (f : X ⟶ Y) :

f = category_theory.eq_to_hom rfl ≫ f ≫ category_theory.eq_to_hom rfl

theorem category_theory.dcongr_arg {C : Type u₁} [category_theory.category C] {ι : Type u_1} {F G : ι → C} (α : Π (i : ι), F i ⟶ G i) {i j : ι} (h : i = j) :

α i = category_theory.eq_to_hom _ ≫ α j ≫ category_theory.eq_to_hom _