Morphisms from equations between objects.

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:

1. 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.
2. Promote h to a morphism using eqToHom h : X ⟶ Y, or eqToIso h : X ≅ Y.

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

def CategoryTheory.eqToHom {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {X : C} {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

• CategoryTheory.eqToHom p = Eq.mpr (_ : (X ⟶ Y) = (Y ⟶ Y)) (CategoryTheory.CategoryStruct.id Y)

@[simp]

theorem CategoryTheory.eqToHom_refl {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] (X : C) (p : X = X) : CategoryTheory.eqToHom p = CategoryTheory.CategoryStruct.id X

@[simp]

theorem CategoryTheory.eqToHom_trans_assoc {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {X : C} {Y : C} {Z : C} (p : X = Y) (q : Y = Z) {Z : C} (h : Z ⟶ Z) : CategoryTheory.CategoryStruct.comp (CategoryTheory.eqToHom p) (CategoryTheory.CategoryStruct.comp (CategoryTheory.eqToHom q) h) = CategoryTheory.CategoryStruct.comp (CategoryTheory.eqToHom (_ : X = Z)) h

@[simp]

theorem CategoryTheory.eqToHom_trans {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {X : C} {Y : C} {Z : C} (p : X = Y) (q : Y = Z) : CategoryTheory.CategoryStruct.comp (CategoryTheory.eqToHom p) (CategoryTheory.eqToHom q) = CategoryTheory.eqToHom (_ : X = Z)

theorem CategoryTheory.comp_eqToHom_iff {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {X : C} {Y : C} {Y' : C} (p : Y = Y') (f : X ⟶ Y) (g : X ⟶ Y') : CategoryTheory.CategoryStruct.comp f (CategoryTheory.eqToHom p) = g ↔ f = CategoryTheory.CategoryStruct.comp g (CategoryTheory.eqToHom (_ : Y' = Y))

theorem CategoryTheory.eqToHom_comp_iff {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {X : C} {X' : C} {Y : C} (p : X = X') (f : X ⟶ Y) (g : X' ⟶ Y) : CategoryTheory.CategoryStruct.comp (CategoryTheory.eqToHom p) g = f ↔ g = CategoryTheory.CategoryStruct.comp (CategoryTheory.eqToHom (_ : X' = X)) f

@[simp]

theorem CategoryTheory.eqToHom_naturality_assoc {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {β : Sort u_1} {f : β → C} {g : β → C} (z : (b : β) → f b ⟶ g b) {j : β} {j' : β} (w : j = j') {Z : C} (h : g j' ⟶ Z) : CategoryTheory.CategoryStruct.comp (z j) (CategoryTheory.CategoryStruct.comp (CategoryTheory.eqToHom (_ : g j = g j')) h) = CategoryTheory.CategoryStruct.comp (CategoryTheory.eqToHom (_ : f j = f j')) (CategoryTheory.CategoryStruct.comp (z j') h)

@[simp]

theorem CategoryTheory.eqToHom_naturality {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {β : Sort u_1} {f : β → C} {g : β → C} (z : (b : β) → f b ⟶ g b) {j : β} {j' : β} (w : j = j') : CategoryTheory.CategoryStruct.comp (z j) (CategoryTheory.eqToHom (_ : g j = g j')) = CategoryTheory.CategoryStruct.comp (CategoryTheory.eqToHom (_ : f j = f j')) (z j')

We can push eqToHom to the left through families of morphisms.

@[simp]

theorem CategoryTheory.eqToHom_iso_hom_naturality_assoc {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {β : Sort u_1} {f : β → C} {g : β → C} (z : (b : β) → f b ≅ g b) {j : β} {j' : β} (w : j = j') {Z : C} (h : g j' ⟶ Z) : CategoryTheory.CategoryStruct.comp (z j).hom (CategoryTheory.CategoryStruct.comp (CategoryTheory.eqToHom (_ : g j = g j')) h) = CategoryTheory.CategoryStruct.comp (CategoryTheory.eqToHom (_ : f j = f j')) (CategoryTheory.CategoryStruct.comp (z j').hom h)

@[simp]

theorem CategoryTheory.eqToHom_iso_hom_naturality {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {β : Sort u_1} {f : β → C} {g : β → C} (z : (b : β) → f b ≅ g b) {j : β} {j' : β} (w : j = j') : CategoryTheory.CategoryStruct.comp (z j).hom (CategoryTheory.eqToHom (_ : g j = g j')) = CategoryTheory.CategoryStruct.comp (CategoryTheory.eqToHom (_ : f j = f j')) (z j').hom

A variant on eqToHom_naturality that helps Lean identify the families f and g.

@[simp]

theorem CategoryTheory.eqToHom_iso_inv_naturality_assoc {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {β : Sort u_1} {f : β → C} {g : β → C} (z : (b : β) → f b ≅ g b) {j : β} {j' : β} (w : j = j') {Z : C} (h : f j' ⟶ Z) : CategoryTheory.CategoryStruct.comp (z j).inv (CategoryTheory.CategoryStruct.comp (CategoryTheory.eqToHom (_ : f j = f j')) h) = CategoryTheory.CategoryStruct.comp (CategoryTheory.eqToHom (_ : g j = g j')) (CategoryTheory.CategoryStruct.comp (z j').inv h)

@[simp]

theorem CategoryTheory.eqToHom_iso_inv_naturality {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {β : Sort u_1} {f : β → C} {g : β → C} (z : (b : β) → f b ≅ g b) {j : β} {j' : β} (w : j = j') : CategoryTheory.CategoryStruct.comp (z j).inv (CategoryTheory.eqToHom (_ : f j = f j')) = CategoryTheory.CategoryStruct.comp (CategoryTheory.eqToHom (_ : g j = g j')) (z j').inv

A variant on eqToHom_naturality that helps Lean identify the families f and g.

@[simp]

theorem CategoryTheory.congrArg_cast_hom_left {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {X : C} {Y : C} {Z : C} (p : X = Y) (q : Y ⟶ Z) : cast (_ : (Y ⟶ Z) = (X ⟶ Z)) q = CategoryTheory.CategoryStruct.comp (CategoryTheory.eqToHom p) q

Reducible form of congrArg_mpr_hom_left

theorem CategoryTheory.congrArg_mpr_hom_left {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {X : C} {Y : C} {Z : C} (p : X = Y) (q : Y ⟶ Z) : Eq.mpr (_ : (X ⟶ Z) = (Y ⟶ Z)) q = CategoryTheory.CategoryStruct.comp (CategoryTheory.eqToHom 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 eqToHom.

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

@[simp]

theorem CategoryTheory.congrArg_cast_hom_right {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {X : C} {Y : C} {Z : C} (p : X ⟶ Y) (q : Z = Y) : cast (_ : (X ⟶ Y) = (X ⟶ Z)) p = CategoryTheory.CategoryStruct.comp p (CategoryTheory.eqToHom (_ : Y = Z))

Reducible form of congrArg_mpr_hom_right

theorem CategoryTheory.congrArg_mpr_hom_right {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {X : C} {Y : C} {Z : C} (p : X ⟶ Y) (q : Z = Y) : Eq.mpr (_ : (X ⟶ Z) = (X ⟶ Y)) p = CategoryTheory.CategoryStruct.comp p (CategoryTheory.eqToHom (_ : Y = Z))

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

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

def CategoryTheory.eqToIso {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {X : C} {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

• CategoryTheory.eqToIso p = CategoryTheory.Iso.mk (CategoryTheory.eqToHom p) (CategoryTheory.eqToHom (_ : Y = X))

@[simp]

theorem CategoryTheory.eqToIso.hom {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {X : C} {Y : C} (p : X = Y) : (CategoryTheory.eqToIso p).hom = CategoryTheory.eqToHom p

@[simp]

theorem CategoryTheory.eqToIso.inv {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {X : C} {Y : C} (p : X = Y) : (CategoryTheory.eqToIso p).inv = CategoryTheory.eqToHom (_ : Y = X)

@[simp]

theorem CategoryTheory.eqToIso_refl {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {X : C} (p : X = X) : CategoryTheory.eqToIso p = CategoryTheory.Iso.refl X

@[simp]

theorem CategoryTheory.eqToIso_trans {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {X : C} {Y : C} {Z : C} (p : X = Y) (q : Y = Z) : CategoryTheory.eqToIso p ≪≫ CategoryTheory.eqToIso q = CategoryTheory.eqToIso (_ : X = Z)

@[simp]

theorem CategoryTheory.eqToHom_op {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {X : C} {Y : C} (h : X = Y) : (CategoryTheory.eqToHom h).op = CategoryTheory.eqToHom (_ : Opposite.op Y = Opposite.op X)

@[simp]

theorem CategoryTheory.eqToHom_unop {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {X : Cᵒᵖ} {Y : Cᵒᵖ} (h : X = Y) : (CategoryTheory.eqToHom h).unop = CategoryTheory.eqToHom (_ : Y.unop = X.unop)

instance CategoryTheory.instIsIsoEqToHom {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {X : C} {Y : C} (h : X = Y) : CategoryTheory.IsIso (CategoryTheory.eqToHom h)

Equations

• @CategoryTheory.instIsIsoEqToHom = @CategoryTheory.instIsIsoEqToHom.proof_1

@[simp]

theorem CategoryTheory.inv_eqToHom {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {X : C} {Y : C} (h : X = Y) : CategoryTheory.inv (CategoryTheory.eqToHom h) = CategoryTheory.eqToHom (_ : Y = X)

theorem CategoryTheory.Functor.ext {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] {F : CategoryTheory.Functor C D} {G : CategoryTheory.Functor C D} (h_obj : ∀ (X : C), F.obj X = G.obj X) (h_map : autoParam (∀ (X Y : C) (f : X ⟶ Y), F.map f = CategoryTheory.CategoryStruct.comp (CategoryTheory.eqToHom (h_obj X)) (CategoryTheory.CategoryStruct.comp (G.map f) (CategoryTheory.eqToHom (_ : G.obj Y = F.obj Y)))) _auto✝) : F = G

Proving equality between functors. This isn't an extensionality lemma, because usually you don't really want to do this.

theorem CategoryTheory.Functor.conj_eqToHom_iff_heq {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {W : C} {X : C} {Y : C} {Z : C} (f : W ⟶ X) (g : Y ⟶ Z) (h : W = Y) (h' : X = Z) : f = CategoryTheory.CategoryStruct.comp (CategoryTheory.eqToHom h) (CategoryTheory.CategoryStruct.comp g (CategoryTheory.eqToHom (_ : Z = X))) ↔ HEq f g

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

theorem CategoryTheory.Functor.hext {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] {F : CategoryTheory.Functor C D} {G : CategoryTheory.Functor C D} (h_obj : ∀ (X : C), F.obj X = G.obj X) (h_map : ∀ (X Y : C) (f : X ⟶ Y), HEq (F.map f) (G.map f)) : F = G

Proving equality between functors using heterogeneous equality.

theorem CategoryTheory.Functor.congr_obj {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] {F : CategoryTheory.Functor C D} {G : CategoryTheory.Functor C D} (h : F = G) (X : C) : F.obj X = G.obj X

theorem CategoryTheory.Functor.congr_hom {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] {F : CategoryTheory.Functor C D} {G : CategoryTheory.Functor C D} (h : F = G) {X : C} {Y : C} (f : X ⟶ Y) : F.map f = CategoryTheory.CategoryStruct.comp (CategoryTheory.eqToHom (_ : F.obj X = G.obj X)) (CategoryTheory.CategoryStruct.comp (G.map f) (CategoryTheory.eqToHom (_ : G.obj Y = F.obj Y)))

theorem CategoryTheory.Functor.congr_inv_of_congr_hom {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] (F : CategoryTheory.Functor C D) (G : CategoryTheory.Functor C D) {X : C} {Y : C} (e : X ≅ Y) (hX : F.obj X = G.obj X) (hY : F.obj Y = G.obj Y) (h₂ : F.map e.hom = CategoryTheory.CategoryStruct.comp (CategoryTheory.eqToHom (_ : F.obj X = G.obj X)) (CategoryTheory.CategoryStruct.comp (G.map e.hom) (CategoryTheory.eqToHom (_ : G.obj Y = F.obj Y)))) : F.map e.inv = CategoryTheory.CategoryStruct.comp (CategoryTheory.eqToHom (_ : F.obj Y = G.obj Y)) (CategoryTheory.CategoryStruct.comp (G.map e.inv) (CategoryTheory.eqToHom (_ : G.obj X = F.obj X)))

theorem CategoryTheory.Functor.congr_map {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] (F : CategoryTheory.Functor C D) {X : C} {Y : C} {f : X ⟶ Y} {g : X ⟶ Y} (h : f = g) : F.map f = F.map g

theorem CategoryTheory.Functor.map_comp_heq {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] {F : CategoryTheory.Functor C D} {G : CategoryTheory.Functor C D} {X : C} {Y : C} {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 : HEq (F.map f) (G.map f)) (hg : HEq (F.map g) (G.map g)) : HEq (F.map (CategoryTheory.CategoryStruct.comp f g)) (G.map (CategoryTheory.CategoryStruct.comp f g))

theorem CategoryTheory.Functor.map_comp_heq' {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] {F : CategoryTheory.Functor C D} {G : CategoryTheory.Functor C D} {X : C} {Y : C} {Z : C} {f : X ⟶ Y} {g : Y ⟶ Z} (hobj : ∀ (X : C), F.obj X = G.obj X) (hmap : ∀ {X Y : C} (f : X ⟶ Y), HEq (F.map f) (G.map f)) : HEq (F.map (CategoryTheory.CategoryStruct.comp f g)) (G.map (CategoryTheory.CategoryStruct.comp f g))

theorem CategoryTheory.Functor.precomp_map_heq {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] {E : Type u₃} [CategoryTheory.Category.{v₃, u₃} E] {F : CategoryTheory.Functor C D} {G : CategoryTheory.Functor C D} (H : CategoryTheory.Functor E C) (hmap : ∀ {X Y : C} (f : X ⟶ Y), HEq (F.map f) (G.map f)) {X : E} {Y : E} (f : X ⟶ Y) : HEq ((CategoryTheory.Functor.comp H F).map f) ((CategoryTheory.Functor.comp H G).map f)

theorem CategoryTheory.Functor.postcomp_map_heq {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] {E : Type u₃} [CategoryTheory.Category.{v₃, u₃} E] {F : CategoryTheory.Functor C D} {G : CategoryTheory.Functor C D} {X : C} {Y : C} {f : X ⟶ Y} (H : CategoryTheory.Functor D E) (hx : F.obj X = G.obj X) (hy : F.obj Y = G.obj Y) (hmap : HEq (F.map f) (G.map f)) : HEq ((CategoryTheory.Functor.comp F H).map f) ((CategoryTheory.Functor.comp G H).map f)

theorem CategoryTheory.Functor.postcomp_map_heq' {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] {E : Type u₃} [CategoryTheory.Category.{v₃, u₃} E] {F : CategoryTheory.Functor C D} {G : CategoryTheory.Functor C D} {X : C} {Y : C} {f : X ⟶ Y} (H : CategoryTheory.Functor D E) (hobj : ∀ (X : C), F.obj X = G.obj X) (hmap : ∀ {X Y : C} (f : X ⟶ Y), HEq (F.map f) (G.map f)) : HEq ((CategoryTheory.Functor.comp F H).map f) ((CategoryTheory.Functor.comp G H).map f)

theorem CategoryTheory.Functor.hcongr_hom {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] {F : CategoryTheory.Functor C D} {G : CategoryTheory.Functor C D} (h : F = G) {X : C} {Y : C} (f : X ⟶ Y) : HEq (F.map f) (G.map f)

theorem CategoryTheory.eqToHom_map {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] (F : CategoryTheory.Functor C D) {X : C} {Y : C} (p : X = Y) : F.map (CategoryTheory.eqToHom p) = CategoryTheory.eqToHom (_ : F.obj X = F.obj Y)

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] eqToHom_map, however.

theorem CategoryTheory.eqToIso_map {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] (F : CategoryTheory.Functor C D) {X : C} {Y : C} (p : X = Y) : F.mapIso (CategoryTheory.eqToIso p) = CategoryTheory.eqToIso (_ : F.obj X = F.obj Y)

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

@[simp]

theorem CategoryTheory.eqToHom_app {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] {F : CategoryTheory.Functor C D} {G : CategoryTheory.Functor C D} (h : F = G) (X : C) : (CategoryTheory.eqToHom h).app X = CategoryTheory.eqToHom (_ : F.obj X = G.obj X)

theorem CategoryTheory.NatTrans.congr {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] {F : CategoryTheory.Functor C D} {G : CategoryTheory.Functor C D} (α : F ⟶ G) {X : C} {Y : C} (h : X = Y) : α.app X = CategoryTheory.CategoryStruct.comp (F.map (CategoryTheory.eqToHom h)) (CategoryTheory.CategoryStruct.comp (α.app Y) (G.map (CategoryTheory.eqToHom (_ : Y = X))))

theorem CategoryTheory.eq_conj_eqToHom {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {X : C} {Y : C} (f : X ⟶ Y) : f = CategoryTheory.CategoryStruct.comp (CategoryTheory.eqToHom (_ : X = X)) (CategoryTheory.CategoryStruct.comp f (CategoryTheory.eqToHom (_ : Y = Y)))

theorem CategoryTheory.dcongr_arg {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {ι : Type u_1} {F : ι → C} {G : ι → C} (α : (i : ι) → F i ⟶ G i) {i : ι} {j : ι} (h : i = j) : α i = CategoryTheory.CategoryStruct.comp (CategoryTheory.eqToHom (_ : F i = F j)) (CategoryTheory.CategoryStruct.comp (α j) (CategoryTheory.eqToHom (_ : G j = G i)))