English
For each q, there is a natural transformation P_q of the alternating face map complex; its components are the morphisms (P_q).f(n).
Русский
Для каждого q существует естественное преобразование P_q чередующегося комплекса граней; его компоненты — это морфизмы (P_q).f(n).
LaTeX
$$$\text{natTransP}(q) : alternatingFaceMapComplex(C) \Rightarrow alternatingFaceMapComplex(C)$ with app at level n given by $(P_q).f(n)$.$$
Lean4
/-- For each `q`, `P q` is a natural transformation. -/
@[simps]
def natTransP (q : ℕ) : alternatingFaceMapComplex C ⟶ alternatingFaceMapComplex C
where
app _ := P q
naturality _ _
f := by
induction q with
| zero =>
dsimp [alternatingFaceMapComplex]
simp only [P_zero, id_comp, comp_id]
| succ q
hq =>
simp only [P_succ, add_comp, comp_add, assoc, comp_id, hq, reassoc_of% hq]
-- `erw` is needed to see through `natTransHσ q).app = Hσ q`
erw [(natTransHσ q).naturality f]
rfl
