Limits in lattice categories are given by infimums and supremums. #
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' := _}}
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' := _}}
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.
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.
A finite product in the category of a semilattice_inf
with order_top
is the same as the infimum.
A finite coproduct in the category of a semilattice_sup
with order_bot
is the same as the
supremum.
The binary product in the category of a semilattice_inf
with order_top
is the same as the
infimum.
The binary coproduct in the category of a semilattice_sup
with order_bot
is the same as the
supremum.
The pullback in the category of a semilattice_inf
with order_top
is the same as the infimum
over the objects.
The pushout in the category of a semilattice_sup
with order_bot
is the same as the supremum
over the objects.
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' := _}}
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' := _}}
The limit of a functor into a complete lattice is the infimum of the objects in the image.
The colimit of a functor into a complete lattice is the supremum of the objects in the image.