CategoryTheory.ComposableArrows.map'.proof_3
theorem CategoryTheory.ComposableArrows.map'.proof_3 :
∀ {n : ℕ} (i j : ℕ) (hij : autoParam (i ≤ j) _auto✝) (hjn : autoParam (j ≤ n) _auto✝¹), ⟨i, ⋯⟩ ≤ ⟨j, ⋯⟩
This theorem, `CategoryTheory.ComposableArrows.map'.proof_3`, asserts that within the context of Category Theory, for any given natural number `n` and any two natural numbers `i` and `j`, given the automatic parameters `hij` and `hjn` which ensure `i` is less than or equal to `j` and `j` is less than or equal to `n` respectively, then the object with value `i` and an undisclosed property `isLt` is less than or equal to the object with value `j` and the same undisclosed property `isLt`. The automatic parameters here are not employed during type class resolution but only during elaboration. The proof of this theorem, however, is not provided in this context.
More concisely: For any natural numbers `i`, `j`, and `n`, if `i ≤ j` and `j ≤ n`, then the object with value `i` is less than or equal to the object with value `j` in the category theory context.
|
CategoryTheory.ComposableArrows.hom_ext_succ
theorem CategoryTheory.ComposableArrows.hom_ext_succ :
∀ {C : Type u_1} [inst : CategoryTheory.Category.{u_2, u_1} C] {n : ℕ}
{F G : CategoryTheory.ComposableArrows C (n + 1)} {f g : F ⟶ G},
CategoryTheory.ComposableArrows.app' f 0 ⋯ = CategoryTheory.ComposableArrows.app' g 0 ⋯ →
CategoryTheory.ComposableArrows.δ₀Functor.map f = CategoryTheory.ComposableArrows.δ₀Functor.map g → f = g
The theorem `CategoryTheory.ComposableArrows.hom_ext_succ` states that for any category `C` and natural number `n`, given two functors `F` and `G` that are instances of `ComposableArrows C (n + 1)` and two morphisms `f` and `g` from `F` to `G`, if the morphism induced on the 0th objects by `f` and `g` are equal and the mappings of `f` and `g` under the functor `δ₀Functor`, which forgets the first arrow, are also equal, then the two morphisms `f` and `g` themselves are equal. This theorem is a uniqueness result asserting that morphisms in the category of composable arrows are uniquely determined by their action on the 0th object and their action under the `δ₀Functor`.
More concisely: If two morphisms in the category of composable arrows of length `n+1` over a category `C`, between functors `F` and `G` that are instances of `ComposableArrows C (n+1)`, have equal actions on the 0-objects and equal images under `δ₀Functor`, then they are equal.
|