CategoryTheory.Limits.CompleteLattice.finite_colimit_eq_finset_univ_sup
theorem CategoryTheory.Limits.CompleteLattice.finite_colimit_eq_finset_univ_sup :
∀ {α : Type u} {J : Type w} [inst : CategoryTheory.SmallCategory J] [inst_1 : CategoryTheory.FinCategory J]
[inst_2 : SemilatticeSup α] [inst_3 : OrderBot α] (F : CategoryTheory.Functor J α),
CategoryTheory.Limits.colimit F = Finset.univ.sup F.obj
The theorem `CategoryTheory.Limits.CompleteLattice.finite_colimit_eq_finset_univ_sup` states that for any category `J` that is both a small category and a finite category, and any `α` that is a semilattice with a minimal element, the colimit of a functor `F` from `J` to `α` equals the supremum of the objects in the image of `F`. Here, the supremum is taken over the universal finite set `Finset.univ` associated with the object type. Hence, this theorem provides a way to express the colimit in terms of supremum operation, under certain conditions on the category and the target object type.
More concisely: For any small and finite category J, functor F from J to a semilattice α with a minimal element, the colimit of F equals the supremum of the images of objects in J taken over the universal set Finset.univ.
|
CategoryTheory.Limits.CompleteLattice.finite_limit_eq_finset_univ_inf
theorem CategoryTheory.Limits.CompleteLattice.finite_limit_eq_finset_univ_inf :
∀ {α : Type u} {J : Type w} [inst : CategoryTheory.SmallCategory J] [inst_1 : CategoryTheory.FinCategory J]
[inst_2 : SemilatticeInf α] [inst_3 : OrderTop α] (F : CategoryTheory.Functor J α),
CategoryTheory.Limits.limit F = Finset.univ.inf F.obj
This theorem states that for any type `α` and any index type `J`, given that `J` forms a small and finite category, and `α` has a semilattice (infimum) structure along with the presence of a top element, for any functor `F` from `J` to `α`, the limit of the functor `F` is the infimum of the objects in the image of `F` over the universal finite set. In other words, in the context of a complete lattice, the limit of a functor from a finite category is equal to the infimum of the set of all objects in the image of the functor.
More concisely: Given a small and finite category `J`, a complete lattice `α` with a top element, and a functor `F` from `J` to `α`, the limit of `F` is the infimum of `F`'s image.
|
CategoryTheory.Limits.CompleteLattice.coprod_eq_sup
theorem CategoryTheory.Limits.CompleteLattice.coprod_eq_sup :
∀ {α : Type u} [inst : SemilatticeSup α] [inst_1 : OrderBot α] (x y : α), (x ⨿ y) = x ⊔ y
This theorem states that for any type `α` that is a `SemilatticeSup` (a semilattice with a supremum operation) and also an `OrderBot` (a total order with a bottom element), the binary coproduct (denoted as `x ⨿ y`) in the category of `α` is equivalent to the supremum (denoted as `x ⊔ y`) of two elements `x` and `y` of type `α`. Essentially, in such a category, the "maximum" or "union" of two elements can be computed using either the category-theoretic notion of coproduct or the order-theoretic notion of supremum, and these two computations will yield the same result.
More concisely: In the category of types equipped with a semilattice supremum and a bottom element, the binary coproduct of any two elements is equivalent to their supremum.
|
CategoryTheory.Limits.CompleteLattice.limit_eq_iInf
theorem CategoryTheory.Limits.CompleteLattice.limit_eq_iInf :
∀ {α : Type u} [inst : CompleteLattice α] {J : Type u} [inst_1 : CategoryTheory.SmallCategory J]
(F : CategoryTheory.Functor J α), CategoryTheory.Limits.limit F = iInf F.obj
This theorem states that for any complete lattice `α` and any small category `J`, if a functor `F` from `J` to `α` is given, then the limit of the functor `F` is equal to the infimum of the objects in the image of `F`. In other words, if we consider the objects of the category `J` as being mapped into the complete lattice `α` by `F`, the limit of this functor (a concept from category theory) is exactly the infimum (a concept from order theory and lattice theory) of the set of these mapped objects. This theorem, therefore, provides a connection between category theory and lattice theory.
More concisely: The limit of a functor from a small category to a complete lattice equals the infimum of the images of the objects under the functor.
|
CategoryTheory.Limits.CompleteLattice.pushout_eq_sup
theorem CategoryTheory.Limits.CompleteLattice.pushout_eq_sup :
∀ {α : Type u} [inst : SemilatticeSup α] [inst_1 : OrderBot α] (x y z : α) (f : z ⟶ x) (g : z ⟶ y),
CategoryTheory.Limits.pushout f g = x ⊔ y
The theorem `CategoryTheory.Limits.CompleteLattice.pushout_eq_sup` states that for any semilattice sup (a partially ordered set where any two elements have a least upper bound) with an order bot (a partially ordered set that has a smallest element), and for any three elements `x`, `y`, and `z` in this set along with morphisms `f : z ⟶ x` and `g : z ⟶ y`, the pushout of the pair of morphisms `f` and `g` is equal to the supremum of `x` and `y`. In mathematical terms, this theorem reveals a relationship between category theory and order theory by showing that the pushout in the category of a semilattice sup with an order bot corresponds to the supremum operation in the semilattice.
More concisely: The pushout of morphisms in the category of a semilattice sup with an order bot equals the supremum of the sources in the semilattice.
|
CategoryTheory.Limits.CompleteLattice.finite_product_eq_finset_inf
theorem CategoryTheory.Limits.CompleteLattice.finite_product_eq_finset_inf :
∀ {α : Type u} [inst : SemilatticeInf α] [inst_1 : OrderTop α] {ι : Type u} [inst_2 : Fintype ι] (f : ι → α),
∏ f = Fintype.elems.inf f
This theorem states that in the category of a `SemilatticeInf` with `OrderTop`, the finite product is equivalent to the infimum. Specifically, for any function `f` from a finite type `ι` to `α`, the product of `f` over all elements in `ι` equals to the infimum of `f` over all elements in `ι`. Here, `SemilatticeInf` refers to a semilattice structure equipped with a binary operation "infimum" (or "greatest lower bound") and `OrderTop` means there is a greatest element in the order. The `Fintype.elems.inf f` is the infimum of `f` over all elements in the finite type `ι`.
More concisely: In the category of a semilattice equipped with an order and a greatest element, the finite product of a function from a finite type equals the infimum of that function over all elements.
|
CategoryTheory.Limits.CompleteLattice.prod_eq_inf
theorem CategoryTheory.Limits.CompleteLattice.prod_eq_inf :
∀ {α : Type u} [inst : SemilatticeInf α] [inst_1 : OrderTop α] (x y : α), (x ⨯ y) = x ⊓ y
This theorem states that for any type `α` that has a structure of a `SemilatticeInf` and an `OrderTop`, the binary product in the category `α` is equivalent to the infimum of two elements of `α`. In other words, for any two elements `x` and `y` of `α`, their binary product `(x ⨯ y)` is equal to their infimum `(x ⊓ y)`.
More concisely: For any type `α` equipped with both a `SemilatticeInf` and `OrderTop` structure, the binary product of any two elements equals their infimum.
|
CategoryTheory.Limits.CompleteLattice.finite_coproduct_eq_finset_sup
theorem CategoryTheory.Limits.CompleteLattice.finite_coproduct_eq_finset_sup :
∀ {α : Type u} [inst : SemilatticeSup α] [inst_1 : OrderBot α] {ι : Type u} [inst_2 : Fintype ι] (f : ι → α),
∐ f = Fintype.elems.sup f
This theorem states that in the category theory context, a finite coproduct in a `semilatticeSup` with a least element (`OrderBot`) is equivalent to the supremum of a `Finset`. More specifically, for any set `ι` of finite type (`Fintype ι`), and a function `f` that maps from `ι` to an element of the `SemilatticeSup`, the coproduct of `f` (∐ f) is equal to the supremum of `f` over the `Finset` of all elements of `ι` (`Fintype.elems.sup f`).
More concisely: In the context of category theory, the finite coproduct of a function from a finite set to a `SemilatticeSup` with a least element is equivalent to the supremum of that function over the set.
|
CategoryTheory.Limits.CompleteLattice.colimit_eq_iSup
theorem CategoryTheory.Limits.CompleteLattice.colimit_eq_iSup :
∀ {α : Type u} [inst : CompleteLattice α] {J : Type u} [inst_1 : CategoryTheory.SmallCategory J]
(F : CategoryTheory.Functor J α), CategoryTheory.Limits.colimit F = iSup F.obj
The theorem `CategoryTheory.Limits.CompleteLattice.colimit_eq_iSup` states that in the context of a complete lattice `α` and a small category `J`, for any functor `F` from `J` to `α`, the colimit of `F` is equal to the indexed supremum of the objects in the image of `F`. That is, it asserts that in a complete lattice, the colimit of a functor can be computed as the supremum of the set of its values.
More concisely: In a complete lattice, the colimit of a functor is equal to the supremum of the images of its objects under that functor.
|
CategoryTheory.Limits.CompleteLattice.pullback_eq_inf
theorem CategoryTheory.Limits.CompleteLattice.pullback_eq_inf :
∀ {α : Type u} [inst : SemilatticeInf α] [inst_1 : OrderTop α] {x y z : α} (f : x ⟶ z) (g : y ⟶ z),
CategoryTheory.Limits.pullback f g = x ⊓ y
This theorem states that, in the category of a semilattice with an infimum operation and a greatest element (`OrderTop`), the pullback of two morphisms `f` and `g` from objects `x` and `y` respectively to the same object `z`, is equal to the infimum (the greatest lower bound - represented as `x ⊓ y` in Lean 4) of `x` and `y`. In other words, in such a category, calculating the pullback of two morphisms can be done by simply finding the greatest lower bound of the objects from which the morphisms originate.
More concisely: In the category of a semilattice with an infimum operation and a greatest element, the pullback of two morphisms is equal to the infimum of their source objects.
|