English
Let r, q, p be formal multilinear series of appropriate types. Then the associative law holds: (r ∘ q) ∘ p = r ∘ (q ∘ p).
Русский
Пусть r, q, p — формальные многочленовые серии соответствующих типов. Тогда выполняется ассоциативное свойство композиции: (r ∘ q) ∘ p = r ∘ (q ∘ p).
LaTeX
$$$(r \\circ q) \\circ p = r \\circ (q \\circ p)\\quad\\text{for } r:\\mathrm{FMS}_{\\mathbb{k}}(G,H),\\ q:\\mathrm{FMS}_{\\mathbb{k}}(F,G),\\ p:\\mathrm{FMS}_{\\mathbb{k}}(E,F).$$$
Lean4
theorem comp_assoc (r : FormalMultilinearSeries 𝕜 G H) (q : FormalMultilinearSeries 𝕜 F G)
(p : FormalMultilinearSeries 𝕜 E F) : (r.comp q).comp p = r.comp (q.comp p) :=
by
ext n v
let f : (Σ a : Composition n, Composition a.length) → H := fun c =>
r c.2.length (applyComposition q c.2 (applyComposition p c.1 v))
let g : (Σ c : Composition n, ∀ i : Fin c.length, Composition (c.blocksFun i)) → H := fun c =>
r c.1.length fun i : Fin c.1.length => q (c.2 i).length (applyComposition p (c.2 i) (v ∘ c.1.embedding i))
suffices ∑ c, f c = ∑ c, g c by
simpa +unfoldPartialApp only [FormalMultilinearSeries.comp, ContinuousMultilinearMap.sum_apply,
compAlongComposition_apply, Finset.sum_sigma', applyComposition, ContinuousMultilinearMap.map_sum]
/- Now, we use `Composition.sigmaEquivSigmaPi n` to change
variables in the second sum, and check that we get exactly the same sums. -/
rw [← (sigmaEquivSigmaPi n).sum_comp]
/- To check that we have the same terms, we should check that we apply the same component of
`r`, and the same component of `q`, and the same component of `p`, to the same coordinate of
`v`. This is true by definition, but at each step one needs to convince Lean that the types
one considers are the same, using a suitable congruence lemma to avoid dependent type issues.
This dance has to be done three times, one for `r`, one for `q` and one for `p`. -/
apply Finset.sum_congr rfl
rintro ⟨a, b⟩ _
dsimp [sigmaEquivSigmaPi]
-- check that the `r` components are the same. Based on `Composition.length_gather`
apply r.congr (Composition.length_gather a b).symm
intro i hi1 hi2
apply q.congr (length_sigmaCompositionAux a b _).symm
intro j hj1 hj2
apply p.congr (blocksFun_sigmaCompositionAux a b _ _).symm
intro k hk1 hk2
refine congr_arg v (Fin.ext ?_)
dsimp [Composition.embedding]
rw [sizeUpTo_sizeUpTo_add _ _ hi1 hj1, add_assoc]
