English
There is a natural transformation natTransHσ parameterized by q, whose component at a q-th level gives the map hσ' q n m hnm as a morphism of simplicial objects, natural in X.
Русский
Существует естественное преобразование natTransHσ, параметризованное q, компонент которого на уровне q даёт отображение hσ' q n m hnm как морфизм симпликциальных объектов и естественно по X.
LaTeX
$$$$ \mathrm{natTransHσ}(q) : \text{SimplicialObject}(C) \to \text{SimplicialObject}(C) $$$$
Lean4
/-- For each q, `Hσ q` is a natural transformation. -/
def natTransHσ (q : ℕ) : alternatingFaceMapComplex C ⟶ alternatingFaceMapComplex C
where
app _ := Hσ q
naturality _ _
f := by
unfold Hσ
rw [nullHomotopicMap'_comp, comp_nullHomotopicMap']
congr
ext n m hnm
simp only [alternatingFaceMapComplex_map_f, hσ'_naturality]
