category_theory.limits.constructions.equalizers

@[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))

source

@[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) :

category_theory.limits.has_equalizers_of_has_pullbacks_and_binary_products.construct_equalizer F ⟶ F.obj category_theory.limits.walking_parallel_pair.zero

Define the equalizing morphism

source

theorem category_theory.limits.has_equalizers_of_has_pullbacks_and_binary_products.pullback_fst_eq_pullback_snd {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) :

category_theory.limits.has_equalizers_of_has_pullbacks_and_binary_products.pullback_fst F = category_theory.limits.pullback.snd

source

@[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) :

category_theory.limits.cone F

Define the equalizing cone

Equations

category_theory.limits.has_equalizers_of_has_pullbacks_and_binary_products.equalizer_cone F = category_theory.limits.cone.of_fork (category_theory.limits.fork.of_ι (category_theory.limits.has_equalizers_of_has_pullbacks_and_binary_products.pullback_fst F) _)

source

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) :

category_theory.limits.is_limit (category_theory.limits.has_equalizers_of_has_pullbacks_and_binary_products.equalizer_cone F)

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' := _}

source

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] :

category_theory.limits.has_equalizers C

Any category with pullbacks and binary products, has equalizers.

source

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] :

category_theory.limits.preserves_limits_of_shape category_theory.limits.walking_parallel_pair 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' := _}}

source

@[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))

source

@[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) :

F.obj category_theory.limits.walking_parallel_pair.one ⟶ category_theory.limits.has_coequalizers_of_has_pushouts_and_binary_coproducts.construct_coequalizer F

Define the equalizing morphism

source

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) :

category_theory.limits.has_coequalizers_of_has_pushouts_and_binary_coproducts.pushout_inl F = category_theory.limits.pushout.inr

source

@[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) :

category_theory.limits.cocone F

Define the equalizing cocone

Equations

category_theory.limits.has_coequalizers_of_has_pushouts_and_binary_coproducts.coequalizer_cocone F = category_theory.limits.cocone.of_cofork (category_theory.limits.cofork.of_π (category_theory.limits.has_coequalizers_of_has_pushouts_and_binary_coproducts.pushout_inl F) _)

source

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) :

category_theory.limits.is_colimit (category_theory.limits.has_coequalizers_of_has_pushouts_and_binary_coproducts.coequalizer_cocone F)

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' := _}

source

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] :

category_theory.limits.has_coequalizers C

Any category with pullbacks and binary products, has equalizers.

source

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] :

category_theory.limits.preserves_colimits_of_shape category_theory.limits.walking_parallel_pair 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' := _}}

mathlib3 documentation

Constructing equalizers from pullbacks and binary products. #