English
mkHomAux provides by induction a family of pairs (f,f') with a compatibility condition ensuring a coherent chain map between P and Q when building a homomorphism.
Русский
mkHomAux даёт по индукции семейство пар (f,f') с условием совместимости, обеспечивающим когерентный цепной мап между P и Q при построении гомоморфизма.
LaTeX
$$$mkHomAux: \\mathbb{N} \\to \\Sigma'(f,f')$ with coherence $f' d = d f$$$
Lean4
/-- A constructor for chain maps between `ℕ`-indexed chain complexes,
working by induction on commutative squares.
You need to provide the components of the chain map in degrees 0 and 1,
show that these form a commutative square,
and then give a construction of each component,
and the fact that it forms a commutative square with the previous component,
using as an inductive hypothesis the data (and commutativity) of the previous two components.
-/
def mkHom : P ⟶ Q where
f n := (mkHomAux P Q zero one one_zero_comm succ n).1
comm' n
m := by
rintro (rfl : m + 1 = n)
exact (mkHomAux P Q zero one one_zero_comm succ m).2.2
