English
For each i, comul after lapply_i equals TensorProduct.map(lapply_i, lapply_i) after comul on the indexed space.
Русский
Для каждого i копуляция после lapply_i равна TensorProduct.map(lapply_i, lapply_i) после копуляции на DFinsupp-структуре.
LaTeX
$$$ \operatorname{comul} \circ \mathrm{lapply}_{i} = (\mathrm{TensorProduct.map} (\mathrm{lapply}_{i}) (\mathrm{lapply}_{i})) \circ (\mathrm{Finsupp.instCoalgebraStruct}\, R\, ι\, A).\mathrm{comul}$$$
Lean4
theorem comul_comp_lapply (i : ι) :
comul ∘ₗ (lapply i : _ →ₗ[R] A) = TensorProduct.map (lapply i) (lapply i) ∘ₗ comul :=
by
ext j : 1
conv_rhs => rw [comp_assoc, comul_comp_lsingle, ← comp_assoc, ← TensorProduct.map_comp]
obtain rfl | hij := eq_or_ne i j
· rw [comp_assoc, lapply_comp_lsingle_same, comp_id, TensorProduct.map_id, id_comp]
· rw [comp_assoc, lapply_comp_lsingle_of_ne _ _ hij, comp_zero, TensorProduct.map_zero_left, zero_comp]
