SimplexCategory.epi_iff_surjective
theorem SimplexCategory.epi_iff_surjective :
∀ {n m : SimplexCategory} {f : n ⟶ m},
CategoryTheory.Epi f ↔ Function.Surjective ⇑(SimplexCategory.Hom.toOrderHom f)
This theorem is stating that a morphism in the `SimplexCategory` is an epimorphism (a morphism which is right-cancellable) if and only if it is a surjective function (a function where every element in the codomain has a pre-image in the domain). Here, `SimplexCategory` is a category where objects are natural numbers, and morphisms from `n` to `m` are monotone functions from the finite set of size `n+1` to the finite set of size `m+1`. The theorem applies to any given natural numbers `n` and `m` in `SimplexCategory` and any morphism `f` from `n` to `m`. The surjectivity of the function is determined by the `Function.Surjective` predicate, which checks that every element in the codomain is the image of at least one element in the domain.
More concisely: A morphism in the SimplexCategory is an epimorphism if and only if it is a surjective function.
|
SimplexCategory.len_le_of_mono
theorem SimplexCategory.len_le_of_mono : ∀ {x y : SimplexCategory} {f : x ⟶ y}, CategoryTheory.Mono f → x.len ≤ y.len
This theorem states that a monomorphism in the SimplexCategory must increase lengths. Specifically, for any two natural numbers `x` and `y` in the SimplexCategory, and any monomorphism `f` from `x` to `y` in the sense of category theory, the length of `x` is less than or equal to the length of `y`. In other words, monomorphisms in the SimplexCategory can't decrease the lengths of their objects.
More concisely: In the SimplexCategory, the length of any object is not decreased by a monomorphism.
|
SimplexCategory.eq_id_of_isIso
theorem SimplexCategory.eq_id_of_isIso :
∀ {x : SimplexCategory} (f : x ⟶ x) [inst : CategoryTheory.IsIso f], f = CategoryTheory.CategoryStruct.id x := by
sorry
The theorem `SimplexCategory.eq_id_of_isIso` states that for all objects `x` in the SimplexCategory, if a morphism `f` from `x` to itself is an isomorphism (i.e., it has an inverse), then `f` is the identity morphism on `x`. In other words, any isomorphism from an object to itself in the SimplexCategory is the identity morphism. It asserts the uniqueness of identity in this category: no other morphism can have the properties of an identity morphism.
More concisely: In the SimplexCategory, every isomorphism from an object to itself is the identity morphism.
|
SimplexCategory.δ_comp_σ_self
theorem SimplexCategory.δ_comp_σ_self :
∀ {n : ℕ} {i : Fin (n + 1)},
CategoryTheory.CategoryStruct.comp (SimplexCategory.δ i.castSucc) (SimplexCategory.σ i) =
CategoryTheory.CategoryStruct.id (SimplexCategory.mk n)
This theorem states the first part of the third simplicial identity in the context of the Simplex Category. Specifically, for any natural number `n` and any element `i` of the finite set `Fin(n + 1)`, the composition of the `i`-th face map from `[n]` to `[n+1]` applied to the successor of `i`, and the `i`-th degeneracy map from `[n+1]` to `[n]`, is equal to the identity morphism on the `n`-th object of the Simplex Category. In other words, it asserts that applying first a face map and then a degeneracy map results in no change to the original object.
More concisely: For any natural number `n` and element `i` of `Fin(n + 1)`, the composition of the `i`-th face map from `[n]` to `[n+1]` and the `i`-th degeneracy map from `[n+1]` to `[n]` is the identity morphism on `[n]` in the Simplex Category.
|
SimplexCategory.δ_comp_σ_of_le
theorem SimplexCategory.δ_comp_σ_of_le :
∀ {n : ℕ} {i : Fin (n + 2)} {j : Fin (n + 1)},
i ≤ j.castSucc →
CategoryTheory.CategoryStruct.comp (SimplexCategory.δ i.castSucc) (SimplexCategory.σ j.succ) =
CategoryTheory.CategoryStruct.comp (SimplexCategory.σ j) (SimplexCategory.δ i)
The theorem `SimplexCategory.δ_comp_σ_of_le` states the second simplicial identity in the context of the Simplex Category. Specifically, for any natural number `n` and for any two 'finite' natural numbers `i` and `j` where `i` is less than or equal to `j` incremented by one (`j.castSucc`), the composition of the `i`-th face map following the successor of `j`-th degeneracy map is equal to the composition of the `j`-th degeneracy map following the `i`-th face map. Essentially, this theorem presents a relation between the morphisms of the Simplex Category, which are fundamental to the structure of a simplicial complex in algebraic topology.
More concisely: For any natural number `n` and finite natural numbers `i` and `j` with `i < j.castSucc`, the composition of the `i`-th face map with the `j`-th degeneracy map is equal to the composition of the `j`-th degeneracy map with the `(i+1)`-th face map in the Simplex Category.
|
SimplexCategory.δ_comp_σ_of_gt
theorem SimplexCategory.δ_comp_σ_of_gt :
∀ {n : ℕ} {i : Fin (n + 2)} {j : Fin (n + 1)},
j.castSucc < i →
CategoryTheory.CategoryStruct.comp (SimplexCategory.δ i.succ) (SimplexCategory.σ j.castSucc) =
CategoryTheory.CategoryStruct.comp (SimplexCategory.σ j) (SimplexCategory.δ i)
This theorem, known as the fourth simplicial identity, is stated within the context of the simplex category. For all natural numbers `n`, and for any `i` in `Fin (n + 2)` and `j` in `Fin (n + 1)`, if `j` embedded into `Fin (n + 2)` via `Fin.castSucc` is less than `i`, then the composition of the `i`-th face map of `[n]` to `[n+1]` after incrementing `i` with the `j`-th degeneracy map from `[n+1]` to `[n]` after embedding `j` into `Fin (n + 2)`, is the same as the composition of the `j`-th degeneracy map from `[n+1]` to `[n]` with the `i`-th face map from `[n]` to `[n+1]`. In mathematical terms, this means δ(i+1) ∘ σ(j+1) = σ(j) ∘ δ(i) whenever j+1 < i.
More concisely: For all natural numbers n and i, j in Fin (n+2), if j < i then the i-th face map of [n] to [n+1] followed by the j-th degeneracy map from [n+1] to [n] equals the j-th degeneracy map from [n+1] to [n] followed by the i-th face map from [n] to [n+1].
|
SimplexCategory.δ_comp_σ_succ
theorem SimplexCategory.δ_comp_σ_succ :
∀ {n : ℕ} {i : Fin (n + 1)},
CategoryTheory.CategoryStruct.comp (SimplexCategory.δ i.succ) (SimplexCategory.σ i) =
CategoryTheory.CategoryStruct.id (SimplexCategory.mk n)
This theorem, `SimplexCategory.δ_comp_σ_succ`, describes the second part of the third simplicial identity, a fundamental property in the context of the Simplex Category. Concretely, it states that for any natural number `n` and for any `i` which is a number from `0` to `n` (represented as a `Fin (n + 1)`), the composition of the `i+1`-th face map from `[n]` to `[n+1]` (denoted `SimplexCategory.δ (Fin.succ i)`) and the `i`-th degeneracy map from `[n+1]` to `[n]` (denoted `SimplexCategory.σ i`) is the identity morphism on the object `[n]` in the Simplex Category. In other words, composing these two operations results in the original object, reflecting the identity `δ_{i+1} ∘ σ_i = id`.
More concisely: The composition of the `(i+1)`-th face map and the `i`-th degeneracy map in the Simplex Category is the identity map on `[n]` for any `n` and `0 ≤ i ≤ n`.
|
SimplexCategory.δ_comp_δ
theorem SimplexCategory.δ_comp_δ :
∀ {n : ℕ} {i j : Fin (n + 2)},
i ≤ j →
CategoryTheory.CategoryStruct.comp (SimplexCategory.δ i) (SimplexCategory.δ j.succ) =
CategoryTheory.CategoryStruct.comp (SimplexCategory.δ j) (SimplexCategory.δ i.castSucc)
The theorem `SimplexCategory.δ_comp_δ` is a statement about the first simplicial identity in the context of a Simplex Category. It states that for any natural number `n` and any two elements `i` and `j` of the finite set {0, ..., n+1} with `i` less than or equal to `j`, the composition of the `i`-th and `succ(j)`-th face maps from `[n]` to `[n+2]` is equal to the composition of the `j`-th and `castSucc(i)`-th face maps. The face maps are morphisms in the Simplex Category, and their composition is defined by the `CategoryTheory.CategoryStruct.comp` function. The `succ` and `castSucc` functions are used to embed a given finite set into a larger one by incrementing the elements or adding 1 to the size of the set, respectively.
More concisely: For any $n$ and $0 \leq i \leq j \leq n+1$, the composition of the $i$-th and $(j+1)$-th face maps in the simplex category of dimension $n$ equals the composition of the $j$-th and $(i+1)$-th face maps.
|
SimplexCategory.mono_iff_injective
theorem SimplexCategory.mono_iff_injective :
∀ {n m : SimplexCategory} {f : n ⟶ m},
CategoryTheory.Mono f ↔ Function.Injective ⇑(SimplexCategory.Hom.toOrderHom f)
This theorem states that a morphism in the 'SimplexCategory' is a monomorphism (a morphism that is left-cancellable) if and only if it is an injective function (a function where distinct inputs always produce distinct outputs). Here, 'SimplexCategory' is a category whose objects are natural numbers and morphisms are monotone functions between finite ordinal sets. The morphism is represented as 'n ⟶ m', and it is converted to a monotone map using the 'SimplexCategory.Hom.toOrderHom' function. The theorem asserts the equivalence of being a monomorphism and being injective in this context.
More concisely: A morphism in the SimplexCategory is a monomorphism if and only if it is an injective function. (Or, equivalently, a morphism n ⟶ m in SimplexCategory is a monomorphism if and only if the corresponding monotone function between finite ordinal sets is an injection.)
|
SimplexCategory.Hom.ext
theorem SimplexCategory.Hom.ext :
∀ {a b : SimplexCategory} (f g : a ⟶ b),
SimplexCategory.Hom.toOrderHom f = SimplexCategory.Hom.toOrderHom g → f = g
This theorem, `SimplexCategory.Hom.ext`, states that for any two objects `a` and `b` in the simplex category, if we have two morphisms `f` and `g` from `a` to `b`, and if the order-preserving maps corresponding to these morphisms (obtained using `SimplexCategory.Hom.toOrderHom`) are identical, then the original morphisms `f` and `g` themselves must be identical. In other words, different morphisms in the simplex category cannot give rise to the same order-preserving map.
More concisely: In the simplex category, if two morphisms from one object to another have identical order-preserving maps, then they are equal as morphisms.
|
SimplexCategory.ext
theorem SimplexCategory.ext : ∀ (a b : SimplexCategory), a.len = b.len → a = b
This theorem, named `SimplexCategory.ext`, states that for any two objects `a` and `b` in the SimplexCategory, if the lengths of `a` and `b` (as determined by the function `SimplexCategory.len`) are equal, then `a` and `b` must be the same object. In other words, no two distinct objects in the SimplexCategory can have the same length.
More concisely: In the SimplexCategory, two objects have equal lengths if and only if they are equal.
|
SimplexCategory.δ_comp_δ_self
theorem SimplexCategory.δ_comp_δ_self :
∀ {n : ℕ} {i : Fin (n + 2)},
CategoryTheory.CategoryStruct.comp (SimplexCategory.δ i) (SimplexCategory.δ i.castSucc) =
CategoryTheory.CategoryStruct.comp (SimplexCategory.δ i) (SimplexCategory.δ i.succ)
This theorem states a special case of the first simplicial identity in the context of a simplicial category. Specifically, for any natural number `n` and any `i` in the set `Fin (n + 2)`, the composition of the `i`-th face map from `[n]` to `[n+1]` with the face map for the successor of `i` (when considered as an element of `Fin n` embedded into `Fin (n+1)`), is equal to the composition of the `i`-th face map with the face map for the successor of `i` (when considered as an element of `Fin n` succeeding to `Fin (Nat.succ n)`). In simpler words, it says that two particular compositions of face maps in the simplicial category are equal.
More concisely: For any natural number `n` and `i` in `Fin (n + 2)`, the composition of the `i`-th face map from `[n]` to `[n+1]` with the face map for `i.succ` (considered as an element of `Fin n` embedded into `Fin (Nat.succ n)`), is equal to the composition of the `i`-th face map with the face map for `i.succ` (considered as an element of `Fin n`).
|
Mathlib.AlgebraicTopology.SimplexCategory._auxLemma.1
theorem Mathlib.AlgebraicTopology.SimplexCategory._auxLemma.1 : ∀ {n : ℕ} (a : Fin (n + 1)), (a < 0) = False
This theorem, located in the `Mathlib.AlgebraicTopology.SimplexCategory` module and named `_auxLemma.1`, states that for any natural number `n` and any element `a` of the finite set of size `n + 1` (denoted as `Fin (n + 1)`), the condition " `a` is less than zero" is False. In mathematical terms, this asserts that no element of a finite set indexed from 0 to `n` can be less than zero.
More concisely: For any natural number $n$ and any element $a$ in the finite set $\{0,1,\dots,n\}$, we have $a \not< 0$.
|
SimplexCategory.len_le_of_epi
theorem SimplexCategory.len_le_of_epi : ∀ {x y : SimplexCategory} {f : x ⟶ y}, CategoryTheory.Epi f → y.len ≤ x.len
This theorem states that for any two objects `x` and `y` in the Simplex Category and a morphism `f` from `x` to `y`, if the morphism `f` is an epimorphism (meaning it is right-cancellable), then the length of `y` must be less than or equal to the length of `x`. In the context of the Simplex Category, objects are natural numbers and morphisms are monotone functions from `Fin (n+1)` to `Fin (m+1)`, so this theorem essentially says that an epimorphic monotone function cannot increase the size of the ordered set it acts upon.
More concisely: In the Simplex Category, if a morphism between objects of different lengths is an epimorphism, then the length of the domain is less than or equal to the length of the codomain.
|
SimplexCategory.σ_comp_σ
theorem SimplexCategory.σ_comp_σ :
∀ {n : ℕ} {i j : Fin (n + 1)},
i ≤ j →
CategoryTheory.CategoryStruct.comp (SimplexCategory.σ i.castSucc) (SimplexCategory.σ j) =
CategoryTheory.CategoryStruct.comp (SimplexCategory.σ j.succ) (SimplexCategory.σ i)
The theorem `SimplexCategory.σ_comp_σ` in Lean 4 states the fifth simplicial identity in the context of the Simplex Category in Category Theory. Specifically, for any natural number `n` and any two ordinal numbers `i` and `j` of `n+1`, if `i` is less than or equal to `j`, then the composition of the `i`-th degeneracy map followed by the `j`-th degeneracy map is equal to the composition of the `j.succ`-th degeneracy map followed by the `i`-th degeneracy map. In other words, if we have two consecutive degeneracy maps, the order in which they are applied doesn't matter, which is a key property in the Simplex Category.
More concisely: For any natural number n and ordinal numbers i < j in n+1 in the Simplex Category, the i-th degeneracy map followed by the j-th degeneracy map is equal to the j.succ-th degeneracy map followed by the i-th degeneracy map.
|