Documentation

Mathlib.CategoryTheory.Limits.Lattice

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

source
def CategoryTheory.Limits.CompleteLattice.finiteLimitCone {α : Type u} {J : Type w} [SmallCategory J] [FinCategory J] [SemilatticeInf α] [OrderTop α] (F : Functor J α) :
LimitCone F

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
    source
    @[simp]
    theorem CategoryTheory.Limits.CompleteLattice.finiteLimitCone_cone_pt {α : Type u} {J : Type w} [SmallCategory J] [FinCategory J] [SemilatticeInf α] [OrderTop α] (F : Functor J α) :
    (finiteLimitCone F).cone.pt = Finset.univ.inf F.obj
    source
    @[simp]
    theorem CategoryTheory.Limits.CompleteLattice.finiteLimitCone_isLimit_lift {α : Type u} {J : Type w} [SmallCategory J] [FinCategory J] [SemilatticeInf α] [OrderTop α] (F : Functor J α) (s : Cone F) :
    (finiteLimitCone F).isLimit.lift s = homOfLE ⋯
    source
    @[simp]
    theorem CategoryTheory.Limits.CompleteLattice.finiteLimitCone_cone_π_app {α : Type u} {J : Type w} [SmallCategory J] [FinCategory J] [SemilatticeInf α] [OrderTop α] (F : Functor J α) (x✝ : J) :
    (finiteLimitCone F).cone.π.app x✝ = homOfLE ⋯
    source
    def CategoryTheory.Limits.CompleteLattice.finiteColimitCocone {α : Type u} {J : Type w} [SmallCategory J] [FinCategory J] [SemilatticeSup α] [OrderBot α] (F : Functor J α) :
    ColimitCocone F

    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
      source
      @[simp]
      theorem CategoryTheory.Limits.CompleteLattice.finiteColimitCocone_cocone_pt {α : Type u} {J : Type w} [SmallCategory J] [FinCategory J] [SemilatticeSup α] [OrderBot α] (F : Functor J α) :
      (finiteColimitCocone F).cocone.pt = Finset.univ.sup F.obj
      source
      @[simp]
      theorem CategoryTheory.Limits.CompleteLattice.finiteColimitCocone_isColimit_desc {α : Type u} {J : Type w} [SmallCategory J] [FinCategory J] [SemilatticeSup α] [OrderBot α] (F : Functor J α) (s : Cocone F) :
      (finiteColimitCocone F).isColimit.desc s = homOfLE ⋯
      source
      @[simp]
      theorem CategoryTheory.Limits.CompleteLattice.finiteColimitCocone_cocone_ι_app {α : Type u} {J : Type w} [SmallCategory J] [FinCategory J] [SemilatticeSup α] [OrderBot α] (F : Functor J α) (x✝ : J) :
      (finiteColimitCocone F).cocone.ι.app x✝ = homOfLE ⋯
      source
      @[instance 100]
      instance CategoryTheory.Limits.CompleteLattice.hasFiniteLimits_of_semilatticeInf_orderTop {α : Type u} [SemilatticeInf α] [OrderTop α] :
      HasFiniteLimits α
      source
      @[instance 100]
      instance CategoryTheory.Limits.CompleteLattice.hasFiniteColimits_of_semilatticeSup_orderBot {α : Type u} [SemilatticeSup α] [OrderBot α] :
      HasFiniteColimits α
      source
      theorem CategoryTheory.Limits.CompleteLattice.finite_limit_eq_finset_univ_inf {α : Type u} {J : Type w} [SmallCategory J] [FinCategory J] [SemilatticeInf α] [OrderTop α] (F : Functor J α) :
      limit F = Finset.univ.inf F.obj

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

      source
      theorem CategoryTheory.Limits.CompleteLattice.finite_colimit_eq_finset_univ_sup {α : Type u} {J : Type w} [SmallCategory J] [FinCategory J] [SemilatticeSup α] [OrderBot α] (F : Functor J α) :
      colimit F = Finset.univ.sup F.obj

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

      source
      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.

      source
      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.

      source
      @[instance 100]
      instance CategoryTheory.Limits.CompleteLattice.instHasBinaryProductsOfOrderTop {α : Type u} [SemilatticeInf α] [OrderTop α] :
      HasBinaryProducts α
      source
      @[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.

      source
      @[instance 100]
      instance CategoryTheory.Limits.CompleteLattice.instHasBinaryCoproductsOfOrderBot {α : Type u} [SemilatticeSup α] [OrderBot α] :
      HasBinaryCoproducts α
      source
      @[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.

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

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

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

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

      source
      def CategoryTheory.Limits.CompleteLattice.limitCone {α : Type u} [CompleteLattice α] {J : Type w} [Category.{w', w} J] (F : Functor J α) :
      LimitCone F

      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
        source
        @[simp]
        theorem CategoryTheory.Limits.CompleteLattice.limitCone_isLimit_lift {α : Type u} [CompleteLattice α] {J : Type w} [Category.{w', w} J] (F : Functor J α) (s : Cone F) :
        (limitCone F).isLimit.lift s = homOfLE ⋯
        source
        @[simp]
        theorem CategoryTheory.Limits.CompleteLattice.limitCone_cone_pt {α : Type u} [CompleteLattice α] {J : Type w} [Category.{w', w} J] (F : Functor J α) :
        (limitCone F).cone.pt = iInf F.obj
        source
        @[simp]
        theorem CategoryTheory.Limits.CompleteLattice.limitCone_cone_π_app {α : Type u} [CompleteLattice α] {J : Type w} [Category.{w', w} J] (F : Functor J α) (x✝ : J) :
        (limitCone F).cone.π.app x✝ = homOfLE ⋯
        source
        def CategoryTheory.Limits.CompleteLattice.colimitCocone {α : Type u} [CompleteLattice α] {J : Type w} [Category.{w', w} J] (F : Functor J α) :
        ColimitCocone F

        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
          source
          @[simp]
          theorem CategoryTheory.Limits.CompleteLattice.colimitCocone_cocone_ι_app {α : Type u} [CompleteLattice α] {J : Type w} [Category.{w', w} J] (F : Functor J α) (x✝ : J) :
          (colimitCocone F).cocone.ι.app x✝ = homOfLE ⋯
          source
          @[simp]
          theorem CategoryTheory.Limits.CompleteLattice.colimitCocone_isColimit_desc {α : Type u} [CompleteLattice α] {J : Type w} [Category.{w', w} J] (F : Functor J α) (s : Cocone F) :
          (colimitCocone F).isColimit.desc s = homOfLE ⋯
          source
          @[simp]
          theorem CategoryTheory.Limits.CompleteLattice.colimitCocone_cocone_pt {α : Type u} [CompleteLattice α] {J : Type w} [Category.{w', w} J] (F : Functor J α) :
          (colimitCocone F).cocone.pt = iSup F.obj
          source
          @[instance 100]
          instance CategoryTheory.Limits.CompleteLattice.hasLimits_of_completeLattice {α : Type u} [CompleteLattice α] :
          HasLimitsOfSize.{w, w', u, u} α
          source
          @[instance 100]
          instance CategoryTheory.Limits.CompleteLattice.hasColimits_of_completeLattice {α : Type u} [CompleteLattice α] :
          HasColimitsOfSize.{w, w', u, u} α
          source
          theorem CategoryTheory.Limits.CompleteLattice.limit_eq_iInf {α : Type u} [CompleteLattice α] {J : Type w} [Category.{w', w} J] (F : Functor J α) :
          limit F = iInf F.obj

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

          source
          theorem CategoryTheory.Limits.CompleteLattice.colimit_eq_iSup {α : Type u} [CompleteLattice α] {J : Type w} [Category.{w', w} J] (F : Functor J α) :
          colimit F = iSup F.obj

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