English
For each i, comul composed with lapply_i equals TensorProduct.map(lapply_i, lapply_i) composed with the coalgebra structure on the dependent function space; i.e. comul ∘ lapply_i = …
Русский
Для каждого i копуляция после lapply_i равна TensorProduct.map(lapply_i, lapply_i) после копиприведения над DFinsupp; то есть comul ∘ lapply_i = …
LaTeX
$$$ \\operatorname{comul} \\circ \\mathrm{lapply}_{i} = (\\mathrm{TensorProduct.map} (\\mathrm{lapply}_{i}) (\\mathrm{lapply}_{i})) \\circ (\\mathrm{DFinsupp.instCoalgebraStruct}\\, R\, ι\, A).\\mathrm{comul} $$$
Lean4
theorem comul_comp_lapply (i : ι) :
comul ∘ₗ (lapply i : _ →ₗ[R] A i) = 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]
