English
The submodule spanned by the range of ιMulti R n equals the nth exterior power: span_R(range(ιMulti R n)) = ⋀[R]^n M.
Русский
Подмодуль, порождённый образами ιMulti R n, равен n-й внешней степени: span_R(range(ιMulti R n)) = ⋀[R]^n M.
LaTeX
$$$ \\operatorname{span}_R(\\operatorname{range}(\\iota\\_{Multi,R}(n))) = \\bigwedge^n_R M. $$$
Lean4
/-- The image of `ExteriorAlgebra.ιMulti R n` spans the `n`th exterior power, as a submodule
of the exterior algebra. -/
theorem ιMulti_span_fixedDegree (n : ℕ) : Submodule.span R (Set.range (ιMulti R n)) = ⋀[R]^n M :=
by
refine le_antisymm (Submodule.span_le.2 (ιMulti_range R n)) ?_
rw [exteriorPower, Submodule.pow_eq_span_pow_set, Submodule.span_le]
refine fun u hu ↦ Submodule.subset_span ?_
obtain ⟨f, rfl⟩ := Set.mem_pow.mp hu
refine ⟨fun i => ιInv (f i).1, ?_⟩
rw [ιMulti_apply]
congr with i
obtain ⟨v, hv⟩ := (f i).prop
rw [← hv, ι_leftInverse]
