CategoryTheory.Arrow.AugmentedCechNerve.ExtraDegeneracy.s.proof_4

theorem CategoryTheory.Arrow.AugmentedCechNerve.ExtraDegeneracy.s.proof_4 : ∀ {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] (S : CategoryTheory.SplitEpi f.hom) (n : ℕ) (i : Fin ((Opposite.op (SimplexCategory.mk (n + 1))).unop.len + 1)), CategoryTheory.CategoryStruct.comp ((fun i => if x : i = 0 then CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.WidePullback.base fun x => f.hom) S.section_ else CategoryTheory.Limits.WidePullback.π (fun x => f.hom) (i.pred x)) i) f.hom = CategoryTheory.Limits.WidePullback.base fun x => f.hom

The theorem `CategoryTheory.Arrow.AugmentedCechNerve.ExtraDegeneracy.s.proof_4` states that for any category `C` and any morphism (or "arrow") `f` in `C`, where for any natural number `n`, `f` has a wide pullback with `f.right` as the base and `f.left` as the objects linked to the base by the morphism `f.hom`. Also, `f.hom` is a split epimorphism. For any natural number `n` and any element `i` drawn from the `n+1`-dimensional simplex, if `i` is not the zero element, the composition of `WidePullback.π (fun x => f.hom) (Fin.pred i x)` (which is the projection from the wide pullback to the `i-1`th object) and `f.hom` is equal to `WidePullback.base fun x => f.hom` (which is the morphism from the limit of the wide pullback to the base). If `i` is the zero element, then the composition of `WidePullback.base fun x => f.hom` and the section of `f.hom` (which is a right inverse of `f.hom`) is also equal to `WidePullback.base fun x => f.hom`.

More concisely: For any morphism `f` in a category `C` with split epimorphic `f.hom`, if `n` is a natural number and `i` is an `(n+1)`-dimensional simplex non-zero element, then the composition of the projection from the wide pullback of `f` to the `i-1`th object and `f.hom` equals `f.hom`; if `i` is the zero element, then the composition of `f.hom` and its section equals `f.hom` from the wide pullback to the base.