mathlib docs: algebra.category.Mon.limits

source

@[instance]

def Mon.monoid_obj {J : Type u} [category_theory.small_category J] (F : J ⥤ Mon) (j : J) :

monoid ((F ⋙ category_theory.forget Mon).obj j)

Equations

Mon.monoid_obj F j = id (F.obj j).monoid

source

@[instance]

def AddMon.add_monoid_obj {J : Type u} [category_theory.small_category J] (F : J ⥤ AddMon) (j : J) :

add_monoid ((F ⋙ category_theory.forget AddMon).obj j)

source

def Mon.sections_submonoid {J : Type u} [category_theory.small_category J] (F : J ⥤ Mon) :

submonoid (Π (j : J), ↥(F.obj j))

The flat sections of a functor into Mon form a submonoid of all sections.

Equations

Mon.sections_submonoid F = {carrier := (F ⋙ category_theory.forget Mon).sections, one_mem' := _, mul_mem' := _}

source

def AddMon.sections_add_submonoid {J : Type u} [category_theory.small_category J] (F : J ⥤ AddMon) :

add_submonoid (Π (j : J), ↥(F.obj j))

The flat sections of a functor into AddMon form an additive submonoid of all sections.

source

@[instance]

def AddMon.limit_add_monoid {J : Type u} [category_theory.small_category J] (F : J ⥤ AddMon) :

add_monoid (category_theory.limits.limit (F ⋙ category_theory.forget AddMon))

source

@[instance]

def Mon.limit_monoid {J : Type u} [category_theory.small_category J] (F : J ⥤ Mon) :

monoid (category_theory.limits.limit (F ⋙ category_theory.forget Mon))

Equations

Mon.limit_monoid F = (Mon.sections_submonoid F).to_monoid

source

def AddMon.limit_π_add_monoid_hom {J : Type u} [category_theory.small_category J] (F : J ⥤ AddMon) (j : J) :

category_theory.limits.limit (F ⋙ category_theory.forget AddMon) →+ (F ⋙ category_theory.forget AddMon).obj j

limit.π (F ⋙ forget AddMon) j as an add_monoid_hom.

source

def Mon.limit_π_monoid_hom {J : Type u} [category_theory.small_category J] (F : J ⥤ Mon) (j : J) :

category_theory.limits.limit (F ⋙ category_theory.forget Mon) →* (F ⋙ category_theory.forget Mon).obj j

limit.π (F ⋙ forget Mon) j as a monoid_hom.

Equations

Mon.limit_π_monoid_hom F j = {to_fun := category_theory.limits.limit.π (F ⋙ category_theory.forget Mon) j, map_one' := _, map_mul' := _}

source

def Mon.has_limits.limit {J : Type u} [category_theory.small_category J] (F : J ⥤ Mon) :

category_theory.limits.cone F

Construction of a limit cone in Mon. (Internal use only; use the limits API.)

Equations

