CategoryTheory.Limits.Types.initial_iff_empty
theorem CategoryTheory.Limits.Types.initial_iff_empty :
∀ (X : Type u), Nonempty (CategoryTheory.Limits.IsInitial X) ↔ IsEmpty X
This theorem states that an object in the category of types (i.e., `Type u`) is initial if and only if it is empty. In the context of category theory, an object is initial if there is precisely one morphism from it to any other object. Here, this theorem is asserting that this property for a type is equivalent to the type being empty.
More concisely: A type is initial in the category of types if and only if it is empty.
|
CategoryTheory.Limits.Types.unique_of_type_equalizer
theorem CategoryTheory.Limits.Types.unique_of_type_equalizer :
∀ {X Y Z : Type u} (f : X ⟶ Y) {g h : Y ⟶ Z}
(w : CategoryTheory.CategoryStruct.comp f g = CategoryTheory.CategoryStruct.comp f h),
CategoryTheory.Limits.IsLimit (CategoryTheory.Limits.Fork.ofι f w) → ∀ (y : Y), g y = h y → ∃! x, f x = y
The theorem `CategoryTheory.Limits.Types.unique_of_type_equalizer` in Lean 4 states that for any three types `X`, `Y`, and `Z` and any morphism `f` from `X` to `Y`, if there exist two morphisms `g` and `h` from `Y` to `Z` such that the composition of `f` and `g` is equal to the composition of `f` and `h` (denoted by `CategoryTheory.CategoryStruct.comp f g = CategoryTheory.CategoryStruct.comp f h`), and if the 'fork' formed by `f` and the equality of the two compositions is a limit in the category of types, then for every element `y` of `Y`, if `g y = h y`, there exists a unique `x` in `X` such that `f x = y`.
In simpler terms, this theorem relates to the concept of equalizers in category theory - if the composition of two morphisms are equal (they 'equalize') and the construct formed is a limit, then for every element that these two morphisms map to the same value, there exists a unique pre-image under the original morphism.
More concisely: Given types `X`, `Y`, and `Z`, and morphisms `f : X -> Y`, `g`, `h : Y -> Z` with `comp (f) (g) = comp (f) (h)` and the diagram formed by `f`, `g`, and `h` being a limit, then for every equal `y : Y` with `g y = h y`, there exists a unique `x : X` such that `f x = y`.
|
Mathlib.CategoryTheory.Limits.Shapes.Types._auxLemma.1
theorem Mathlib.CategoryTheory.Limits.Shapes.Types._auxLemma.1 :
∀ (α : Type u) (p : α → Prop), (∀ (x : (CategoryTheory.forget (Type u)).obj α), p x) = ∀ (x : α), p x
This theorem, often called as `_auxLemma.1`, describes a relationship between objects in a category and a particular property. Specifically, for all types `α` and any property `p` that might apply to elements of `α`, the theorem states that checking this property for every element in the image of `α` under the forgetful functor from the category of types to the category of sets is equivalent to checking the property for every element of `α` itself.
In more mathematical terms, if `α` is a type and `p` is some property, then `∀ (x : (CategoryTheory.forget (Type u)).obj α), p x` is equivalent to `∀ (x : α), p x`. This essentially says that the forgetful functor doesn't change the underlying set of elements, so checking a property `p` on all elements remains the same before and after applying the functor.
More concisely: The forgetful functor from the category of types to sets preserves the property of element-wise satisfaction of a given property.
|
CategoryTheory.Limits.Types.pi_map_π_apply
theorem CategoryTheory.Limits.Types.pi_map_π_apply :
∀ {β : Type v} [inst : Small.{u, v} β] {f g : β → Type u} (α : (j : β) → f j ⟶ g j) (b : β) (x : ∏ fun b => f b),
CategoryTheory.Limits.Pi.π g b (CategoryTheory.Limits.Pi.map α x) = α b (CategoryTheory.Limits.Pi.π f b x)
The theorem `CategoryTheory.Limits.Types.pi_map_π_apply` is a restatement of `Types.Limit.map_π_apply` in the context of category theory, using the `Pi.π` and `Pi.map` functions. It states that for any types `β`, `f` and `g`, where `f` and `g` are functions from `β` to `Type u`, any natural transformation `α` from `f` to `g`, any element `b` of type `β`, and any `x` in the product type over `f`, applying the projection map `Pi.π` for `g` at `b` to the result of mapping `α` over `x` equals the result of applying `α` at `b` to the projection of `x` at `b` under `f`. In other words, in terms of category theory, this theorem asserts the commutativity of a certain diagram involving products and projection maps in the category of types.
More concisely: For any natural transformation between two functions from a type to Type u, and for any element in the domain type and any element in the product type over the function, the projection maps commute up to the action of the natural transformation.
|
CategoryTheory.Limits.Types.pi_map_π_apply'
theorem CategoryTheory.Limits.Types.pi_map_π_apply' :
∀ {β : Type v} {f g : β → Type v} (α : (j : β) → f j ⟶ g j) (b : β) (x : ∏ fun b => f b),
CategoryTheory.Limits.Pi.π g b (CategoryTheory.Limits.Pi.map α x) = α b (CategoryTheory.Limits.Pi.π f b x)
This theorem, `CategoryTheory.Limits.Types.pi_map_π_apply'`, states that for any types `β`, function `f` and `g` mapping `β` to Type `v`, a natural transformation `α` from `f` to `g`, an element `b` of type `β`, and an object `x` in the product of `f`, the `b`-th projection of the result of applying `CategoryTheory.Limits.Pi.map` with `α` to `x` is equal to the result of applying the `b`-th morphism of `α` to the `b`-th projection of `x`. In other words, this theorem expresses the commutativity of a certain diagram in the category of types, which is essentially a specialized version of the naturality condition in category theory.
More concisely: For any types β, functions f and g from β to Type v, a natural transformation α from f to g, and an element b in β, the application of the b-th projection of the image of a product object under CategoryTheory.Limits.Pi.map using α is equal to the application of the b-th component of α to the b-th projection of the original product object.
|
CategoryTheory.Limits.Types.coequalizer_preimage_image_eq_of_preimage_eq
theorem CategoryTheory.Limits.Types.coequalizer_preimage_image_eq_of_preimage_eq :
∀ {X Y Z : Type u} (f g : X ⟶ Y) (π : Y ⟶ Z)
(e : CategoryTheory.CategoryStruct.comp f π = CategoryTheory.CategoryStruct.comp g π),
CategoryTheory.Limits.IsColimit (CategoryTheory.Limits.Cofork.ofπ π e) →
∀ (U : Set Y), f ⁻¹' U = g ⁻¹' U → π ⁻¹' (π '' U) = U
This theorem states that if a morphism `π` from `Y` to `Z` is an equalizer for a pair of morphisms `(f, g)` from `X` to `Y`, and there exists a subset `U` of `Y` such that the preimage of `U` under `f` equals the preimage of `U` under `g`, then the preimage of the image of `U` under `π` equals `U`. In other words, in the category of types, if two morphisms have the same preimage, then the preimage of the image under the equalizer morphism corresponds to the original set.
More concisely: If morphisms `π: Y ▶ Z`, `f, g: X ▶ Y` are such that `π` is the equalizer of `(f, g)` and the preimages of a subset `U` of `Y` under `f` and `g` are equal, then the preimage of the image of `U` under `π` equals `U`.
|
CategoryTheory.Limits.Types.pi_lift_π_apply
theorem CategoryTheory.Limits.Types.pi_lift_π_apply :
∀ {β : Type v} [inst : Small.{u, v} β] (f : β → Type u) {P : Type u} (s : (b : β) → P ⟶ f b) (b : β) (x : P),
CategoryTheory.Limits.Pi.π f b (CategoryTheory.Limits.Pi.lift s x) = s b x
This theorem expresses a fundamental property of product objects in category theory, specifically for types. Given a family of types `f : β → Type u`, a type `P : Type u`, and a collection of morphisms `s : (b : β) → P ⟶ f b` (in this context, morphisms are functions from `P` to each `f b`), for any element `x : P` and index `b : β`, applying the morphism `CategoryTheory.Limits.Pi.lift s` to `x` and then projecting onto the `b`-th component (using `CategoryTheory.Limits.Pi.π f b`) is the same as directly applying the `b`-th morphism `s b` to `x`. In other words, lifting `x` into the product type and then projecting it back down to `f b` gives the same result as directly mapping `x` to `f b` using `s b`.
More concisely: For any family of types `f : β → Type u`, type `P : Type u`, and morphisms `s : (b : β) → P → f b`, the application of `s b` to an element `x : P` is equal to the composition of lifting `x` to the product type `Π (b : β) f b` using `CategoryTheory.Limits.Pi.lift s`, and then projecting it back down to `f b` using `CategoryTheory.Limits.Pi.π`.
|
CategoryTheory.Limits.Types.pi_lift_π_apply'
theorem CategoryTheory.Limits.Types.pi_lift_π_apply' :
∀ {β : Type v} (f : β → Type v) {P : Type v} (s : (b : β) → P ⟶ f b) (b : β) (x : P),
CategoryTheory.Limits.Pi.π f b (CategoryTheory.Limits.Pi.lift s x) = s b x
The theorem `CategoryTheory.Limits.Types.pi_lift_π_apply'` states that for any indexing type `β`, any function `f` from `β` to some type, any type `P`, and any function `s` from `β` to the set of morphisms from `P` to `f b` (for some `b` in `β`), and any element `x` of `P`, the `b`-th projection of the product of `f` after applying the lift operation with s to x equals the application of the function `s` at `b` to `x`. In other words, lifting `s` on `x` and then projecting to the `b`-th factor gives the same result as directly applying `s` to `x` at `b`. This is a result about the interaction of lifting and projection operations in the context of categorical limits in the category of types.
More concisely: For any function `f` from an indexing type `β` to a type, any function `s` from `β` to the morphisms from a type `P` to `f b`, and any `x` in `P`, the application of `s` to `b` to `x` is equal to the projection of the product of `f` after lifting `s` on `x` to the `b`-th factor.
|