English
The degeneracy map s followed by the projection π_0 equals the base projection after applying the section.
Русский
Раз degeneracy map s затем проекция π_0 равны базовой проекции после применения секции.
LaTeX
$$$ s \;\;\cdot\;\; π_0 = Base \;\circ\; Section $$$
Lean4
/-- The extra degeneracy map on the Čech nerve of a split epi. It is
given on the `0`-projection by the given section of the split epi,
and by shifting the indices on the other projections. -/
noncomputable def s (n : ℕ) : f.cechNerve.obj (op ⦋n⦌) ⟶ f.cechNerve.obj (op ⦋n + 1⦌) :=
WidePullback.lift (WidePullback.base _) (Fin.cases (WidePullback.base _ ≫ S.section_) (WidePullback.π _)) fun i => by
cases i using Fin.cases <;>
simp
-- Porting note (https://github.com/leanprover-community/mathlib4/issues/11119): @[simp] removed as the linter complains the LHS is not in normal form
-- The problem is that the type of `ExtraDegeneracy.s` is not in normal form, this causes the `erw`
-- in the proofs below.
