algebra.category.Mon.limits

source

@[protected, instance]

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

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

Equations

AddMon.add_monoid_obj F j = id (F.obj j).add_monoid

source

@[protected, instance]

def Mon.monoid_obj {J : Type v} [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

def AddMon.sections_add_submonoid {J : Type v} [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.

Equations

AddMon.sections_add_submonoid F = {carrier := (F ⋙ category_theory.forget AddMon).sections, add_mem' := _, zero_mem' := _}

source

def Mon.sections_submonoid {J : Type v} [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, mul_mem' := _, one_mem' := _}

source

@[protected, instance]

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

add_monoid (category_theory.limits.types.limit_cone (F ⋙ category_theory.forget AddMon)).X

Equations

AddMon.limit_add_monoid F = (AddMon.sections_add_submonoid F).to_add_monoid

source

@[protected, instance]

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

monoid (category_theory.limits.types.limit_cone (F ⋙ category_theory.forget Mon)).X

Equations

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

source

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

(category_theory.limits.types.limit_cone (F ⋙ category_theory.forget AddMon)).X →+ (F ⋙ category_theory.forget AddMon).obj j

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

Equations

AddMon.limit_π_add_monoid_hom F j = {to_fun := (category_theory.limits.types.limit_cone (F ⋙ category_theory.forget AddMon)).π.app j, map_zero' := _, map_add' := _}

source

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

(category_theory.limits.types.limit_cone (F ⋙ category_theory.forget Mon)).X →* (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.types.limit_cone (F ⋙ category_theory.forget Mon)).π.app j, map_one' := _, map_mul' := _}

source

def Mon.has_limits.limit_cone {J : Type v} [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_cone F = {X := Mon.of (category_theory.limits.types.limit_cone (F ⋙ category_theory.forget Mon)).X (Mon.limit_monoid F), π := {app := Mon.limit_π_monoid_hom F, naturality' := _}}

source

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

category_theory.limits.cone F

(Internal use only; use the limits API.)

Equations

AddMon.has_limits.limit_cone F = {X := AddMon.of (category_theory.limits.types.limit_cone (F ⋙ category_theory.forget AddMon)).X (AddMon.limit_add_monoid F), π := {app := AddMon.limit_π_add_monoid_hom F, naturality' := _}}

source

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

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

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

Equations

Mon.has_limits.limit_cone_is_limit F = category_theory.limits.is_limit.of_faithful (category_theory.forget Mon) (category_theory.limits.types.limit_cone_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_cone_is_limit {J : Type v} [category_theory.small_category J] (F : J ⥤ AddMon) :

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

(Internal use only; use the limits API.)

Equations

AddMon.has_limits.limit_cone_is_limit F = category_theory.limits.is_limit.of_faithful (category_theory.forget AddMon) (category_theory.limits.types.limit_cone_is_limit (F ⋙ category_theory.forget AddMon)) (λ (s : category_theory.limits.cone F), {to_fun := λ (v : ((category_theory.forget AddMon).map_cone s).X), ⟨λ (j : J), ((category_theory.forget AddMon).map_cone s).π.app j v, _⟩, map_zero' := _, map_add' := _}) _

source

@[protected, instance]

def Mon.has_limits_of_size :

category_theory.limits.has_limits_of_size Mon

The category of monoids has all limits.

source

@[protected, instance]

def AddMon.has_limits_of_size :

category_theory.limits.has_limits_of_size AddMon

The category of additive monoids has all limits.

source

@[protected, instance]

def Mon.has_limits :

category_theory.limits.has_limits Mon

source

@[protected, instance]

def AddMon.has_limits :

category_theory.limits.has_limits AddMon

source

@[protected, instance]

def Mon.forget_preserves_limits_of_size :

category_theory.limits.preserves_limits_of_size (category_theory.forget Mon)

The forgetful functor from monoids to types preserves all limits.

This means the underlying type of a limit can be computed as a limit in the category of types.

Equations

Mon.forget_preserves_limits_of_size = {preserves_limits_of_shape := λ (J : Type v) (𝒥 : category_theory.category J), {preserves_limit := λ (F : J ⥤ Mon), category_theory.limits.preserves_limit_of_preserves_limit_cone (Mon.has_limits.limit_cone_is_limit F) (category_theory.limits.types.limit_cone_is_limit (F ⋙ category_theory.forget Mon))}}

source

@[protected, instance]

def AddMon.forget_preserves_limits_of_size :

category_theory.limits.preserves_limits_of_size (category_theory.forget AddMon)

The forgetful functor from additive monoids to types preserves all limits.

This means the underlying type of a limit can be computed as a limit in the category of types.

Equations

AddMon.forget_preserves_limits_of_size = {preserves_limits_of_shape := λ (J : Type v) (𝒥 : category_theory.category J), {preserves_limit := λ (F : J ⥤ AddMon), category_theory.limits.preserves_limit_of_preserves_limit_cone (AddMon.has_limits.limit_cone_is_limit F) (category_theory.limits.types.limit_cone_is_limit (F ⋙ category_theory.forget AddMon))}}

source

@[protected, instance]

def AddMon.forget_preserves_limits :

category_theory.limits.preserves_limits (category_theory.forget AddMon)

Equations

AddMon.forget_preserves_limits = AddMon.forget_preserves_limits_of_size

source

@[protected, instance]

def Mon.forget_preserves_limits :

category_theory.limits.preserves_limits (category_theory.forget Mon)

Equations

Mon.forget_preserves_limits = Mon.forget_preserves_limits_of_size

source

@[protected, instance]

def CommMon.comm_monoid_obj {J : Type v} [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

@[protected, instance]

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

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

Equations

AddCommMon.add_comm_monoid_obj F j = id (F.obj j).add_comm_monoid

source

@[protected, instance]

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

add_comm_monoid (category_theory.limits.types.limit_cone (F ⋙ category_theory.forget AddCommMon)).X

Equations

AddCommMon.limit_add_comm_monoid F = (AddMon.sections_add_submonoid (F ⋙ category_theory.forget₂ AddCommMon AddMon)).to_add_comm_monoid

source

@[protected, instance]

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

comm_monoid (category_theory.limits.types.limit_cone (F ⋙ category_theory.forget CommMon)).X

Equations

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

source

@[protected, instance]

noncomputable def CommMon.category_theory.forget₂.category_theory.creates_limit {J : Type v} [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.forget₂.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.types.limit_cone (F ⋙ category_theory.forget CommMon)).X (CommMon.limit_comm_monoid F), π := {app := Mon.limit_π_monoid_hom (F ⋙ category_theory.forget₂ CommMon Mon), naturality' := _}}, valid_lift := (Mon.has_limits.limit_cone_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) (Mon.has_limits.limit_cone_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

@[protected, instance]

noncomputable def AddCommMon.category_theory.forget₂.category_theory.creates_limit {J : Type v} [category_theory.small_category J] (F : J ⥤ AddCommMon) :

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

We show that the forgetful functor AddCommMon ⥤ AddMon creates limits.

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

Equations

AddCommMon.category_theory.forget₂.category_theory.creates_limit F = category_theory.creates_limit_of_reflects_iso (λ (c' : category_theory.limits.cone (F ⋙ category_theory.forget₂ AddCommMon AddMon)) (t : category_theory.limits.is_limit c'), {to_liftable_cone := {lifted_cone := {X := AddCommMon.of (category_theory.limits.types.limit_cone (F ⋙ category_theory.forget AddCommMon)).X (AddCommMon.limit_add_comm_monoid F), π := {app := AddMon.limit_π_add_monoid_hom (F ⋙ category_theory.forget₂ AddCommMon AddMon), naturality' := _}}, valid_lift := (AddMon.has_limits.limit_cone_is_limit (F ⋙ category_theory.forget₂ AddCommMon AddMon)).unique_up_to_iso t}, makes_limit := category_theory.limits.is_limit.of_faithful (category_theory.forget₂ AddCommMon AddMon) (AddMon.has_limits.limit_cone_is_limit (F ⋙ category_theory.forget₂ AddCommMon AddMon)) (λ (s : category_theory.limits.cone F), {to_fun := λ (v : ((category_theory.forget AddMon).map_cone ((category_theory.forget₂ AddCommMon AddMon).map_cone s)).X), ⟨λ (j : J), ((category_theory.forget AddMon).map_cone ((category_theory.forget₂ AddCommMon AddMon).map_cone s)).π.app j v, _⟩, map_zero' := _, map_add' := _}) _})

source

noncomputable def CommMon.limit_cone {J : Type v} [category_theory.small_category J] (F : J ⥤ CommMon) :

category_theory.limits.cone F

A choice of limit cone for a functor into CommMon. (Generally, you'll just want to use limit F.)

Equations

CommMon.limit_cone F = category_theory.lift_limit (category_theory.limits.limit.is_limit (F ⋙ category_theory.forget₂ CommMon Mon))

source

noncomputable def AddCommMon.limit_cone {J : Type v} [category_theory.small_category J] (F : J ⥤ AddCommMon) :

category_theory.limits.cone F

A choice of limit cone for a functor into CommMon. (Generally, you'll just want to use limit F.)

Equations

AddCommMon.limit_cone F = category_theory.lift_limit (category_theory.limits.limit.is_limit (F ⋙ category_theory.forget₂ AddCommMon AddMon))

source

noncomputable def AddCommMon.limit_cone_is_limit {J : Type v} [category_theory.small_category J] (F : J ⥤ AddCommMon) :

category_theory.limits.is_limit (AddCommMon.limit_cone F)

The chosen cone is a limit cone. (Generally, you'll just want to use limit.cone F.)

Equations

AddCommMon.limit_cone_is_limit F = category_theory.lifted_limit_is_limit (category_theory.limits.limit.is_limit (F ⋙ category_theory.forget₂ AddCommMon AddMon))

source

noncomputable def CommMon.limit_cone_is_limit {J : Type v} [category_theory.small_category J] (F : J ⥤ CommMon) :

category_theory.limits.is_limit (CommMon.limit_cone F)

The chosen cone is a limit cone. (Generally, you'll just want to use limit.cone F.)

Equations

CommMon.limit_cone_is_limit F = category_theory.lifted_limit_is_limit (category_theory.limits.limit.is_limit (F ⋙ category_theory.forget₂ CommMon Mon))

source

@[protected, instance]

def AddCommMon.has_limits_of_size :

category_theory.limits.has_limits_of_size AddCommMon

The category of commutative monoids has all limits.

source

@[protected, instance]

def CommMon.has_limits_of_size :

category_theory.limits.has_limits_of_size CommMon

The category of commutative monoids has all limits.

source

@[protected, instance]

def CommMon.has_limits :

category_theory.limits.has_limits CommMon

source

@[protected, instance]

def AddCommMon.has_limits :

category_theory.limits.has_limits AddCommMon

source

@[protected, instance]

noncomputable def CommMon.forget₂_Mon_preserves_limits_of_size :

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

The forgetful functor from commutative monoids to monoids preserves all limits.

This means the underlying type of a limit can be computed as a limit in the category of monoids.

Equations

CommMon.forget₂_Mon_preserves_limits_of_size = {preserves_limits_of_shape := λ (J : Type v) (𝒥 : category_theory.category J), {preserves_limit := λ (F : J ⥤ CommMon), category_theory.preserves_limit_of_creates_limit_and_has_limit F (category_theory.forget₂ CommMon Mon)}}

source

@[protected, instance]

noncomputable def AddCommMon.forget₂_AddMon_preserves_limits :

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

The forgetful functor from additive commutative monoids to additive monoids preserves all limits.

This means the underlying type of a limit can be computed as a limit in the category of additive monoids.

Equations

AddCommMon.forget₂_AddMon_preserves_limits = {preserves_limits_of_shape := λ (J : Type v) (𝒥 : category_theory.category J), {preserves_limit := λ (F : J ⥤ AddCommMon), category_theory.preserves_limit_of_creates_limit_and_has_limit F (category_theory.forget₂ AddCommMon AddMon)}}

source

@[protected, instance]

noncomputable def CommMon.forget₂_Mon_preserves_limits :

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

Equations

CommMon.forget₂_Mon_preserves_limits = CommMon.forget₂_Mon_preserves_limits_of_size

source

@[protected, instance]

noncomputable def AddCommMon.forget₂_Mon_preserves_limits :

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

Equations

AddCommMon.forget₂_Mon_preserves_limits = AddCommMon.forget₂_AddMon_preserves_limits

source

@[protected, instance]

noncomputable def AddCommMon.forget_preserves_limits_of_size :

category_theory.limits.preserves_limits_of_size (category_theory.forget AddCommMon)

The forgetful functor from additive commutative monoids to types preserves all limits.

This means the underlying type of a limit can be computed as a limit in the category of types.

Equations

AddCommMon.forget_preserves_limits_of_size = {preserves_limits_of_shape := λ (J : Type v) (𝒥 : category_theory.category J), {preserves_limit := λ (F : J ⥤ AddCommMon), category_theory.limits.comp_preserves_limit (category_theory.forget₂ AddCommMon AddMon) (category_theory.forget AddMon)}}

source

@[protected, instance]

noncomputable def CommMon.forget_preserves_limits_of_size :

category_theory.limits.preserves_limits_of_size (category_theory.forget CommMon)

The forgetful functor from commutative monoids to types preserves all limits.

This means the underlying type of a limit can be computed as a limit in the category of types.

Equations

CommMon.forget_preserves_limits_of_size = {preserves_limits_of_shape := λ (J : Type v) (𝒥 : category_theory.category J), {preserves_limit := λ (F : J ⥤ CommMon), category_theory.limits.comp_preserves_limit (category_theory.forget₂ CommMon Mon) (category_theory.forget Mon)}}

source

@[protected, instance]

noncomputable def AddCommMon.forget_preserves_limits :

category_theory.limits.preserves_limits (category_theory.forget AddCommMon)

Equations

AddCommMon.forget_preserves_limits = AddCommMon.forget_preserves_limits_of_size

source

@[protected, instance]

noncomputable def CommMon.forget_preserves_limits :

category_theory.limits.preserves_limits (category_theory.forget CommMon)

Equations

CommMon.forget_preserves_limits = CommMon.forget_preserves_limits_of_size

mathlib3 documentation

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