Mon.has_limits.limit F = {X := Mon.of (category_theory.limits.limit (F ⋙ category_theory.forget Mon)) (Mon.limit_monoid F), π := {app := Mon.limit_π_monoid_hom F, naturality' := _}}

source

def AddMon.has_limits.limit {J : Type u} [category_theory.small_category J] (F : J ⥤ AddMon) :

category_theory.limits.cone F

(Internal use only; use the limits API.)

source

def Mon.has_limits.limit_is_limit {J : Type u} [category_theory.small_category J] (F : J ⥤ Mon) :

category_theory.limits.is_limit (Mon.has_limits.limit F)

Witness that the limit cone in Mon is a limit cone. (Internal use only; use the limits API.)

Equations

Mon.has_limits.limit_is_limit F = category_theory.limits.is_limit.of_faithful (category_theory.forget Mon) (category_theory.limits.limit.is_limit (F ⋙ category_theory.forget Mon)) (λ (s : category_theory.limits.cone F), {to_fun := λ (v : ((category_theory.forget Mon).map_cone s).X), ⟨λ (j : J), ((category_theory.forget Mon).map_cone s).π.app j v, _⟩, map_one' := _, map_mul' := _}) _

source

def AddMon.has_limits.limit_is_limit {J : Type u} [category_theory.small_category J] (F : J ⥤ AddMon) :

category_theory.limits.is_limit (AddMon.has_limits.limit F)

(Internal use only; use the limits API.)

source

@[instance]

def Mon.has_limits :

category_theory.limits.has_limits Mon

The category of monoids has all limits.

Equations

Mon.has_limits = {has_limits_of_shape := λ (J : Type u_1) (𝒥 : category_theory.small_category J), {has_limit := λ (F : J ⥤ Mon), {cone := Mon.has_limits.limit F, is_limit := Mon.has_limits.limit_is_limit F}}}

source

@[instance]

def AddMon.has_limits :

category_theory.limits.has_limits AddMon

source

@[instance]

def Mon.forget_preserves_limits :

category_theory.limits.preserves_limits (category_theory.forget Mon)

The forgetful functor from monoids to types preserves all limits. (That is, the underlying types could have been computed instead as limits in the category of types.)

Equations

Mon.forget_preserves_limits = {preserves_limits_of_shape := λ (J : Type u_1) (𝒥 : category_theory.small_category J), {preserves_limit := λ (F : J ⥤ Mon), category_theory.limits.preserves_limit_of_preserves_limit_cone (category_theory.limits.limit.is_limit F) (category_theory.limits.limit.is_limit (F ⋙ category_theory.forget Mon))}}

source

@[instance]

def AddMon.forget_preserves_limits :

category_theory.limits.preserves_limits (category_theory.forget AddMon)

source

@[instance]

def AddCommMon.add_comm_monoid_obj {J : Type u} [category_theory.small_category J] (F : J ⥤ AddCommMon) (j : J) :

add_comm_monoid ((F ⋙ category_theory.forget AddCommMon).obj j)

source

@[instance]

def CommMon.comm_monoid_obj {J : Type u} [category_theory.small_category J] (F : J ⥤ CommMon) (j : J) :

comm_monoid ((F ⋙ category_theory.forget CommMon).obj j)

Equations

CommMon.comm_monoid_obj F j = id (F.obj j).comm_monoid

source

@[instance]

def AddCommMon.limit_add_comm_monoid {J : Type u} [category_theory.small_category J] (F : J ⥤ AddCommMon) :

add_comm_monoid (category_theory.limits.limit (F ⋙ category_theory.forget AddCommMon))

source

@[instance]

def CommMon.limit_comm_monoid {J : Type u} [category_theory.small_category J] (F : J ⥤ CommMon) :

comm_monoid (category_theory.limits.limit (F ⋙ category_theory.forget CommMon))

Equations

CommMon.limit_comm_monoid F = (Mon.sections_submonoid (F ⋙ category_theory.forget₂ CommMon Mon)).to_comm_monoid

source

@[instance]

def AddCommMon.creates_limit {J : Type u} [category_theory.small_category J] (F : J ⥤ AddCommMon) :

category_theory.creates_limit F (category_theory.forget₂ AddCommMon AddMon)

source

@[instance]

def CommMon.category_theory.creates_limit {J : Type u} [category_theory.small_category J] (F : J ⥤ CommMon) :

category_theory.creates_limit F (category_theory.forget₂ CommMon Mon)

We show that the forgetful functor CommMon ⥤ Mon creates limits.

All we need to do is notice that the limit point has a comm_monoid instance available, and then reuse the existing limit.

Equations

CommMon.category_theory.creates_limit F = category_theory.creates_limit_of_reflects_iso (λ (c' : category_theory.limits.cone (F ⋙ category_theory.forget₂ CommMon Mon)) (t : category_theory.limits.is_limit c'), {to_liftable_cone := {lifted_cone := {X := CommMon.of (category_theory.limits.limit (F ⋙ category_theory.forget CommMon)) (CommMon.limit_comm_monoid F), π := {app := Mon.limit_π_monoid_hom (F ⋙ category_theory.forget₂ CommMon Mon), naturality' := _}}, valid_lift := (category_theory.limits.limit.is_limit (F ⋙ category_theory.forget₂ CommMon Mon)).unique_up_to_iso t}, makes_limit := category_theory.limits.is_limit.of_faithful (category_theory.forget₂ CommMon Mon) (category_theory.limits.limit.is_limit (F ⋙ category_theory.forget₂ CommMon Mon)) (λ (s : category_theory.limits.cone F), {to_fun := λ (v : ((category_theory.forget Mon).map_cone ((category_theory.forget₂ CommMon Mon).map_cone s)).X), ⟨λ (j : J), ((category_theory.forget Mon).map_cone ((category_theory.forget₂ CommMon Mon).map_cone s)).π.app j v, _⟩, map_one' := _, map_mul' := _}) _})

source

@[instance]

def CommMon.has_limits :

category_theory.limits.has_limits CommMon

The category of commutative monoids has all limits.

Equations

CommMon.has_limits = {has_limits_of_shape := λ (J : Type u_1) (𝒥 : category_theory.small_category J), {has_limit := λ (F : J ⥤ CommMon), category_theory.has_limit_of_created F (category_theory.forget₂ CommMon Mon)}}

source

@[instance]

def AddCommMon.has_limits :

category_theory.limits.has_limits AddCommMon

source

@[instance]

def CommMon.forget₂_Mon_preserves_limits :

category_theory.limits.preserves_limits (category_theory.forget₂ CommMon Mon)

The forgetful functor from commutative monoids to monoids preserves all limits. (That is, the underlying monoid could have been computed instead as limits in the category of monoids.)

Equations

CommMon.forget₂_Mon_preserves_limits = {preserves_limits_of_shape := λ (J : Type u_1) (𝒥 : category_theory.small_category J), {preserves_limit := λ (F : J ⥤ CommMon), category_theory.preserves_limit_of_creates_limit_and_has_limit F (category_theory.forget₂ CommMon Mon)}}

source

@[instance]

def AddCommMon.forget₂_AddMon_preserves_limits :

category_theory.limits.preserves_limits (category_theory.forget₂ AddCommMon AddMon)

source

@[instance]

def CommMon.forget_preserves_limits :

category_theory.limits.preserves_limits (category_theory.forget CommMon)

The forgetful functor from commutative monoids to types preserves all limits. (That is, the underlying types could have been computed instead as limits in the category of types.)

Equations

CommMon.forget_preserves_limits = {preserves_limits_of_shape := λ (J : Type u_1) (𝒥 : category_theory.small_category J), {preserves_limit := λ (F : J ⥤ CommMon), category_theory.limits.preserves_limit_of_preserves_limit_cone (category_theory.limits.limit.is_limit F) (category_theory.limits.limit.is_limit (F ⋙ category_theory.forget CommMon))}}

source

@[instance]

def AddCommMon.forget_preserves_limits :

category_theory.limits.preserves_limits (category_theory.forget AddCommMon)

mathlib documentation

algebra.category.Mon.limits

The category of (commutative) (additive) monoids has all limits

General documentation

Additional documentation

Library

mathlib documentation

algebra.​category.​Mon.​limits

The category of (commutative) (additive) monoids has all limits

General documentation

Additional documentation

Library

algebra.category.Mon.limits