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.
Instances For
Equations
- CategoryTheory.Limits.instDecidableEqWalkingParallelPair x y = if h : x.toCtorIdx = y.toCtorIdx then isTrue ⋯ else isFalse ⋯
The type family of morphisms for the diagram indexing a (co)equalizer.
- left: CategoryTheory.Limits.WalkingParallelPairHom CategoryTheory.Limits.WalkingParallelPair.zero CategoryTheory.Limits.WalkingParallelPair.one
- right: CategoryTheory.Limits.WalkingParallelPairHom CategoryTheory.Limits.WalkingParallelPair.zero CategoryTheory.Limits.WalkingParallelPair.one
- id: (X : CategoryTheory.Limits.WalkingParallelPair) → CategoryTheory.Limits.WalkingParallelPairHom X X
Instances For
Equations
- CategoryTheory.Limits.instDecidableEqWalkingParallelPairHom = CategoryTheory.Limits.decEqWalkingParallelPairHom✝
Satisfying the inhabited linter
def
CategoryTheory.Limits.WalkingParallelPairHom.comp
{X : CategoryTheory.Limits.WalkingParallelPair}
{Y : CategoryTheory.Limits.WalkingParallelPair}
{Z : CategoryTheory.Limits.WalkingParallelPair}
:
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
Instances For
theorem
CategoryTheory.Limits.WalkingParallelPairHom.assoc
{X : CategoryTheory.Limits.WalkingParallelPair}
{Y : CategoryTheory.Limits.WalkingParallelPair}
{Z : CategoryTheory.Limits.WalkingParallelPair}
{W : CategoryTheory.Limits.WalkingParallelPair}
(f : CategoryTheory.Limits.WalkingParallelPairHom X Y)
(g : CategoryTheory.Limits.WalkingParallelPairHom Y Z)
(h : CategoryTheory.Limits.WalkingParallelPairHom Z W)
:
(f.comp g).comp h = f.comp (g.comp h)
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.
Instances For
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.
Instances For
def
CategoryTheory.Limits.parallelPair
{C : Type u}
[CategoryTheory.Category.{v, u} C]
{X : C}
{Y : C}
(f : X ⟶ Y)
(g : X ⟶ Y)
:
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.
Instances For
@[simp]
theorem
CategoryTheory.Limits.parallelPair_obj_zero
{C : Type u}
[CategoryTheory.Category.{v, u} C]
{X : C}
{Y : C}
(f : X ⟶ Y)
(g : X ⟶ Y)
:
@[simp]
theorem
CategoryTheory.Limits.parallelPair_obj_one
{C : Type u}
[CategoryTheory.Category.{v, u} C]
{X : C}
{Y : C}
(f : X ⟶ Y)
(g : X ⟶ Y)
:
@[simp]
theorem
CategoryTheory.Limits.parallelPair_map_left
{C : Type u}
[CategoryTheory.Category.{v, u} C]
{X : C}
{Y : C}
(f : X ⟶ Y)
(g : X ⟶ Y)
:
@[simp]
theorem
CategoryTheory.Limits.parallelPair_map_right
{C : Type u}
[CategoryTheory.Category.{v, u} C]
{X : C}
{Y : C}
(f : X ⟶ Y)
(g : X ⟶ Y)
:
@[simp]
theorem
CategoryTheory.Limits.parallelPair_functor_obj
{C : Type u}
[CategoryTheory.Category.{v, u} C]
{F : CategoryTheory.Functor CategoryTheory.Limits.WalkingParallelPair C}
(j : CategoryTheory.Limits.WalkingParallelPair)
:
(CategoryTheory.Limits.parallelPair (F.map CategoryTheory.Limits.WalkingParallelPairHom.left)
(F.map CategoryTheory.Limits.WalkingParallelPairHom.right)).obj
j = F.obj j
@[simp]
theorem
CategoryTheory.Limits.diagramIsoParallelPair_hom_app
{C : Type u}
[CategoryTheory.Category.{v, u} C]
(F : CategoryTheory.Functor CategoryTheory.Limits.WalkingParallelPair C)
(X : CategoryTheory.Limits.WalkingParallelPair)
:
(CategoryTheory.Limits.diagramIsoParallelPair F).hom.app X = CategoryTheory.eqToHom ⋯
@[simp]
theorem
CategoryTheory.Limits.diagramIsoParallelPair_inv_app
{C : Type u}
[CategoryTheory.Category.{v, u} C]
(F : CategoryTheory.Functor CategoryTheory.Limits.WalkingParallelPair C)
(X : CategoryTheory.Limits.WalkingParallelPair)
:
(CategoryTheory.Limits.diagramIsoParallelPair F).inv.app X = CategoryTheory.eqToHom ⋯
def
CategoryTheory.Limits.diagramIsoParallelPair
{C : Type u}
[CategoryTheory.Category.{v, u} C]
(F : CategoryTheory.Functor CategoryTheory.Limits.WalkingParallelPair C)
:
Every functor indexing a (co)equalizer is naturally isomorphic (actually, equal) to a
parallelPair
Equations
Instances For
def
CategoryTheory.Limits.parallelPairHom
{C : Type u}
[CategoryTheory.Category.{v, u} C]
{X : C}
{Y : C}
{X' : C}
{Y' : C}
(f : X ⟶ Y)
(g : X ⟶ Y)
(f' : X' ⟶ Y')
(g' : X' ⟶ Y')
(p : X ⟶ X')
(q : Y ⟶ Y')
(wf : CategoryTheory.CategoryStruct.comp f q = CategoryTheory.CategoryStruct.comp p f')
(wg : CategoryTheory.CategoryStruct.comp g q = CategoryTheory.CategoryStruct.comp p g')
:
Construct a morphism between parallel pairs.
Equations
- One or more equations did not get rendered due to their size.
Instances For
@[simp]
theorem
CategoryTheory.Limits.parallelPairHom_app_zero
{C : Type u}
[CategoryTheory.Category.{v, u} C]
{X : C}
{Y : C}
{X' : C}
{Y' : C}
(f : X ⟶ Y)
(g : X ⟶ Y)
(f' : X' ⟶ Y')
(g' : X' ⟶ Y')
(p : X ⟶ X')
(q : Y ⟶ Y')
(wf : CategoryTheory.CategoryStruct.comp f q = CategoryTheory.CategoryStruct.comp p f')
(wg : CategoryTheory.CategoryStruct.comp g q = CategoryTheory.CategoryStruct.comp p g')
:
(CategoryTheory.Limits.parallelPairHom f g f' g' p q wf wg).app CategoryTheory.Limits.WalkingParallelPair.zero = p
@[simp]
theorem
CategoryTheory.Limits.parallelPairHom_app_one
{C : Type u}
[CategoryTheory.Category.{v, u} C]
{X : C}
{Y : C}
{X' : C}
{Y' : C}
(f : X ⟶ Y)
(g : X ⟶ Y)
(f' : X' ⟶ Y')
(g' : X' ⟶ Y')
(p : X ⟶ X')
(q : Y ⟶ Y')
(wf : CategoryTheory.CategoryStruct.comp f q = CategoryTheory.CategoryStruct.comp p f')
(wg : CategoryTheory.CategoryStruct.comp g q = CategoryTheory.CategoryStruct.comp p g')
:
(CategoryTheory.Limits.parallelPairHom f g f' g' p q wf wg).app CategoryTheory.Limits.WalkingParallelPair.one = q
@[simp]
theorem
CategoryTheory.Limits.parallelPair.ext_hom_app
{C : Type u}
[CategoryTheory.Category.{v, u} C]
{F : CategoryTheory.Functor CategoryTheory.Limits.WalkingParallelPair C}
{G : CategoryTheory.Functor CategoryTheory.Limits.WalkingParallelPair C}
(zero : F.obj CategoryTheory.Limits.WalkingParallelPair.zero ≅ G.obj CategoryTheory.Limits.WalkingParallelPair.zero)
(one : F.obj CategoryTheory.Limits.WalkingParallelPair.one ≅ G.obj CategoryTheory.Limits.WalkingParallelPair.one)
(left : CategoryTheory.CategoryStruct.comp (F.map CategoryTheory.Limits.WalkingParallelPairHom.left) one.hom = CategoryTheory.CategoryStruct.comp zero.hom (G.map CategoryTheory.Limits.WalkingParallelPairHom.left))
(right : CategoryTheory.CategoryStruct.comp (F.map CategoryTheory.Limits.WalkingParallelPairHom.right) one.hom = CategoryTheory.CategoryStruct.comp zero.hom (G.map CategoryTheory.Limits.WalkingParallelPairHom.right))
(X : CategoryTheory.Limits.WalkingParallelPair)
:
(CategoryTheory.Limits.parallelPair.ext zero one left right).hom.app X = (CategoryTheory.Limits.WalkingParallelPair.rec zero one X).hom
@[simp]
theorem
CategoryTheory.Limits.parallelPair.ext_inv_app
{C : Type u}
[CategoryTheory.Category.{v, u} C]
{F : CategoryTheory.Functor CategoryTheory.Limits.WalkingParallelPair C}
{G : CategoryTheory.Functor CategoryTheory.Limits.WalkingParallelPair C}
(zero : F.obj CategoryTheory.Limits.WalkingParallelPair.zero ≅ G.obj CategoryTheory.Limits.WalkingParallelPair.zero)
(one : F.obj CategoryTheory.Limits.WalkingParallelPair.one ≅ G.obj CategoryTheory.Limits.WalkingParallelPair.one)
(left : CategoryTheory.CategoryStruct.comp (F.map CategoryTheory.Limits.WalkingParallelPairHom.left) one.hom = CategoryTheory.CategoryStruct.comp zero.hom (G.map CategoryTheory.Limits.WalkingParallelPairHom.left))
(right : CategoryTheory.CategoryStruct.comp (F.map CategoryTheory.Limits.WalkingParallelPairHom.right) one.hom = CategoryTheory.CategoryStruct.comp zero.hom (G.map CategoryTheory.Limits.WalkingParallelPairHom.right))
(X : CategoryTheory.Limits.WalkingParallelPair)
:
(CategoryTheory.Limits.parallelPair.ext zero one left right).inv.app X = (CategoryTheory.Limits.WalkingParallelPair.rec zero one X).inv
def
CategoryTheory.Limits.parallelPair.ext
{C : Type u}
[CategoryTheory.Category.{v, u} C]
{F : CategoryTheory.Functor CategoryTheory.Limits.WalkingParallelPair C}
{G : CategoryTheory.Functor CategoryTheory.Limits.WalkingParallelPair C}
(zero : F.obj CategoryTheory.Limits.WalkingParallelPair.zero ≅ G.obj CategoryTheory.Limits.WalkingParallelPair.zero)
(one : F.obj CategoryTheory.Limits.WalkingParallelPair.one ≅ G.obj CategoryTheory.Limits.WalkingParallelPair.one)
(left : CategoryTheory.CategoryStruct.comp (F.map CategoryTheory.Limits.WalkingParallelPairHom.left) one.hom = CategoryTheory.CategoryStruct.comp zero.hom (G.map CategoryTheory.Limits.WalkingParallelPairHom.left))
(right : CategoryTheory.CategoryStruct.comp (F.map CategoryTheory.Limits.WalkingParallelPairHom.right) one.hom = CategoryTheory.CategoryStruct.comp zero.hom (G.map CategoryTheory.Limits.WalkingParallelPairHom.right))
:
F ≅ G
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.
Instances For
@[simp]
theorem
CategoryTheory.Limits.parallelPair.eqOfHomEq_inv_app
{C : Type u}
[CategoryTheory.Category.{v, u} C]
{X : C}
{Y : C}
{f : X✝ ⟶ Y}
{g : X✝ ⟶ Y}
{f' : X✝ ⟶ Y}
{g' : X✝ ⟶ Y}
(hf : f = f')
(hg : g = g')
(X : CategoryTheory.Limits.WalkingParallelPair)
:
(CategoryTheory.Limits.parallelPair.eqOfHomEq hf hg).inv.app X = (CategoryTheory.Limits.WalkingParallelPair.rec (CategoryTheory.Iso.refl X✝) (CategoryTheory.Iso.refl Y) X).inv
@[simp]
theorem
CategoryTheory.Limits.parallelPair.eqOfHomEq_hom_app
{C : Type u}
[CategoryTheory.Category.{v, u} C]
{X : C}
{Y : C}
{f : X✝ ⟶ Y}
{g : X✝ ⟶ Y}
{f' : X✝ ⟶ Y}
{g' : X✝ ⟶ Y}
(hf : f = f')
(hg : g = g')
(X : CategoryTheory.Limits.WalkingParallelPair)
:
(CategoryTheory.Limits.parallelPair.eqOfHomEq hf hg).hom.app X = (CategoryTheory.Limits.WalkingParallelPair.rec (CategoryTheory.Iso.refl X✝) (CategoryTheory.Iso.refl Y) X).hom
def
CategoryTheory.Limits.parallelPair.eqOfHomEq
{C : Type u}
[CategoryTheory.Category.{v, u} C]
{X : C}
{Y : C}
{f : X ⟶ Y}
{g : X ⟶ Y}
{f' : X ⟶ Y}
{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.
Instances For
@[reducible, inline]
abbrev
CategoryTheory.Limits.Fork
{C : Type u}
[CategoryTheory.Category.{v, u} C]
{X : C}
{Y : C}
(f : X ⟶ Y)
(g : X ⟶ Y)
:
Type (max (max 0 u) v)
A fork on f and g is just a Cone (parallelPair f g).
Equations
Instances For
@[reducible, inline]
abbrev
CategoryTheory.Limits.Cofork
{C : Type u}
[CategoryTheory.Category.{v, u} C]
{X : C}
{Y : C}
(f : X ⟶ Y)
(g : X ⟶ Y)
:
Type (max (max 0 u) v)
A cofork on f and g is just a Cocone (parallelPair f g).
Equations
Instances For
def
CategoryTheory.Limits.Fork.ι
{C : Type u}
[CategoryTheory.Category.{v, u} C]
{X : C}
{Y : C}
{f : X ⟶ Y}
{g : X ⟶ Y}
(t : CategoryTheory.Limits.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
- t.ι = t.π.app CategoryTheory.Limits.WalkingParallelPair.zero
Instances For
@[simp]
theorem
CategoryTheory.Limits.Fork.app_zero_eq_ι
{C : Type u}
[CategoryTheory.Category.{v, u} C]
{X : C}
{Y : C}
{f : X ⟶ Y}
{g : X ⟶ Y}
(t : CategoryTheory.Limits.Fork f g)
:
t.π.app CategoryTheory.Limits.WalkingParallelPair.zero = t.ι
def
CategoryTheory.Limits.Cofork.π
{C : Type u}
[CategoryTheory.Category.{v, u} C]
{X : C}
{Y : C}
{f : X ⟶ Y}
{g : X ⟶ Y}
(t : CategoryTheory.Limits.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
- t.π = t.ι.app CategoryTheory.Limits.WalkingParallelPair.one
Instances For
@[simp]
theorem
CategoryTheory.Limits.Cofork.app_one_eq_π
{C : Type u}
[CategoryTheory.Category.{v, u} C]
{X : C}
{Y : C}
{f : X ⟶ Y}
{g : X ⟶ Y}
(t : CategoryTheory.Limits.Cofork f g)
:
t.ι.app CategoryTheory.Limits.WalkingParallelPair.one = t.π
@[simp]
theorem
CategoryTheory.Limits.Fork.app_one_eq_ι_comp_left
{C : Type u}
[CategoryTheory.Category.{v, u} C]
{X : C}
{Y : C}
{f : X ⟶ Y}
{g : X ⟶ Y}
(s : CategoryTheory.Limits.Fork f g)
:
theorem
CategoryTheory.Limits.Fork.app_one_eq_ι_comp_right_assoc
{C : Type u}
[CategoryTheory.Category.{v, u} C]
{X : C}
{Y : C}
{f : X ⟶ Y}
{g : X ⟶ Y}
(s : CategoryTheory.Limits.Fork f g)
{Z : C}
(h : (CategoryTheory.Limits.parallelPair f g).obj CategoryTheory.Limits.WalkingParallelPair.one ⟶ Z)
:
theorem
CategoryTheory.Limits.Fork.app_one_eq_ι_comp_right
{C : Type u}
[CategoryTheory.Category.{v, u} C]
{X : C}
{Y : C}
{f : X ⟶ Y}
{g : X ⟶ Y}
(s : CategoryTheory.Limits.Fork f g)
:
@[simp]
theorem
CategoryTheory.Limits.Cofork.app_zero_eq_comp_π_left
{C : Type u}
[CategoryTheory.Category.{v, u} C]
{X : C}
{Y : C}
{f : X ⟶ Y}
{g : X ⟶ Y}
(s : CategoryTheory.Limits.Cofork f g)
:
theorem
CategoryTheory.Limits.Cofork.app_zero_eq_comp_π_right_assoc
{C : Type u}
[CategoryTheory.Category.{v, u} C]
{X : C}
{Y : C}
{f : X ⟶ Y}
{g : X ⟶ Y}
(s : CategoryTheory.Limits.Cofork f g)
{Z : C}
(h : ((CategoryTheory.Functor.const CategoryTheory.Limits.WalkingParallelPair).obj s.pt).obj
CategoryTheory.Limits.WalkingParallelPair.zero ⟶ Z)
:
theorem
CategoryTheory.Limits.Cofork.app_zero_eq_comp_π_right
{C : Type u}
[CategoryTheory.Category.{v, u} C]
{X : C}
{Y : C}
{f : X ⟶ Y}
{g : X ⟶ Y}
(s : CategoryTheory.Limits.Cofork f g)
:
@[simp]
theorem
CategoryTheory.Limits.Fork.ofι_pt
{C : Type u}
[CategoryTheory.Category.{v, u} C]
{X : C}
{Y : C}
{f : X ⟶ Y}
{g : X ⟶ Y}
{P : C}
(ι : P ⟶ X)
(w : CategoryTheory.CategoryStruct.comp ι f = CategoryTheory.CategoryStruct.comp ι g)
:
(CategoryTheory.Limits.Fork.ofι ι w).pt = P
@[simp]
theorem
CategoryTheory.Limits.Fork.ofι_π_app
{C : Type u}
[CategoryTheory.Category.{v, u} C]
{X : C}
{Y : C}
{f : X✝ ⟶ Y}
{g : X✝ ⟶ Y}
{P : C}
(ι : P ⟶ X✝)
(w : CategoryTheory.CategoryStruct.comp ι f = CategoryTheory.CategoryStruct.comp ι g)
(X : CategoryTheory.Limits.WalkingParallelPair)
:
(CategoryTheory.Limits.Fork.ofι ι w).π.app X = CategoryTheory.Limits.WalkingParallelPair.casesOn (motive := fun (t : CategoryTheory.Limits.WalkingParallelPair) =>
X = t →
(((CategoryTheory.Functor.const CategoryTheory.Limits.WalkingParallelPair).obj P).obj X ⟶ (CategoryTheory.Limits.parallelPair f g).obj X))
X (fun (h : X = CategoryTheory.Limits.WalkingParallelPair.zero) => ⋯ ▸ ι)
(fun (h : X = CategoryTheory.Limits.WalkingParallelPair.one) => ⋯ ▸ CategoryTheory.CategoryStruct.comp ι f) ⋯
def
CategoryTheory.Limits.Fork.ofι
{C : Type u}
[CategoryTheory.Category.{v, u} C]
{X : C}
{Y : C}
{f : X ⟶ Y}
{g : X ⟶ Y}
{P : C}
(ι : P ⟶ X)
(w : CategoryTheory.CategoryStruct.comp ι f = CategoryTheory.CategoryStruct.comp ι 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.
Instances For
@[simp]
theorem
CategoryTheory.Limits.Cofork.ofπ_ι_app
{C : Type u}
[CategoryTheory.Category.{v, u} C]
{X : C}
{Y : C}
{f : X✝ ⟶ Y}
{g : X✝ ⟶ Y}
{P : C}
(π : Y ⟶ P)
(w : CategoryTheory.CategoryStruct.comp f π = CategoryTheory.CategoryStruct.comp g π)
(X : CategoryTheory.Limits.WalkingParallelPair)
:
@[simp]
theorem
CategoryTheory.Limits.Cofork.ofπ_pt
{C : Type u}
[CategoryTheory.Category.{v, u} C]
{X : C}
{Y : C}
{f : X ⟶ Y}
{g : X ⟶ Y}
{P : C}
(π : Y ⟶ P)
(w : CategoryTheory.CategoryStruct.comp f π = CategoryTheory.CategoryStruct.comp g π)
:
(CategoryTheory.Limits.Cofork.ofπ π w).pt = P
def
CategoryTheory.Limits.Cofork.ofπ
{C : Type u}
[CategoryTheory.Category.{v, u} C]
{X : C}
{Y : C}
{f : X ⟶ Y}
{g : X ⟶ Y}
{P : C}
(π : Y ⟶ P)
(w : CategoryTheory.CategoryStruct.comp f π = CategoryTheory.CategoryStruct.comp 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.
Instances For
@[simp]
theorem
CategoryTheory.Limits.Fork.ι_ofι
{C : Type u}
[CategoryTheory.Category.{v, u} C]
{X : C}
{Y : C}
{f : X ⟶ Y}
{g : X ⟶ Y}
{P : C}
(ι : P ⟶ X)
(w : CategoryTheory.CategoryStruct.comp ι f = CategoryTheory.CategoryStruct.comp ι g)
:
(CategoryTheory.Limits.Fork.ofι ι w).ι = ι
@[simp]
theorem
CategoryTheory.Limits.Cofork.π_ofπ
{C : Type u}
[CategoryTheory.Category.{v, u} C]
{X : C}
{Y : C}
{f : X ⟶ Y}
{g : X ⟶ Y}
{P : C}
(π : Y ⟶ P)
(w : CategoryTheory.CategoryStruct.comp f π = CategoryTheory.CategoryStruct.comp g π)
:
(CategoryTheory.Limits.Cofork.ofπ π w).π = π
@[simp]
theorem
CategoryTheory.Limits.Fork.condition_assoc
{C : Type u}
[CategoryTheory.Category.{v, u} C]
{X : C}
{Y : C}
{f : X ⟶ Y}
{g : X ⟶ Y}
(t : CategoryTheory.Limits.Fork f g)
{Z : C}
(h : Y ⟶ Z)
:
@[simp]
theorem
CategoryTheory.Limits.Fork.condition
{C : Type u}
[CategoryTheory.Category.{v, u} C]
{X : C}
{Y : C}
{f : X ⟶ Y}
{g : X ⟶ Y}
(t : CategoryTheory.Limits.Fork f g)
:
@[simp]
theorem
CategoryTheory.Limits.Cofork.condition_assoc
{C : Type u}
[CategoryTheory.Category.{v, u} C]
{X : C}
{Y : C}
{f : X ⟶ Y}
{g : X ⟶ Y}
(t : CategoryTheory.Limits.Cofork f g)
{Z : C}
(h : ((CategoryTheory.Functor.const CategoryTheory.Limits.WalkingParallelPair).obj t.pt).obj
CategoryTheory.Limits.WalkingParallelPair.one ⟶ Z)
:
@[simp]
theorem
CategoryTheory.Limits.Cofork.condition
{C : Type u}
[CategoryTheory.Category.{v, u} C]
{X : C}
{Y : C}
{f : X ⟶ Y}
{g : X ⟶ Y}
(t : CategoryTheory.Limits.Cofork f g)
:
theorem
CategoryTheory.Limits.Fork.equalizer_ext
{C : Type u}
[CategoryTheory.Category.{v, u} C]
{X : C}
{Y : C}
{f : X ⟶ Y}
{g : X ⟶ Y}
(s : CategoryTheory.Limits.Fork f g)
{W : C}
{k : W ⟶ s.pt}
{l : W ⟶ s.pt}
(h : CategoryTheory.CategoryStruct.comp k s.ι = CategoryTheory.CategoryStruct.comp l s.ι)
(j : CategoryTheory.Limits.WalkingParallelPair)
:
CategoryTheory.CategoryStruct.comp k (s.π.app j) = CategoryTheory.CategoryStruct.comp l (s.π.app j)
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}
[CategoryTheory.Category.{v, u} C]
{X : C}
{Y : C}
{f : X ⟶ Y}
{g : X ⟶ Y}
(s : CategoryTheory.Limits.Cofork f g)
{W : C}
{k : s.pt ⟶ W}
{l : s.pt ⟶ W}
(h : CategoryTheory.CategoryStruct.comp s.π k = CategoryTheory.CategoryStruct.comp s.π l)
(j : CategoryTheory.Limits.WalkingParallelPair)
:
CategoryTheory.CategoryStruct.comp (s.ι.app j) k = CategoryTheory.CategoryStruct.comp (s.ι.app j) l
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}
[CategoryTheory.Category.{v, u} C]
{X : C}
{Y : C}
{f : X ⟶ Y}
{g : X ⟶ Y}
{s : CategoryTheory.Limits.Fork f g}
(hs : CategoryTheory.Limits.IsLimit s)
{W : C}
{k : W ⟶ s.pt}
{l : W ⟶ s.pt}
(h : CategoryTheory.CategoryStruct.comp k s.ι = CategoryTheory.CategoryStruct.comp l s.ι)
:
k = l
theorem
CategoryTheory.Limits.Cofork.IsColimit.hom_ext
{C : Type u}
[CategoryTheory.Category.{v, u} C]
{X : C}
{Y : C}
{f : X ⟶ Y}
{g : X ⟶ Y}
{s : CategoryTheory.Limits.Cofork f g}
(hs : CategoryTheory.Limits.IsColimit s)
{W : C}
{k : s.pt ⟶ W}
{l : s.pt ⟶ W}
(h : CategoryTheory.CategoryStruct.comp s.π k = CategoryTheory.CategoryStruct.comp s.π l)
:
k = l
@[simp]
theorem
CategoryTheory.Limits.Fork.IsLimit.lift_ι_assoc
{C : Type u}
[CategoryTheory.Category.{v, u} C]
{X : C}
{Y : C}
{f : X ⟶ Y}
{g : X ⟶ Y}
{s : CategoryTheory.Limits.Fork f g}
{t : CategoryTheory.Limits.Fork f g}
(hs : CategoryTheory.Limits.IsLimit s)
{Z : C}
(h : (CategoryTheory.Limits.parallelPair f g).obj CategoryTheory.Limits.WalkingParallelPair.zero ⟶ Z)
:
CategoryTheory.CategoryStruct.comp (hs.lift t) (CategoryTheory.CategoryStruct.comp s.ι h) = CategoryTheory.CategoryStruct.comp t.ι h
@[simp]
theorem
CategoryTheory.Limits.Fork.IsLimit.lift_ι
{C : Type u}
[CategoryTheory.Category.{v, u} C]
{X : C}
{Y : C}
{f : X ⟶ Y}
{g : X ⟶ Y}
{s : CategoryTheory.Limits.Fork f g}
{t : CategoryTheory.Limits.Fork f g}
(hs : CategoryTheory.Limits.IsLimit s)
:
CategoryTheory.CategoryStruct.comp (hs.lift t) s.ι = t.ι
@[simp]
theorem
CategoryTheory.Limits.Cofork.IsColimit.π_desc_assoc
{C : Type u}
[CategoryTheory.Category.{v, u} C]
{X : C}
{Y : C}
{f : X ⟶ Y}
{g : X ⟶ Y}
{s : CategoryTheory.Limits.Cofork f g}
{t : CategoryTheory.Limits.Cofork f g}
(hs : CategoryTheory.Limits.IsColimit s)
{Z : C}
(h : t.pt ⟶ Z)
:
CategoryTheory.CategoryStruct.comp s.π (CategoryTheory.CategoryStruct.comp (hs.desc t) h) = CategoryTheory.CategoryStruct.comp t.π h
@[simp]
theorem
CategoryTheory.Limits.Cofork.IsColimit.π_desc
{C : Type u}
[CategoryTheory.Category.{v, u} C]
{X : C}
{Y : C}
{f : X ⟶ Y}
{g : X ⟶ Y}
{s : CategoryTheory.Limits.Cofork f g}
{t : CategoryTheory.Limits.Cofork f g}
(hs : CategoryTheory.Limits.IsColimit s)
:
CategoryTheory.CategoryStruct.comp s.π (hs.desc t) = t.π
def
CategoryTheory.Limits.Fork.IsLimit.lift
{C : Type u}
[CategoryTheory.Category.{v, u} C]
{X : C}
{Y : C}
{f : X ⟶ Y}
{g : X ⟶ Y}
{s : CategoryTheory.Limits.Fork f g}
(hs : CategoryTheory.Limits.IsLimit s)
{W : C}
(k : W ⟶ X)
(h : CategoryTheory.CategoryStruct.comp k f = CategoryTheory.CategoryStruct.comp k g)
:
W ⟶ s.pt
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)
Instances For
@[simp]
theorem
CategoryTheory.Limits.Fork.IsLimit.lift_ι'_assoc
{C : Type u}
[CategoryTheory.Category.{v, u} C]
{X : C}
{Y : C}
{f : X ⟶ Y}
{g : X ⟶ Y}
{s : CategoryTheory.Limits.Fork f g}
(hs : CategoryTheory.Limits.IsLimit s)
{W : C}
(k : W ⟶ X)
(h : CategoryTheory.CategoryStruct.comp k f = CategoryTheory.CategoryStruct.comp k g)
{Z : C}
(h : (CategoryTheory.Limits.parallelPair f g).obj CategoryTheory.Limits.WalkingParallelPair.zero ⟶ Z)
:
@[simp]
theorem
CategoryTheory.Limits.Fork.IsLimit.lift_ι'
{C : Type u}
[CategoryTheory.Category.{v, u} C]
{X : C}
{Y : C}
{f : X ⟶ Y}
{g : X ⟶ Y}
{s : CategoryTheory.Limits.Fork f g}
(hs : CategoryTheory.Limits.IsLimit s)
{W : C}
(k : W ⟶ X)
(h : CategoryTheory.CategoryStruct.comp k f = CategoryTheory.CategoryStruct.comp k g)
:
def
CategoryTheory.Limits.Fork.IsLimit.lift'
{C : Type u}
[CategoryTheory.Category.{v, u} C]
{X : C}
{Y : C}
{f : X ⟶ Y}
{g : X ⟶ Y}
{s : CategoryTheory.Limits.Fork f g}
(hs : CategoryTheory.Limits.IsLimit s)
{W : C}
(k : W ⟶ X)
(h : CategoryTheory.CategoryStruct.comp k f = CategoryTheory.CategoryStruct.comp k g)
:
{ l : W ⟶ s.pt // CategoryTheory.CategoryStruct.comp l s.ι = k }
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, ⋯⟩
Instances For
def
CategoryTheory.Limits.Cofork.IsColimit.desc
{C : Type u}
[CategoryTheory.Category.{v, u} C]
{X : C}
{Y : C}
{f : X ⟶ Y}
{g : X ⟶ Y}
{s : CategoryTheory.Limits.Cofork f g}
(hs : CategoryTheory.Limits.IsColimit s)
{W : C}
(k : Y ⟶ W)
(h : CategoryTheory.CategoryStruct.comp f k = CategoryTheory.CategoryStruct.comp g k)
:
s.pt ⟶ W
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
- CategoryTheory.Limits.Cofork.IsColimit.desc hs k h = hs.desc (CategoryTheory.Limits.Cofork.ofπ k h)
Instances For
@[simp]
theorem
CategoryTheory.Limits.Cofork.IsColimit.π_desc'_assoc
{C : Type u}
[CategoryTheory.Category.{v, u} C]
{X : C}
{Y : C}
{f : X ⟶ Y}
{g : X ⟶ Y}
{s : CategoryTheory.Limits.Cofork f g}
(hs : CategoryTheory.Limits.IsColimit s)
{W : C}
(k : Y ⟶ W)
(h : CategoryTheory.CategoryStruct.comp f k = CategoryTheory.CategoryStruct.comp g k)
{Z : C}
(h : W ⟶ Z)
:
@[simp]
theorem
CategoryTheory.Limits.Cofork.IsColimit.π_desc'
{C : Type u}
[CategoryTheory.Category.{v, u} C]
{X : C}
{Y : C}
{f : X ⟶ Y}
{g : X ⟶ Y}
{s : CategoryTheory.Limits.Cofork f g}
(hs : CategoryTheory.Limits.IsColimit s)
{W : C}
(k : Y ⟶ W)
(h : CategoryTheory.CategoryStruct.comp f k = CategoryTheory.CategoryStruct.comp g k)
:
def
CategoryTheory.Limits.Cofork.IsColimit.desc'
{C : Type u}
[CategoryTheory.Category.{v, u} C]
{X : C}
{Y : C}
{f : X ⟶ Y}
{g : X ⟶ Y}
{s : CategoryTheory.Limits.Cofork f g}
(hs : CategoryTheory.Limits.IsColimit s)
{W : C}
(k : Y ⟶ W)
(h : CategoryTheory.CategoryStruct.comp f k = CategoryTheory.CategoryStruct.comp g k)
:
{ l : s.pt ⟶ W // CategoryTheory.CategoryStruct.comp s.π l = 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
Instances For
theorem
CategoryTheory.Limits.Fork.IsLimit.existsUnique
{C : Type u}
[CategoryTheory.Category.{v, u} C]
{X : C}
{Y : C}
{f : X ⟶ Y}
{g : X ⟶ Y}
{s : CategoryTheory.Limits.Fork f g}
(hs : CategoryTheory.Limits.IsLimit s)
{W : C}
(k : W ⟶ X)
(h : CategoryTheory.CategoryStruct.comp k f = CategoryTheory.CategoryStruct.comp k g)
:
∃! l : W ⟶ s.pt, CategoryTheory.CategoryStruct.comp l s.ι = k
theorem
CategoryTheory.Limits.Cofork.IsColimit.existsUnique
{C : Type u}
[CategoryTheory.Category.{v, u} C]
{X : C}
{Y : C}
{f : X ⟶ Y}
{g : X ⟶ Y}
{s : CategoryTheory.Limits.Cofork f g}
(hs : CategoryTheory.Limits.IsColimit s)
{W : C}
(k : Y ⟶ W)
(h : CategoryTheory.CategoryStruct.comp f k = CategoryTheory.CategoryStruct.comp g k)
:
∃! d : s.pt ⟶ W, CategoryTheory.CategoryStruct.comp s.π d = k
@[simp]
theorem
CategoryTheory.Limits.Fork.IsLimit.mk_lift
{C : Type u}
[CategoryTheory.Category.{v, u} C]
{X : C}
{Y : C}
{f : X ⟶ Y}
{g : X ⟶ Y}
(t : CategoryTheory.Limits.Fork f g)
(lift : (s : CategoryTheory.Limits.Fork f g) → s.pt ⟶ t.pt)
(fac : ∀ (s : CategoryTheory.Limits.Fork f g), CategoryTheory.CategoryStruct.comp (lift s) t.ι = s.ι)
(uniq : ∀ (s : CategoryTheory.Limits.Fork f g) (m : s.pt ⟶ t.pt), CategoryTheory.CategoryStruct.comp m t.ι = s.ι → m = lift s)
(s : CategoryTheory.Limits.Fork f g)
:
(CategoryTheory.Limits.Fork.IsLimit.mk t lift fac uniq).lift s = lift s
def
CategoryTheory.Limits.Fork.IsLimit.mk
{C : Type u}
[CategoryTheory.Category.{v, u} C]
{X : C}
{Y : C}
{f : X ⟶ Y}
{g : X ⟶ Y}
(t : CategoryTheory.Limits.Fork f g)
(lift : (s : CategoryTheory.Limits.Fork f g) → s.pt ⟶ t.pt)
(fac : ∀ (s : CategoryTheory.Limits.Fork f g), CategoryTheory.CategoryStruct.comp (lift s) t.ι = s.ι)
(uniq : ∀ (s : CategoryTheory.Limits.Fork f g) (m : s.pt ⟶ t.pt), CategoryTheory.CategoryStruct.comp m t.ι = s.ι → m = lift s)
:
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 := ⋯ }
Instances For
def
CategoryTheory.Limits.Fork.IsLimit.mk'
{C : Type u}
[CategoryTheory.Category.{v, u} C]
{X : C}
{Y : C}
{f : X ⟶ Y}
{g : X ⟶ Y}
(t : CategoryTheory.Limits.Fork f g)
(create : (s : CategoryTheory.Limits.Fork f g) →
{ l :
((CategoryTheory.Functor.const CategoryTheory.Limits.WalkingParallelPair).obj s.pt).obj
CategoryTheory.Limits.WalkingParallelPair.zero ⟶ ((CategoryTheory.Functor.const CategoryTheory.Limits.WalkingParallelPair).obj t.pt).obj
CategoryTheory.Limits.WalkingParallelPair.zero //
CategoryTheory.CategoryStruct.comp l t.ι = s.ι ∧ ∀
{m :
((CategoryTheory.Functor.const CategoryTheory.Limits.WalkingParallelPair).obj s.pt).obj
CategoryTheory.Limits.WalkingParallelPair.zero ⟶ ((CategoryTheory.Functor.const CategoryTheory.Limits.WalkingParallelPair).obj t.pt).obj
CategoryTheory.Limits.WalkingParallelPair.zero},
CategoryTheory.CategoryStruct.comp m t.ι = 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.Fork.IsLimit.mk' t create = CategoryTheory.Limits.Fork.IsLimit.mk t (fun (s : CategoryTheory.Limits.Fork f g) => ↑(create s)) ⋯ ⋯
Instances For
def
CategoryTheory.Limits.Cofork.IsColimit.mk
{C : Type u}
[CategoryTheory.Category.{v, u} C]
{X : C}
{Y : C}
{f : X ⟶ Y}
{g : X ⟶ Y}
(t : CategoryTheory.Limits.Cofork f g)
(desc : (s : CategoryTheory.Limits.Cofork f g) → t.pt ⟶ s.pt)
(fac : ∀ (s : CategoryTheory.Limits.Cofork f g), CategoryTheory.CategoryStruct.comp t.π (desc s) = s.π)
(uniq : ∀ (s : CategoryTheory.Limits.Cofork f g) (m : t.pt ⟶ s.pt), CategoryTheory.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 := ⋯ }
Instances For
def
CategoryTheory.Limits.Cofork.IsColimit.mk'
{C : Type u}
[CategoryTheory.Category.{v, u} C]
{X : C}
{Y : C}
{f : X ⟶ Y}
{g : X ⟶ Y}
(t : CategoryTheory.Limits.Cofork f g)
(create : (s : CategoryTheory.Limits.Cofork f g) →
{ l : t.pt ⟶ s.pt //
CategoryTheory.CategoryStruct.comp t.π l = s.π ∧ ∀
{m :
((CategoryTheory.Functor.const CategoryTheory.Limits.WalkingParallelPair).obj t.pt).obj
CategoryTheory.Limits.WalkingParallelPair.one ⟶ ((CategoryTheory.Functor.const CategoryTheory.Limits.WalkingParallelPair).obj s.pt).obj
CategoryTheory.Limits.WalkingParallelPair.one},
CategoryTheory.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)) ⋯ ⋯
Instances For
noncomputable def
CategoryTheory.Limits.Fork.IsLimit.ofExistsUnique
{C : Type u}
[CategoryTheory.Category.{v, u} C]
{X : C}
{Y : C}
{f : X ⟶ Y}
{g : X ⟶ Y}
{t : CategoryTheory.Limits.Fork f g}
(hs : ∀ (s : CategoryTheory.Limits.Fork f g), ∃! l : s.pt ⟶ t.pt, CategoryTheory.CategoryStruct.comp l t.ι = s.ι)
:
Noncomputably make a limit cone from the existence of unique factorizations.
Equations
- One or more equations did not get rendered due to their size.
Instances For
noncomputable def
CategoryTheory.Limits.Cofork.IsColimit.ofExistsUnique
{C : Type u}
[CategoryTheory.Category.{v, u} C]
{X : C}
{Y : C}
{f : X ⟶ Y}
{g : X ⟶ Y}
{t : CategoryTheory.Limits.Cofork f g}
(hs : ∀ (s : CategoryTheory.Limits.Cofork f g), ∃! d : t.pt ⟶ s.pt, CategoryTheory.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.
Instances For
@[simp]
theorem
CategoryTheory.Limits.Fork.IsLimit.homIso_symm_apply
{C : Type u}
[CategoryTheory.Category.{v, u} C]
{X : C}
{Y : C}
{f : X ⟶ Y}
{g : X ⟶ Y}
{t : CategoryTheory.Limits.Fork f g}
(ht : CategoryTheory.Limits.IsLimit t)
(Z : C)
(h : { h : Z ⟶ X // CategoryTheory.CategoryStruct.comp h f = CategoryTheory.CategoryStruct.comp h g })
:
(CategoryTheory.Limits.Fork.IsLimit.homIso ht Z).symm h = ↑(CategoryTheory.Limits.Fork.IsLimit.lift' ht ↑h ⋯)
@[simp]
theorem
CategoryTheory.Limits.Fork.IsLimit.homIso_apply_coe
{C : Type u}
[CategoryTheory.Category.{v, u} C]
{X : C}
{Y : C}
{f : X ⟶ Y}
{g : X ⟶ Y}
{t : CategoryTheory.Limits.Fork f g}
(ht : CategoryTheory.Limits.IsLimit t)
(Z : C)
(k : Z ⟶ t.pt)
:
↑((CategoryTheory.Limits.Fork.IsLimit.homIso ht Z) k) = CategoryTheory.CategoryStruct.comp k t.ι
def
CategoryTheory.Limits.Fork.IsLimit.homIso
{C : Type u}
[CategoryTheory.Category.{v, u} C]
{X : C}
{Y : C}
{f : X ⟶ Y}
{g : X ⟶ Y}
{t : CategoryTheory.Limits.Fork f g}
(ht : CategoryTheory.Limits.IsLimit t)
(Z : C)
:
(Z ⟶ t.pt) ≃ { h : Z ⟶ X // CategoryTheory.CategoryStruct.comp h f = CategoryTheory.CategoryStruct.comp h g }
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.
Instances For
theorem
CategoryTheory.Limits.Fork.IsLimit.homIso_natural
{C : Type u}
[CategoryTheory.Category.{v, u} C]
{X : C}
{Y : C}
{f : X ⟶ Y}
{g : X ⟶ Y}
{t : CategoryTheory.Limits.Fork f g}
(ht : CategoryTheory.Limits.IsLimit t)
{Z : C}
{Z' : C}
(q : Z' ⟶ Z)
(k : Z ⟶ t.pt)
:
The bijection of Fork.IsLimit.homIso is natural in Z.
@[simp]
theorem
CategoryTheory.Limits.Cofork.IsColimit.homIso_symm_apply
{C : Type u}
[CategoryTheory.Category.{v, u} C]
{X : C}
{Y : C}
{f : X ⟶ Y}
{g : X ⟶ Y}
{t : CategoryTheory.Limits.Cofork f g}
(ht : CategoryTheory.Limits.IsColimit t)
(Z : C)
(h : { h : Y ⟶ Z // CategoryTheory.CategoryStruct.comp f h = CategoryTheory.CategoryStruct.comp g h })
:
(CategoryTheory.Limits.Cofork.IsColimit.homIso ht Z).symm h = ↑(CategoryTheory.Limits.Cofork.IsColimit.desc' ht ↑h ⋯)
@[simp]
theorem
CategoryTheory.Limits.Cofork.IsColimit.homIso_apply_coe
{C : Type u}
[CategoryTheory.Category.{v, u} C]
{X : C}
{Y : C}
{f : X ⟶ Y}
{g : X ⟶ Y}
{t : CategoryTheory.Limits.Cofork f g}
(ht : CategoryTheory.Limits.IsColimit t)
(Z : C)
(k : t.pt ⟶ Z)
:
↑((CategoryTheory.Limits.Cofork.IsColimit.homIso ht Z) k) = CategoryTheory.CategoryStruct.comp t.π k
def
CategoryTheory.Limits.Cofork.IsColimit.homIso
{C : Type u}
[CategoryTheory.Category.{v, u} C]
{X : C}
{Y : C}
{f : X ⟶ Y}
{g : X ⟶ Y}
{t : CategoryTheory.Limits.Cofork f g}
(ht : CategoryTheory.Limits.IsColimit t)
(Z : C)
:
(t.pt ⟶ Z) ≃ { h : Y ⟶ Z // CategoryTheory.CategoryStruct.comp f h = CategoryTheory.CategoryStruct.comp g h }
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.
Instances For
theorem
CategoryTheory.Limits.Cofork.IsColimit.homIso_natural
{C : Type u}
[CategoryTheory.Category.{v, u} C]
{X : C}
{Y : C}
{f : X ⟶ Y}
{g : X ⟶ Y}
{t : CategoryTheory.Limits.Cofork f g}
{Z : C}
{Z' : C}
(q : Z ⟶ Z')
(ht : CategoryTheory.Limits.IsColimit t)
(k : t.pt ⟶ Z)
:
The bijection of Cofork.IsColimit.homIso is natural in Z.
def
CategoryTheory.Limits.Cone.ofFork
{C : Type u}
[CategoryTheory.Category.{v, u} C]
{F : CategoryTheory.Functor CategoryTheory.Limits.WalkingParallelPair C}
(t : CategoryTheory.Limits.Fork (F.map CategoryTheory.Limits.WalkingParallelPairHom.left)
(F.map CategoryTheory.Limits.WalkingParallelPairHom.right))
:
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.
Instances For
def
CategoryTheory.Limits.Cocone.ofCofork
{C : Type u}
[CategoryTheory.Category.{v, u} C]
{F : CategoryTheory.Functor CategoryTheory.Limits.WalkingParallelPair C}
(t : CategoryTheory.Limits.Cofork (F.map CategoryTheory.Limits.WalkingParallelPairHom.left)
(F.map CategoryTheory.Limits.WalkingParallelPairHom.right))
:
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.
Instances For
@[simp]
theorem
CategoryTheory.Limits.Cone.ofFork_π
{C : Type u}
[CategoryTheory.Category.{v, u} C]
{F : CategoryTheory.Functor CategoryTheory.Limits.WalkingParallelPair C}
(t : CategoryTheory.Limits.Fork (F.map CategoryTheory.Limits.WalkingParallelPairHom.left)
(F.map CategoryTheory.Limits.WalkingParallelPairHom.right))
(j : CategoryTheory.Limits.WalkingParallelPair)
:
(CategoryTheory.Limits.Cone.ofFork t).π.app j = CategoryTheory.CategoryStruct.comp (t.π.app j) (CategoryTheory.eqToHom ⋯)
@[simp]
theorem
CategoryTheory.Limits.Cocone.ofCofork_ι
{C : Type u}
[CategoryTheory.Category.{v, u} C]
{F : CategoryTheory.Functor CategoryTheory.Limits.WalkingParallelPair C}
(t : CategoryTheory.Limits.Cofork (F.map CategoryTheory.Limits.WalkingParallelPairHom.left)
(F.map CategoryTheory.Limits.WalkingParallelPairHom.right))
(j : CategoryTheory.Limits.WalkingParallelPair)
:
(CategoryTheory.Limits.Cocone.ofCofork t).ι.app j = CategoryTheory.CategoryStruct.comp (CategoryTheory.eqToHom ⋯) (t.ι.app j)
def
CategoryTheory.Limits.Fork.ofCone
{C : Type u}
[CategoryTheory.Category.{v, u} C]
{F : CategoryTheory.Functor CategoryTheory.Limits.WalkingParallelPair C}
(t : CategoryTheory.Limits.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.
Instances For
def
CategoryTheory.Limits.Cofork.ofCocone
{C : Type u}
[CategoryTheory.Category.{v, u} C]
{F : CategoryTheory.Functor CategoryTheory.Limits.WalkingParallelPair C}
(t : CategoryTheory.Limits.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.
Instances For
@[simp]
theorem
CategoryTheory.Limits.Fork.ofCone_π
{C : Type u}
[CategoryTheory.Category.{v, u} C]
{F : CategoryTheory.Functor CategoryTheory.Limits.WalkingParallelPair C}
(t : CategoryTheory.Limits.Cone F)
(j : CategoryTheory.Limits.WalkingParallelPair)
:
(CategoryTheory.Limits.Fork.ofCone t).π.app j = CategoryTheory.CategoryStruct.comp (t.π.app j) (CategoryTheory.eqToHom ⋯)
@[simp]
theorem
CategoryTheory.Limits.Cofork.ofCocone_ι
{C : Type u}
[CategoryTheory.Category.{v, u} C]
{F : CategoryTheory.Functor CategoryTheory.Limits.WalkingParallelPair C}
(t : CategoryTheory.Limits.Cocone F)
(j : CategoryTheory.Limits.WalkingParallelPair)
:
(CategoryTheory.Limits.Cofork.ofCocone t).ι.app j = CategoryTheory.CategoryStruct.comp (CategoryTheory.eqToHom ⋯) (t.ι.app j)
@[simp]
theorem
CategoryTheory.Limits.Fork.ι_postcompose
{C : Type u}
[CategoryTheory.Category.{v, u} C]
{X : C}
{Y : C}
{f : X ⟶ Y}
{g : X ⟶ Y}
{f' : X ⟶ Y}
{g' : X ⟶ Y}
{α : CategoryTheory.Limits.parallelPair f g ⟶ CategoryTheory.Limits.parallelPair f' g'}
{c : CategoryTheory.Limits.Fork f g}
:
@[simp]
theorem
CategoryTheory.Limits.Cofork.π_precompose
{C : Type u}
[CategoryTheory.Category.{v, u} C]
{X : C}
{Y : C}
{f : X ⟶ Y}
{g : X ⟶ Y}
{f' : X ⟶ Y}
{g' : X ⟶ Y}
{α : CategoryTheory.Limits.parallelPair f g ⟶ CategoryTheory.Limits.parallelPair f' g'}
{c : CategoryTheory.Limits.Cofork f' g'}
:
@[simp]
theorem
CategoryTheory.Limits.Fork.mkHom_hom
{C : Type u}
[CategoryTheory.Category.{v, u} C]
{X : C}
{Y : C}
{f : X ⟶ Y}
{g : X ⟶ Y}
{s : CategoryTheory.Limits.Fork f g}
{t : CategoryTheory.Limits.Fork f g}
(k : s.pt ⟶ t.pt)
(w : CategoryTheory.CategoryStruct.comp k t.ι = s.ι)
:
(CategoryTheory.Limits.Fork.mkHom k w).hom = k
def
CategoryTheory.Limits.Fork.mkHom
{C : Type u}
[CategoryTheory.Category.{v, u} C]
{X : C}
{Y : C}
{f : X ⟶ Y}
{g : X ⟶ Y}
{s : CategoryTheory.Limits.Fork f g}
{t : CategoryTheory.Limits.Fork f g}
(k : s.pt ⟶ t.pt)
(w : CategoryTheory.CategoryStruct.comp k t.ι = s.ι)
:
s ⟶ t
Helper function for constructing morphisms between equalizer forks.
Equations
- CategoryTheory.Limits.Fork.mkHom k w = { hom := k, w := ⋯ }
Instances For
@[simp]
theorem
CategoryTheory.Limits.Fork.ext_inv
{C : Type u}
[CategoryTheory.Category.{v, u} C]
{X : C}
{Y : C}
{f : X ⟶ Y}
{g : X ⟶ Y}
{s : CategoryTheory.Limits.Fork f g}
{t : CategoryTheory.Limits.Fork f g}
(i : s.pt ≅ t.pt)
(w : autoParam (CategoryTheory.CategoryStruct.comp i.hom t.ι = s.ι) _auto✝)
:
(CategoryTheory.Limits.Fork.ext i w).inv = CategoryTheory.Limits.Fork.mkHom i.inv ⋯
@[simp]
theorem
CategoryTheory.Limits.Fork.ext_hom
{C : Type u}
[CategoryTheory.Category.{v, u} C]
{X : C}
{Y : C}
{f : X ⟶ Y}
{g : X ⟶ Y}
{s : CategoryTheory.Limits.Fork f g}
{t : CategoryTheory.Limits.Fork f g}
(i : s.pt ≅ t.pt)
(w : autoParam (CategoryTheory.CategoryStruct.comp i.hom t.ι = s.ι) _auto✝)
:
(CategoryTheory.Limits.Fork.ext i w).hom = CategoryTheory.Limits.Fork.mkHom i.hom w
def
CategoryTheory.Limits.Fork.ext
{C : Type u}
[CategoryTheory.Category.{v, u} C]
{X : C}
{Y : C}
{f : X ⟶ Y}
{g : X ⟶ Y}
{s : CategoryTheory.Limits.Fork f g}
{t : CategoryTheory.Limits.Fork f g}
(i : s.pt ≅ t.pt)
(w : autoParam (CategoryTheory.CategoryStruct.comp i.hom t.ι = s.ι) _auto✝)
:
s ≅ t
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 := ⋯ }
Instances For
def
CategoryTheory.Limits.ForkOfι.ext
{C : Type u}
[CategoryTheory.Category.{v, u} C]
{X : C}
{Y : C}
{f : X ⟶ Y}
{g : X ⟶ Y}
{P : C}
{ι : P ⟶ X}
{ι' : P ⟶ X}
(w : CategoryTheory.CategoryStruct.comp ι f = CategoryTheory.CategoryStruct.comp ι g)
(w' : CategoryTheory.CategoryStruct.comp ι' f = CategoryTheory.CategoryStruct.comp ι' g)
(h : ι = ι')
:
Two forks of the form ofι are isomorphic whenever their ι's are equal.
Equations
Instances For
def
CategoryTheory.Limits.Fork.isoForkOfι
{C : Type u}
[CategoryTheory.Category.{v, u} C]
{X : C}
{Y : C}
{f : X ⟶ Y}
{g : X ⟶ Y}
(c : CategoryTheory.Limits.Fork f g)
:
c ≅ CategoryTheory.Limits.Fork.ofι c.ι ⋯
Every fork is isomorphic to one of the form Fork.of_ι _ _.
Equations
- c.isoForkOfι = CategoryTheory.Limits.Fork.ext (id (CategoryTheory.Iso.refl c.pt)) ⋯
Instances For
def
CategoryTheory.Limits.Fork.isLimitOfIsos
{C : Type u}
[CategoryTheory.Category.{v, u} C]
{X : C}
{Y : C}
{f : X ⟶ Y}
{g : X ⟶ Y}
{X' : C}
{Y' : C}
(c : CategoryTheory.Limits.Fork f g)
(hc : CategoryTheory.Limits.IsLimit c)
{f' : X' ⟶ Y'}
{g' : X' ⟶ Y'}
(c' : CategoryTheory.Limits.Fork f' g')
(e₀ : X ≅ X')
(e₁ : Y ≅ Y')
(e : c.pt ≅ c'.pt)
(comm₁ : autoParam (CategoryTheory.CategoryStruct.comp e₀.hom f' = CategoryTheory.CategoryStruct.comp f e₁.hom) _auto✝)
(comm₂ : autoParam (CategoryTheory.CategoryStruct.comp e₀.hom g' = CategoryTheory.CategoryStruct.comp g e₁.hom) _auto✝)
(comm₃ : autoParam (CategoryTheory.CategoryStruct.comp e.hom c'.ι = CategoryTheory.CategoryStruct.comp c.ι e₀.hom) _auto✝)
:
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.
Instances For
@[simp]
theorem
CategoryTheory.Limits.Cofork.mkHom_hom
{C : Type u}
[CategoryTheory.Category.{v, u} C]
{X : C}
{Y : C}
{f : X ⟶ Y}
{g : X ⟶ Y}
{s : CategoryTheory.Limits.Cofork f g}
{t : CategoryTheory.Limits.Cofork f g}
(k : s.pt ⟶ t.pt)
(w : CategoryTheory.CategoryStruct.comp s.π k = t.π)
:
(CategoryTheory.Limits.Cofork.mkHom k w).hom = k
def
CategoryTheory.Limits.Cofork.mkHom
{C : Type u}
[CategoryTheory.Category.{v, u} C]
{X : C}
{Y : C}
{f : X ⟶ Y}
{g : X ⟶ Y}
{s : CategoryTheory.Limits.Cofork f g}
{t : CategoryTheory.Limits.Cofork f g}
(k : s.pt ⟶ t.pt)
(w : CategoryTheory.CategoryStruct.comp s.π k = t.π)
:
s ⟶ t
Helper function for constructing morphisms between coequalizer coforks.
Equations
- CategoryTheory.Limits.Cofork.mkHom k w = { hom := k, w := ⋯ }
Instances For
@[simp]
theorem
CategoryTheory.Limits.Fork.hom_comp_ι_assoc
{C : Type u}
[CategoryTheory.Category.{v, u} C]
{X : C}
{Y : C}
{f : X ⟶ Y}
{g : X ⟶ Y}
{s : CategoryTheory.Limits.Fork f✝ g}
{t : CategoryTheory.Limits.Fork f✝ g}
(f : s ⟶ t)
{Z : C}
(h : (CategoryTheory.Limits.parallelPair f✝ g).obj CategoryTheory.Limits.WalkingParallelPair.zero ⟶ Z)
:
@[simp]
theorem
CategoryTheory.Limits.Fork.hom_comp_ι
{C : Type u}
[CategoryTheory.Category.{v, u} C]
{X : C}
{Y : C}
{f : X ⟶ Y}
{g : X ⟶ Y}
{s : CategoryTheory.Limits.Fork f✝ g}
{t : CategoryTheory.Limits.Fork f✝ g}
(f : s ⟶ t)
:
CategoryTheory.CategoryStruct.comp f.hom t.ι = s.ι
@[simp]
theorem
CategoryTheory.Limits.Fork.π_comp_hom_assoc
{C : Type u}
[CategoryTheory.Category.{v, u} C]
{X : C}
{Y : C}
{f : X ⟶ Y}
{g : X ⟶ Y}
{s : CategoryTheory.Limits.Cofork f✝ g}
{t : CategoryTheory.Limits.Cofork f✝ g}
(f : s ⟶ t)
{Z : C}
(h : t.pt ⟶ Z)
:
@[simp]
theorem
CategoryTheory.Limits.Fork.π_comp_hom
{C : Type u}
[CategoryTheory.Category.{v, u} C]
{X : C}
{Y : C}
{f : X ⟶ Y}
{g : X ⟶ Y}
{s : CategoryTheory.Limits.Cofork f✝ g}
{t : CategoryTheory.Limits.Cofork f✝ g}
(f : s ⟶ t)
:
CategoryTheory.CategoryStruct.comp s.π f.hom = t.π
@[simp]
theorem
CategoryTheory.Limits.Cofork.ext_hom
{C : Type u}
[CategoryTheory.Category.{v, u} C]
{X : C}
{Y : C}
{f : X ⟶ Y}
{g : X ⟶ Y}
{s : CategoryTheory.Limits.Cofork f g}
{t : CategoryTheory.Limits.Cofork f g}
(i : s.pt ≅ t.pt)
(w : autoParam (CategoryTheory.CategoryStruct.comp s.π i.hom = t.π) _auto✝)
:
(CategoryTheory.Limits.Cofork.ext i w).hom = CategoryTheory.Limits.Cofork.mkHom i.hom w
@[simp]
theorem
CategoryTheory.Limits.Cofork.ext_inv
{C : Type u}
[CategoryTheory.Category.{v, u} C]
{X : C}
{Y : C}
{f : X ⟶ Y}
{g : X ⟶ Y}
{s : CategoryTheory.Limits.Cofork f g}
{t : CategoryTheory.Limits.Cofork f g}
(i : s.pt ≅ t.pt)
(w : autoParam (CategoryTheory.CategoryStruct.comp s.π i.hom = t.π) _auto✝)
:
(CategoryTheory.Limits.Cofork.ext i w).inv = CategoryTheory.Limits.Cofork.mkHom i.inv ⋯
def
CategoryTheory.Limits.Cofork.ext
{C : Type u}
[CategoryTheory.Category.{v, u} C]
{X : C}
{Y : C}
{f : X ⟶ Y}
{g : X ⟶ Y}
{s : CategoryTheory.Limits.Cofork f g}
{t : CategoryTheory.Limits.Cofork f g}
(i : s.pt ≅ t.pt)
(w : autoParam (CategoryTheory.CategoryStruct.comp s.π i.hom = t.π) _auto✝)
:
s ≅ t
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 := ⋯ }
Instances For
def
CategoryTheory.Limits.Cofork.isoCoforkOfπ
{C : Type u}
[CategoryTheory.Category.{v, u} C]
{X : C}
{Y : C}
{f : X ⟶ Y}
{g : X ⟶ Y}
(c : CategoryTheory.Limits.Cofork f g)
:
c ≅ CategoryTheory.Limits.Cofork.ofπ c.π ⋯
Every cofork is isomorphic to one of the form Cofork.ofπ _ _.
Equations
- c.isoCoforkOfπ = CategoryTheory.Limits.Cofork.ext (id (CategoryTheory.Iso.refl c.pt)) ⋯
Instances For
@[reducible, inline]
abbrev
CategoryTheory.Limits.HasEqualizer
{C : Type u}
[CategoryTheory.Category.{v, u} C]
{X : C}
{Y : C}
(f : X ⟶ Y)
(g : X ⟶ Y)
:
HasEqualizer f g represents a particular choice of limiting cone
for the parallel pair of morphisms f and g.
Equations
Instances For
@[reducible, inline]
noncomputable abbrev
CategoryTheory.Limits.equalizer
{C : Type u}
[CategoryTheory.Category.{v, u} C]
{X : C}
{Y : C}
(f : X ⟶ Y)
(g : X ⟶ Y)
[CategoryTheory.Limits.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.
Equations
Instances For
@[reducible, inline]
noncomputable abbrev
CategoryTheory.Limits.equalizer.ι
{C : Type u}
[CategoryTheory.Category.{v, u} C]
{X : C}
{Y : C}
(f : X ⟶ Y)
(g : X ⟶ Y)
[CategoryTheory.Limits.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
Instances For
@[reducible, inline]
noncomputable abbrev
CategoryTheory.Limits.equalizer.fork
{C : Type u}
[CategoryTheory.Category.{v, u} C]
{X : C}
{Y : C}
(f : X ⟶ Y)
(g : X ⟶ Y)
[CategoryTheory.Limits.HasEqualizer f g]
:
An equalizer cone for a parallel pair f and g
Equations
Instances For
@[simp]
theorem
CategoryTheory.Limits.equalizer.fork_ι
{C : Type u}
[CategoryTheory.Category.{v, u} C]
{X : C}
{Y : C}
(f : X ⟶ Y)
(g : X ⟶ Y)
[CategoryTheory.Limits.HasEqualizer f g]
:
@[simp]
theorem
CategoryTheory.Limits.equalizer.fork_π_app_zero
{C : Type u}
[CategoryTheory.Category.{v, u} C]
{X : C}
{Y : C}
(f : X ⟶ Y)
(g : X ⟶ Y)
[CategoryTheory.Limits.HasEqualizer f g]
:
theorem
CategoryTheory.Limits.equalizer.condition_assoc
{C : Type u}
[CategoryTheory.Category.{v, u} C]
{X : C}
{Y : C}
(f : X ⟶ Y)
(g : X ⟶ Y)
[CategoryTheory.Limits.HasEqualizer f g]
{Z : C}
(h : Y ⟶ Z)
:
theorem
CategoryTheory.Limits.equalizer.condition
{C : Type u}
[CategoryTheory.Category.{v, u} C]
{X : C}
{Y : C}
(f : X ⟶ Y)
(g : X ⟶ Y)
[CategoryTheory.Limits.HasEqualizer f g]
:
noncomputable def
CategoryTheory.Limits.equalizerIsEqualizer
{C : Type u}
[CategoryTheory.Category.{v, u} C]
{X : C}
{Y : C}
(f : X ⟶ Y)
(g : X ⟶ Y)
[CategoryTheory.Limits.HasEqualizer f g]
:
The equalizer built from equalizer.ι f g is limiting.
Equations
- One or more equations did not get rendered due to their size.
Instances For
@[reducible, inline]
noncomputable abbrev
CategoryTheory.Limits.equalizer.lift
{C : Type u}
[CategoryTheory.Category.{v, u} C]
{X : C}
{Y : C}
{f : X ⟶ Y}
{g : X ⟶ Y}
[CategoryTheory.Limits.HasEqualizer f g]
{W : C}
(k : W ⟶ X)
(h : CategoryTheory.CategoryStruct.comp k f = CategoryTheory.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.
Equations
Instances For
theorem
CategoryTheory.Limits.equalizer.lift_ι_assoc
{C : Type u}
[CategoryTheory.Category.{v, u} C]
{X : C}
{Y : C}
{f : X ⟶ Y}
{g : X ⟶ Y}
[CategoryTheory.Limits.HasEqualizer f g]
{W : C}
(k : W ⟶ X)
(h : CategoryTheory.CategoryStruct.comp k f = CategoryTheory.CategoryStruct.comp k g)
{Z : C}
(h : X ⟶ Z)
:
theorem
CategoryTheory.Limits.equalizer.lift_ι
{C : Type u}
[CategoryTheory.Category.{v, u} C]
{X : C}
{Y : C}
{f : X ⟶ Y}
{g : X ⟶ Y}
[CategoryTheory.Limits.HasEqualizer f g]
{W : C}
(k : W ⟶ X)
(h : CategoryTheory.CategoryStruct.comp k f = CategoryTheory.CategoryStruct.comp k g)
:
noncomputable def
CategoryTheory.Limits.equalizer.lift'
{C : Type u}
[CategoryTheory.Category.{v, u} C]
{X : C}
{Y : C}
{f : X ⟶ Y}
{g : X ⟶ Y}
[CategoryTheory.Limits.HasEqualizer f g]
{W : C}
(k : W ⟶ X)
(h : CategoryTheory.CategoryStruct.comp k f = CategoryTheory.CategoryStruct.comp k g)
:
{ l : W ⟶ CategoryTheory.Limits.equalizer f g //
CategoryTheory.CategoryStruct.comp l (CategoryTheory.Limits.equalizer.ι f g) = k }
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
Instances For
theorem
CategoryTheory.Limits.equalizer.hom_ext_iff
{C : Type u}
[CategoryTheory.Category.{v, u} C]
{X : C}
{Y : C}
{f : X ⟶ Y}
{g : X ⟶ Y}
[CategoryTheory.Limits.HasEqualizer f g]
{W : C}
{k : W ⟶ CategoryTheory.Limits.equalizer f g}
{l : W ⟶ CategoryTheory.Limits.equalizer f g}
:
theorem
CategoryTheory.Limits.equalizer.hom_ext
{C : Type u}
[CategoryTheory.Category.{v, u} C]
{X : C}
{Y : C}
{f : X ⟶ Y}
{g : X ⟶ Y}
[CategoryTheory.Limits.HasEqualizer f g]
{W : C}
{k : W ⟶ CategoryTheory.Limits.equalizer f g}
{l : W ⟶ CategoryTheory.Limits.equalizer f g}
(h : CategoryTheory.CategoryStruct.comp k (CategoryTheory.Limits.equalizer.ι f g) = CategoryTheory.CategoryStruct.comp l (CategoryTheory.Limits.equalizer.ι f g))
:
k = l
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}
[CategoryTheory.Category.{v, u} C]
{X : C}
{Y : C}
{f : X ⟶ Y}
{g : X ⟶ Y}
[CategoryTheory.Limits.HasEqualizer f g]
{W : C}
(k : W ⟶ X)
(h : CategoryTheory.CategoryStruct.comp k f = CategoryTheory.CategoryStruct.comp k g)
:
∃! l : W ⟶ CategoryTheory.Limits.equalizer f g,
CategoryTheory.CategoryStruct.comp l (CategoryTheory.Limits.equalizer.ι f g) = k
instance
CategoryTheory.Limits.equalizer.ι_mono
{C : Type u}
[CategoryTheory.Category.{v, u} C]
{X : C}
{Y : C}
{f : X ⟶ Y}
{g : X ⟶ Y}
[CategoryTheory.Limits.HasEqualizer f g]
:
An equalizer morphism is a monomorphism
Equations
- ⋯ = ⋯
theorem
CategoryTheory.Limits.mono_of_isLimit_fork
{C : Type u}
[CategoryTheory.Category.{v, u} C]
{X : C}
{Y : C}
{f : X ⟶ Y}
{g : X ⟶ Y}
{c : CategoryTheory.Limits.Fork f g}
(i : CategoryTheory.Limits.IsLimit c)
:
The equalizer morphism in any limit cone is a monomorphism.
def
CategoryTheory.Limits.idFork
{C : Type u}
[CategoryTheory.Category.{v, u} C]
{X : C}
{Y : C}
{f : X ⟶ Y}
{g : X ⟶ Y}
(h : f = g)
:
The identity determines a cone on the equalizer diagram of f and g if f = g.
Equations
Instances For
def
CategoryTheory.Limits.isLimitIdFork
{C : Type u}
[CategoryTheory.Category.{v, u} C]
{X : C}
{Y : C}
{f : X ⟶ Y}
{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.ι) ⋯ ⋯
Instances For
theorem
CategoryTheory.Limits.isIso_limit_cone_parallelPair_of_eq
{C : Type u}
[CategoryTheory.Category.{v, u} C]
{X : C}
{Y : C}
{f : X ⟶ Y}
{g : X ⟶ Y}
(h₀ : f = g)
{c : CategoryTheory.Limits.Fork f g}
(h : CategoryTheory.Limits.IsLimit c)
:
Every equalizer of (f, g), where f = g, is an isomorphism.
theorem
CategoryTheory.Limits.equalizer.ι_of_eq
{C : Type u}
[CategoryTheory.Category.{v, u} C]
{X : C}
{Y : C}
{f : X ⟶ Y}
{g : X ⟶ Y}
[CategoryTheory.Limits.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}
[CategoryTheory.Category.{v, u} C]
{X : C}
{Y : C}
{f : X ⟶ Y}
{c : CategoryTheory.Limits.Fork f f}
(h : CategoryTheory.Limits.IsLimit c)
:
Every equalizer of (f, f) is an isomorphism.
theorem
CategoryTheory.Limits.isIso_limit_cone_parallelPair_of_epi
{C : Type u}
[CategoryTheory.Category.{v, u} C]
{X : C}
{Y : C}
{f : X ⟶ Y}
{g : X ⟶ Y}
{c : CategoryTheory.Limits.Fork f g}
(h : CategoryTheory.Limits.IsLimit c)
[CategoryTheory.Epi c.ι]
:
An equalizer that is an epimorphism is an isomorphism.
theorem
CategoryTheory.Limits.eq_of_epi_fork_ι
{C : Type u}
[CategoryTheory.Category.{v, u} C]
{X : C}
{Y : C}
{f : X ⟶ Y}
{g : X ⟶ Y}
(t : CategoryTheory.Limits.Fork f g)
[CategoryTheory.Epi t.ι]
:
f = g
Two morphisms are equal if there is a fork whose inclusion is epi.
theorem
CategoryTheory.Limits.eq_of_epi_equalizer
{C : Type u}
[CategoryTheory.Category.{v, u} C]
{X : C}
{Y : C}
{f : X ⟶ Y}
{g : X ⟶ Y}
[CategoryTheory.Limits.HasEqualizer f g]
[CategoryTheory.Epi (CategoryTheory.Limits.equalizer.ι f g)]
:
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}
[CategoryTheory.Category.{v, u} C]
{X : C}
{Y : C}
(f : X ⟶ Y)
:
Equations
- ⋯ = ⋯
instance
CategoryTheory.Limits.equalizer.ι_of_self
{C : Type u}
[CategoryTheory.Category.{v, u} C]
{X : C}
{Y : C}
(f : X ⟶ Y)
:
The equalizer inclusion for (f, f) is an isomorphism.
Equations
- ⋯ = ⋯
noncomputable def
CategoryTheory.Limits.equalizer.isoSourceOfSelf
{C : Type u}
[CategoryTheory.Category.{v, u} C]
{X : C}
{Y : C}
(f : X ⟶ Y)
:
The equalizer of a morphism with itself is isomorphic to the source.
Equations
Instances For
@[simp]
theorem
CategoryTheory.Limits.equalizer.isoSourceOfSelf_hom
{C : Type u}
[CategoryTheory.Category.{v, u} C]
{X : C}
{Y : C}
(f : X ⟶ Y)
:
@[simp]
theorem
CategoryTheory.Limits.equalizer.isoSourceOfSelf_inv
{C : Type u}
[CategoryTheory.Category.{v, u} C]
{X : C}
{Y : C}
(f : X ⟶ Y)
:
@[reducible, inline]
abbrev
CategoryTheory.Limits.HasCoequalizer
{C : Type u}
[CategoryTheory.Category.{v, u} C]
{X : C}
{Y : C}
(f : X ⟶ Y)
(g : X ⟶ Y)
:
HasCoequalizer f g represents a particular choice of colimiting cocone
for the parallel pair of morphisms f and g.
Equations
Instances For
@[reducible, inline]
noncomputable abbrev
CategoryTheory.Limits.coequalizer
{C : Type u}
[CategoryTheory.Category.{v, u} C]
{X : C}
{Y : C}
(f : X ⟶ Y)
(g : X ⟶ Y)
[CategoryTheory.Limits.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.
Equations
Instances For
@[reducible, inline]
noncomputable abbrev
CategoryTheory.Limits.coequalizer.π
{C : Type u}
[CategoryTheory.Category.{v, u} C]
{X : C}
{Y : C}
(f : X ⟶ Y)
(g : X ⟶ Y)
[CategoryTheory.Limits.HasCoequalizer f g]
:
If a coequalizer of f and g exists, we can access the corresponding projection by
saying coequalizer.π f g.
Equations
Instances For
@[reducible, inline]
noncomputable abbrev
CategoryTheory.Limits.coequalizer.cofork
{C : Type u}
[CategoryTheory.Category.{v, u} C]
{X : C}
{Y : C}
(f : X ⟶ Y)
(g : X ⟶ Y)
[CategoryTheory.Limits.HasCoequalizer f g]
:
An arbitrary choice of coequalizer cocone for a parallel pair f and g.
Equations
Instances For
@[simp]
theorem
CategoryTheory.Limits.coequalizer.cofork_π
{C : Type u}
[CategoryTheory.Category.{v, u} C]
{X : C}
{Y : C}
(f : X ⟶ Y)
(g : X ⟶ Y)
[CategoryTheory.Limits.HasCoequalizer f g]
:
theorem
CategoryTheory.Limits.coequalizer.cofork_ι_app_one
{C : Type u}
[CategoryTheory.Category.{v, u} C]
{X : C}
{Y : C}
(f : X ⟶ Y)
(g : X ⟶ Y)
[CategoryTheory.Limits.HasCoequalizer f g]
:
theorem
CategoryTheory.Limits.coequalizer.condition_assoc
{C : Type u}
[CategoryTheory.Category.{v, u} C]
{X : C}
{Y : C}
(f : X ⟶ Y)
(g : X ⟶ Y)
[CategoryTheory.Limits.HasCoequalizer f g]
{Z : C}
(h : CategoryTheory.Limits.coequalizer f g ⟶ Z)
:
theorem
CategoryTheory.Limits.coequalizer.condition
{C : Type u}
[CategoryTheory.Category.{v, u} C]
{X : C}
{Y : C}
(f : X ⟶ Y)
(g : X ⟶ Y)
[CategoryTheory.Limits.HasCoequalizer f g]
:
noncomputable def
CategoryTheory.Limits.coequalizerIsCoequalizer
{C : Type u}
[CategoryTheory.Category.{v, u} C]
{X : C}
{Y : C}
(f : X ⟶ Y)
(g : X ⟶ Y)
[CategoryTheory.Limits.HasCoequalizer f g]
:
The cofork built from coequalizer.π f g is colimiting.
Equations
- One or more equations did not get rendered due to their size.
Instances For
@[reducible, inline]
noncomputable abbrev
CategoryTheory.Limits.coequalizer.desc
{C : Type u}
[CategoryTheory.Category.{v, u} C]
{X : C}
{Y : C}
{f : X ⟶ Y}
{g : X ⟶ Y}
[CategoryTheory.Limits.HasCoequalizer f g]
{W : C}
(k : Y ⟶ W)
(h : CategoryTheory.CategoryStruct.comp f k = CategoryTheory.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.
Equations
Instances For
theorem
CategoryTheory.Limits.coequalizer.π_desc_assoc
{C : Type u}
[CategoryTheory.Category.{v, u} C]
{X : C}
{Y : C}
{f : X ⟶ Y}
{g : X ⟶ Y}
[CategoryTheory.Limits.HasCoequalizer f g]
{W : C}
(k : Y ⟶ W)
(h : CategoryTheory.CategoryStruct.comp f k = CategoryTheory.CategoryStruct.comp g k)
{Z : C}
(h : W ⟶ Z)
:
theorem
CategoryTheory.Limits.coequalizer.π_desc
{C : Type u}
[CategoryTheory.Category.{v, u} C]
{X : C}
{Y : C}
{f : X ⟶ Y}
{g : X ⟶ Y}
[CategoryTheory.Limits.HasCoequalizer f g]
{W : C}
(k : Y ⟶ W)
(h : CategoryTheory.CategoryStruct.comp f k = CategoryTheory.CategoryStruct.comp g k)
:
theorem
CategoryTheory.Limits.coequalizer.π_colimMap_desc
{C : Type u}
[CategoryTheory.Category.{v, u} C]
{X : C}
{Y : C}
{f : X ⟶ Y}
{g : X ⟶ Y}
[CategoryTheory.Limits.HasCoequalizer f g]
{X' : C}
{Y' : C}
{Z : C}
(f' : X' ⟶ Y')
(g' : X' ⟶ Y')
[CategoryTheory.Limits.HasCoequalizer f' g']
(p : X ⟶ X')
(q : Y ⟶ Y')
(wf : CategoryTheory.CategoryStruct.comp f q = CategoryTheory.CategoryStruct.comp p f')
(wg : CategoryTheory.CategoryStruct.comp g q = CategoryTheory.CategoryStruct.comp p g')
(h : Y' ⟶ Z)
(wh : CategoryTheory.CategoryStruct.comp f' h = CategoryTheory.CategoryStruct.comp g' h)
:
noncomputable def
CategoryTheory.Limits.coequalizer.desc'
{C : Type u}
[CategoryTheory.Category.{v, u} C]
{X : C}
{Y : C}
{f : X ⟶ Y}
{g : X ⟶ Y}
[CategoryTheory.Limits.HasCoequalizer f g]
{W : C}
(k : Y ⟶ W)
(h : CategoryTheory.CategoryStruct.comp f k = CategoryTheory.CategoryStruct.comp g k)
:
{ l : CategoryTheory.Limits.coequalizer f g ⟶ W //
CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.coequalizer.π f g) l = k }
Any morphism k : Y ⟶ W satisfying f ≫ k = g ≫ k induces a morphism
l : coequalizer f g ⟶ W satisfying coequalizer.π ≫ g = l.
Equations
Instances For
theorem
CategoryTheory.Limits.coequalizer.hom_ext_iff
{C : Type u}
[CategoryTheory.Category.{v, u} C]
{X : C}
{Y : C}
{f : X ⟶ Y}
{g : X ⟶ Y}
[CategoryTheory.Limits.HasCoequalizer f g]
{W : C}
{k : CategoryTheory.Limits.coequalizer f g ⟶ W}
{l : CategoryTheory.Limits.coequalizer f g ⟶ W}
:
theorem
CategoryTheory.Limits.coequalizer.hom_ext
{C : Type u}
[CategoryTheory.Category.{v, u} C]
{X : C}
{Y : C}
{f : X ⟶ Y}
{g : X ⟶ Y}
[CategoryTheory.Limits.HasCoequalizer f g]
{W : C}
{k : CategoryTheory.Limits.coequalizer f g ⟶ W}
{l : CategoryTheory.Limits.coequalizer f g ⟶ W}
(h : CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.coequalizer.π f g) k = CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.coequalizer.π f g) l)
:
k = 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}
[CategoryTheory.Category.{v, u} C]
{X : C}
{Y : C}
{f : X ⟶ Y}
{g : X ⟶ Y}
[CategoryTheory.Limits.HasCoequalizer f g]
{W : C}
(k : Y ⟶ W)
(h : CategoryTheory.CategoryStruct.comp f k = CategoryTheory.CategoryStruct.comp g k)
:
∃! d : CategoryTheory.Limits.coequalizer f g ⟶ W,
CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.coequalizer.π f g) d = k
instance
CategoryTheory.Limits.coequalizer.π_epi
{C : Type u}
[CategoryTheory.Category.{v, u} C]
{X : C}
{Y : C}
{f : X ⟶ Y}
{g : X ⟶ Y}
[CategoryTheory.Limits.HasCoequalizer f g]
:
A coequalizer morphism is an epimorphism
Equations
- ⋯ = ⋯
theorem
CategoryTheory.Limits.epi_of_isColimit_cofork
{C : Type u}
[CategoryTheory.Category.{v, u} C]
{X : C}
{Y : C}
{f : X ⟶ Y}
{g : X ⟶ Y}
{c : CategoryTheory.Limits.Cofork f g}
(i : CategoryTheory.Limits.IsColimit c)
:
The coequalizer morphism in any colimit cocone is an epimorphism.
def
CategoryTheory.Limits.idCofork
{C : Type u}
[CategoryTheory.Category.{v, u} C]
{X : C}
{Y : C}
{f : X ⟶ Y}
{g : X ⟶ Y}
(h : f = g)
:
The identity determines a cocone on the coequalizer diagram of f and g, if f = g.
Equations
Instances For
def
CategoryTheory.Limits.isColimitIdCofork
{C : Type u}
[CategoryTheory.Category.{v, u} C]
{X : C}
{Y : C}
{f : X ⟶ Y}
{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.π) ⋯ ⋯
Instances For
theorem
CategoryTheory.Limits.isIso_colimit_cocone_parallelPair_of_eq
{C : Type u}
[CategoryTheory.Category.{v, u} C]
{X : C}
{Y : C}
{f : X ⟶ Y}
{g : X ⟶ Y}
(h₀ : f = g)
{c : CategoryTheory.Limits.Cofork f g}
(h : CategoryTheory.Limits.IsColimit c)
:
Every coequalizer of (f, g), where f = g, is an isomorphism.
theorem
CategoryTheory.Limits.coequalizer.π_of_eq
{C : Type u}
[CategoryTheory.Category.{v, u} C]
{X : C}
{Y : C}
{f : X ⟶ Y}
{g : X ⟶ Y}
[CategoryTheory.Limits.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}
[CategoryTheory.Category.{v, u} C]
{X : C}
{Y : C}
{f : X ⟶ Y}
{c : CategoryTheory.Limits.Cofork f f}
(h : CategoryTheory.Limits.IsColimit c)
:
Every coequalizer of (f, f) is an isomorphism.
theorem
CategoryTheory.Limits.isIso_limit_cocone_parallelPair_of_epi
{C : Type u}
[CategoryTheory.Category.{v, u} C]
{X : C}
{Y : C}
{f : X ⟶ Y}
{g : X ⟶ Y}
{c : CategoryTheory.Limits.Cofork f g}
(h : CategoryTheory.Limits.IsColimit c)
[CategoryTheory.Mono c.π]
:
A coequalizer that is a monomorphism is an isomorphism.
theorem
CategoryTheory.Limits.eq_of_mono_cofork_π
{C : Type u}
[CategoryTheory.Category.{v, u} C]
{X : C}
{Y : C}
{f : X ⟶ Y}
{g : X ⟶ Y}
(t : CategoryTheory.Limits.Cofork f g)
[CategoryTheory.Mono t.π]
:
f = g
Two morphisms are equal if there is a cofork whose projection is mono.
theorem
CategoryTheory.Limits.eq_of_mono_coequalizer
{C : Type u}
[CategoryTheory.Category.{v, u} C]
{X : C}
{Y : C}
{f : X ⟶ Y}
{g : X ⟶ Y}
[CategoryTheory.Limits.HasCoequalizer f g]
[CategoryTheory.Mono (CategoryTheory.Limits.coequalizer.π f g)]
:
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}
[CategoryTheory.Category.{v, u} C]
{X : C}
{Y : C}
(f : X ⟶ Y)
:
Equations
- ⋯ = ⋯
instance
CategoryTheory.Limits.coequalizer.π_of_self
{C : Type u}
[CategoryTheory.Category.{v, u} C]
{X : C}
{Y : C}
(f : X ⟶ Y)
:
The coequalizer projection for (f, f) is an isomorphism.
Equations
- ⋯ = ⋯
noncomputable def
CategoryTheory.Limits.coequalizer.isoTargetOfSelf
{C : Type u}
[CategoryTheory.Category.{v, u} C]
{X : C}
{Y : C}
(f : X ⟶ Y)
:
The coequalizer of a morphism with itself is isomorphic to the target.
Equations
Instances For
@[simp]
theorem
CategoryTheory.Limits.coequalizer.isoTargetOfSelf_hom
{C : Type u}
[CategoryTheory.Category.{v, u} C]
{X : C}
{Y : C}
(f : X ⟶ Y)
:
@[simp]
theorem
CategoryTheory.Limits.coequalizer.isoTargetOfSelf_inv
{C : Type u}
[CategoryTheory.Category.{v, u} C]
{X : C}
{Y : C}
(f : X ⟶ Y)
:
noncomputable def
CategoryTheory.Limits.equalizerComparison
{C : Type u}
[CategoryTheory.Category.{v, u} C]
{X : C}
{Y : C}
(f : X ⟶ Y)
(g : X ⟶ Y)
{D : Type u₂}
[CategoryTheory.Category.{v₂, u₂} D]
(G : CategoryTheory.Functor C D)
[CategoryTheory.Limits.HasEqualizer f g]
[CategoryTheory.Limits.HasEqualizer (G.map f) (G.map g)]
:
G.obj (CategoryTheory.Limits.equalizer f g) ⟶ CategoryTheory.Limits.equalizer (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
Instances For
@[simp]
theorem
CategoryTheory.Limits.equalizerComparison_comp_π_assoc
{C : Type u}
[CategoryTheory.Category.{v, u} C]
{X : C}
{Y : C}
(f : X ⟶ Y)
(g : X ⟶ Y)
{D : Type u₂}
[CategoryTheory.Category.{v₂, u₂} D]
(G : CategoryTheory.Functor C D)
[CategoryTheory.Limits.HasEqualizer f g]
[CategoryTheory.Limits.HasEqualizer (G.map f) (G.map g)]
{Z : D}
(h : G.obj X ⟶ Z)
:
CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.equalizerComparison f g G)
(CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.equalizer.ι (G.map f) (G.map g)) h) = CategoryTheory.CategoryStruct.comp (G.map (CategoryTheory.Limits.equalizer.ι f g)) h
@[simp]
theorem
CategoryTheory.Limits.equalizerComparison_comp_π
{C : Type u}
[CategoryTheory.Category.{v, u} C]
{X : C}
{Y : C}
(f : X ⟶ Y)
(g : X ⟶ Y)
{D : Type u₂}
[CategoryTheory.Category.{v₂, u₂} D]
(G : CategoryTheory.Functor C D)
[CategoryTheory.Limits.HasEqualizer f g]
[CategoryTheory.Limits.HasEqualizer (G.map f) (G.map g)]
:
CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.equalizerComparison f g G)
(CategoryTheory.Limits.equalizer.ι (G.map f) (G.map g)) = G.map (CategoryTheory.Limits.equalizer.ι f g)
@[simp]
theorem
CategoryTheory.Limits.map_lift_equalizerComparison_assoc
{C : Type u}
[CategoryTheory.Category.{v, u} C]
{X : C}
{Y : C}
(f : X ⟶ Y)
(g : X ⟶ Y)
{D : Type u₂}
[CategoryTheory.Category.{v₂, u₂} D]
(G : CategoryTheory.Functor C D)
[CategoryTheory.Limits.HasEqualizer f g]
[CategoryTheory.Limits.HasEqualizer (G.map f) (G.map g)]
{Z : C}
{h : Z✝ ⟶ X}
(w : CategoryTheory.CategoryStruct.comp h✝ f = CategoryTheory.CategoryStruct.comp h✝ g)
{Z : D}
(h : CategoryTheory.Limits.equalizer (G.map f) (G.map g) ⟶ Z)
:
@[simp]
theorem
CategoryTheory.Limits.map_lift_equalizerComparison
{C : Type u}
[CategoryTheory.Category.{v, u} C]
{X : C}
{Y : C}
(f : X ⟶ Y)
(g : X ⟶ Y)
{D : Type u₂}
[CategoryTheory.Category.{v₂, u₂} D]
(G : CategoryTheory.Functor C D)
[CategoryTheory.Limits.HasEqualizer f g]
[CategoryTheory.Limits.HasEqualizer (G.map f) (G.map g)]
{Z : C}
{h : Z ⟶ X}
(w : CategoryTheory.CategoryStruct.comp h f = CategoryTheory.CategoryStruct.comp h g)
:
CategoryTheory.CategoryStruct.comp (G.map (CategoryTheory.Limits.equalizer.lift h w))
(CategoryTheory.Limits.equalizerComparison f g G) = CategoryTheory.Limits.equalizer.lift (G.map h) ⋯
noncomputable def
CategoryTheory.Limits.coequalizerComparison
{C : Type u}
[CategoryTheory.Category.{v, u} C]
{X : C}
{Y : C}
(f : X ⟶ Y)
(g : X ⟶ Y)
{D : Type u₂}
[CategoryTheory.Category.{v₂, u₂} D]
(G : CategoryTheory.Functor C D)
[CategoryTheory.Limits.HasCoequalizer f g]
[CategoryTheory.Limits.HasCoequalizer (G.map f) (G.map g)]
:
CategoryTheory.Limits.coequalizer (G.map f) (G.map g) ⟶ G.obj (CategoryTheory.Limits.coequalizer f g)
The comparison morphism for the coequalizer of f,g.
Equations
Instances For
@[simp]
theorem
CategoryTheory.Limits.ι_comp_coequalizerComparison_assoc
{C : Type u}
[CategoryTheory.Category.{v, u} C]
{X : C}
{Y : C}
(f : X ⟶ Y)
(g : X ⟶ Y)
{D : Type u₂}
[CategoryTheory.Category.{v₂, u₂} D]
(G : CategoryTheory.Functor C D)
[CategoryTheory.Limits.HasCoequalizer f g]
[CategoryTheory.Limits.HasCoequalizer (G.map f) (G.map g)]
{Z : D}
(h : G.obj (CategoryTheory.Limits.coequalizer f g) ⟶ Z)
:
CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.coequalizer.π (G.map f) (G.map g))
(CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.coequalizerComparison f g G) h) = CategoryTheory.CategoryStruct.comp (G.map (CategoryTheory.Limits.coequalizer.π f g)) h
@[simp]
theorem
CategoryTheory.Limits.ι_comp_coequalizerComparison
{C : Type u}
[CategoryTheory.Category.{v, u} C]
{X : C}
{Y : C}
(f : X ⟶ Y)
(g : X ⟶ Y)
{D : Type u₂}
[CategoryTheory.Category.{v₂, u₂} D]
(G : CategoryTheory.Functor C D)
[CategoryTheory.Limits.HasCoequalizer f g]
[CategoryTheory.Limits.HasCoequalizer (G.map f) (G.map g)]
:
CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.coequalizer.π (G.map f) (G.map g))
(CategoryTheory.Limits.coequalizerComparison f g G) = G.map (CategoryTheory.Limits.coequalizer.π f g)
@[simp]
theorem
CategoryTheory.Limits.coequalizerComparison_map_desc_assoc
{C : Type u}
[CategoryTheory.Category.{v, u} C]
{X : C}
{Y : C}
(f : X ⟶ Y)
(g : X ⟶ Y)
{D : Type u₂}
[CategoryTheory.Category.{v₂, u₂} D]
(G : CategoryTheory.Functor C D)
[CategoryTheory.Limits.HasCoequalizer f g]
[CategoryTheory.Limits.HasCoequalizer (G.map f) (G.map g)]
{Z : C}
{h : Y ⟶ Z✝}
(w : CategoryTheory.CategoryStruct.comp f h✝ = CategoryTheory.CategoryStruct.comp g h✝)
{Z : D}
(h : G.obj Z✝ ⟶ Z)
:
@[simp]
theorem
CategoryTheory.Limits.coequalizerComparison_map_desc
{C : Type u}
[CategoryTheory.Category.{v, u} C]
{X : C}
{Y : C}
(f : X ⟶ Y)
(g : X ⟶ Y)
{D : Type u₂}
[CategoryTheory.Category.{v₂, u₂} D]
(G : CategoryTheory.Functor C D)
[CategoryTheory.Limits.HasCoequalizer f g]
[CategoryTheory.Limits.HasCoequalizer (G.map f) (G.map g)]
{Z : C}
{h : Y ⟶ Z}
(w : CategoryTheory.CategoryStruct.comp f h = CategoryTheory.CategoryStruct.comp g h)
:
@[reducible, inline]
HasEqualizers represents a choice of equalizer for every pair of morphisms
Equations
Instances For
@[reducible, inline]
HasCoequalizers represents a choice of coequalizer for every pair of morphisms
Equations
Instances For
theorem
CategoryTheory.Limits.hasEqualizers_of_hasLimit_parallelPair
(C : Type u)
[CategoryTheory.Category.{v, u} C]
[∀ {X Y : C} {f g : X ⟶ Y}, CategoryTheory.Limits.HasLimit (CategoryTheory.Limits.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)
[CategoryTheory.Category.{v, u} C]
[∀ {X Y : C} {f g : X ⟶ Y}, CategoryTheory.Limits.HasColimit (CategoryTheory.Limits.parallelPair f g)]
:
If C has all colimits of diagrams parallelPair f g, then it has all coequalizers
@[simp]
theorem
CategoryTheory.Limits.coneOfIsSplitMono_pt
{C : Type u}
[CategoryTheory.Category.{v, u} C]
{X : C}
{Y : C}
(f : X ⟶ Y)
[CategoryTheory.IsSplitMono f]
:
(CategoryTheory.Limits.coneOfIsSplitMono f).pt = X
@[simp]
theorem
CategoryTheory.Limits.coneOfIsSplitMono_π_app
{C : Type u}
[CategoryTheory.Category.{v, u} C]
{X : C}
{Y : C}
(f : X✝ ⟶ Y)
[CategoryTheory.IsSplitMono f]
(X : CategoryTheory.Limits.WalkingParallelPair)
:
(CategoryTheory.Limits.coneOfIsSplitMono f).π.app X = CategoryTheory.Limits.WalkingParallelPair.rec (motive := fun (t : CategoryTheory.Limits.WalkingParallelPair) =>
X = t →
(X✝ ⟶ (CategoryTheory.Limits.parallelPair (CategoryTheory.CategoryStruct.id Y)
(CategoryTheory.CategoryStruct.comp (CategoryTheory.retraction f) f)).obj
X))
(fun (h : X = CategoryTheory.Limits.WalkingParallelPair.zero) => ⋯ ▸ f)
(fun (h : X = CategoryTheory.Limits.WalkingParallelPair.one) => ⋯ ▸ f) X ⋯
noncomputable def
CategoryTheory.Limits.coneOfIsSplitMono
{C : Type u}
[CategoryTheory.Category.{v, u} C]
{X : C}
{Y : C}
(f : X ⟶ Y)
[CategoryTheory.IsSplitMono 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.
Instances For
@[simp]
theorem
CategoryTheory.Limits.coneOfIsSplitMono_ι
{C : Type u}
[CategoryTheory.Category.{v, u} C]
{X : C}
{Y : C}
(f : X ⟶ Y)
[CategoryTheory.IsSplitMono f]
:
noncomputable def
CategoryTheory.Limits.isSplitMonoEqualizes
{C : Type u}
[CategoryTheory.Category.{v, u} C]
{X : C}
{Y : C}
(f : X ⟶ Y)
[CategoryTheory.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.
Instances For
def
CategoryTheory.Limits.splitMonoOfEqualizer
(C : Type u)
[CategoryTheory.Category.{v, u} C]
{X : C}
{Y : C}
{f : X ⟶ Y}
{r : Y ⟶ X}
(hr : CategoryTheory.CategoryStruct.comp f (CategoryTheory.CategoryStruct.comp r f) = f)
(h : CategoryTheory.Limits.IsLimit (CategoryTheory.Limits.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 := ⋯ }
Instances For
def
CategoryTheory.Limits.isEqualizerCompMono
{C : Type u}
[CategoryTheory.Category.{v, u} C]
{X : C}
{Y : C}
{f : X ⟶ Y}
{g : X ⟶ Y}
{c : CategoryTheory.Limits.Fork f g}
(i : CategoryTheory.Limits.IsLimit c)
{Z : C}
(h : Y ⟶ Z)
[hm : CategoryTheory.Mono h]
:
let_fun this := ⋯;
CategoryTheory.Limits.IsLimit (CategoryTheory.Limits.Fork.ofι c.ι ⋯)
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.
Instances For
theorem
CategoryTheory.Limits.hasEqualizer_comp_mono
(C : Type u)
[CategoryTheory.Category.{v, u} C]
{X : C}
{Y : C}
(f : X ⟶ Y)
(g : X ⟶ Y)
[CategoryTheory.Limits.HasEqualizer f g]
{Z : C}
(h : Y ⟶ Z)
[CategoryTheory.Mono h]
:
@[simp]
theorem
CategoryTheory.Limits.splitMonoOfIdempotentOfIsLimitFork_retraction
(C : Type u)
[CategoryTheory.Category.{v, u} C]
{X : C}
{f : X ⟶ X}
(hf : CategoryTheory.CategoryStruct.comp f f = f)
{c : CategoryTheory.Limits.Fork (CategoryTheory.CategoryStruct.id X) f}
(i : CategoryTheory.Limits.IsLimit c)
:
(CategoryTheory.Limits.splitMonoOfIdempotentOfIsLimitFork C hf i).retraction = i.lift (CategoryTheory.Limits.Fork.ofι f ⋯)
def
CategoryTheory.Limits.splitMonoOfIdempotentOfIsLimitFork
(C : Type u)
[CategoryTheory.Category.{v, u} C]
{X : C}
{f : X ⟶ X}
(hf : CategoryTheory.CategoryStruct.comp f f = f)
{c : CategoryTheory.Limits.Fork (CategoryTheory.CategoryStruct.id X) f}
(i : CategoryTheory.Limits.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 := ⋯ }
Instances For
noncomputable def
CategoryTheory.Limits.splitMonoOfIdempotentEqualizer
(C : Type u)
[CategoryTheory.Category.{v, u} C]
{X : C}
{f : X ⟶ X}
(hf : CategoryTheory.CategoryStruct.comp f f = f)
[CategoryTheory.Limits.HasEqualizer (CategoryTheory.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.
Instances For
@[simp]
theorem
CategoryTheory.Limits.coconeOfIsSplitEpi_pt
{C : Type u}
[CategoryTheory.Category.{v, u} C]
{X : C}
{Y : C}
(f : X ⟶ Y)
[CategoryTheory.IsSplitEpi f]
:
@[simp]
theorem
CategoryTheory.Limits.coconeOfIsSplitEpi_ι_app
{C : Type u}
[CategoryTheory.Category.{v, u} C]
{X : C}
{Y : C}
(f : X✝ ⟶ Y)
[CategoryTheory.IsSplitEpi f]
(X : CategoryTheory.Limits.WalkingParallelPair)
:
noncomputable def
CategoryTheory.Limits.coconeOfIsSplitEpi
{C : Type u}
[CategoryTheory.Category.{v, u} C]
{X : C}
{Y : C}
(f : X ⟶ Y)
[CategoryTheory.IsSplitEpi 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.
Instances For
@[simp]
theorem
CategoryTheory.Limits.coconeOfIsSplitEpi_π
{C : Type u}
[CategoryTheory.Category.{v, u} C]
{X : C}
{Y : C}
(f : X ⟶ Y)
[CategoryTheory.IsSplitEpi f]
:
noncomputable def
CategoryTheory.Limits.isSplitEpiCoequalizes
{C : Type u}
[CategoryTheory.Category.{v, u} C]
{X : C}
{Y : C}
(f : X ⟶ Y)
[CategoryTheory.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.
Instances For
def
CategoryTheory.Limits.splitEpiOfCoequalizer
(C : Type u)
[CategoryTheory.Category.{v, u} C]
{X : C}
{Y : C}
{f : X ⟶ Y}
{s : Y ⟶ X}
(hs : CategoryTheory.CategoryStruct.comp f (CategoryTheory.CategoryStruct.comp s f) = f)
(h : CategoryTheory.Limits.IsColimit (CategoryTheory.Limits.Cofork.ofπ 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 := ⋯ }
Instances For
def
CategoryTheory.Limits.isCoequalizerEpiComp
{C : Type u}
[CategoryTheory.Category.{v, u} C]
{X : C}
{Y : C}
{f : X ⟶ Y}
{g : X ⟶ Y}
{c : CategoryTheory.Limits.Cofork f g}
(i : CategoryTheory.Limits.IsColimit c)
{W : C}
(h : W ⟶ X)
[hm : CategoryTheory.Epi h]
:
let_fun this := ⋯;
CategoryTheory.Limits.IsColimit (CategoryTheory.Limits.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.
Instances For
theorem
CategoryTheory.Limits.hasCoequalizer_epi_comp
{C : Type u}
[CategoryTheory.Category.{v, u} C]
{X : C}
{Y : C}
{f : X ⟶ Y}
{g : X ⟶ Y}
[CategoryTheory.Limits.HasCoequalizer f g]
{W : C}
(h : W ⟶ X)
[CategoryTheory.Epi h]
:
@[simp]
theorem
CategoryTheory.Limits.splitEpiOfIdempotentOfIsColimitCofork_section_
(C : Type u)
[CategoryTheory.Category.{v, u} C]
{X : C}
{f : X ⟶ X}
(hf : CategoryTheory.CategoryStruct.comp f f = f)
{c : CategoryTheory.Limits.Cofork (CategoryTheory.CategoryStruct.id X) f}
(i : CategoryTheory.Limits.IsColimit c)
:
(CategoryTheory.Limits.splitEpiOfIdempotentOfIsColimitCofork C hf i).section_ = i.desc (CategoryTheory.Limits.Cofork.ofπ f ⋯)
def
CategoryTheory.Limits.splitEpiOfIdempotentOfIsColimitCofork
(C : Type u)
[CategoryTheory.Category.{v, u} C]
{X : C}
{f : X ⟶ X}
(hf : CategoryTheory.CategoryStruct.comp f f = f)
{c : CategoryTheory.Limits.Cofork (CategoryTheory.CategoryStruct.id X) f}
(i : CategoryTheory.Limits.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 := ⋯ }
Instances For
noncomputable def
CategoryTheory.Limits.splitEpiOfIdempotentCoequalizer
(C : Type u)
[CategoryTheory.Category.{v, u} C]
{X : C}
{f : X ⟶ X}
(hf : CategoryTheory.CategoryStruct.comp f f = f)
[CategoryTheory.Limits.HasCoequalizer (CategoryTheory.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.