Documentation

Mathlib.CategoryTheory.Limits.Lattice

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

The limit cone over any functor from a finite diagram into a SemilatticeInf with OrderTop.

Equations
  • One or more equations did not get rendered due to their size.
Instances For

    The colimit cocone over any functor from a finite diagram into a SemilatticeSup with OrderBot.

    Equations
    • One or more equations did not get rendered due to their size.
    Instances For

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

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

      theorem CategoryTheory.Limits.CompleteLattice.finite_product_eq_finset_inf {α : Type u} [SemilatticeInf α] [OrderTop α] {ι : Type u} [Fintype ι] (f : ια) :
      ∏ᶜ f = Fintype.elems.inf f

      A finite product in the category of a SemilatticeInf with OrderTop is the same as the infimum.

      theorem CategoryTheory.Limits.CompleteLattice.finite_coproduct_eq_finset_sup {α : Type u} [SemilatticeSup α] [OrderBot α] {ι : Type u} [Fintype ι] (f : ια) :
      f = Fintype.elems.sup f

      A finite coproduct in the category of a SemilatticeSup with OrderBot is the same as the supremum.

      @[simp]
      theorem CategoryTheory.Limits.CompleteLattice.prod_eq_inf {α : Type u} [SemilatticeInf α] [OrderTop α] (x : α) (y : α) :
      (x y) = x y

      The binary product in the category of a SemilatticeInf with OrderTop is the same as the infimum.

      @[simp]
      theorem CategoryTheory.Limits.CompleteLattice.coprod_eq_sup {α : Type u} [SemilatticeSup α] [OrderBot α] (x : α) (y : α) :
      (x ⨿ y) = x y

      The binary coproduct in the category of a SemilatticeSup with OrderBot is the same as the supremum.

      @[simp]
      theorem CategoryTheory.Limits.CompleteLattice.pullback_eq_inf {α : Type u} [SemilatticeInf α] [OrderTop α] {x : α} {y : α} {z : α} (f : x z) (g : y z) :

      The pullback in the category of a SemilatticeInf with OrderTop is the same as the infimum over the objects.

      @[simp]
      theorem CategoryTheory.Limits.CompleteLattice.pushout_eq_sup {α : Type u} [SemilatticeSup α] [OrderBot α] (x : α) (y : α) (z : α) (f : z x) (g : z y) :

      The pushout in the category of a SemilatticeSup with OrderBot is the same as the supremum over the objects.

      The limit cone over any functor into a complete lattice.

      Equations
      • One or more equations did not get rendered due to their size.
      Instances For

        The colimit cocone over any functor into a complete lattice.

        Equations
        • One or more equations did not get rendered due to their size.
        Instances For

          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.