Mathlib.AlgebraicTopology.SimplicialObject._auxLemma.2
theorem Mathlib.AlgebraicTopology.SimplicialObject._auxLemma.2 : ∀ {n : ℕ} (a : Fin (n + 1)), (a < 0) = False := by
sorry
This theorem, `Mathlib.AlgebraicTopology.SimplicialObject._auxLemma.2`, asserts that for any natural number `n` and any value `a` that is a finite number in the range `0` to `n+1`, the condition `(a < 0)` is always false. Essentially, this is stating that a nonnegative finite number can never be less than zero.
More concisely: For any natural number `n` and any finite value `a` in the range `[0, n+1]`, `a` is not less than zero.
|
CategoryTheory.CosimplicialObject.δ_comp_σ_succ
theorem CategoryTheory.CosimplicialObject.δ_comp_σ_succ :
∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] (X : CategoryTheory.CosimplicialObject C) {n : ℕ}
{i : Fin (n + 1)},
CategoryTheory.CategoryStruct.comp (X.δ i.succ) (X.σ i) =
CategoryTheory.CategoryStruct.id (X.obj (SimplexCategory.mk n))
The theorem `CategoryTheory.CosimplicialObject.δ_comp_σ_succ` presents the second part of the third cosimplicial identity in category theory. In the context of a given category `C` and a `CosimplicialObject` `X` in `C`, for any natural number `n` and any `i` of `Fin (n + 1)`, the composition of the δ morphism applied to the successor of `i` and the σ morphism applied to `i` equals the identity morphism on the object `X.obj` of `SimplexCategory` corresponding to `n`. This identity is fundamentally important in the theory of cosimplicial objects, which in turn plays a significant role in areas like algebraic topology.
More concisely: For any cosimplicial object X in a category C and natural number n, the composition of the δ morphism applied to the successor of i and the σ morphism applied to i equals the identity morphism on X.obj of SimplexCategory(n).
|
CategoryTheory.SimplicialObject.δ_comp_σ_of_le
theorem CategoryTheory.SimplicialObject.δ_comp_σ_of_le :
∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] (X : CategoryTheory.SimplicialObject C) {n : ℕ}
{i : Fin (n + 2)} {j : Fin (n + 1)},
i ≤ j.castSucc →
CategoryTheory.CategoryStruct.comp (X.σ j.succ) (X.δ i.castSucc) =
CategoryTheory.CategoryStruct.comp (X.δ i) (X.σ j)
This theorem, known as "The Second Simplicial Identity", holds in the context of category theory. It states that for any category `C`, and for any simplicial object `X` in `C` (which is a contravariant functor from the simplex category to `C`), given natural numbers `n`, `i` and `j` such that `i` is less than or equal to `j.castSucc`, the composition of the morphisms `X.σ j.succ` and `X.δ i.castSucc` is the same as the composition of the morphisms `X.δ i` and `X.σ j`. This identity is a fundamental property of simplicial objects in a category, and is a part of the combinatorial structure that makes these objects useful in many areas of mathematics.
More concisely: For any simplicial object X in a category C, the composition of X.σ (j.castSucc) and X.δ (i.castSucc) equals the composition of X.δ i and X.σ j, where i ≤ j in the category of natural numbers.
|
CategoryTheory.CosimplicialObject.δ_comp_σ_self
theorem CategoryTheory.CosimplicialObject.δ_comp_σ_self :
∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] (X : CategoryTheory.CosimplicialObject C) {n : ℕ}
{i : Fin (n + 1)},
CategoryTheory.CategoryStruct.comp (X.δ i.castSucc) (X.σ i) =
CategoryTheory.CategoryStruct.id (X.obj (SimplexCategory.mk n))
This theorem states the first part of the third cosimplicial identity in category theory. Given a cosimplicial object `X` in a category `C` and a natural number `n`, for any `i` which is a finite number less than `n + 1`, the composition of the δ-morphism at `i.castSucc` and the σ-morphism at `i` of `X` is equivalent to the identity morphism on the object of `X` associated with `n` in the simplex category. The δ and σ are certain natural transformations associated with a cosimplicial object in category theory.
More concisely: For any cosimplicial object X in a category C and natural number n, the composition of the δ-morphism at i.succ and the σ-morphism at i of X is equal to the identity morphism on X(n) in the simplex category.
|
CategoryTheory.CosimplicialObject.δ_comp_δ_self
theorem CategoryTheory.CosimplicialObject.δ_comp_δ_self :
∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] (X : CategoryTheory.CosimplicialObject C) {n : ℕ}
{i : Fin (n + 2)},
CategoryTheory.CategoryStruct.comp (X.δ i) (X.δ i.castSucc) =
CategoryTheory.CategoryStruct.comp (X.δ i) (X.δ i.succ)
The theorem `CategoryTheory.CosimplicialObject.δ_comp_δ_self` is a special case of the first cosimplicial identity in category theory. This theorem states that for any type `C` that forms a category, and for any cosimplicial object `X` in that category, for any natural number `n` and for any finite ordinal `i` within the range `0` to `n + 2`, the composition of the `i`-th face map `δ` with the successor of `i` in the face maps is equal to the composition of the `i`-th face map `δ` with the `i`-th face map itself. In other words, it holds that `(X.δ i) ≫ (X.δ i.castSucc) = (X.δ i) ≫ (X.δ i.succ)`. This identity is a key part of the structure of a cosimplicial object in any category.
More concisely: For any cosimplicial object X in a category C and natural number n, for all i in 0 to n+1, the composition of the i-th face map with its successor is equal to the composition of the i-th face map with itself: (X.δ i) ≫ (X.δ (i.castSucc)) = (X.δ i) ≫ (X.δ i.succ).
|
CategoryTheory.CosimplicialObject.δ_comp_σ_of_le
theorem CategoryTheory.CosimplicialObject.δ_comp_σ_of_le :
∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] (X : CategoryTheory.CosimplicialObject C) {n : ℕ}
{i : Fin (n + 2)} {j : Fin (n + 1)},
i ≤ j.castSucc →
CategoryTheory.CategoryStruct.comp (X.δ i.castSucc) (X.σ j.succ) =
CategoryTheory.CategoryStruct.comp (X.σ j) (X.δ i)
This theorem, known as the second cosimplicial identity, applies to a cosimplicial object `X` in a category `C`. It states that for any natural number `n`, and for any two finite ordinal numbers `i` and `j` such that `i` is less than or equal to the successor of `j`, the composition of the morphism `δ` at the successor of `i` and the morphism `σ` at the successor of `j` in `X` is equal to the composition of the morphism `σ` at `j` and the morphism `δ` at `i` in `X`. Here, `δ` and `σ` are morphisms that are generally associated with face and degeneracy maps in a cosimplicial object, a structure that is often used in algebraic topology and in the theory of simplicial sets.
More concisely: For any cosimplicial object X in a category C and natural numbers n, i < succ(j), the composition of δ(X(succ(i))) and σ(X(succ(j))) equals the composition of σ(X(j)) and δ(X(i)).
|
CategoryTheory.SimplicialObject.δ_comp_σ_succ
theorem CategoryTheory.SimplicialObject.δ_comp_σ_succ :
∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] (X : CategoryTheory.SimplicialObject C) {n : ℕ}
{i : Fin (n + 1)},
CategoryTheory.CategoryStruct.comp (X.σ i) (X.δ i.succ) =
CategoryTheory.CategoryStruct.id (X.obj (Opposite.op (SimplexCategory.mk n)))
This theorem, named `CategoryTheory.SimplicialObject.δ_comp_σ_succ`, is part of the mathematical theory of simplicial objects in a category `C`. It states that for any simplicial object `X` in a given category, and for any natural number `n` and any element `i` in the finite set `Fin (n + 1)`, the composition of the morphisms `X.σ i` and `X.δ i.succ` is equal to the identity morphism on the object `X.obj (Opposite.op (SimplexCategory.mk n))`. This is the second part of the so-called third simplicial identity, an important identity in the theory of simplicial objects. The `σ` and `δ` functions are characteristic operations on simplicial objects, often referred to as "face" and "degeneracy" maps, respectively.
More concisely: For any simplicial object X in a category, and for any natural number n and elements i in Fin (n+1), the composition of X.σ i and X.δ i.succ equals the identity morphism on X.obj (Opposite.op (SimplexCategory.mk n)).
|
CategoryTheory.SimplicialObject.δ_comp_σ_self
theorem CategoryTheory.SimplicialObject.δ_comp_σ_self :
∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] (X : CategoryTheory.SimplicialObject C) {n : ℕ}
{i : Fin (n + 1)},
CategoryTheory.CategoryStruct.comp (X.σ i) (X.δ i.castSucc) =
CategoryTheory.CategoryStruct.id (X.obj (Opposite.op (SimplexCategory.mk n)))
This theorem represents the first part of the third simplicial identity in the category of simplicial objects. For any category 'C', and any simplicial object 'X' in 'C', and for any natural number 'n', and any index 'i' in a finite set of size 'n+1', the composition of the morphism 'σ i' followed by 'δ i.castSucc' on 'X' is equal to the identity morphism on the object 'X.obj' in the opposite category of the simplex category with 'n' as the object. This identity is a key property in the theory of simplicial objects in a category.
More concisely: For any simplicial object X in a category C and natural number n, the composition of σ i and δ i.castSucc on X is equal to the identity morphism on X.obj in the opposites simplex category, where i is an index of a finite set of size n+1.
|
CategoryTheory.SimplicialObject.Augmented.w₀
theorem CategoryTheory.SimplicialObject.Augmented.w₀ :
∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {X Y : CategoryTheory.SimplicialObject.Augmented C}
(f : X ⟶ Y),
CategoryTheory.CategoryStruct.comp
((CategoryTheory.SimplicialObject.Augmented.drop.map f).app (Opposite.op (SimplexCategory.mk 0)))
(Y.hom.app (Opposite.op (SimplexCategory.mk 0))) =
CategoryTheory.CategoryStruct.comp (X.hom.app (Opposite.op (SimplexCategory.mk 0)))
(CategoryTheory.SimplicialObject.Augmented.point.map f)
This theorem states that for any category `C` and any two augmented simplicial objects `X` and `Y` in this category, for any morphism `f` from `X` to `Y`, the composition of the map induced by `f` on the non-augmented part of `X` (result of `CategoryTheory.SimplicialObject.Augmented.drop.map f`) and the 0-simplex map of `Y` is equal to the composition of the 0-simplex map of `X` and the map induced by `f` on the point of the augmentation. This expresses the compatibility of a morphism with the augmentation, specifically on 0-simplices.
More concisely: For any category `C` and augmented simplicial objects `X` and `Y` in `C`, and any morphism `f : X → Y`, the diagram commutes:
```
X.0 → Y.0 ≅ X.drop.map f (Y.augmentation.app)
```
where `X.0` and `Y.0` are the 0-simplices of `X` and `Y`, respectively, `X.drop` is the non-augmented part of `X`, and `Y.augmentation.app` is the application of the augmentation of `Y` to the point.
|
CategoryTheory.SimplicialObject.δ_comp_δ
theorem CategoryTheory.SimplicialObject.δ_comp_δ :
∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] (X : CategoryTheory.SimplicialObject C) {n : ℕ}
{i j : Fin (n + 2)},
i ≤ j →
CategoryTheory.CategoryStruct.comp (X.δ j.succ) (X.δ i) =
CategoryTheory.CategoryStruct.comp (X.δ i.castSucc) (X.δ j)
This is a theorem in category theory, particularly in the study of simplicial objects. The theorem is known as the generic case of the first simplicial identity. It states that, for any category `C`, any simplicial object `X` in `C`, any natural number `n` and any two finite numbers `i` and `j` in the set `{0,1,...,n+1}` with `i` less than or equal to `j`, the composition of morphisms `X.δ j.succ` and `X.δ i` is equal to the composition of morphisms `X.δ i.castSucc` and `X.δ j`. Here, `.succ` is the successor function, `.castSucc` is a function that casts a finite number to its successor in the context of simplicial objects, and `X.δ` represents a morphism in the simplicial object `X`. In mathematical terms, it's saying that in a simplicial object, specific sequences of morphisms (maps between objects) commute, which is a fundamental property in category theory.
More concisely: For any simplicial object X in a category C and natural numbers n, i, j with i <= j, the compositions X.δ j . succ and X.δ i are equal: X.δ i . castSucc = X.δ j.
|
CategoryTheory.SimplicialObject.hom_ext
theorem CategoryTheory.SimplicialObject.hom_ext :
∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {X Y : CategoryTheory.SimplicialObject C} (f g : X ⟶ Y),
(∀ (n : SimplexCategoryᵒᵖ), f.app n = g.app n) → f = g
This theorem states that for any category `C` and for any two simplicial objects `X` and `Y` in category `C`, if two morphisms `f` and `g` from `X` to `Y` are such that their respective applications to any object `n` in the opposite of the SimplexCategory (denoted `SimplexCategoryᵒᵖ`) are equal, then the two morphisms `f` and `g` themselves are equal. In other words, it establishes the principle of extensionality for morphisms in the category of simplicial objects.
More concisely: If two morphisms between simplicial objects in a category have equal applications to all simplices in the opposite SimplexCategory, then they are equal.
|
CategoryTheory.CosimplicialObject.σ_comp_σ
theorem CategoryTheory.CosimplicialObject.σ_comp_σ :
∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] (X : CategoryTheory.CosimplicialObject C) {n : ℕ}
{i j : Fin (n + 1)},
i ≤ j →
CategoryTheory.CategoryStruct.comp (X.σ i.castSucc) (X.σ j) =
CategoryTheory.CategoryStruct.comp (X.σ j.succ) (X.σ i)
This theorem states the fifth cosimplicial identity in the context of category theory. Given a category `C` and a cosimplicial object `X` in `C`, for any natural number `n` and any two finite numbers `i` and `j` from the set `{0, 1, ..., n}`, if `i` is less than or equal to `j`, then the composition of the morphism associated with `i.castSucc` and the morphism associated with `j` in `X` is equal to the composition of the morphism associated with `j.succ` and the morphism associated with `i` in `X`. In other words, if we have two morphisms in a cosimplicial object such that they satisfy a certain order, their compositions in two different orders are equal.
More concisely: For any cosimplicial object X in a category C and natural numbers n, i, j with i <= j, the composition of X(i) with X(j) is equal to the composition of X(j) with X(i) in X.
|
CategoryTheory.SimplicialObject.δ_comp_δ_self
theorem CategoryTheory.SimplicialObject.δ_comp_δ_self :
∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] (X : CategoryTheory.SimplicialObject C) {n : ℕ}
{i : Fin (n + 2)},
CategoryTheory.CategoryStruct.comp (X.δ i.castSucc) (X.δ i) =
CategoryTheory.CategoryStruct.comp (X.δ i.succ) (X.δ i)
This theorem, named `CategoryTheory.SimplicialObject.δ_comp_δ_self`, states a specific case of the first simplicial identity in the category theory. For any category 'C' and any simplicial object 'X' in 'C', and given a natural number 'n' and an index 'i' which is a finite number in the range from 0 to 'n+2', the composition of the morphisms 'X.δ i.castSucc' and 'X.δ i' is equal to the composition of the morphisms 'X.δ i.succ' and 'X.δ i'. This is a property related to the internal structure of simplicial objects.
More concisely: For any simplicial object X in a category C and natural number n, the compositions X.δ i.castSucc ∘ X.δ i and X.δ i ∘ X.δ i.succ are equal for all i in the range 0 to n+2.
|
CategoryTheory.SimplicialObject.δ_comp_σ_of_gt
theorem CategoryTheory.SimplicialObject.δ_comp_σ_of_gt :
∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] (X : CategoryTheory.SimplicialObject C) {n : ℕ}
{i : Fin (n + 2)} {j : Fin (n + 1)},
j.castSucc < i →
CategoryTheory.CategoryStruct.comp (X.σ j.castSucc) (X.δ i.succ) =
CategoryTheory.CategoryStruct.comp (X.δ i) (X.σ j)
This theorem states the fourth simplicial identity in the context of category theory. Specifically, for any category `C`, and any simplicial object `X` in this category, given natural numbers `n`, `i` in the range 0 to `n + 2`, and `j` in the range 0 to `n + 1`, if `j.castSucc < i`, then the composition of the `σ`-morphism at `j.castSucc` and the `δ`-morphism at `i.succ` in the simplicial object `X` is equal to the composition of the `δ`-morphism at `i` and the `σ`-morphism at `j` in the simplicial object `X`. The `σ` and `δ` morphisms are maps that are used to define the structure of a simplicial object in a category.
More concisely: For any simplicial object X in a category C and natural numbers n, i, j such that j < i and i <= n+1, the composition of the σ-morphism at i.succ and the δ-morphism at j in X equals the composition of the δ-morphism at i and the σ-morphism at j.
|
CategoryTheory.CosimplicialObject.hom_ext
theorem CategoryTheory.CosimplicialObject.hom_ext :
∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {X Y : CategoryTheory.CosimplicialObject C} (f g : X ⟶ Y),
(∀ (n : SimplexCategory), f.app n = g.app n) → f = g
This theorem states that, given any type `C` with a category structure, and any two cosimplicial objects `X` and `Y` in this category, if we have two morphisms `f` and `g` from `X` to `Y`, then `f` is equal to `g` if and only if their application to every object `n` in the simplex category produces the same results. In simpler terms, two morphisms between the same pair of cosimplicial objects are identical if they coincide on every natural number in the simplex category.
More concisely: Given any category `C` with cosimplicial objects `X` and `Y`, and morphisms `f` and `g` from `X` to `Y`, they are equal if and only if for all `n`, `Fn = Gn` in `C(X(n), Y(n))`, where `Fn` and `Gn` are the application of `f` and `g` to the `n`-simplexes.
|
CategoryTheory.CosimplicialObject.δ_comp_δ
theorem CategoryTheory.CosimplicialObject.δ_comp_δ :
∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] (X : CategoryTheory.CosimplicialObject C) {n : ℕ}
{i j : Fin (n + 2)},
i ≤ j →
CategoryTheory.CategoryStruct.comp (X.δ i) (X.δ j.succ) =
CategoryTheory.CategoryStruct.comp (X.δ j) (X.δ i.castSucc)
This theorem, known as the generic case of the first cosimplicial identity, applies to a category `C` and a cosimplicial object `X` in the category `C`. It states that for any natural number `n` and any two elements `i` and `j` of the finite set `Fin (n + 2)` such that `i` is less than or equal to `j`, the composition of the `i-th` and the `j.succ-th` morphisms of `X` (denoted `X.δ i` and `X.δ j.succ`, respectively), is equal to the composition of the `j-th` and the `i.castSucc-th` morphisms of `X` (denoted `X.δ j` and `X.δ i.castSucc`, respectively). In mathematical terms, we have `(X.δ i) ≫ (X.δ j.succ) = (X.δ j) ≫ (X.δ i.castSucc)`.
More concisely: For any cosimplicial object X in a category C and natural numbers n, i <= j, the composition of X.δ i and X.δ (j.succ) equals the composition of X.δ j and X.δ (i.castSucc): X.δ i ≫ X.δ (j.succ) = X.δ j ≫ X.δ (i.castSucc).
|
CategoryTheory.SimplicialObject.σ_comp_σ
theorem CategoryTheory.SimplicialObject.σ_comp_σ :
∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] (X : CategoryTheory.SimplicialObject C) {n : ℕ}
{i j : Fin (n + 1)},
i ≤ j →
CategoryTheory.CategoryStruct.comp (X.σ j) (X.σ i.castSucc) =
CategoryTheory.CategoryStruct.comp (X.σ i) (X.σ j.succ)
The theorem `CategoryTheory.SimplicialObject.σ_comp_σ` states that in the category of simplicial objects valued in a category `C`, for any simplicial object `X`, and for any natural numbers `n`, `i` and `j` such that `i` is less than or equal to `j`, the composition of the morphisms `X.σ j` and `X.σ i.castSucc` equals the composition of the morphisms `X.σ i` and `X.σ j.succ`. This statement is an expression of the fifth simplicial identity in category theory.
More concisely: In the category of simplicial objects over a category `C`, for any `X:` `C`^Δ, and all `n`, `i`, and `j` with `i ≤ j`, `X.σ i ∘ X.σ^(-1) (j) = X.σ (j.succ ∘ i)`.
|
CategoryTheory.CosimplicialObject.δ_comp_σ_of_gt
theorem CategoryTheory.CosimplicialObject.δ_comp_σ_of_gt :
∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] (X : CategoryTheory.CosimplicialObject C) {n : ℕ}
{i : Fin (n + 2)} {j : Fin (n + 1)},
j.castSucc < i →
CategoryTheory.CategoryStruct.comp (X.δ i.succ) (X.σ j.castSucc) =
CategoryTheory.CategoryStruct.comp (X.σ j) (X.δ i)
The theorem `CategoryTheory.CosimplicialObject.δ_comp_σ_of_gt` states the fourth cosimplicial identity in the context of category theory. In particular, it states that for any category `C`, any cosimplicial object `X` in `C`, any natural numbers `n`, and any two finite ordinal numbers `i` and `j` such that `i` is greater than the successor of `j`, the composition of the morphisms `δ` of the successor of `i` and `σ` of the successor of `j` in `X` is equal to the composition of the morphisms `σ` of `j` and `δ` of `i` in `X`. Here, `δ` and `σ` are specific functions associated with the cosimplicial object, representing certain naturality conditions and relationships in the structure.
More concisely: For any cosimplicial object X in a category C, and for natural numbers n, i, and j with i > succ j, the composition of δ(succ i) and σ(succ j) equals the composition of σ(j) and δ(i) in X.
|