CategoryTheory.Limits.hasWidePullbacks_shrink
theorem CategoryTheory.Limits.hasWidePullbacks_shrink :
∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Limits.HasWidePullbacks C],
CategoryTheory.Limits.HasWidePullbacks C
This theorem states that if a category has wide pullbacks on a higher universe level, it also possesses wide pullbacks on a lower universe level. In the context of category theory, a wide pullback is a type of limit utilized to describe certain types of commutative diagrams. This theorem is essentially about the preservation of this property (having wide pullbacks) when we move from a higher universe level to a lower one within the same category.
More concisely: If a category has wide pullbacks in a higher universe level, it also has wide pullbacks in a lower universe level.
|
CategoryTheory.Limits.WidePushout.arrow_ι
theorem CategoryTheory.Limits.WidePushout.arrow_ι :
∀ {J : Type w} {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {B : C} {objs : J → C}
(arrows : (j : J) → B ⟶ objs j) [inst_1 : CategoryTheory.Limits.HasWidePushout B objs arrows] (j : J),
CategoryTheory.CategoryStruct.comp (arrows j) (CategoryTheory.Limits.WidePushout.ι arrows j) =
CategoryTheory.Limits.WidePushout.head arrows
The theorem `CategoryTheory.Limits.WidePushout.arrow_ι` states that for all types `J` and `D`, where 'D' is a category, and for all objects `B` in `D` and a function `objs` from `J` to `D`, if a `widePushout` exists for `B` and `objs` with a specified set of arrows, then for each `j` in `J`, the composite of the arrow from `B` to `objs j` and the unique arrow from `objs j` to the `widePushout` is equal to the unique arrow from the head, `B`, to the `widePushout`. This is a property of the universal property of `widePushout` in category theory which says that given a diagram with a specified set of arrows (functions) from `B` to `objs j` for all `j` in `J`, there exists a unique arrow from the head of the diagram, `B`, to the `widePushout` such that the diagram commutes.
More concisely: Given a category `D`, an object `B` in `D`, a function `objs : J -> D` from a type `J` to `D`, and a wide pushout of `B` and `objs` with a specified set of arrows, the composite of the arrow from `B` to `objs j` and the unique arrow from `objs j` to the wide pushout equals the unique arrow from `B` to the wide pushout for all `j` in `J`.
|
CategoryTheory.Limits.WidePullback.lift_π
theorem CategoryTheory.Limits.WidePullback.lift_π :
∀ {J : Type w} {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {B : C} {objs : J → C}
(arrows : (j : J) → objs j ⟶ B) [inst_1 : CategoryTheory.Limits.HasWidePullback B objs arrows] {X : C} (f : X ⟶ B)
(fs : (j : J) → X ⟶ objs j) (w : ∀ (j : J), CategoryTheory.CategoryStruct.comp (fs j) (arrows j) = f) (j : J),
CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.WidePullback.lift f fs w)
(CategoryTheory.Limits.WidePullback.π arrows j) =
fs j
The theorem `CategoryTheory.Limits.WidePullback.lift_π` states that in a category `D` with a wide pullback indexed by `J`, given objects `B`, `objs`, a morphism `f` from some object `X` to `B`, and a family of morphisms `fs` from `X` to each of the `objs`, satisfying that the composition of the morphism `fs j` and `arrows j` is equal to `f` for each `j` in `J`, then the composition of the 'lift' of `f` over the wide pullback and the projection from the pullback to the object indexed by `j` is equal to `fs j`. In the context of category theory, this means that the 'lift' operation is consistent with the projections in the pullback diagram.
More concisely: Given a wide pullback diagram in a category with a morphism `f` and a family of morphisms `fs` such that `fs j ∘ arrows j = f` for all `j`, the 'lift' of `f` over the pullback and the projection to the object indexed by `j` compose to `fs j`.
|
CategoryTheory.Limits.WidePullback.π_arrow
theorem CategoryTheory.Limits.WidePullback.π_arrow :
∀ {J : Type w} {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {B : C} {objs : J → C}
(arrows : (j : J) → objs j ⟶ B) [inst_1 : CategoryTheory.Limits.HasWidePullback B objs arrows] (j : J),
CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.WidePullback.π arrows j) (arrows j) =
CategoryTheory.Limits.WidePullback.base arrows
The theorem `CategoryTheory.Limits.WidePullback.π_arrow` is a statement about the structure of wide pullbacks in a category. If we have a wide pullback in a category, indexed by a type `J` and defined for a base object `B` and a family of objects `objs : J → D`, where `D` is the type of objects in the category and each object in `objs` comes with a morphism `arrows : (j : J) → objs j ⟶ B` to `B`, then for any index `j` in `J`, the composition of the projection morphism from the wide pullback to the object `objs j` and the corresponding `arrows j` morphism is equal to the base morphism of the wide pullback. This is essentially the universal property of the wide pullback in categorical terms.
More concisely: Given a wide pullback in a category indexed by type J and defined for a base object B and a family of morphisms arrows : J → Obj(C) × Morp(C) with Obj(C) the type of objects and Morp(C) the type of morphisms in C, for each j in J, the composition of the projection morphism to objs j and arrows j is equal to the base morphism of the wide pullback.
|
CategoryTheory.Limits.hasWidePushouts_shrink
theorem CategoryTheory.Limits.hasWidePushouts_shrink :
∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Limits.HasWidePushouts C],
CategoryTheory.Limits.HasWidePushouts C
This theorem states that if a category `C` has wide pushouts at a certain universe level, then it also has wide pushouts at any lower universe level. In terms of category theory, a wide pushout is a generalization of the notion of a pushout to arbitrary diagrams. This theorem essentially guarantees that the existence of wide pushouts is preserved when moving to lower universe levels in the category `C`.
More concisely: If a category `C` has wide pushouts at a given universe level, then it also has wide pushouts at any lower universe level.
|
CategoryTheory.Limits.WidePullback.lift_base
theorem CategoryTheory.Limits.WidePullback.lift_base :
∀ {J : Type w} {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {B : C} {objs : J → C}
(arrows : (j : J) → objs j ⟶ B) [inst_1 : CategoryTheory.Limits.HasWidePullback B objs arrows] {X : C} (f : X ⟶ B)
(fs : (j : J) → X ⟶ objs j) (w : ∀ (j : J), CategoryTheory.CategoryStruct.comp (fs j) (arrows j) = f),
CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.WidePullback.lift f fs w)
(CategoryTheory.Limits.WidePullback.base arrows) =
f
This theorem, `CategoryTheory.Limits.WidePullback.lift_base`, states that in any category with a wide pullback along a collection of arrows from objects to a base object `B`, if we have an object `X` and morphisms from `X` to each object in the collection such that each composition of a morphism from `X` to an object in the collection and the arrow from that object to `B` is equal to a given morphism from `X` to `B`, then the composition of the lift (constructed from these morphisms from `X` and the equality conditions) and the base morphism of the wide pullback is equal to the given morphism from `X` to `B`. In simpler terms, it's saying that a certain diagram involving the wide pullback, the object `X` and the given morphisms commutes.
More concisely: In a category with wide pullbacks, if for each object in a collection, there exists a morphism from an object X to it such that the composition of the morphism from X to the object and the arrow from that object to the base object is equal to a given morphism from X to the base object, then the lift constructed from these morphisms commutes with the base morphism of the wide pullback, resulting in the equality of the given morphism from X to the base object.
|
Mathlib.CategoryTheory.Limits.Shapes.WidePullbacks._auxLemma.1
theorem Mathlib.CategoryTheory.Limits.Shapes.WidePullbacks._auxLemma.1 :
∀ {α : Sort u_1} [inst : Subsingleton α] (x y : α), (x = y) = True
This theorem is from the Category Theory section of the Mathlib library, specifically dealing with Limits and Shapes, and Wide Pullbacks. It states that for any type `α` which is a subsingleton (i.e., a type with at most one element), any two elements `x` and `y` of `α` are equal. This is expressed as `(x = y) = True`. This makes intuitive sense, because if `α` can only have one element, any two elements of `α` must be the same element.
More concisely: For any subsingleton type `α`, any two elements `x` and `y` of `α` are equal. (i.e., `x = y` holds in `α`).
|