English
Construct a morphism of cochain complexes by inductively defining components in each degree via mkHomAux, ensuring commutativity with the differentials.
Русский
Построение гомоморфизма коCHAIN комплексов посредством индуктивного определения компонент по степеням через mkHomAux, обеспечивая коммутативность с дифференциалами.
LaTeX
$$$\\mathrm{mkHom} : P \\to Q \\text{ with } f_n = (\\mathrm{mkHomAux}\\; P\\; Q\\; zero\\; one\\; one\\_zero\\_comm\\; succ\\; n).1\\;\\text{ and }\\mathrm{comm}'_n = (\\mathrm{mkHomAux}\\; P\\; Q\\; zero\\; one\\; one\\_zero\\_comm\\; succ\\; n).2.2$$$
Lean4
/-- A constructor for chain maps between `ℕ`-indexed cochain 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 : n + 1 = m)
exact (mkHomAux P Q zero one one_zero_comm succ n).2.2
