Equalizers and coequalizers #
This file defines (co)equalizers as special cases of (co)limits.
An equalizer is the categorical generalization of the subobject {a ∈ A | f(a) = g(a)} known
from abelian groups or modules. It is a limit cone over the diagram formed by f and g.
A coequalizer is the dual concept.
Main definitions #
WalkingParallelPairis the indexing category used for (co)equalizer_diagramsparallelPairis a functor fromWalkingParallelPairto our categoryC.- a
forkis a cone over a parallel pair.- there is really only one interesting morphism in a fork: the arrow from the vertex of the fork
to the domain of f and g. It is called
fork.ι.
- there is really only one interesting morphism in a fork: the arrow from the vertex of the fork
to the domain of f and g. It is called
- an
equalizeris now just alimit (parallelPair f g)
Each of these has a dual.
Main statements #
equalizer.ι_monostates that every equalizer map is a monomorphismisIso_limit_cone_parallelPair_of_selfstates that the identity on the domain offis an equalizer offandf.
Implementation notes #
As with the other special shapes in the limits library, all the definitions here are given as
abbreviations of the general statements for limits, so all the simp lemmas and theorems about
general limits can be used.
References #
- [F. Borceux, Handbook of Categorical Algebra 1][borceux-vol1]
The type of objects for the diagram indexing a (co)equalizer.
- zero : WalkingParallelPair
- one : WalkingParallelPair
The type family of morphisms for the diagram indexing a (co)equalizer.
Satisfying the inhabited linter
def
CategoryTheory.Limits.WalkingParallelPairHom.comp
{X Y Z : WalkingParallelPair}
:
WalkingParallelPairHom X Y → WalkingParallelPairHom Y Z → WalkingParallelPairHom X Z
Composition of morphisms in the indexing diagram for (co)equalizers.
Equations
- One or more equations did not get rendered due to their size.
- (CategoryTheory.Limits.WalkingParallelPairHom.id x✝²).comp x✝ = x✝
theorem
CategoryTheory.Limits.WalkingParallelPairHom.id_comp
{X Y : WalkingParallelPair}
(g : WalkingParallelPairHom X Y)
:
theorem
CategoryTheory.Limits.WalkingParallelPairHom.comp_id
{X Y : WalkingParallelPair}
(f : WalkingParallelPairHom X Y)
:
theorem
CategoryTheory.Limits.WalkingParallelPairHom.assoc
{X Y Z W : WalkingParallelPair}
(f : WalkingParallelPairHom X Y)
(g : WalkingParallelPairHom Y Z)
(h : WalkingParallelPairHom Z W)
:
@[simp]
The functor WalkingParallelPair ⥤ WalkingParallelPairᵒᵖ sending left to left and right to
right.
Equations
- One or more equations did not get rendered due to their size.
The equivalence WalkingParallelPair ⥤ WalkingParallelPairᵒᵖ sending left to left and right to
right.
Equations
- One or more equations did not get rendered due to their size.
parallelPair f g is the diagram in C consisting of the two morphisms f and g with
common domain and codomain.
Equations
- One or more equations did not get rendered due to their size.
@[simp]
theorem
CategoryTheory.Limits.parallelPair_obj_zero
{C : Type u}
[Category.{v, u} C]
{X Y : C}
(f g : X ⟶ Y)
:
@[simp]
theorem
CategoryTheory.Limits.parallelPair_obj_one
{C : Type u}
[Category.{v, u} C]
{X Y : C}
(f g : X ⟶ Y)
:
@[simp]
theorem
CategoryTheory.Limits.parallelPair_map_left
{C : Type u}
[Category.{v, u} C]
{X Y : C}
(f g : X ⟶ Y)
:
@[simp]
theorem
CategoryTheory.Limits.parallelPair_map_right
{C : Type u}
[Category.{v, u} C]
{X Y : C}
(f g : X ⟶ Y)
:
@[simp]
theorem
CategoryTheory.Limits.parallelPair_functor_obj
{C : Type u}
[Category.{v, u} C]
{F : Functor WalkingParallelPair C}
(j : WalkingParallelPair)
:
(parallelPair (F.map WalkingParallelPairHom.left) (F.map WalkingParallelPairHom.right)).obj j = F.obj j
def
CategoryTheory.Limits.diagramIsoParallelPair
{C : Type u}
[Category.{v, u} C]
(F : Functor WalkingParallelPair C)
:
Every functor indexing a (co)equalizer is naturally isomorphic (actually, equal) to a
parallelPair
@[simp]
theorem
CategoryTheory.Limits.diagramIsoParallelPair_hom_app
{C : Type u}
[Category.{v, u} C]
(F : Functor WalkingParallelPair C)
(X : WalkingParallelPair)
:
@[simp]
theorem
CategoryTheory.Limits.diagramIsoParallelPair_inv_app
{C : Type u}
[Category.{v, u} C]
(F : Functor WalkingParallelPair C)
(X : WalkingParallelPair)
:
def
CategoryTheory.Limits.parallelPairHom
{C : Type u}
[Category.{v, u} C]
{X Y X' Y' : C}
(f g : X ⟶ Y)
(f' g' : X' ⟶ Y')
(p : X ⟶ X')
(q : Y ⟶ Y')
(wf : CategoryStruct.comp f q = CategoryStruct.comp p f')
(wg : CategoryStruct.comp g q = CategoryStruct.comp p g')
:
Construct a morphism between parallel pairs.
Equations
- One or more equations did not get rendered due to their size.
@[simp]
theorem
CategoryTheory.Limits.parallelPairHom_app_zero
{C : Type u}
[Category.{v, u} C]
{X Y X' Y' : C}
(f g : X ⟶ Y)
(f' g' : X' ⟶ Y')
(p : X ⟶ X')
(q : Y ⟶ Y')
(wf : CategoryStruct.comp f q = CategoryStruct.comp p f')
(wg : CategoryStruct.comp g q = CategoryStruct.comp p g')
:
@[simp]
theorem
CategoryTheory.Limits.parallelPairHom_app_one
{C : Type u}
[Category.{v, u} C]
{X Y X' Y' : C}
(f g : X ⟶ Y)
(f' g' : X' ⟶ Y')
(p : X ⟶ X')
(q : Y ⟶ Y')
(wf : CategoryStruct.comp f q = CategoryStruct.comp p f')
(wg : CategoryStruct.comp g q = CategoryStruct.comp p g')
:
def
CategoryTheory.Limits.parallelPair.ext
{C : Type u}
[Category.{v, u} C]
{F G : Functor WalkingParallelPair C}
(zero : F.obj WalkingParallelPair.zero ≅ G.obj WalkingParallelPair.zero)
(one : F.obj WalkingParallelPair.one ≅ G.obj WalkingParallelPair.one)
(left :
CategoryStruct.comp (F.map WalkingParallelPairHom.left) one.hom = CategoryStruct.comp zero.hom (G.map WalkingParallelPairHom.left))
(right :
CategoryStruct.comp (F.map WalkingParallelPairHom.right) one.hom = CategoryStruct.comp zero.hom (G.map WalkingParallelPairHom.right))
:
Construct a natural isomorphism between functors out of the walking parallel pair from its components.
Equations
- One or more equations did not get rendered due to their size.
@[simp]
theorem
CategoryTheory.Limits.parallelPair.ext_hom_app
{C : Type u}
[Category.{v, u} C]
{F G : Functor WalkingParallelPair C}
(zero : F.obj WalkingParallelPair.zero ≅ G.obj WalkingParallelPair.zero)
(one : F.obj WalkingParallelPair.one ≅ G.obj WalkingParallelPair.one)
(left :
CategoryStruct.comp (F.map WalkingParallelPairHom.left) one.hom = CategoryStruct.comp zero.hom (G.map WalkingParallelPairHom.left))
(right :
CategoryStruct.comp (F.map WalkingParallelPairHom.right) one.hom = CategoryStruct.comp zero.hom (G.map WalkingParallelPairHom.right))
(X : WalkingParallelPair)
:
@[simp]
theorem
CategoryTheory.Limits.parallelPair.ext_inv_app
{C : Type u}
[Category.{v, u} C]
{F G : Functor WalkingParallelPair C}
(zero : F.obj WalkingParallelPair.zero ≅ G.obj WalkingParallelPair.zero)
(one : F.obj WalkingParallelPair.one ≅ G.obj WalkingParallelPair.one)
(left :
CategoryStruct.comp (F.map WalkingParallelPairHom.left) one.hom = CategoryStruct.comp zero.hom (G.map WalkingParallelPairHom.left))
(right :
CategoryStruct.comp (F.map WalkingParallelPairHom.right) one.hom = CategoryStruct.comp zero.hom (G.map WalkingParallelPairHom.right))
(X : WalkingParallelPair)
:
def
CategoryTheory.Limits.parallelPair.eqOfHomEq
{C : Type u}
[Category.{v, u} C]
{X Y : C}
{f g f' g' : X ⟶ Y}
(hf : f = f')
(hg : g = g')
:
Construct a natural isomorphism between parallelPair f g and parallelPair f' g' given
equalities f = f' and g = g'.
Equations
- One or more equations did not get rendered due to their size.
@[simp]
theorem
CategoryTheory.Limits.parallelPair.eqOfHomEq_hom_app
{C : Type u}
[Category.{v, u} C]
{X Y : C}
{f g f' g' : X ⟶ Y}
(hf : f = f')
(hg : g = g')
(X✝ : WalkingParallelPair)
:
@[simp]
theorem
CategoryTheory.Limits.parallelPair.eqOfHomEq_inv_app
{C : Type u}
[Category.{v, u} C]
{X Y : C}
{f g f' g' : X ⟶ Y}
(hf : f = f')
(hg : g = g')
(X✝ : WalkingParallelPair)
:
@[reducible, inline]
abbrev
CategoryTheory.Limits.Fork
{C : Type u}
[Category.{v, u} C]
{X Y : C}
(f g : X ⟶ Y)
:
Type (max u v)
A fork on f and g is just a Cone (parallelPair f g).
Equations
@[reducible, inline]
abbrev
CategoryTheory.Limits.Cofork
{C : Type u}
[Category.{v, u} C]
{X Y : C}
(f g : X ⟶ Y)
:
Type (max u v)
A cofork on f and g is just a Cocone (parallelPair f g).
def
CategoryTheory.Limits.Fork.ι
{C : Type u}
[Category.{v, u} C]
{X Y : C}
{f g : X ⟶ Y}
(t : Fork f g)
:
A fork t on the parallel pair f g : X ⟶ Y consists of two morphisms
t.π.app zero : t.pt ⟶ X
and t.π.app one : t.pt ⟶ Y. Of these, only the first one is interesting, and we give it the
shorter name Fork.ι t.
Equations
@[simp]
theorem
CategoryTheory.Limits.Fork.app_zero_eq_ι
{C : Type u}
[Category.{v, u} C]
{X Y : C}
{f g : X ⟶ Y}
(t : Fork f g)
:
def
CategoryTheory.Limits.Cofork.π
{C : Type u}
[Category.{v, u} C]
{X Y : C}
{f g : X ⟶ Y}
(t : Cofork f g)
:
A cofork t on the parallelPair f g : X ⟶ Y consists of two morphisms
t.ι.app zero : X ⟶ t.pt and t.ι.app one : Y ⟶ t.pt. Of these, only the second one is
interesting, and we give it the shorter name Cofork.π t.
Equations
@[simp]
theorem
CategoryTheory.Limits.Cofork.app_one_eq_π
{C : Type u}
[Category.{v, u} C]
{X Y : C}
{f g : X ⟶ Y}
(t : Cofork f g)
:
@[simp]
theorem
CategoryTheory.Limits.Fork.app_one_eq_ι_comp_left
{C : Type u}
[Category.{v, u} C]
{X Y : C}
{f g : X ⟶ Y}
(s : Fork f g)
:
theorem
CategoryTheory.Limits.Fork.app_one_eq_ι_comp_right
{C : Type u}
[Category.{v, u} C]
{X Y : C}
{f g : X ⟶ Y}
(s : Fork f g)
:
theorem
CategoryTheory.Limits.Fork.app_one_eq_ι_comp_right_assoc
{C : Type u}
[Category.{v, u} C]
{X Y : C}
{f g : X ⟶ Y}
(s : Fork f g)
{Z : C}
(h : (parallelPair f g).obj WalkingParallelPair.one ⟶ Z)
:
@[simp]
theorem
CategoryTheory.Limits.Cofork.app_zero_eq_comp_π_left
{C : Type u}
[Category.{v, u} C]
{X Y : C}
{f g : X ⟶ Y}
(s : Cofork f g)
:
theorem
CategoryTheory.Limits.Cofork.app_zero_eq_comp_π_right
{C : Type u}
[Category.{v, u} C]
{X Y : C}
{f g : X ⟶ Y}
(s : Cofork f g)
:
theorem
CategoryTheory.Limits.Cofork.app_zero_eq_comp_π_right_assoc
{C : Type u}
[Category.{v, u} C]
{X Y : C}
{f g : X ⟶ Y}
(s : Cofork f g)
{Z : C}
(h : ((Functor.const WalkingParallelPair).obj s.pt).obj WalkingParallelPair.zero ⟶ Z)
:
def
CategoryTheory.Limits.Fork.ofι
{C : Type u}
[Category.{v, u} C]
{X Y : C}
{f g : X ⟶ Y}
{P : C}
(ι : P ⟶ X)
(w : CategoryStruct.comp ι f = CategoryStruct.comp ι g)
:
Fork f g
A fork on f g : X ⟶ Y is determined by the morphism ι : P ⟶ X satisfying ι ≫ f = ι ≫ g.
Equations
- One or more equations did not get rendered due to their size.
@[simp]
theorem
CategoryTheory.Limits.Fork.ofι_pt
{C : Type u}
[Category.{v, u} C]
{X Y : C}
{f g : X ⟶ Y}
{P : C}
(ι : P ⟶ X)
(w : CategoryStruct.comp ι f = CategoryStruct.comp ι g)
:
@[simp]
theorem
CategoryTheory.Limits.Fork.ofι_π_app
{C : Type u}
[Category.{v, u} C]
{X Y : C}
{f g : X ⟶ Y}
{P : C}
(ι : P ⟶ X)
(w : CategoryStruct.comp ι f = CategoryStruct.comp ι g)
(X✝ : WalkingParallelPair)
:
(ofι ι w).π.app X✝ = WalkingParallelPair.casesOn (motive := fun (t : WalkingParallelPair) =>
X✝ = t → (((Functor.const WalkingParallelPair).obj P).obj X✝ ⟶ (parallelPair f g).obj X✝)) X✝
(fun (h : X✝ = WalkingParallelPair.zero) => ⋯ ▸ ι)
(fun (h : X✝ = WalkingParallelPair.one) => ⋯ ▸ CategoryStruct.comp ι f) ⋯
def
CategoryTheory.Limits.Cofork.ofπ
{C : Type u}
[Category.{v, u} C]
{X Y : C}
{f g : X ⟶ Y}
{P : C}
(π : Y ⟶ P)
(w : CategoryStruct.comp f π = CategoryStruct.comp g π)
:
Cofork f g
A cofork on f g : X ⟶ Y is determined by the morphism π : Y ⟶ P satisfying
f ≫ π = g ≫ π.
Equations
- One or more equations did not get rendered due to their size.
@[simp]
theorem
CategoryTheory.Limits.Cofork.ofπ_ι_app
{C : Type u}
[Category.{v, u} C]
{X Y : C}
{f g : X ⟶ Y}
{P : C}
(π : Y ⟶ P)
(w : CategoryStruct.comp f π = CategoryStruct.comp g π)
(X✝ : WalkingParallelPair)
:
@[simp]
theorem
CategoryTheory.Limits.Cofork.ofπ_pt
{C : Type u}
[Category.{v, u} C]
{X Y : C}
{f g : X ⟶ Y}
{P : C}
(π : Y ⟶ P)
(w : CategoryStruct.comp f π = CategoryStruct.comp g π)
:
@[simp]
theorem
CategoryTheory.Limits.Fork.ι_ofι
{C : Type u}
[Category.{v, u} C]
{X Y : C}
{f g : X ⟶ Y}
{P : C}
(ι : P ⟶ X)
(w : CategoryStruct.comp ι f = CategoryStruct.comp ι g)
:
@[simp]
theorem
CategoryTheory.Limits.Cofork.π_ofπ
{C : Type u}
[Category.{v, u} C]
{X Y : C}
{f g : X ⟶ Y}
{P : C}
(π : Y ⟶ P)
(w : CategoryStruct.comp f π = CategoryStruct.comp g π)
:
@[simp]
theorem
CategoryTheory.Limits.Fork.condition
{C : Type u}
[Category.{v, u} C]
{X Y : C}
{f g : X ⟶ Y}
(t : Fork f g)
:
@[simp]
theorem
CategoryTheory.Limits.Fork.condition_assoc
{C : Type u}
[Category.{v, u} C]
{X Y : C}
{f g : X ⟶ Y}
(t : Fork f g)
{Z : C}
(h : Y ⟶ Z)
:
CategoryStruct.comp t.ι (CategoryStruct.comp f h) = CategoryStruct.comp t.ι (CategoryStruct.comp g h)
@[simp]
theorem
CategoryTheory.Limits.Cofork.condition
{C : Type u}
[Category.{v, u} C]
{X Y : C}
{f g : X ⟶ Y}
(t : Cofork f g)
:
@[simp]
theorem
CategoryTheory.Limits.Cofork.condition_assoc
{C : Type u}
[Category.{v, u} C]
{X Y : C}
{f g : X ⟶ Y}
(t : Cofork f g)
{Z : C}
(h : ((Functor.const WalkingParallelPair).obj t.pt).obj WalkingParallelPair.one ⟶ Z)
:
CategoryStruct.comp f (CategoryStruct.comp t.π h) = CategoryStruct.comp g (CategoryStruct.comp t.π h)
theorem
CategoryTheory.Limits.Fork.equalizer_ext
{C : Type u}
[Category.{v, u} C]
{X Y : C}
{f g : X ⟶ Y}
(s : Fork f g)
{W : C}
{k l : W ⟶ s.pt}
(h : CategoryStruct.comp k s.ι = CategoryStruct.comp l s.ι)
(j : WalkingParallelPair)
:
To check whether two maps are equalized by both maps of a fork, it suffices to check it for the first map
theorem
CategoryTheory.Limits.Cofork.coequalizer_ext
{C : Type u}
[Category.{v, u} C]
{X Y : C}
{f g : X ⟶ Y}
(s : Cofork f g)
{W : C}
{k l : s.pt ⟶ W}
(h : CategoryStruct.comp s.π k = CategoryStruct.comp s.π l)
(j : WalkingParallelPair)
:
To check whether two maps are coequalized by both maps of a cofork, it suffices to check it for the second map
theorem
CategoryTheory.Limits.Fork.IsLimit.hom_ext
{C : Type u}
[Category.{v, u} C]
{X Y : C}
{f g : X ⟶ Y}
{s : Fork f g}
(hs : IsLimit s)
{W : C}
{k l : W ⟶ s.pt}
(h : CategoryStruct.comp k s.ι = CategoryStruct.comp l s.ι)
:
theorem
CategoryTheory.Limits.Cofork.IsColimit.hom_ext
{C : Type u}
[Category.{v, u} C]
{X Y : C}
{f g : X ⟶ Y}
{s : Cofork f g}
(hs : IsColimit s)
{W : C}
{k l : s.pt ⟶ W}
(h : CategoryStruct.comp s.π k = CategoryStruct.comp s.π l)
:
@[simp]
theorem
CategoryTheory.Limits.Fork.IsLimit.lift_ι
{C : Type u}
[Category.{v, u} C]
{X Y : C}
{f g : X ⟶ Y}
{s t : Fork f g}
(hs : IsLimit s)
:
@[simp]
theorem
CategoryTheory.Limits.Fork.IsLimit.lift_ι_assoc
{C : Type u}
[Category.{v, u} C]
{X Y : C}
{f g : X ⟶ Y}
{s t : Fork f g}
(hs : IsLimit s)
{Z : C}
(h : (parallelPair f g).obj WalkingParallelPair.zero ⟶ Z)
:
@[simp]
theorem
CategoryTheory.Limits.Cofork.IsColimit.π_desc
{C : Type u}
[Category.{v, u} C]
{X Y : C}
{f g : X ⟶ Y}
{s t : Cofork f g}
(hs : IsColimit s)
:
@[simp]
theorem
CategoryTheory.Limits.Cofork.IsColimit.π_desc_assoc
{C : Type u}
[Category.{v, u} C]
{X Y : C}
{f g : X ⟶ Y}
{s t : Cofork f g}
(hs : IsColimit s)
{Z : C}
(h : t.pt ⟶ Z)
:
def
CategoryTheory.Limits.Fork.IsLimit.lift
{C : Type u}
[Category.{v, u} C]
{X Y : C}
{f g : X ⟶ Y}
{s : Fork f g}
(hs : IsLimit s)
{W : C}
(k : W ⟶ X)
(h : CategoryStruct.comp k f = CategoryStruct.comp k g)
:
If s is a limit fork over f and g, then a morphism k : W ⟶ X satisfying
k ≫ f = k ≫ g induces a morphism l : W ⟶ s.pt such that l ≫ fork.ι s = k.
Equations
- CategoryTheory.Limits.Fork.IsLimit.lift hs k h = hs.lift (CategoryTheory.Limits.Fork.ofι k h)
@[simp]
theorem
CategoryTheory.Limits.Fork.IsLimit.lift_ι'
{C : Type u}
[Category.{v, u} C]
{X Y : C}
{f g : X ⟶ Y}
{s : Fork f g}
(hs : IsLimit s)
{W : C}
(k : W ⟶ X)
(h : CategoryStruct.comp k f = CategoryStruct.comp k g)
:
@[simp]
theorem
CategoryTheory.Limits.Fork.IsLimit.lift_ι'_assoc
{C : Type u}
[Category.{v, u} C]
{X Y : C}
{f g : X ⟶ Y}
{s : Fork f g}
(hs : IsLimit s)
{W : C}
(k : W ⟶ X)
(h : CategoryStruct.comp k f = CategoryStruct.comp k g)
{Z : C}
(h✝ : (parallelPair f g).obj WalkingParallelPair.zero ⟶ Z)
:
def
CategoryTheory.Limits.Fork.IsLimit.lift'
{C : Type u}
[Category.{v, u} C]
{X Y : C}
{f g : X ⟶ Y}
{s : Fork f g}
(hs : IsLimit s)
{W : C}
(k : W ⟶ X)
(h : CategoryStruct.comp k f = CategoryStruct.comp k g)
:
If s is a limit fork over f and g, then a morphism k : W ⟶ X satisfying
k ≫ f = k ≫ g induces a morphism l : W ⟶ s.pt such that l ≫ fork.ι s = k.
Equations
- CategoryTheory.Limits.Fork.IsLimit.lift' hs k h = ⟨CategoryTheory.Limits.Fork.IsLimit.lift hs k h, ⋯⟩
def
CategoryTheory.Limits.Cofork.IsColimit.desc
{C : Type u}
[Category.{v, u} C]
{X Y : C}
{f g : X ⟶ Y}
{s : Cofork f g}
(hs : IsColimit s)
{W : C}
(k : Y ⟶ W)
(h : CategoryStruct.comp f k = CategoryStruct.comp g k)
:
If s is a colimit cofork over f and g, then a morphism k : Y ⟶ W satisfying
f ≫ k = g ≫ k induces a morphism l : s.pt ⟶ W such that cofork.π s ≫ l = k.
Equations
@[simp]
theorem
CategoryTheory.Limits.Cofork.IsColimit.π_desc'
{C : Type u}
[Category.{v, u} C]
{X Y : C}
{f g : X ⟶ Y}
{s : Cofork f g}
(hs : IsColimit s)
{W : C}
(k : Y ⟶ W)
(h : CategoryStruct.comp f k = CategoryStruct.comp g k)
:
@[simp]
theorem
CategoryTheory.Limits.Cofork.IsColimit.π_desc'_assoc
{C : Type u}
[Category.{v, u} C]
{X Y : C}
{f g : X ⟶ Y}
{s : Cofork f g}
(hs : IsColimit s)
{W : C}
(k : Y ⟶ W)
(h : CategoryStruct.comp f k = CategoryStruct.comp g k)
{Z : C}
(h✝ : W ⟶ Z)
:
def
CategoryTheory.Limits.Cofork.IsColimit.desc'
{C : Type u}
[Category.{v, u} C]
{X Y : C}
{f g : X ⟶ Y}
{s : Cofork f g}
(hs : IsColimit s)
{W : C}
(k : Y ⟶ W)
(h : CategoryStruct.comp f k = CategoryStruct.comp g k)
:
If s is a colimit cofork over f and g, then a morphism k : Y ⟶ W satisfying
f ≫ k = g ≫ k induces a morphism l : s.pt ⟶ W such that cofork.π s ≫ l = k.
Equations
theorem
CategoryTheory.Limits.Fork.IsLimit.existsUnique
{C : Type u}
[Category.{v, u} C]
{X Y : C}
{f g : X ⟶ Y}
{s : Fork f g}
(hs : IsLimit s)
{W : C}
(k : W ⟶ X)
(h : CategoryStruct.comp k f = CategoryStruct.comp k g)
:
theorem
CategoryTheory.Limits.Cofork.IsColimit.existsUnique
{C : Type u}
[Category.{v, u} C]
{X Y : C}
{f g : X ⟶ Y}
{s : Cofork f g}
(hs : IsColimit s)
{W : C}
(k : Y ⟶ W)
(h : CategoryStruct.comp f k = CategoryStruct.comp g k)
:
def
CategoryTheory.Limits.Fork.IsLimit.mk
{C : Type u}
[Category.{v, u} C]
{X Y : C}
{f g : X ⟶ Y}
(t : Fork f g)
(lift : (s : Fork f g) → s.pt ⟶ t.pt)
(fac : ∀ (s : Fork f g), CategoryStruct.comp (lift s) t.ι = s.ι)
(uniq : ∀ (s : Fork f g) (m : s.pt ⟶ t.pt), CategoryStruct.comp m t.ι = s.ι → m = lift s)
:
IsLimit t
This is a slightly more convenient method to verify that a fork is a limit cone. It only asks for a proof of facts that carry any mathematical content
Equations
- CategoryTheory.Limits.Fork.IsLimit.mk t lift fac uniq = { lift := lift, fac := ⋯, uniq := ⋯ }
@[simp]
theorem
CategoryTheory.Limits.Fork.IsLimit.mk_lift
{C : Type u}
[Category.{v, u} C]
{X Y : C}
{f g : X ⟶ Y}
(t : Fork f g)
(lift : (s : Fork f g) → s.pt ⟶ t.pt)
(fac : ∀ (s : Fork f g), CategoryStruct.comp (lift s) t.ι = s.ι)
(uniq : ∀ (s : Fork f g) (m : s.pt ⟶ t.pt), CategoryStruct.comp m t.ι = s.ι → m = lift s)
(s : Fork f g)
:
def
CategoryTheory.Limits.Fork.IsLimit.mk'
{C : Type u}
[Category.{v, u} C]
{X Y : C}
{f g : X ⟶ Y}
(t : Fork f g)
(create :
(s : Fork f g) →
{ l : ((Functor.const WalkingParallelPair).obj s.pt).obj WalkingParallelPair.zero ⟶ ((Functor.const WalkingParallelPair).obj t.pt).obj WalkingParallelPair.zero // CategoryStruct.comp l t.ι = s.ι ∧ ∀
{m :
((Functor.const WalkingParallelPair).obj s.pt).obj WalkingParallelPair.zero ⟶ ((Functor.const WalkingParallelPair).obj t.pt).obj WalkingParallelPair.zero},
CategoryStruct.comp m t.ι = s.ι → m = l })
:
IsLimit t
This is another convenient method to verify that a fork is a limit cone. It
only asks for a proof of facts that carry any mathematical content, and allows access to the
same s for all parts.
Equations
- CategoryTheory.Limits.Fork.IsLimit.mk' t create = CategoryTheory.Limits.Fork.IsLimit.mk t (fun (s : CategoryTheory.Limits.Fork f g) => ↑(create s)) ⋯ ⋯
def
CategoryTheory.Limits.Cofork.IsColimit.mk
{C : Type u}
[Category.{v, u} C]
{X Y : C}
{f g : X ⟶ Y}
(t : Cofork f g)
(desc : (s : Cofork f g) → t.pt ⟶ s.pt)
(fac : ∀ (s : Cofork f g), CategoryStruct.comp t.π (desc s) = s.π)
(uniq : ∀ (s : Cofork f g) (m : t.pt ⟶ s.pt), CategoryStruct.comp t.π m = s.π → m = desc s)
:
This is a slightly more convenient method to verify that a cofork is a colimit cocone. It only asks for a proof of facts that carry any mathematical content
Equations
- CategoryTheory.Limits.Cofork.IsColimit.mk t desc fac uniq = { desc := desc, fac := ⋯, uniq := ⋯ }
def
CategoryTheory.Limits.Cofork.IsColimit.mk'
{C : Type u}
[Category.{v, u} C]
{X Y : C}
{f g : X ⟶ Y}
(t : Cofork f g)
(create :
(s : Cofork f g) →
{ l : t.pt ⟶ s.pt // CategoryStruct.comp t.π l = s.π ∧ ∀
{m :
((Functor.const WalkingParallelPair).obj t.pt).obj WalkingParallelPair.one ⟶ ((Functor.const WalkingParallelPair).obj s.pt).obj WalkingParallelPair.one},
CategoryStruct.comp t.π m = s.π → m = l })
:
This is another convenient method to verify that a fork is a limit cone. It
only asks for a proof of facts that carry any mathematical content, and allows access to the
same s for all parts.
Equations
- CategoryTheory.Limits.Cofork.IsColimit.mk' t create = CategoryTheory.Limits.Cofork.IsColimit.mk t (fun (s : CategoryTheory.Limits.Cofork f g) => ↑(create s)) ⋯ ⋯
noncomputable def
CategoryTheory.Limits.Fork.IsLimit.ofExistsUnique
{C : Type u}
[Category.{v, u} C]
{X Y : C}
{f g : X ⟶ Y}
{t : Fork f g}
(hs : ∀ (s : Fork f g), ∃! l : s.pt ⟶ t.pt, CategoryStruct.comp l t.ι = s.ι)
:
IsLimit t
Noncomputably make a limit cone from the existence of unique factorizations.
Equations
- One or more equations did not get rendered due to their size.
noncomputable def
CategoryTheory.Limits.Cofork.IsColimit.ofExistsUnique
{C : Type u}
[Category.{v, u} C]
{X Y : C}
{f g : X ⟶ Y}
{t : Cofork f g}
(hs : ∀ (s : Cofork f g), ∃! d : t.pt ⟶ s.pt, CategoryStruct.comp t.π d = s.π)
:
Noncomputably make a colimit cocone from the existence of unique factorizations.
Equations
- One or more equations did not get rendered due to their size.
def
CategoryTheory.Limits.Fork.IsLimit.homIso
{C : Type u}
[Category.{v, u} C]
{X Y : C}
{f g : X ⟶ Y}
{t : Fork f g}
(ht : IsLimit t)
(Z : C)
:
Given a limit cone for the pair f g : X ⟶ Y, for any Z, morphisms from Z to its point are in
bijection with morphisms h : Z ⟶ X such that h ≫ f = h ≫ g.
Further, this bijection is natural in Z: see Fork.IsLimit.homIso_natural.
This is a special case of IsLimit.homIso', often useful to construct adjunctions.
Equations
- One or more equations did not get rendered due to their size.
@[simp]
theorem
CategoryTheory.Limits.Fork.IsLimit.homIso_symm_apply
{C : Type u}
[Category.{v, u} C]
{X Y : C}
{f g : X ⟶ Y}
{t : Fork f g}
(ht : IsLimit t)
(Z : C)
(h : { h : Z ⟶ X // CategoryStruct.comp h f = CategoryStruct.comp h g })
:
@[simp]
theorem
CategoryTheory.Limits.Fork.IsLimit.homIso_apply_coe
{C : Type u}
[Category.{v, u} C]
{X Y : C}
{f g : X ⟶ Y}
{t : Fork f g}
(ht : IsLimit t)
(Z : C)
(k : Z ⟶ t.pt)
:
theorem
CategoryTheory.Limits.Fork.IsLimit.homIso_natural
{C : Type u}
[Category.{v, u} C]
{X Y : C}
{f g : X ⟶ Y}
{t : Fork f g}
(ht : IsLimit t)
{Z Z' : C}
(q : Z' ⟶ Z)
(k : Z ⟶ t.pt)
:
The bijection of Fork.IsLimit.homIso is natural in Z.
def
CategoryTheory.Limits.Cofork.IsColimit.homIso
{C : Type u}
[Category.{v, u} C]
{X Y : C}
{f g : X ⟶ Y}
{t : Cofork f g}
(ht : IsColimit t)
(Z : C)
:
Given a colimit cocone for the pair f g : X ⟶ Y, for any Z, morphisms from the cocone point
to Z are in bijection with morphisms h : Y ⟶ Z such that f ≫ h = g ≫ h.
Further, this bijection is natural in Z: see Cofork.IsColimit.homIso_natural.
This is a special case of IsColimit.homIso', often useful to construct adjunctions.
Equations
- One or more equations did not get rendered due to their size.
@[simp]
theorem
CategoryTheory.Limits.Cofork.IsColimit.homIso_apply_coe
{C : Type u}
[Category.{v, u} C]
{X Y : C}
{f g : X ⟶ Y}
{t : Cofork f g}
(ht : IsColimit t)
(Z : C)
(k : t.pt ⟶ Z)
:
@[simp]
theorem
CategoryTheory.Limits.Cofork.IsColimit.homIso_symm_apply
{C : Type u}
[Category.{v, u} C]
{X Y : C}
{f g : X ⟶ Y}
{t : Cofork f g}
(ht : IsColimit t)
(Z : C)
(h : { h : Y ⟶ Z // CategoryStruct.comp f h = CategoryStruct.comp g h })
:
theorem
CategoryTheory.Limits.Cofork.IsColimit.homIso_natural
{C : Type u}
[Category.{v, u} C]
{X Y : C}
{f g : X ⟶ Y}
{t : Cofork f g}
{Z Z' : C}
(q : Z ⟶ Z')
(ht : IsColimit t)
(k : t.pt ⟶ Z)
:
The bijection of Cofork.IsColimit.homIso is natural in Z.
def
CategoryTheory.Limits.Cone.ofFork
{C : Type u}
[Category.{v, u} C]
{F : Functor WalkingParallelPair C}
(t : Fork (F.map WalkingParallelPairHom.left) (F.map WalkingParallelPairHom.right))
:
Cone F
This is a helper construction that can be useful when verifying that a category has all
equalizers. Given F : WalkingParallelPair ⥤ C, which is really the same as
parallelPair (F.map left) (F.map right), and a fork on F.map left and F.map right,
we get a cone on F.
If you're thinking about using this, have a look at hasEqualizers_of_hasLimit_parallelPair,
which you may find to be an easier way of achieving your goal.
Equations
- One or more equations did not get rendered due to their size.
def
CategoryTheory.Limits.Cocone.ofCofork
{C : Type u}
[Category.{v, u} C]
{F : Functor WalkingParallelPair C}
(t : Cofork (F.map WalkingParallelPairHom.left) (F.map WalkingParallelPairHom.right))
:
Cocone F
This is a helper construction that can be useful when verifying that a category has all
coequalizers. Given F : WalkingParallelPair ⥤ C, which is really the same as
parallelPair (F.map left) (F.map right), and a cofork on F.map left and F.map right,
we get a cocone on F.
If you're thinking about using this, have a look at
hasCoequalizers_of_hasColimit_parallelPair, which you may find to be an easier way of
achieving your goal.
Equations
- One or more equations did not get rendered due to their size.
@[simp]
theorem
CategoryTheory.Limits.Cone.ofFork_π
{C : Type u}
[Category.{v, u} C]
{F : Functor WalkingParallelPair C}
(t : Fork (F.map WalkingParallelPairHom.left) (F.map WalkingParallelPairHom.right))
(j : WalkingParallelPair)
:
@[simp]
theorem
CategoryTheory.Limits.Cocone.ofCofork_ι
{C : Type u}
[Category.{v, u} C]
{F : Functor WalkingParallelPair C}
(t : Cofork (F.map WalkingParallelPairHom.left) (F.map WalkingParallelPairHom.right))
(j : WalkingParallelPair)
:
def
CategoryTheory.Limits.Fork.ofCone
{C : Type u}
[Category.{v, u} C]
{F : Functor WalkingParallelPair C}
(t : Cone F)
:
Given F : WalkingParallelPair ⥤ C, which is really the same as
parallelPair (F.map left) (F.map right) and a cone on F, we get a fork on
F.map left and F.map right.
Equations
- One or more equations did not get rendered due to their size.
def
CategoryTheory.Limits.Cofork.ofCocone
{C : Type u}
[Category.{v, u} C]
{F : Functor WalkingParallelPair C}
(t : Cocone F)
:
Given F : WalkingParallelPair ⥤ C, which is really the same as
parallelPair (F.map left) (F.map right) and a cocone on F, we get a cofork on
F.map left and F.map right.
Equations
- One or more equations did not get rendered due to their size.
@[simp]
theorem
CategoryTheory.Limits.Fork.ofCone_π
{C : Type u}
[Category.{v, u} C]
{F : Functor WalkingParallelPair C}
(t : Cone F)
(j : WalkingParallelPair)
:
@[simp]
theorem
CategoryTheory.Limits.Cofork.ofCocone_ι
{C : Type u}
[Category.{v, u} C]
{F : Functor WalkingParallelPair C}
(t : Cocone F)
(j : WalkingParallelPair)
:
@[simp]
theorem
CategoryTheory.Limits.Fork.ι_postcompose
{C : Type u}
[Category.{v, u} C]
{X Y : C}
{f g f' g' : X ⟶ Y}
{α : parallelPair f g ⟶ parallelPair f' g'}
{c : Fork f g}
:
@[simp]
theorem
CategoryTheory.Limits.Cofork.π_precompose
{C : Type u}
[Category.{v, u} C]
{X Y : C}
{f g f' g' : X ⟶ Y}
{α : parallelPair f g ⟶ parallelPair f' g'}
{c : Cofork f' g'}
:
def
CategoryTheory.Limits.Fork.mkHom
{C : Type u}
[Category.{v, u} C]
{X Y : C}
{f g : X ⟶ Y}
{s t : Fork f g}
(k : s.pt ⟶ t.pt)
(w : CategoryStruct.comp k t.ι = s.ι)
:
Helper function for constructing morphisms between equalizer forks.
Equations
- CategoryTheory.Limits.Fork.mkHom k w = { hom := k, w := ⋯ }
def
CategoryTheory.Limits.Fork.ext
{C : Type u}
[Category.{v, u} C]
{X Y : C}
{f g : X ⟶ Y}
{s t : Fork f g}
(i : s.pt ≅ t.pt)
(w : CategoryStruct.comp i.hom t.ι = s.ι := by aesop_cat)
:
To construct an isomorphism between forks,
it suffices to give an isomorphism between the cone points
and check that it commutes with the ι morphisms.
Equations
- CategoryTheory.Limits.Fork.ext i w = { hom := CategoryTheory.Limits.Fork.mkHom i.hom w, inv := CategoryTheory.Limits.Fork.mkHom i.inv ⋯, hom_inv_id := ⋯, inv_hom_id := ⋯ }
def
CategoryTheory.Limits.ForkOfι.ext
{C : Type u}
[Category.{v, u} C]
{X Y : C}
{f g : X ⟶ Y}
{P : C}
{ι ι' : P ⟶ X}
(w : CategoryStruct.comp ι f = CategoryStruct.comp ι g)
(w' : CategoryStruct.comp ι' f = CategoryStruct.comp ι' g)
(h : ι = ι')
:
Two forks of the form ofι are isomorphic whenever their ι's are equal.
Equations
def
CategoryTheory.Limits.Fork.isoForkOfι
{C : Type u}
[Category.{v, u} C]
{X Y : C}
{f g : X ⟶ Y}
(c : Fork f g)
:
Every fork is isomorphic to one of the form Fork.of_ι _ _.
Equations
def
CategoryTheory.Limits.Fork.isLimitOfIsos
{C : Type u}
[Category.{v, u} C]
{X Y : C}
{f g : X ⟶ Y}
{X' Y' : C}
(c : Fork f g)
(hc : IsLimit c)
{f' g' : X' ⟶ Y'}
(c' : Fork f' g')
(e₀ : X ≅ X')
(e₁ : Y ≅ Y')
(e : c.pt ≅ c'.pt)
(comm₁ : CategoryStruct.comp e₀.hom f' = CategoryStruct.comp f e₁.hom := by aesop_cat)
(comm₂ : CategoryStruct.comp e₀.hom g' = CategoryStruct.comp g e₁.hom := by aesop_cat)
(comm₃ : CategoryStruct.comp e.hom c'.ι = CategoryStruct.comp c.ι e₀.hom := by aesop_cat)
:
IsLimit c'
Given two forks with isomorphic components in such a way that the natural diagrams commute, then if one is a limit, then the other one is as well.
Equations
- One or more equations did not get rendered due to their size.
def
CategoryTheory.Limits.Cofork.mkHom
{C : Type u}
[Category.{v, u} C]
{X Y : C}
{f g : X ⟶ Y}
{s t : Cofork f g}
(k : s.pt ⟶ t.pt)
(w : CategoryStruct.comp s.π k = t.π)
:
Helper function for constructing morphisms between coequalizer coforks.
Equations
- CategoryTheory.Limits.Cofork.mkHom k w = { hom := k, w := ⋯ }
@[simp]
theorem
CategoryTheory.Limits.Fork.hom_comp_ι
{C : Type u}
[Category.{v, u} C]
{X Y : C}
{f g : X ⟶ Y}
{s t : Fork f g}
(f✝ : s ⟶ t)
:
@[simp]
theorem
CategoryTheory.Limits.Fork.hom_comp_ι_assoc
{C : Type u}
[Category.{v, u} C]
{X Y : C}
{f g : X ⟶ Y}
{s t : Fork f g}
(f✝ : s ⟶ t)
{Z : C}
(h : (parallelPair f g).obj WalkingParallelPair.zero ⟶ Z)
:
@[simp]
theorem
CategoryTheory.Limits.Fork.π_comp_hom
{C : Type u}
[Category.{v, u} C]
{X Y : C}
{f g : X ⟶ Y}
{s t : Cofork f g}
(f✝ : s ⟶ t)
:
@[simp]
theorem
CategoryTheory.Limits.Fork.π_comp_hom_assoc
{C : Type u}
[Category.{v, u} C]
{X Y : C}
{f g : X ⟶ Y}
{s t : Cofork f g}
(f✝ : s ⟶ t)
{Z : C}
(h : t.pt ⟶ Z)
:
def
CategoryTheory.Limits.Cofork.ext
{C : Type u}
[Category.{v, u} C]
{X Y : C}
{f g : X ⟶ Y}
{s t : Cofork f g}
(i : s.pt ≅ t.pt)
(w : CategoryStruct.comp s.π i.hom = t.π := by aesop_cat)
:
To construct an isomorphism between coforks,
it suffices to give an isomorphism between the cocone points
and check that it commutes with the π morphisms.
Equations
- CategoryTheory.Limits.Cofork.ext i w = { hom := CategoryTheory.Limits.Cofork.mkHom i.hom w, inv := CategoryTheory.Limits.Cofork.mkHom i.inv ⋯, hom_inv_id := ⋯, inv_hom_id := ⋯ }
def
CategoryTheory.Limits.Cofork.isoCoforkOfπ
{C : Type u}
[Category.{v, u} C]
{X Y : C}
{f g : X ⟶ Y}
(c : Cofork f g)
:
Every cofork is isomorphic to one of the form Cofork.ofπ _ _.
Equations
@[reducible, inline]
abbrev
CategoryTheory.Limits.HasEqualizer
{C : Type u}
[Category.{v, u} C]
{X Y : C}
(f g : X ⟶ Y)
:
HasEqualizer f g represents a particular choice of limiting cone
for the parallel pair of morphisms f and g.
@[reducible, inline]
noncomputable abbrev
CategoryTheory.Limits.equalizer
{C : Type u}
[Category.{v, u} C]
{X Y : C}
(f g : X ⟶ Y)
[HasEqualizer f g]
:
C
If an equalizer of f and g exists, we can access an arbitrary choice of such by
saying equalizer f g.
@[reducible, inline]
noncomputable abbrev
CategoryTheory.Limits.equalizer.ι
{C : Type u}
[Category.{v, u} C]
{X Y : C}
(f g : X ⟶ Y)
[HasEqualizer f g]
:
If an equalizer of f and g exists, we can access the inclusion
equalizer f g ⟶ X by saying equalizer.ι f g.
Equations
@[reducible, inline]
noncomputable abbrev
CategoryTheory.Limits.equalizer.fork
{C : Type u}
[Category.{v, u} C]
{X Y : C}
(f g : X ⟶ Y)
[HasEqualizer f g]
:
Fork f g
An equalizer cone for a parallel pair f and g
@[simp]
theorem
CategoryTheory.Limits.equalizer.fork_ι
{C : Type u}
[Category.{v, u} C]
{X Y : C}
(f g : X ⟶ Y)
[HasEqualizer f g]
:
@[simp]
theorem
CategoryTheory.Limits.equalizer.fork_π_app_zero
{C : Type u}
[Category.{v, u} C]
{X Y : C}
(f g : X ⟶ Y)
[HasEqualizer f g]
:
theorem
CategoryTheory.Limits.equalizer.condition
{C : Type u}
[Category.{v, u} C]
{X Y : C}
(f g : X ⟶ Y)
[HasEqualizer f g]
:
theorem
CategoryTheory.Limits.equalizer.condition_assoc
{C : Type u}
[Category.{v, u} C]
{X Y : C}
(f g : X ⟶ Y)
[HasEqualizer f g]
{Z : C}
(h : Y ⟶ Z)
:
CategoryStruct.comp (ι f g) (CategoryStruct.comp f h) = CategoryStruct.comp (ι f g) (CategoryStruct.comp g h)
noncomputable def
CategoryTheory.Limits.equalizerIsEqualizer
{C : Type u}
[Category.{v, u} C]
{X Y : C}
(f g : X ⟶ Y)
[HasEqualizer f g]
:
IsLimit (Fork.ofι (equalizer.ι f g) ⋯)
The equalizer built from equalizer.ι f g is limiting.
Equations
- One or more equations did not get rendered due to their size.
@[reducible, inline]
noncomputable abbrev
CategoryTheory.Limits.equalizer.lift
{C : Type u}
[Category.{v, u} C]
{X Y : C}
{f g : X ⟶ Y}
[HasEqualizer f g]
{W : C}
(k : W ⟶ X)
(h : CategoryStruct.comp k f = CategoryStruct.comp k g)
:
A morphism k : W ⟶ X satisfying k ≫ f = k ≫ g factors through the equalizer of f and g
via equalizer.lift : W ⟶ equalizer f g.
theorem
CategoryTheory.Limits.equalizer.lift_ι
{C : Type u}
[Category.{v, u} C]
{X Y : C}
{f g : X ⟶ Y}
[HasEqualizer f g]
{W : C}
(k : W ⟶ X)
(h : CategoryStruct.comp k f = CategoryStruct.comp k g)
:
theorem
CategoryTheory.Limits.equalizer.lift_ι_assoc
{C : Type u}
[Category.{v, u} C]
{X Y : C}
{f g : X ⟶ Y}
[HasEqualizer f g]
{W : C}
(k : W ⟶ X)
(h : CategoryStruct.comp k f = CategoryStruct.comp k g)
{Z : C}
(h✝ : X ⟶ Z)
:
noncomputable def
CategoryTheory.Limits.equalizer.lift'
{C : Type u}
[Category.{v, u} C]
{X Y : C}
{f g : X ⟶ Y}
[HasEqualizer f g]
{W : C}
(k : W ⟶ X)
(h : CategoryStruct.comp k f = CategoryStruct.comp k g)
:
A morphism k : W ⟶ X satisfying k ≫ f = k ≫ g induces a morphism l : W ⟶ equalizer f g
satisfying l ≫ equalizer.ι f g = k.
Equations
theorem
CategoryTheory.Limits.equalizer.hom_ext
{C : Type u}
[Category.{v, u} C]
{X Y : C}
{f g : X ⟶ Y}
[HasEqualizer f g]
{W : C}
{k l : W ⟶ equalizer f g}
(h : CategoryStruct.comp k (ι f g) = CategoryStruct.comp l (ι f g))
:
Two maps into an equalizer are equal if they are equal when composed with the equalizer map.
theorem
CategoryTheory.Limits.equalizer.existsUnique
{C : Type u}
[Category.{v, u} C]
{X Y : C}
{f g : X ⟶ Y}
[HasEqualizer f g]
{W : C}
(k : W ⟶ X)
(h : CategoryStruct.comp k f = CategoryStruct.comp k g)
:
instance
CategoryTheory.Limits.equalizer.ι_mono
{C : Type u}
[Category.{v, u} C]
{X Y : C}
{f g : X ⟶ Y}
[HasEqualizer f g]
:
An equalizer morphism is a monomorphism
theorem
CategoryTheory.Limits.mono_of_isLimit_fork
{C : Type u}
[Category.{v, u} C]
{X Y : C}
{f g : X ⟶ Y}
{c : Fork f g}
(i : IsLimit c)
:
The equalizer morphism in any limit cone is a monomorphism.
def
CategoryTheory.Limits.idFork
{C : Type u}
[Category.{v, u} C]
{X Y : C}
{f g : X ⟶ Y}
(h : f = g)
:
Fork f g
The identity determines a cone on the equalizer diagram of f and g if f = g.
def
CategoryTheory.Limits.isLimitIdFork
{C : Type u}
[Category.{v, u} C]
{X Y : C}
{f g : X ⟶ Y}
(h : f = g)
:
The identity on X is an equalizer of (f, g), if f = g.
Equations
- CategoryTheory.Limits.isLimitIdFork h = CategoryTheory.Limits.Fork.IsLimit.mk (CategoryTheory.Limits.idFork h) (fun (s : CategoryTheory.Limits.Fork f g) => s.ι) ⋯ ⋯
theorem
CategoryTheory.Limits.isIso_limit_cone_parallelPair_of_eq
{C : Type u}
[Category.{v, u} C]
{X Y : C}
{f g : X ⟶ Y}
(h₀ : f = g)
{c : Fork f g}
(h : IsLimit c)
:
Every equalizer of (f, g), where f = g, is an isomorphism.
theorem
CategoryTheory.Limits.equalizer.ι_of_eq
{C : Type u}
[Category.{v, u} C]
{X Y : C}
{f g : X ⟶ Y}
[HasEqualizer f g]
(h : f = g)
:
The equalizer of (f, g), where f = g, is an isomorphism.
theorem
CategoryTheory.Limits.isIso_limit_cone_parallelPair_of_self
{C : Type u}
[Category.{v, u} C]
{X Y : C}
{f : X ⟶ Y}
{c : Fork f f}
(h : IsLimit c)
:
Every equalizer of (f, f) is an isomorphism.
theorem
CategoryTheory.Limits.eq_of_epi_fork_ι
{C : Type u}
[Category.{v, u} C]
{X Y : C}
{f g : X ⟶ Y}
(t : Fork f g)
[Epi t.ι]
:
Two morphisms are equal if there is a fork whose inclusion is epi.
theorem
CategoryTheory.Limits.eq_of_epi_equalizer
{C : Type u}
[Category.{v, u} C]
{X Y : C}
{f g : X ⟶ Y}
[HasEqualizer f g]
[Epi (equalizer.ι f g)]
:
If the equalizer of two morphisms is an epimorphism, then the two morphisms are equal.
instance
CategoryTheory.Limits.hasEqualizer_of_self
{C : Type u}
[Category.{v, u} C]
{X Y : C}
(f : X ⟶ Y)
:
HasEqualizer f f
instance
CategoryTheory.Limits.equalizer.ι_of_self
{C : Type u}
[Category.{v, u} C]
{X Y : C}
(f : X ⟶ Y)
:
The equalizer inclusion for (f, f) is an isomorphism.
noncomputable def
CategoryTheory.Limits.equalizer.isoSourceOfSelf
{C : Type u}
[Category.{v, u} C]
{X Y : C}
(f : X ⟶ Y)
:
The equalizer of a morphism with itself is isomorphic to the source.
@[simp]
theorem
CategoryTheory.Limits.equalizer.isoSourceOfSelf_hom
{C : Type u}
[Category.{v, u} C]
{X Y : C}
(f : X ⟶ Y)
:
@[simp]
theorem
CategoryTheory.Limits.equalizer.isoSourceOfSelf_inv
{C : Type u}
[Category.{v, u} C]
{X Y : C}
(f : X ⟶ Y)
:
@[reducible, inline]
abbrev
CategoryTheory.Limits.HasCoequalizer
{C : Type u}
[Category.{v, u} C]
{X Y : C}
(f g : X ⟶ Y)
:
HasCoequalizer f g represents a particular choice of colimiting cocone
for the parallel pair of morphisms f and g.
@[reducible, inline]
noncomputable abbrev
CategoryTheory.Limits.coequalizer
{C : Type u}
[Category.{v, u} C]
{X Y : C}
(f g : X ⟶ Y)
[HasCoequalizer f g]
:
C
If a coequalizer of f and g exists, we can access an arbitrary choice of such by
saying coequalizer f g.
@[reducible, inline]
noncomputable abbrev
CategoryTheory.Limits.coequalizer.π
{C : Type u}
[Category.{v, u} C]
{X Y : C}
(f g : X ⟶ Y)
[HasCoequalizer f g]
:
If a coequalizer of f and g exists, we can access the corresponding projection by
saying coequalizer.π f g.
Equations
@[reducible, inline]
noncomputable abbrev
CategoryTheory.Limits.coequalizer.cofork
{C : Type u}
[Category.{v, u} C]
{X Y : C}
(f g : X ⟶ Y)
[HasCoequalizer f g]
:
Cofork f g
An arbitrary choice of coequalizer cocone for a parallel pair f and g.
@[simp]
theorem
CategoryTheory.Limits.coequalizer.cofork_π
{C : Type u}
[Category.{v, u} C]
{X Y : C}
(f g : X ⟶ Y)
[HasCoequalizer f g]
:
theorem
CategoryTheory.Limits.coequalizer.cofork_ι_app_one
{C : Type u}
[Category.{v, u} C]
{X Y : C}
(f g : X ⟶ Y)
[HasCoequalizer f g]
:
theorem
CategoryTheory.Limits.coequalizer.condition
{C : Type u}
[Category.{v, u} C]
{X Y : C}
(f g : X ⟶ Y)
[HasCoequalizer f g]
:
theorem
CategoryTheory.Limits.coequalizer.condition_assoc
{C : Type u}
[Category.{v, u} C]
{X Y : C}
(f g : X ⟶ Y)
[HasCoequalizer f g]
{Z : C}
(h : coequalizer f g ⟶ Z)
:
CategoryStruct.comp f (CategoryStruct.comp (π f g) h) = CategoryStruct.comp g (CategoryStruct.comp (π f g) h)
noncomputable def
CategoryTheory.Limits.coequalizerIsCoequalizer
{C : Type u}
[Category.{v, u} C]
{X Y : C}
(f g : X ⟶ Y)
[HasCoequalizer f g]
:
IsColimit (Cofork.ofπ (coequalizer.π f g) ⋯)
The cofork built from coequalizer.π f g is colimiting.
Equations
- One or more equations did not get rendered due to their size.
@[reducible, inline]
noncomputable abbrev
CategoryTheory.Limits.coequalizer.desc
{C : Type u}
[Category.{v, u} C]
{X Y : C}
{f g : X ⟶ Y}
[HasCoequalizer f g]
{W : C}
(k : Y ⟶ W)
(h : CategoryStruct.comp f k = CategoryStruct.comp g k)
:
Any morphism k : Y ⟶ W satisfying f ≫ k = g ≫ k factors through the coequalizer of f
and g via coequalizer.desc : coequalizer f g ⟶ W.
theorem
CategoryTheory.Limits.coequalizer.π_desc
{C : Type u}
[Category.{v, u} C]
{X Y : C}
{f g : X ⟶ Y}
[HasCoequalizer f g]
{W : C}
(k : Y ⟶ W)
(h : CategoryStruct.comp f k = CategoryStruct.comp g k)
:
theorem
CategoryTheory.Limits.coequalizer.π_desc_assoc
{C : Type u}
[Category.{v, u} C]
{X Y : C}
{f g : X ⟶ Y}
[HasCoequalizer f g]
{W : C}
(k : Y ⟶ W)
(h : CategoryStruct.comp f k = CategoryStruct.comp g k)
{Z : C}
(h✝ : W ⟶ Z)
:
theorem
CategoryTheory.Limits.coequalizer.π_colimMap_desc
{C : Type u}
[Category.{v, u} C]
{X Y : C}
{f g : X ⟶ Y}
[HasCoequalizer f g]
{X' Y' Z : C}
(f' g' : X' ⟶ Y')
[HasCoequalizer f' g']
(p : X ⟶ X')
(q : Y ⟶ Y')
(wf : CategoryStruct.comp f q = CategoryStruct.comp p f')
(wg : CategoryStruct.comp g q = CategoryStruct.comp p g')
(h : Y' ⟶ Z)
(wh : CategoryStruct.comp f' h = CategoryStruct.comp g' h)
:
CategoryStruct.comp (π f g) (CategoryStruct.comp (colimMap (parallelPairHom f g f' g' p q wf wg)) (desc h wh)) = CategoryStruct.comp q h
noncomputable def
CategoryTheory.Limits.coequalizer.desc'
{C : Type u}
[Category.{v, u} C]
{X Y : C}
{f g : X ⟶ Y}
[HasCoequalizer f g]
{W : C}
(k : Y ⟶ W)
(h : CategoryStruct.comp f k = CategoryStruct.comp g k)
:
Any morphism k : Y ⟶ W satisfying f ≫ k = g ≫ k induces a morphism
l : coequalizer f g ⟶ W satisfying coequalizer.π ≫ g = l.
Equations
theorem
CategoryTheory.Limits.coequalizer.hom_ext
{C : Type u}
[Category.{v, u} C]
{X Y : C}
{f g : X ⟶ Y}
[HasCoequalizer f g]
{W : C}
{k l : coequalizer f g ⟶ W}
(h : CategoryStruct.comp (π f g) k = CategoryStruct.comp (π f g) l)
:
Two maps from a coequalizer are equal if they are equal when composed with the coequalizer map
theorem
CategoryTheory.Limits.coequalizer.existsUnique
{C : Type u}
[Category.{v, u} C]
{X Y : C}
{f g : X ⟶ Y}
[HasCoequalizer f g]
{W : C}
(k : Y ⟶ W)
(h : CategoryStruct.comp f k = CategoryStruct.comp g k)
:
instance
CategoryTheory.Limits.coequalizer.π_epi
{C : Type u}
[Category.{v, u} C]
{X Y : C}
{f g : X ⟶ Y}
[HasCoequalizer f g]
:
A coequalizer morphism is an epimorphism
theorem
CategoryTheory.Limits.epi_of_isColimit_cofork
{C : Type u}
[Category.{v, u} C]
{X Y : C}
{f g : X ⟶ Y}
{c : Cofork f g}
(i : IsColimit c)
:
The coequalizer morphism in any colimit cocone is an epimorphism.
def
CategoryTheory.Limits.idCofork
{C : Type u}
[Category.{v, u} C]
{X Y : C}
{f g : X ⟶ Y}
(h : f = g)
:
Cofork f g
The identity determines a cocone on the coequalizer diagram of f and g, if f = g.
def
CategoryTheory.Limits.isColimitIdCofork
{C : Type u}
[Category.{v, u} C]
{X Y : C}
{f g : X ⟶ Y}
(h : f = g)
:
The identity on Y is a coequalizer of (f, g), where f = g.
Equations
- CategoryTheory.Limits.isColimitIdCofork h = CategoryTheory.Limits.Cofork.IsColimit.mk (CategoryTheory.Limits.idCofork h) (fun (s : CategoryTheory.Limits.Cofork f g) => s.π) ⋯ ⋯
theorem
CategoryTheory.Limits.isIso_colimit_cocone_parallelPair_of_eq
{C : Type u}
[Category.{v, u} C]
{X Y : C}
{f g : X ⟶ Y}
(h₀ : f = g)
{c : Cofork f g}
(h : IsColimit c)
:
Every coequalizer of (f, g), where f = g, is an isomorphism.
theorem
CategoryTheory.Limits.coequalizer.π_of_eq
{C : Type u}
[Category.{v, u} C]
{X Y : C}
{f g : X ⟶ Y}
[HasCoequalizer f g]
(h : f = g)
:
The coequalizer of (f, g), where f = g, is an isomorphism.
theorem
CategoryTheory.Limits.isIso_colimit_cocone_parallelPair_of_self
{C : Type u}
[Category.{v, u} C]
{X Y : C}
{f : X ⟶ Y}
{c : Cofork f f}
(h : IsColimit c)
:
Every coequalizer of (f, f) is an isomorphism.
theorem
CategoryTheory.Limits.eq_of_mono_cofork_π
{C : Type u}
[Category.{v, u} C]
{X Y : C}
{f g : X ⟶ Y}
(t : Cofork f g)
[Mono t.π]
:
Two morphisms are equal if there is a cofork whose projection is mono.
theorem
CategoryTheory.Limits.eq_of_mono_coequalizer
{C : Type u}
[Category.{v, u} C]
{X Y : C}
{f g : X ⟶ Y}
[HasCoequalizer f g]
[Mono (coequalizer.π f g)]
:
If the coequalizer of two morphisms is a monomorphism, then the two morphisms are equal.
instance
CategoryTheory.Limits.hasCoequalizer_of_self
{C : Type u}
[Category.{v, u} C]
{X Y : C}
(f : X ⟶ Y)
:
HasCoequalizer f f
instance
CategoryTheory.Limits.coequalizer.π_of_self
{C : Type u}
[Category.{v, u} C]
{X Y : C}
(f : X ⟶ Y)
:
The coequalizer projection for (f, f) is an isomorphism.
noncomputable def
CategoryTheory.Limits.coequalizer.isoTargetOfSelf
{C : Type u}
[Category.{v, u} C]
{X Y : C}
(f : X ⟶ Y)
:
The coequalizer of a morphism with itself is isomorphic to the target.
@[simp]
theorem
CategoryTheory.Limits.coequalizer.isoTargetOfSelf_hom
{C : Type u}
[Category.{v, u} C]
{X Y : C}
(f : X ⟶ Y)
:
@[simp]
theorem
CategoryTheory.Limits.coequalizer.isoTargetOfSelf_inv
{C : Type u}
[Category.{v, u} C]
{X Y : C}
(f : X ⟶ Y)
:
noncomputable def
CategoryTheory.Limits.equalizerComparison
{C : Type u}
[Category.{v, u} C]
{X Y : C}
(f g : X ⟶ Y)
{D : Type u₂}
[Category.{v₂, u₂} D]
(G : Functor C D)
[HasEqualizer f g]
[HasEqualizer (G.map f) (G.map g)]
:
The comparison morphism for the equalizer of f,g.
This is an isomorphism iff G preserves the equalizer of f,g; see
CategoryTheory/Limits/Preserves/Shapes/Equalizers.lean
Equations
@[simp]
theorem
CategoryTheory.Limits.equalizerComparison_comp_π
{C : Type u}
[Category.{v, u} C]
{X Y : C}
(f g : X ⟶ Y)
{D : Type u₂}
[Category.{v₂, u₂} D]
(G : Functor C D)
[HasEqualizer f g]
[HasEqualizer (G.map f) (G.map g)]
:
CategoryStruct.comp (equalizerComparison f g G) (equalizer.ι (G.map f) (G.map g)) = G.map (equalizer.ι f g)
@[simp]
theorem
CategoryTheory.Limits.equalizerComparison_comp_π_assoc
{C : Type u}
[Category.{v, u} C]
{X Y : C}
(f g : X ⟶ Y)
{D : Type u₂}
[Category.{v₂, u₂} D]
(G : Functor C D)
[HasEqualizer f g]
[HasEqualizer (G.map f) (G.map g)]
{Z : D}
(h : G.obj X ⟶ Z)
:
CategoryStruct.comp (equalizerComparison f g G) (CategoryStruct.comp (equalizer.ι (G.map f) (G.map g)) h) = CategoryStruct.comp (G.map (equalizer.ι f g)) h
@[simp]
theorem
CategoryTheory.Limits.map_lift_equalizerComparison
{C : Type u}
[Category.{v, u} C]
{X Y : C}
(f g : X ⟶ Y)
{D : Type u₂}
[Category.{v₂, u₂} D]
(G : Functor C D)
[HasEqualizer f g]
[HasEqualizer (G.map f) (G.map g)]
{Z : C}
{h : Z ⟶ X}
(w : CategoryStruct.comp h f = CategoryStruct.comp h g)
:
CategoryStruct.comp (G.map (equalizer.lift h w)) (equalizerComparison f g G) = equalizer.lift (G.map h) ⋯
@[simp]
theorem
CategoryTheory.Limits.map_lift_equalizerComparison_assoc
{C : Type u}
[Category.{v, u} C]
{X Y : C}
(f g : X ⟶ Y)
{D : Type u₂}
[Category.{v₂, u₂} D]
(G : Functor C D)
[HasEqualizer f g]
[HasEqualizer (G.map f) (G.map g)]
{Z : C}
{h : Z ⟶ X}
(w : CategoryStruct.comp h f = CategoryStruct.comp h g)
{Z✝ : D}
(h✝ : equalizer (G.map f) (G.map g) ⟶ Z✝)
:
CategoryStruct.comp (G.map (equalizer.lift h w)) (CategoryStruct.comp (equalizerComparison f g G) h✝) = CategoryStruct.comp (equalizer.lift (G.map h) ⋯) h✝
noncomputable def
CategoryTheory.Limits.coequalizerComparison
{C : Type u}
[Category.{v, u} C]
{X Y : C}
(f g : X ⟶ Y)
{D : Type u₂}
[Category.{v₂, u₂} D]
(G : Functor C D)
[HasCoequalizer f g]
[HasCoequalizer (G.map f) (G.map g)]
:
The comparison morphism for the coequalizer of f,g.
Equations
@[simp]
theorem
CategoryTheory.Limits.ι_comp_coequalizerComparison
{C : Type u}
[Category.{v, u} C]
{X Y : C}
(f g : X ⟶ Y)
{D : Type u₂}
[Category.{v₂, u₂} D]
(G : Functor C D)
[HasCoequalizer f g]
[HasCoequalizer (G.map f) (G.map g)]
:
CategoryStruct.comp (coequalizer.π (G.map f) (G.map g)) (coequalizerComparison f g G) = G.map (coequalizer.π f g)
@[simp]
theorem
CategoryTheory.Limits.ι_comp_coequalizerComparison_assoc
{C : Type u}
[Category.{v, u} C]
{X Y : C}
(f g : X ⟶ Y)
{D : Type u₂}
[Category.{v₂, u₂} D]
(G : Functor C D)
[HasCoequalizer f g]
[HasCoequalizer (G.map f) (G.map g)]
{Z : D}
(h : G.obj (coequalizer f g) ⟶ Z)
:
CategoryStruct.comp (coequalizer.π (G.map f) (G.map g)) (CategoryStruct.comp (coequalizerComparison f g G) h) = CategoryStruct.comp (G.map (coequalizer.π f g)) h
@[simp]
theorem
CategoryTheory.Limits.coequalizerComparison_map_desc
{C : Type u}
[Category.{v, u} C]
{X Y : C}
(f g : X ⟶ Y)
{D : Type u₂}
[Category.{v₂, u₂} D]
(G : Functor C D)
[HasCoequalizer f g]
[HasCoequalizer (G.map f) (G.map g)]
{Z : C}
{h : Y ⟶ Z}
(w : CategoryStruct.comp f h = CategoryStruct.comp g h)
:
CategoryStruct.comp (coequalizerComparison f g G) (G.map (coequalizer.desc h w)) = coequalizer.desc (G.map h) ⋯
@[simp]
theorem
CategoryTheory.Limits.coequalizerComparison_map_desc_assoc
{C : Type u}
[Category.{v, u} C]
{X Y : C}
(f g : X ⟶ Y)
{D : Type u₂}
[Category.{v₂, u₂} D]
(G : Functor C D)
[HasCoequalizer f g]
[HasCoequalizer (G.map f) (G.map g)]
{Z : C}
{h : Y ⟶ Z}
(w : CategoryStruct.comp f h = CategoryStruct.comp g h)
{Z✝ : D}
(h✝ : G.obj Z ⟶ Z✝)
:
CategoryStruct.comp (coequalizerComparison f g G) (CategoryStruct.comp (G.map (coequalizer.desc h w)) h✝) = CategoryStruct.comp (coequalizer.desc (G.map h) ⋯) h✝
@[reducible, inline]
HasEqualizers represents a choice of equalizer for every pair of morphisms
@[reducible, inline]
HasCoequalizers represents a choice of coequalizer for every pair of morphisms
theorem
CategoryTheory.Limits.hasEqualizers_of_hasLimit_parallelPair
(C : Type u)
[Category.{v, u} C]
[∀ {X Y : C} {f g : X ⟶ Y}, HasLimit (parallelPair f g)]
:
If C has all limits of diagrams parallelPair f g, then it has all equalizers
theorem
CategoryTheory.Limits.hasCoequalizers_of_hasColimit_parallelPair
(C : Type u)
[Category.{v, u} C]
[∀ {X Y : C} {f g : X ⟶ Y}, HasColimit (parallelPair f g)]
:
If C has all colimits of diagrams parallelPair f g, then it has all coequalizers
noncomputable def
CategoryTheory.Limits.coneOfIsSplitMono
{C : Type u}
[Category.{v, u} C]
{X Y : C}
(f : X ⟶ Y)
[IsSplitMono f]
:
Fork (CategoryStruct.id Y) (CategoryStruct.comp (retraction f) f)
A split mono f equalizes (retraction f ≫ f) and (𝟙 Y).
Here we build the cone, and show in isSplitMonoEqualizes that it is a limit cone.
@[simp]
theorem
CategoryTheory.Limits.coneOfIsSplitMono_π_app
{C : Type u}
[Category.{v, u} C]
{X Y : C}
(f : X ⟶ Y)
[IsSplitMono f]
(X✝ : WalkingParallelPair)
:
(coneOfIsSplitMono f).π.app X✝ = WalkingParallelPair.rec (motive := fun (t : WalkingParallelPair) =>
X✝ = t → (X ⟶ (parallelPair (CategoryStruct.id Y) (CategoryStruct.comp (retraction f) f)).obj X✝))
(fun (h : X✝ = WalkingParallelPair.zero) => ⋯ ▸ f) (fun (h : X✝ = WalkingParallelPair.one) => ⋯ ▸ f) X✝ ⋯
@[simp]
theorem
CategoryTheory.Limits.coneOfIsSplitMono_pt
{C : Type u}
[Category.{v, u} C]
{X Y : C}
(f : X ⟶ Y)
[IsSplitMono f]
:
@[simp]
theorem
CategoryTheory.Limits.coneOfIsSplitMono_ι
{C : Type u}
[Category.{v, u} C]
{X Y : C}
(f : X ⟶ Y)
[IsSplitMono f]
:
noncomputable def
CategoryTheory.Limits.isSplitMonoEqualizes
{C : Type u}
[Category.{v, u} C]
{X Y : C}
(f : X ⟶ Y)
[IsSplitMono f]
:
A split mono f equalizes (retraction f ≫ f) and (𝟙 Y).
Equations
- One or more equations did not get rendered due to their size.
def
CategoryTheory.Limits.splitMonoOfEqualizer
(C : Type u)
[Category.{v, u} C]
{X Y : C}
{f : X ⟶ Y}
{r : Y ⟶ X}
(hr : CategoryStruct.comp f (CategoryStruct.comp r f) = f)
(h : IsLimit (Fork.ofι f ⋯))
:
We show that the converse to isSplitMonoEqualizes is true:
Whenever f equalizes (r ≫ f) and (𝟙 Y), then r is a retraction of f.
Equations
- CategoryTheory.Limits.splitMonoOfEqualizer C hr h = { retraction := r, id := ⋯ }
def
CategoryTheory.Limits.isEqualizerCompMono
{C : Type u}
[Category.{v, u} C]
{X Y : C}
{f g : X ⟶ Y}
{c : Fork f g}
(i : IsLimit c)
{Z : C}
(h : Y ⟶ Z)
[hm : Mono h]
:
The fork obtained by postcomposing an equalizer fork with a monomorphism is an equalizer.
Equations
- One or more equations did not get rendered due to their size.
instance
CategoryTheory.Limits.hasEqualizer_comp_mono
(C : Type u)
[Category.{v, u} C]
{X Y : C}
(f g : X ⟶ Y)
[HasEqualizer f g]
{Z : C}
(h : Y ⟶ Z)
[Mono h]
:
HasEqualizer (CategoryStruct.comp f h) (CategoryStruct.comp g h)
def
CategoryTheory.Limits.splitMonoOfIdempotentOfIsLimitFork
(C : Type u)
[Category.{v, u} C]
{X : C}
{f : X ⟶ X}
(hf : CategoryStruct.comp f f = f)
{c : Fork (CategoryStruct.id X) f}
(i : IsLimit c)
:
An equalizer of an idempotent morphism and the identity is split mono.
Equations
- CategoryTheory.Limits.splitMonoOfIdempotentOfIsLimitFork C hf i = { retraction := i.lift (CategoryTheory.Limits.Fork.ofι f ⋯), id := ⋯ }
@[simp]
theorem
CategoryTheory.Limits.splitMonoOfIdempotentOfIsLimitFork_retraction
(C : Type u)
[Category.{v, u} C]
{X : C}
{f : X ⟶ X}
(hf : CategoryStruct.comp f f = f)
{c : Fork (CategoryStruct.id X) f}
(i : IsLimit c)
:
noncomputable def
CategoryTheory.Limits.splitMonoOfIdempotentEqualizer
(C : Type u)
[Category.{v, u} C]
{X : C}
{f : X ⟶ X}
(hf : CategoryStruct.comp f f = f)
[HasEqualizer (CategoryStruct.id X) f]
:
SplitMono (equalizer.ι (CategoryStruct.id X) f)
The equalizer of an idempotent morphism and the identity is split mono.
Equations
- One or more equations did not get rendered due to their size.
noncomputable def
CategoryTheory.Limits.coconeOfIsSplitEpi
{C : Type u}
[Category.{v, u} C]
{X Y : C}
(f : X ⟶ Y)
[IsSplitEpi f]
:
Cofork (CategoryStruct.id X) (CategoryStruct.comp f (section_ f))
A split epi f coequalizes (f ≫ section_ f) and (𝟙 X).
Here we build the cocone, and show in isSplitEpiCoequalizes that it is a colimit cocone.
@[simp]
theorem
CategoryTheory.Limits.coconeOfIsSplitEpi_pt
{C : Type u}
[Category.{v, u} C]
{X Y : C}
(f : X ⟶ Y)
[IsSplitEpi f]
:
@[simp]
theorem
CategoryTheory.Limits.coconeOfIsSplitEpi_ι_app
{C : Type u}
[Category.{v, u} C]
{X Y : C}
(f : X ⟶ Y)
[IsSplitEpi f]
(X✝ : WalkingParallelPair)
:
@[simp]
theorem
CategoryTheory.Limits.coconeOfIsSplitEpi_π
{C : Type u}
[Category.{v, u} C]
{X Y : C}
(f : X ⟶ Y)
[IsSplitEpi f]
:
noncomputable def
CategoryTheory.Limits.isSplitEpiCoequalizes
{C : Type u}
[Category.{v, u} C]
{X Y : C}
(f : X ⟶ Y)
[IsSplitEpi f]
:
A split epi f coequalizes (f ≫ section_ f) and (𝟙 X).
Equations
- One or more equations did not get rendered due to their size.
def
CategoryTheory.Limits.splitEpiOfCoequalizer
(C : Type u)
[Category.{v, u} C]
{X Y : C}
{f : X ⟶ Y}
{s : Y ⟶ X}
(hs : CategoryStruct.comp f (CategoryStruct.comp s f) = f)
(h : IsColimit (Cofork.ofπ f ⋯))
:
SplitEpi f
We show that the converse to isSplitEpiEqualizes is true:
Whenever f coequalizes (f ≫ s) and (𝟙 X), then s is a section of f.
Equations
- CategoryTheory.Limits.splitEpiOfCoequalizer C hs h = { section_ := s, id := ⋯ }
def
CategoryTheory.Limits.isCoequalizerEpiComp
{C : Type u}
[Category.{v, u} C]
{X Y : C}
{f g : X ⟶ Y}
{c : Cofork f g}
(i : IsColimit c)
{W : C}
(h : W ⟶ X)
[hm : Epi h]
:
let_fun this := ⋯;
IsColimit (Cofork.ofπ c.π this)
The cofork obtained by precomposing a coequalizer cofork with an epimorphism is a coequalizer.
Equations
- One or more equations did not get rendered due to their size.
theorem
CategoryTheory.Limits.hasCoequalizer_epi_comp
{C : Type u}
[Category.{v, u} C]
{X Y : C}
{f g : X ⟶ Y}
[HasCoequalizer f g]
{W : C}
(h : W ⟶ X)
[Epi h]
:
HasCoequalizer (CategoryStruct.comp h f) (CategoryStruct.comp h g)
def
CategoryTheory.Limits.splitEpiOfIdempotentOfIsColimitCofork
(C : Type u)
[Category.{v, u} C]
{X : C}
{f : X ⟶ X}
(hf : CategoryStruct.comp f f = f)
{c : Cofork (CategoryStruct.id X) f}
(i : IsColimit c)
:
A coequalizer of an idempotent morphism and the identity is split epi.
Equations
- CategoryTheory.Limits.splitEpiOfIdempotentOfIsColimitCofork C hf i = { section_ := i.desc (CategoryTheory.Limits.Cofork.ofπ f ⋯), id := ⋯ }
@[simp]
theorem
CategoryTheory.Limits.splitEpiOfIdempotentOfIsColimitCofork_section_
(C : Type u)
[Category.{v, u} C]
{X : C}
{f : X ⟶ X}
(hf : CategoryStruct.comp f f = f)
{c : Cofork (CategoryStruct.id X) f}
(i : IsColimit c)
:
noncomputable def
CategoryTheory.Limits.splitEpiOfIdempotentCoequalizer
(C : Type u)
[Category.{v, u} C]
{X : C}
{f : X ⟶ X}
(hf : CategoryStruct.comp f f = f)
[HasCoequalizer (CategoryStruct.id X) f]
:
SplitEpi (coequalizer.π (CategoryStruct.id X) f)
The coequalizer of an idempotent morphism and the identity is split epi.
Equations
- One or more equations did not get rendered due to their size.