CategoryTheory.Arrow.cechNerve.proof_1
theorem CategoryTheory.Arrow.cechNerve.proof_1 :
∀ {C : Type u_2} [inst : CategoryTheory.Category.{u_1, u_2} C] (f : CategoryTheory.Arrow C)
[inst_1 : ∀ (n : ℕ), CategoryTheory.Limits.HasWidePullback f.right (fun x => f.left) fun x => f.hom]
(n : SimplexCategoryᵒᵖ), CategoryTheory.Limits.HasWidePullback f.right (fun x => f.left) fun x => f.hom
The theorem `CategoryTheory.Arrow.cechNerve.proof_1` states that for any category `C`, any arrow `f` in this category, and any natural number `n`, if `f` has a wide pullback in `C` for all `n`, then the wide pullback of `f` exists in the opposite simplex category. Here, an arrow is a morphism in `C`, a wide pullback is a limit of a wide cospan, and the simplex category consists of natural numbers as objects and monotone functions as morphisms.
More concisely: If for every arrow `f` in a category `C` and natural number `n`, `f` has a wide pullback in `C`, then `f` has a wide pullback in the opposite simplex category.
|
CategoryTheory.Arrow.cechConerve.proof_1
theorem CategoryTheory.Arrow.cechConerve.proof_1 :
∀ {C : Type u_2} [inst : CategoryTheory.Category.{u_1, u_2} C] (f : CategoryTheory.Arrow C)
[inst_1 : ∀ (n : ℕ), CategoryTheory.Limits.HasWidePushout f.left (fun x => f.right) fun x => f.hom]
(n : SimplexCategory), CategoryTheory.Limits.HasWidePushout f.left (fun x => f.right) fun x => f.hom
This theorem states that for any category `C`, and for any arrow `f` in the arrow category of `C`, if for each natural number `n`, the wide pushout of `f.left`, `f.right` and `f.hom` exists, then for any object `n` in the simplex category (which is a natural number), the wide pushout of `f.left`, `f.right` and `f.hom` also exists. In the context of category theory, a wide pushout (also known as a coproduct or an amalgamated sum) is a colimit of a diagram which is a shape of "cospan", i.e., a diagram with two objects mapping to a third one. In this theorem, the wide pushout is obtained from the diagram specified by `f.left`, `f.right` and `f.hom`.
More concisely: If, for every natural number `n`, the wide pushout of `f.left`, `f.right`, and `f.hom` exists in a category `C`, then the wide pushout of `f.left`, `f.right`, and `f.hom` exists in the simplex category for any object `n` (represented as an arrow from the terminal object to itself).
|