English
For any p, the identity on the target space composed with p returns p: (id 𝕜 F (p 0 v0)).comp p = p for any v0 ∈ Fin 0 → E.
Русский
Для любого p тождественный отображение на целевом пространстве после композиции с p возвращает p: (id 𝕜 F (p 0 v0)).comp p = p для любого v0 ∈ Fin 0 → E.
LaTeX
$$$(id\\ 𝕜\\ F (p\\ 0\\ v_0)).comp\\ p = p$.$$
Lean4
@[simp]
theorem id_comp (p : FormalMultilinearSeries 𝕜 E F) (v0 : Fin 0 → E) : (id 𝕜 F (p 0 v0)).comp p = p :=
by
ext1 n
obtain rfl | n_pos := n.eq_zero_or_pos
· ext v
simp only [comp_coeff_zero', id_apply_zero]
congr with i
exact i.elim0
· dsimp [FormalMultilinearSeries.comp]
rw [Finset.sum_eq_single (Composition.single n n_pos)]
· show compAlongComposition (id 𝕜 F (p 0 v0)) p (Composition.single n n_pos) = p n
ext v
rw [compAlongComposition_apply, id_apply_one' _ _ _ (Composition.single_length n_pos)]
dsimp [applyComposition]
refine p.congr rfl fun i him hin => congr_arg v <| ?_
ext; simp
· change
∀ b : Composition n,
b ∈ Finset.univ → b ≠ Composition.single n n_pos → compAlongComposition (id 𝕜 F (p 0 v0)) p b = 0
intro b _ hb
have A : 1 < b.length :=
by
have : b.length ≠ 1 := by simpa [Composition.eq_single_iff_length] using hb
have : 0 < b.length := Composition.length_pos_of_pos b n_pos
omega
ext v
rw [compAlongComposition_apply, id_apply_of_one_lt _ _ _ A, ContinuousMultilinearMap.zero_apply,
ContinuousMultilinearMap.zero_apply]
· simp
