English
The submodule generated by all images of the maps ExteriorAlgebra.ιMulti_R n is the whole ExteriorAlgebra_R(M); in other words, the exterior algebra is spanned by all images of these maps across all n.
Русский
Подмодуль, генерируемый всеми образами отображений ExteriorAlgebra.ιMulti_R n, равен всей ExteriorAlgebra_R(M); внешняя алгебра порождается всеми образами этих отображений по всем n.
LaTeX
$$$\operatorname{span}_R\{ \iota^{\mathrm{Multi}}_R(n)(v) \mid n\in\mathbb{N}, v\text{ подходящий} \} = \top$$$
Lean4
/-- The union of the images of the maps `ExteriorAlgebra.ιMulti R n` for `n` running through
all natural numbers spans the exterior algebra. -/
theorem ιMulti_span : Submodule.span R (Set.range fun x : Σ n, (Fin n → M) => ιMulti R x.1 x.2) = ⊤ :=
by
rw [Submodule.eq_top_iff']
intro x
induction x using DirectSum.Decomposition.inductionOn fun i => ⋀[R]^i M with
| zero => exact Submodule.zero_mem _
| add _ _ hm hm' => exact Submodule.add_mem _ hm hm'
| homogeneous hm =>
let ⟨m, hm⟩ := hm
apply Set.mem_of_mem_of_subset hm
rw [← ιMulti_span_fixedDegree]
refine Submodule.span_mono fun _ hx ↦ ?_
obtain ⟨y, rfl⟩ := hx
exact ⟨⟨_, y⟩, rfl⟩
