Limits of monoid objects. #
THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4.
If C has limits, so does Mon_ C, and the forgetful functor preserves these limits.
(This could potentially replace many individual constructions for concrete categories,
in particular Mon, SemiRing, Ring, and Algebra R.)
noncomputable
def
Mon_.limit
{J : Type v}
[category_theory.small_category J]
{C : Type u}
[category_theory.category C]
[category_theory.limits.has_limits C]
[category_theory.monoidal_category C]
(F : J ⥤ Mon_ C) :
Mon_ C
We construct the (candidate) limit of a functor F : J ⥤ Mon_ C
by interpreting it as a functor Mon_ (J ⥤ C),
and noting that taking limits is a lax monoidal functor,
and hence sends monoid objects to monoid objects.
@[simp]
theorem
Mon_.limit_one
{J : Type v}
[category_theory.small_category J]
{C : Type u}
[category_theory.category C]
[category_theory.limits.has_limits C]
[category_theory.monoidal_category C]
(F : J ⥤ Mon_ C) :
(Mon_.limit F).one = category_theory.limits.limit.lift (F ⋙ Mon_.forget C) ((category_theory.limits.cones.postcompose (category_theory.monoidal.Mon_functor_category_equivalence.inverse.obj F).one).obj {X := 𝟙_ C _inst_4, π := {app := λ (j : J), 𝟙 (𝟙_ C), naturality' := _}})
@[simp]
theorem
Mon_.limit_X
{J : Type v}
[category_theory.small_category J]
{C : Type u}
[category_theory.category C]
[category_theory.limits.has_limits C]
[category_theory.monoidal_category C]
(F : J ⥤ Mon_ C) :
(Mon_.limit F).X = category_theory.limits.limit (F ⋙ Mon_.forget C)
@[simp]
theorem
Mon_.limit_mul
{J : Type v}
[category_theory.small_category J]
{C : Type u}
[category_theory.category C]
[category_theory.limits.has_limits C]
[category_theory.monoidal_category C]
(F : J ⥤ Mon_ C) :
(Mon_.limit F).mul = category_theory.limits.limit.lift (F ⋙ Mon_.forget C) ((category_theory.limits.cones.postcompose (category_theory.monoidal.Mon_functor_category_equivalence.inverse.obj F).mul).obj {X := category_theory.limits.limit (F ⋙ Mon_.forget C) ⊗ category_theory.limits.limit (F ⋙ Mon_.forget C), π := {app := λ (j : J), category_theory.limits.limit.π (F ⋙ Mon_.forget C) j ⊗ category_theory.limits.limit.π (F ⋙ Mon_.forget C) j, naturality' := _}})
@[simp]
theorem
Mon_.limit_cone_X
{J : Type v}
[category_theory.small_category J]
{C : Type u}
[category_theory.category C]
[category_theory.limits.has_limits C]
[category_theory.monoidal_category C]
(F : J ⥤ Mon_ C) :
(Mon_.limit_cone F).X = Mon_.limit F
noncomputable
def
Mon_.limit_cone
{J : Type v}
[category_theory.small_category J]
{C : Type u}
[category_theory.category C]
[category_theory.limits.has_limits C]
[category_theory.monoidal_category C]
(F : J ⥤ Mon_ C) :
Implementation of Mon_.has_limits: a limiting cone over a functor F : J ⥤ Mon_ C.
Equations
- Mon_.limit_cone F = {X := Mon_.limit F, π := {app := λ (j : J), {hom := category_theory.limits.limit.π (F ⋙ Mon_.forget C) j, one_hom' := _, mul_hom' := _}, naturality' := _}}
@[simp]
theorem
Mon_.limit_cone_π_app_hom
{J : Type v}
[category_theory.small_category J]
{C : Type u}
[category_theory.category C]
[category_theory.limits.has_limits C]
[category_theory.monoidal_category C]
(F : J ⥤ Mon_ C)
(j : J) :
((Mon_.limit_cone F).π.app j).hom = category_theory.limits.limit.π (F ⋙ Mon_.forget C) j
noncomputable
def
Mon_.forget_map_cone_limit_cone_iso
{J : Type v}
[category_theory.small_category J]
{C : Type u}
[category_theory.category C]
[category_theory.limits.has_limits C]
[category_theory.monoidal_category C]
(F : J ⥤ Mon_ C) :
(Mon_.forget C).map_cone (Mon_.limit_cone F) ≅ category_theory.limits.limit.cone (F ⋙ Mon_.forget C)
The image of the proposed limit cone for F : J ⥤ Mon_ C under the forgetful functor
forget C : Mon_ C ⥤ C is isomorphic to the limit cone of F ⋙ forget C.
Equations
noncomputable
def
Mon_.limit_cone_is_limit
{J : Type v}
[category_theory.small_category J]
{C : Type u}
[category_theory.category C]
[category_theory.limits.has_limits C]
[category_theory.monoidal_category C]
(F : J ⥤ Mon_ C) :
Implementation of Mon_.has_limits:
the proposed cone over a functor F : J ⥤ Mon_ C is a limit cone.
Equations
- Mon_.limit_cone_is_limit F = {lift := λ (s : category_theory.limits.cone F), {hom := category_theory.limits.limit.lift (F ⋙ Mon_.forget C) ((Mon_.forget C).map_cone s), one_hom' := _, mul_hom' := _}, fac' := _, uniq' := _}
@[simp]
theorem
Mon_.limit_cone_is_limit_lift_hom
{J : Type v}
[category_theory.small_category J]
{C : Type u}
[category_theory.category C]
[category_theory.limits.has_limits C]
[category_theory.monoidal_category C]
(F : J ⥤ Mon_ C)
(s : category_theory.limits.cone F) :
((Mon_.limit_cone_is_limit F).lift s).hom = category_theory.limits.limit.lift (F ⋙ Mon_.forget C) ((Mon_.forget C).map_cone s)
@[protected, instance]
@[protected, instance]
noncomputable
def
Mon_.forget_preserves_limits
{C : Type u}
[category_theory.category C]
[category_theory.limits.has_limits C]
[category_theory.monoidal_category C] :
Equations
- Mon_.forget_preserves_limits = {preserves_limits_of_shape := λ (J : Type v) (𝒥 : category_theory.category J), {preserves_limit := λ (F : J ⥤ Mon_ C), category_theory.limits.preserves_limit_of_preserves_limit_cone (Mon_.limit_cone_is_limit F) ((category_theory.limits.limit.is_limit (F ⋙ Mon_.forget C)).of_iso_limit (Mon_.forget_map_cone_limit_cone_iso F).symm)}}