mathlib docs: category_theory.limits.lattice

@[instance]

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

category_theory.limits.has_finite_limits α

source

@[instance]

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

category_theory.limits.has_finite_colimits α

source

def category_theory.limits.complete_lattice.limit_cone {α J : Type u} [category_theory.small_category J] [complete_lattice α] (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 {α J : Type u} [category_theory.small_category J] [complete_lattice α] (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

@[instance]

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

category_theory.limits.has_limits α

source

@[instance]

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

category_theory.limits.has_colimits α

source

def category_theory.limits.complete_lattice.limit_iso_infi {α J : Type u} [category_theory.small_category J] [complete_lattice α] (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.

Equations

category_theory.limits.complete_lattice.limit_iso_infi F = (category_theory.limits.limit.is_limit F).cone_point_unique_up_to_iso (category_theory.limits.complete_lattice.limit_cone F).is_limit

source

@[simp]

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

(category_theory.limits.complete_lattice.limit_iso_infi F).hom ≫ category_theory.hom_of_le _ = category_theory.limits.limit.π F j

source

@[simp]

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

(category_theory.limits.complete_lattice.limit_iso_infi F).inv ≫ category_theory.limits.limit.π F j = category_theory.hom_of_le _

source

def category_theory.limits.complete_lattice.colimit_iso_supr {α J : Type u} [category_theory.small_category J] [complete_lattice α] (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.

Equations

category_theory.limits.complete_lattice.colimit_iso_supr F = (category_theory.limits.colimit.is_colimit F).cocone_point_unique_up_to_iso (category_theory.limits.complete_lattice.colimit_cocone F).is_colimit

source

@[simp]

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

category_theory.limits.colimit.ι F j ≫ (category_theory.limits.complete_lattice.colimit_iso_supr F).hom = category_theory.hom_of_le _

source

@[simp]

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

category_theory.hom_of_le _ ≫ (category_theory.limits.complete_lattice.colimit_iso_supr F).inv = category_theory.limits.colimit.ι F j