Constructing equalizers from pullbacks and binary products. #
If a category has pullbacks and binary products, then it has equalizers.
TODO: generalize universe
@[reducible]
noncomputable
def
category_theory.limits.has_equalizers_of_has_pullbacks_and_binary_products.construct_equalizer
{C : Type u}
[category_theory.category C]
[category_theory.limits.has_binary_products C]
[category_theory.limits.has_pullbacks C]
(F : category_theory.limits.walking_parallel_pair ⥤ C) :
C
Define the equalizing object
Equations
- category_theory.limits.has_equalizers_of_has_pullbacks_and_binary_products.construct_equalizer F = category_theory.limits.pullback (category_theory.limits.prod.lift (𝟙 (F.obj category_theory.limits.walking_parallel_pair.zero)) (F.map category_theory.limits.walking_parallel_pair_hom.left)) (category_theory.limits.prod.lift (𝟙 (F.obj category_theory.limits.walking_parallel_pair.zero)) (F.map category_theory.limits.walking_parallel_pair_hom.right))
@[reducible]
noncomputable
def
category_theory.limits.has_equalizers_of_has_pullbacks_and_binary_products.pullback_fst
{C : Type u}
[category_theory.category C]
[category_theory.limits.has_binary_products C]
[category_theory.limits.has_pullbacks C]
(F : category_theory.limits.walking_parallel_pair ⥤ C) :
Define the equalizing morphism
@[reducible]
noncomputable
def
category_theory.limits.has_equalizers_of_has_pullbacks_and_binary_products.equalizer_cone
{C : Type u}
[category_theory.category C]
[category_theory.limits.has_binary_products C]
[category_theory.limits.has_pullbacks C]
(F : category_theory.limits.walking_parallel_pair ⥤ C) :
Define the equalizing cone
noncomputable
def
category_theory.limits.has_equalizers_of_has_pullbacks_and_binary_products.equalizer_cone_is_limit
{C : Type u}
[category_theory.category C]
[category_theory.limits.has_binary_products C]
[category_theory.limits.has_pullbacks C]
(F : category_theory.limits.walking_parallel_pair ⥤ C) :
Show the equalizing cone is a limit
Equations
- category_theory.limits.has_equalizers_of_has_pullbacks_and_binary_products.equalizer_cone_is_limit F = {lift := λ (c : category_theory.limits.cone F), category_theory.limits.pullback.lift (c.π.app category_theory.limits.walking_parallel_pair.zero) (c.π.app category_theory.limits.walking_parallel_pair.zero) _, fac' := _, uniq' := _}
theorem
category_theory.limits.has_equalizers_of_has_pullbacks_and_binary_products
{C : Type u}
[category_theory.category C]
[category_theory.limits.has_binary_products C]
[category_theory.limits.has_pullbacks C] :
Any category with pullbacks and binary products, has equalizers.
noncomputable
def
category_theory.limits.preserves_equalizers_of_preserves_pullbacks_and_binary_products
{C : Type u}
[category_theory.category C]
{D : Type u'}
[category_theory.category D]
(G : C ⥤ D)
[category_theory.limits.has_binary_products C]
[category_theory.limits.has_pullbacks C]
[category_theory.limits.preserves_limits_of_shape (category_theory.discrete category_theory.limits.walking_pair) G]
[category_theory.limits.preserves_limits_of_shape category_theory.limits.walking_cospan G] :
A functor that preserves pullbacks and binary products also presrves equalizers.
Equations
- category_theory.limits.preserves_equalizers_of_preserves_pullbacks_and_binary_products G = {preserves_limit := λ (K : category_theory.limits.walking_parallel_pair ⥤ C), category_theory.limits.preserves_limit_of_preserves_limit_cone (category_theory.limits.has_equalizers_of_has_pullbacks_and_binary_products.equalizer_cone_is_limit K) {lift := λ (c : category_theory.limits.cone (K ⋙ G)), category_theory.limits.pullback.lift (c.π.app category_theory.limits.walking_parallel_pair.zero) (c.π.app category_theory.limits.walking_parallel_pair.zero) _ ≫ (category_theory.limits.preserves_pullback.iso G (category_theory.limits.prod.lift (𝟙 (K.obj category_theory.limits.walking_parallel_pair.zero)) (K.map category_theory.limits.walking_parallel_pair_hom.left)) (category_theory.limits.prod.lift (𝟙 (K.obj category_theory.limits.walking_parallel_pair.zero)) (K.map category_theory.limits.walking_parallel_pair_hom.right))).inv, fac' := _, uniq' := _}}
@[reducible]
noncomputable
def
category_theory.limits.has_coequalizers_of_has_pushouts_and_binary_coproducts.construct_coequalizer
{C : Type u}
[category_theory.category C]
[category_theory.limits.has_binary_coproducts C]
[category_theory.limits.has_pushouts C]
(F : category_theory.limits.walking_parallel_pair ⥤ C) :
C
Define the equalizing object
Equations
- category_theory.limits.has_coequalizers_of_has_pushouts_and_binary_coproducts.construct_coequalizer F = category_theory.limits.pushout (category_theory.limits.coprod.desc (𝟙 (F.obj category_theory.limits.walking_parallel_pair.one)) (F.map category_theory.limits.walking_parallel_pair_hom.left)) (category_theory.limits.coprod.desc (𝟙 (F.obj category_theory.limits.walking_parallel_pair.one)) (F.map category_theory.limits.walking_parallel_pair_hom.right))
@[reducible]
noncomputable
def
category_theory.limits.has_coequalizers_of_has_pushouts_and_binary_coproducts.pushout_inl
{C : Type u}
[category_theory.category C]
[category_theory.limits.has_binary_coproducts C]
[category_theory.limits.has_pushouts C]
(F : category_theory.limits.walking_parallel_pair ⥤ C) :
Define the equalizing morphism
theorem
category_theory.limits.has_coequalizers_of_has_pushouts_and_binary_coproducts.pushout_inl_eq_pushout_inr
{C : Type u}
[category_theory.category C]
[category_theory.limits.has_binary_coproducts C]
[category_theory.limits.has_pushouts C]
(F : category_theory.limits.walking_parallel_pair ⥤ C) :
@[reducible]
noncomputable
def
category_theory.limits.has_coequalizers_of_has_pushouts_and_binary_coproducts.coequalizer_cocone
{C : Type u}
[category_theory.category C]
[category_theory.limits.has_binary_coproducts C]
[category_theory.limits.has_pushouts C]
(F : category_theory.limits.walking_parallel_pair ⥤ C) :
Define the equalizing cocone
noncomputable
def
category_theory.limits.has_coequalizers_of_has_pushouts_and_binary_coproducts.coequalizer_cocone_is_colimit
{C : Type u}
[category_theory.category C]
[category_theory.limits.has_binary_coproducts C]
[category_theory.limits.has_pushouts C]
(F : category_theory.limits.walking_parallel_pair ⥤ C) :
Show the equalizing cocone is a colimit
Equations
- category_theory.limits.has_coequalizers_of_has_pushouts_and_binary_coproducts.coequalizer_cocone_is_colimit F = {desc := λ (c : category_theory.limits.cocone F), category_theory.limits.pushout.desc (c.ι.app category_theory.limits.walking_parallel_pair.one) (c.ι.app category_theory.limits.walking_parallel_pair.one) _, fac' := _, uniq' := _}
theorem
category_theory.limits.has_coequalizers_of_has_pushouts_and_binary_coproducts
{C : Type u}
[category_theory.category C]
[category_theory.limits.has_binary_coproducts C]
[category_theory.limits.has_pushouts C] :
Any category with pullbacks and binary products, has equalizers.
noncomputable
def
category_theory.limits.preserves_coequalizers_of_preserves_pushouts_and_binary_coproducts
{C : Type u}
[category_theory.category C]
{D : Type u'}
[category_theory.category D]
(G : C ⥤ D)
[category_theory.limits.has_binary_coproducts C]
[category_theory.limits.has_pushouts C]
[category_theory.limits.preserves_colimits_of_shape (category_theory.discrete category_theory.limits.walking_pair) G]
[category_theory.limits.preserves_colimits_of_shape category_theory.limits.walking_span G] :
A functor that preserves pushouts and binary coproducts also presrves coequalizers.
Equations
- category_theory.limits.preserves_coequalizers_of_preserves_pushouts_and_binary_coproducts G = {preserves_colimit := λ (K : category_theory.limits.walking_parallel_pair ⥤ C), category_theory.limits.preserves_colimit_of_preserves_colimit_cocone (category_theory.limits.has_coequalizers_of_has_pushouts_and_binary_coproducts.coequalizer_cocone_is_colimit K) {desc := λ (c : category_theory.limits.cocone (K ⋙ G)), (category_theory.limits.preserves_pushout.iso G (category_theory.limits.coprod.desc (𝟙 (K.obj category_theory.limits.walking_parallel_pair.one)) (K.map category_theory.limits.walking_parallel_pair_hom.left)) (category_theory.limits.coprod.desc (𝟙 (K.obj category_theory.limits.walking_parallel_pair.one)) (K.map category_theory.limits.walking_parallel_pair_hom.right))).inv ≫ category_theory.limits.pushout.desc (c.ι.app category_theory.limits.walking_parallel_pair.one) (c.ι.app category_theory.limits.walking_parallel_pair.one) _, fac' := _, uniq' := _}}