category_theory.limits.lattice

source

def category_theory.limits.complete_lattice.finite_limit_cone {α : Type u} {J : Type w} [category_theory.small_category J] [category_theory.fin_category J] [semilattice_inf α] [order_top α] (F : J ⥤ α) :

category_theory.limits.limit_cone F

The limit cone over any functor from a finite diagram into a semilattice_inf with order_top.

Equations

category_theory.limits.complete_lattice.finite_limit_cone F = {cone := {X := finset.univ.inf F.obj, π := {app := λ (j : J), category_theory.hom_of_le _, naturality' := _}}, is_limit := {lift := λ (s : category_theory.limits.cone F), category_theory.hom_of_le _, fac' := _, uniq' := _}}

source

def category_theory.limits.complete_lattice.finite_colimit_cocone {α : Type u} {J : Type w} [category_theory.small_category J] [category_theory.fin_category J] [semilattice_sup α] [order_bot α] (F : J ⥤ α) :

category_theory.limits.colimit_cocone F

The colimit cocone over any functor from a finite diagram into a semilattice_sup with order_bot.

Equations

category_theory.limits.complete_lattice.finite_colimit_cocone F = {cocone := {X := finset.univ.sup F.obj, ι := {app := λ (i : J), category_theory.hom_of_le _, naturality' := _}}, is_colimit := {desc := λ (s : category_theory.limits.cocone F), category_theory.hom_of_le _, fac' := _, uniq' := _}}

source

@[protected, instance]

def category_theory.limits.complete_lattice.has_finite_limits_of_semilattice_inf_order_top {α : Type u} [semilattice_inf α] [order_top α] :

category_theory.limits.has_finite_limits α

source

@[protected, instance]

def category_theory.limits.complete_lattice.has_finite_colimits_of_semilattice_sup_order_bot {α : Type u} [semilattice_sup α] [order_bot α] :

category_theory.limits.has_finite_colimits α

source

theorem category_theory.limits.complete_lattice.finite_limit_eq_finset_univ_inf {α : Type u} {J : Type w} [category_theory.small_category J] [category_theory.fin_category J] [semilattice_inf α] [order_top α] (F : J ⥤ α) :

category_theory.limits.limit F = finset.univ.inf F.obj

The limit of a functor from a finite diagram into a semilattice_inf with order_top is the infimum of the objects in the image.

source

theorem category_theory.limits.complete_lattice.finite_colimit_eq_finset_univ_sup {α : Type u} {J : Type w} [category_theory.small_category J] [category_theory.fin_category J] [semilattice_sup α] [order_bot α] (F : J ⥤ α) :

category_theory.limits.colimit F = finset.univ.sup F.obj

The colimit of a functor from a finite diagram into a semilattice_sup with order_bot is the supremum of the objects in the image.

source

theorem category_theory.limits.complete_lattice.finite_product_eq_finset_inf {α : Type u} [semilattice_inf α] [order_top α] {ι : Type u} [fintype ι] (f : ι → α) :

(∏ f) = (fintype.elems ι).inf f

A finite product in the category of a semilattice_inf with order_top is the same as the infimum.

source

theorem category_theory.limits.complete_lattice.finite_coproduct_eq_finset_sup {α : Type u} [semilattice_sup α] [order_bot α] {ι : Type u} [fintype ι] (f : ι → α) :

(∐ f) = (fintype.elems ι).sup f

A finite coproduct in the category of a semilattice_sup with order_bot is the same as the supremum.

source

@[protected, instance]

def category_theory.limits.complete_lattice.category_theory.limits.has_binary_products {α : Type u} [semilattice_inf α] [order_top α] :

category_theory.limits.has_binary_products α

source

@[simp]

theorem category_theory.limits.complete_lattice.prod_eq_inf {α : Type u} [semilattice_inf α] [order_top α] (x y : α) :

(x ⨯ y) = x ⊓ y

The binary product in the category of a semilattice_inf with order_top is the same as the infimum.

source

@[protected, instance]

def category_theory.limits.complete_lattice.category_theory.limits.has_binary_coproducts {α : Type u} [semilattice_sup α] [order_bot α] :

category_theory.limits.has_binary_coproducts α

source

@[simp]

theorem category_theory.limits.complete_lattice.coprod_eq_sup {α : Type u} [semilattice_sup α] [order_bot α] (x y : α) :

(x ⨿ y) = x ⊔ y

The binary coproduct in the category of a semilattice_sup with order_bot is the same as the supremum.

source

@[simp]

theorem category_theory.limits.complete_lattice.pullback_eq_inf {α : Type u} [semilattice_inf α] [order_top α] {x y z : α} (f : x ⟶ z) (g : y ⟶ z) :

category_theory.limits.pullback f g = x ⊓ y

The pullback in the category of a semilattice_inf with order_top is the same as the infimum over the objects.

source

@[simp]

theorem category_theory.limits.complete_lattice.pushout_eq_sup {α : Type u} [semilattice_sup α] [order_bot α] (x y z : α) (f : z ⟶ x) (g : z ⟶ y) :

category_theory.limits.pushout f g = x ⊔ y

The pushout in the category of a semilattice_sup with order_bot is the same as the supremum over the objects.

source

def category_theory.limits.complete_lattice.limit_cone {α : Type u} [complete_lattice α] {J : Type u} [category_theory.small_category J] (F : J ⥤ α) :

category_theory.limits.limit_cone F

The limit cone over any functor into a complete lattice.

Equations

category_theory.limits.complete_lattice.limit_cone F = {cone := {X := infi F.obj, π := {app := λ (j : J), category_theory.hom_of_le _, naturality' := _}}, is_limit := {lift := λ (s : category_theory.limits.cone F), category_theory.hom_of_le _, fac' := _, uniq' := _}}

source

def category_theory.limits.complete_lattice.colimit_cocone {α : Type u} [complete_lattice α] {J : Type u} [category_theory.small_category J] (F : J ⥤ α) :

category_theory.limits.colimit_cocone F

The colimit cocone over any functor into a complete lattice.

Equations

category_theory.limits.complete_lattice.colimit_cocone F = {cocone := {X := supr F.obj, ι := {app := λ (j : J), category_theory.hom_of_le _, naturality' := _}}, is_colimit := {desc := λ (s : category_theory.limits.cocone F), category_theory.hom_of_le _, fac' := _, uniq' := _}}

source

@[protected, instance]

def category_theory.limits.complete_lattice.has_limits_of_complete_lattice {α : Type u} [complete_lattice α] :

category_theory.limits.has_limits α

source

@[protected, instance]

def category_theory.limits.complete_lattice.has_colimits_of_complete_lattice {α : Type u} [complete_lattice α] :

category_theory.limits.has_colimits α

source

theorem category_theory.limits.complete_lattice.limit_eq_infi {α : Type u} [complete_lattice α] {J : Type u} [category_theory.small_category J] (F : J ⥤ α) :

category_theory.limits.limit F = infi F.obj

The limit of a functor into a complete lattice is the infimum of the objects in the image.

source

theorem category_theory.limits.complete_lattice.colimit_eq_supr {α : Type u} [complete_lattice α] {J : Type u} [category_theory.small_category J] (F : J ⥤ α) :

category_theory.limits.colimit F = supr F.obj

The colimit of a functor into a complete lattice is the supremum of the objects in the image.

mathlib3 documentation

Limits in lattice categories are given by infimums and supremums. #