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:
- Use the equality
has one normally would in Lean (e.g. usingrwandsubst). This may immediately cause difficulties, because in category theory everything is dependently typed, and equations between objects quickly lead to nasty goals witheq.rec. - Promote
hto a morphism usingeqToHom h : X ⟶ Y, oreqToIso 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 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 = ⋯.mpr (CategoryTheory.CategoryStruct.id Y)
Instances For
@[simp]
theorem
CategoryTheory.eqToHom_refl
{C : Type u₁}
[CategoryTheory.Category.{v₁, u₁} C]
(X : C)
(p : X = X)
:
@[simp]
theorem
CategoryTheory.eqToHom_trans
{C : Type u₁}
[CategoryTheory.Category.{v₁, u₁} C]
{X Y Z : C}
(p : X = Y)
(q : Y = Z)
:
@[simp]
theorem
CategoryTheory.eqToHom_trans_assoc
{C : Type u₁}
[CategoryTheory.Category.{v₁, u₁} C]
{X Y Z : C}
(p : X = Y)
(q : Y = Z)
{Z✝ : C}
(h : Z ⟶ Z✝)
:
theorem
CategoryTheory.conj_eqToHom_iff_heq
{C : Type u₁}
[CategoryTheory.Category.{v₁, u₁} C]
{W X Y Z : C}
(f : W ⟶ X)
(g : Y ⟶ Z)
(h : W = Y)
(h' : X = Z)
:
Two morphisms are conjugate via eqToHom if and only if they are heterogeneously equal. Note this used to be in the Functor namespace, where it doesn't belong.
theorem
CategoryTheory.conj_eqToHom_iff_heq'
{C : Type u_1}
[CategoryTheory.Category.{u_2, u_1} C]
{W X Y Z : C}
(f : W ⟶ X)
(g : Y ⟶ Z)
(h : W = Y)
(h' : Z = X)
:
theorem
CategoryTheory.comp_eqToHom_iff
{C : Type u₁}
[CategoryTheory.Category.{v₁, u₁} C]
{X Y Y' : C}
(p : Y = Y')
(f : X ⟶ Y)
(g : X ⟶ Y')
:
theorem
CategoryTheory.eqToHom_comp_iff
{C : Type u₁}
[CategoryTheory.Category.{v₁, u₁} C]
{X X' Y : C}
(p : X = X')
(f : X ⟶ Y)
(g : X' ⟶ Y)
:
theorem
CategoryTheory.eqToHom_comp_heq
{C : Type u_1}
[CategoryTheory.Category.{u_2, u_1} C]
{W X Y : C}
(f : Y ⟶ X)
(h : W = Y)
:
@[simp]
theorem
CategoryTheory.eqToHom_comp_heq_iff
{C : Type u_1}
[CategoryTheory.Category.{u_2, u_1} C]
{W X Y Z Z' : C}
(f : Y ⟶ X)
(g : Z ⟶ Z')
(h : W = Y)
:
HEq (CategoryTheory.CategoryStruct.comp (CategoryTheory.eqToHom h) f) g ↔ HEq f g
@[simp]
theorem
CategoryTheory.heq_eqToHom_comp_iff
{C : Type u_1}
[CategoryTheory.Category.{u_2, u_1} C]
{W X Y Z Z' : C}
(f : Y ⟶ X)
(g : Z ⟶ Z')
(h : W = Y)
:
HEq g (CategoryTheory.CategoryStruct.comp (CategoryTheory.eqToHom h) f) ↔ HEq g f
theorem
CategoryTheory.comp_eqToHom_heq
{C : Type u_1}
[CategoryTheory.Category.{u_2, u_1} C]
{X Y Z : C}
(f : X ⟶ Y)
(h : Y = Z)
:
@[simp]
theorem
CategoryTheory.comp_eqToHom_heq_iff
{C : Type u_1}
[CategoryTheory.Category.{u_2, u_1} C]
{W X Y Z Z' : C}
(f : X ⟶ Y)
(g : Z ⟶ Z')
(h : Y = W)
:
HEq (CategoryTheory.CategoryStruct.comp f (CategoryTheory.eqToHom h)) g ↔ HEq f g
@[simp]
theorem
CategoryTheory.heq_comp_eqToHom_iff
{C : Type u_1}
[CategoryTheory.Category.{u_2, u_1} C]
{W X Y Z Z' : C}
(f : X ⟶ Y)
(g : Z ⟶ Z')
(h : Y = W)
:
HEq g (CategoryTheory.CategoryStruct.comp f (CategoryTheory.eqToHom h)) ↔ HEq g f
@[simp]
theorem
CategoryTheory.eqToHom_naturality
{C : Type u₁}
[CategoryTheory.Category.{v₁, u₁} C]
{β : Sort u_1}
{f g : β → C}
(z : (b : β) → f b ⟶ g b)
{j j' : β}
(w : j = j')
:
We can push eqToHom to the left through families of morphisms.
@[simp]
theorem
CategoryTheory.eqToHom_naturality_assoc
{C : Type u₁}
[CategoryTheory.Category.{v₁, u₁} C]
{β : Sort u_1}
{f g : β → C}
(z : (b : β) → f b ⟶ g b)
{j j' : β}
(w : j = j')
{Z : C}
(h : g j' ⟶ Z)
:
@[simp]
theorem
CategoryTheory.eqToHom_iso_hom_naturality
{C : Type u₁}
[CategoryTheory.Category.{v₁, u₁} C]
{β : Sort u_1}
{f g : β → C}
(z : (b : β) → f b ≅ g b)
{j j' : β}
(w : j = j')
:
CategoryTheory.CategoryStruct.comp (z j).hom (CategoryTheory.eqToHom ⋯) = CategoryTheory.CategoryStruct.comp (CategoryTheory.eqToHom ⋯) (z j').hom
A variant on eqToHom_naturality that helps Lean identify the families f and g.
@[simp]
theorem
CategoryTheory.eqToHom_iso_hom_naturality_assoc
{C : Type u₁}
[CategoryTheory.Category.{v₁, u₁} C]
{β : Sort u_1}
{f g : β → C}
(z : (b : β) → f b ≅ g b)
{j j' : β}
(w : j = j')
{Z : C}
(h : g j' ⟶ Z)
:
@[simp]
theorem
CategoryTheory.eqToHom_iso_inv_naturality
{C : Type u₁}
[CategoryTheory.Category.{v₁, u₁} C]
{β : Sort u_1}
{f g : β → C}
(z : (b : β) → f b ≅ g b)
{j j' : β}
(w : j = j')
:
CategoryTheory.CategoryStruct.comp (z j).inv (CategoryTheory.eqToHom ⋯) = CategoryTheory.CategoryStruct.comp (CategoryTheory.eqToHom ⋯) (z j').inv
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 g : β → C}
(z : (b : β) → f b ≅ g b)
{j j' : β}
(w : j = j')
{Z : C}
(h : f j' ⟶ Z)
:
@[simp]
theorem
CategoryTheory.congrArg_cast_hom_left
{C : Type u₁}
[CategoryTheory.Category.{v₁, u₁} C]
{X Y Z : C}
(p : X = Y)
(q : Y ⟶ Z)
:
Reducible form of congrArg_mpr_hom_left
theorem
CategoryTheory.congrArg_mpr_hom_left
{C : Type u₁}
[CategoryTheory.Category.{v₁, u₁} C]
{X Y Z : C}
(p : X = Y)
(q : Y ⟶ Z)
:
⋯.mpr 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 Y Z : C}
(p : X ⟶ Y)
(q : Z = Y)
:
Reducible form of congrArg_mpr_hom_right
theorem
CategoryTheory.congrArg_mpr_hom_right
{C : Type u₁}
[CategoryTheory.Category.{v₁, u₁} C]
{X Y Z : C}
(p : X ⟶ Y)
(q : Z = Y)
:
⋯.mpr p = CategoryTheory.CategoryStruct.comp p (CategoryTheory.eqToHom ⋯)
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 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 = { hom := CategoryTheory.eqToHom p, inv := CategoryTheory.eqToHom ⋯, hom_inv_id := ⋯, inv_hom_id := ⋯ }
Instances For
@[simp]
theorem
CategoryTheory.eqToIso.hom
{C : Type u₁}
[CategoryTheory.Category.{v₁, u₁} C]
{X 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 Y : C}
(p : X = Y)
:
(CategoryTheory.eqToIso p).inv = CategoryTheory.eqToHom ⋯
@[simp]
theorem
CategoryTheory.eqToIso_refl
{C : Type u₁}
[CategoryTheory.Category.{v₁, u₁} C]
{X : C}
(p : X = X)
:
@[simp]
theorem
CategoryTheory.eqToIso_trans
{C : Type u₁}
[CategoryTheory.Category.{v₁, u₁} C]
{X Y Z : C}
(p : X = Y)
(q : Y = Z)
:
@[simp]
theorem
CategoryTheory.eqToHom_op
{C : Type u₁}
[CategoryTheory.Category.{v₁, u₁} C]
{X Y : C}
(h : X = Y)
:
@[simp]
theorem
CategoryTheory.eqToHom_unop
{C : Type u₁}
[CategoryTheory.Category.{v₁, u₁} C]
{X Y : Cᵒᵖ}
(h : X = Y)
:
(CategoryTheory.eqToHom h).unop = CategoryTheory.eqToHom ⋯
instance
CategoryTheory.instIsIsoEqToHom
{C : Type u₁}
[CategoryTheory.Category.{v₁, u₁} C]
{X Y : C}
(h : X = Y)
:
Equations
- ⋯ = ⋯
@[simp]
theorem
CategoryTheory.inv_eqToHom
{C : Type u₁}
[CategoryTheory.Category.{v₁, u₁} C]
{X Y : C}
(h : X = Y)
:
theorem
CategoryTheory.Functor.ext
{C : Type u₁}
[CategoryTheory.Category.{v₁, u₁} C]
{D : Type u₂}
[CategoryTheory.Category.{v₂, u₂} D]
{F G : CategoryTheory.Functor C D}
(h_obj : ∀ (X : C), F.obj X = G.obj X)
(h_map :
∀ (X Y : C) (f : X ⟶ Y),
F.map f = CategoryTheory.CategoryStruct.comp (CategoryTheory.eqToHom ⋯)
(CategoryTheory.CategoryStruct.comp (G.map f) (CategoryTheory.eqToHom ⋯)) := by
aesop_cat)
:
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.ext_of_iso
{C : Type u₁}
[CategoryTheory.Category.{v₁, u₁} C]
{D : Type u₂}
[CategoryTheory.Category.{v₂, u₂} D]
{F G : CategoryTheory.Functor C D}
(e : F ≅ G)
(hobj : ∀ (X : C), F.obj X = G.obj X)
(happ : ∀ (X : C), e.hom.app X = CategoryTheory.eqToHom ⋯)
:
F = G
theorem
CategoryTheory.Functor.hext
{C : Type u₁}
[CategoryTheory.Category.{v₁, u₁} C]
{D : Type u₂}
[CategoryTheory.Category.{v₂, u₂} D]
{F 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 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 G : CategoryTheory.Functor C D}
(h : F = G)
{X Y : C}
(f : X ⟶ Y)
:
F.map f = CategoryTheory.CategoryStruct.comp (CategoryTheory.eqToHom ⋯)
(CategoryTheory.CategoryStruct.comp (G.map f) (CategoryTheory.eqToHom ⋯))
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 G : CategoryTheory.Functor 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 = CategoryTheory.CategoryStruct.comp (CategoryTheory.eqToHom ⋯)
(CategoryTheory.CategoryStruct.comp (G.map e.hom) (CategoryTheory.eqToHom ⋯)))
:
F.map e.inv = CategoryTheory.CategoryStruct.comp (CategoryTheory.eqToHom ⋯)
(CategoryTheory.CategoryStruct.comp (G.map e.inv) (CategoryTheory.eqToHom ⋯))
theorem
CategoryTheory.Functor.map_comp_heq
{C : Type u₁}
[CategoryTheory.Category.{v₁, u₁} C]
{D : Type u₂}
[CategoryTheory.Category.{v₂, u₂} D]
{F G : CategoryTheory.Functor 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 : 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 G : CategoryTheory.Functor 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), 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 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 Y : E}
(f : X ⟶ Y)
:
HEq ((H.comp F).map f) ((H.comp 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 G : CategoryTheory.Functor C D}
{X 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 ((F.comp H).map f) ((G.comp 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 G : CategoryTheory.Functor C D}
{X 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 ((F.comp H).map f) ((G.comp 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 G : CategoryTheory.Functor C D}
(h : F = G)
{X 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 Y : C}
(p : X = Y)
:
F.map (CategoryTheory.eqToHom p) = CategoryTheory.eqToHom ⋯
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 attribute [local simp] eqToHom_map, however.
@[simp]
theorem
CategoryTheory.eqToHom_map_comp
{C : Type u₁}
[CategoryTheory.Category.{v₁, u₁} C]
{D : Type u₂}
[CategoryTheory.Category.{v₂, u₂} D]
(F : CategoryTheory.Functor C D)
{X Y Z : C}
(p : X = Y)
(q : Y = Z)
:
CategoryTheory.CategoryStruct.comp (F.map (CategoryTheory.eqToHom p)) (F.map (CategoryTheory.eqToHom q)) = F.map (CategoryTheory.eqToHom ⋯)
@[simp]
theorem
CategoryTheory.eqToHom_map_comp_assoc
{C : Type u₁}
[CategoryTheory.Category.{v₁, u₁} C]
{D : Type u₂}
[CategoryTheory.Category.{v₂, u₂} D]
(F : CategoryTheory.Functor C D)
{X Y Z : C}
(p : X = Y)
(q : Y = Z)
{Z✝ : D}
(h : F.obj Z ⟶ Z✝)
:
CategoryTheory.CategoryStruct.comp (F.map (CategoryTheory.eqToHom p))
(CategoryTheory.CategoryStruct.comp (F.map (CategoryTheory.eqToHom q)) h) = CategoryTheory.CategoryStruct.comp (F.map (CategoryTheory.eqToHom ⋯)) h
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 Y : C}
(p : X = Y)
:
F.mapIso (CategoryTheory.eqToIso p) = CategoryTheory.eqToIso ⋯
See the note on eqToHom_map regarding using this as a simp lemma.
@[simp]
theorem
CategoryTheory.eqToIso_map_trans
{C : Type u₁}
[CategoryTheory.Category.{v₁, u₁} C]
{D : Type u₂}
[CategoryTheory.Category.{v₂, u₂} D]
(F : CategoryTheory.Functor C D)
{X Y Z : C}
(p : X = Y)
(q : Y = Z)
:
F.mapIso (CategoryTheory.eqToIso p) ≪≫ F.mapIso (CategoryTheory.eqToIso q) = F.mapIso (CategoryTheory.eqToIso ⋯)
@[simp]
theorem
CategoryTheory.eqToHom_app
{C : Type u₁}
[CategoryTheory.Category.{v₁, u₁} C]
{D : Type u₂}
[CategoryTheory.Category.{v₂, u₂} D]
{F G : CategoryTheory.Functor C D}
(h : F = G)
(X : C)
:
(CategoryTheory.eqToHom h).app X = CategoryTheory.eqToHom ⋯
theorem
CategoryTheory.NatTrans.congr
{C : Type u₁}
[CategoryTheory.Category.{v₁, u₁} C]
{D : Type u₂}
[CategoryTheory.Category.{v₂, u₂} D]
{F G : CategoryTheory.Functor C D}
(α : F ⟶ G)
{X Y : C}
(h : X = Y)
:
α.app X = CategoryTheory.CategoryStruct.comp (F.map (CategoryTheory.eqToHom h))
(CategoryTheory.CategoryStruct.comp (α.app Y) (G.map (CategoryTheory.eqToHom ⋯)))
theorem
CategoryTheory.eq_conj_eqToHom
{C : Type u₁}
[CategoryTheory.Category.{v₁, u₁} C]
{X Y : C}
(f : X ⟶ Y)
:
theorem
CategoryTheory.dcongr_arg
{C : Type u₁}
[CategoryTheory.Category.{v₁, u₁} C]
{ι : Type u_2}
{F G : ι → C}
(α : (i : ι) → F i ⟶ G i)
{i j : ι}
(h : i = j)
: