English
Let R be a commutative ring, M an R-module, and n a positive integer. The nth exterior power ⊗^n_R M is generated by the images of the canonical maps ιMulti R n from all indexings; equivalently, the submodule of ⊗^n_R M generated by all such images is the whole exterior power.
Русский
Пусть R — коммутативное кольцо, M — R-модуль, n — положительное целое. Внешнее произведение ⊗^n_R M порождается образами канонических отображений ιMulti R n по всем индексам; эквивалентно, подмодуль, порожденный всеми такими образами, равен всей внешней степенью.
LaTeX
$$$\\operatorname{span}_R\\bigl(\\{ \\iota_{\\mathrm{Multi}}(R,n)(m) \\mid m \\in \\iota \\to M \\}\\bigr) = \\top \\quad\\text{in } (\\bigwedge^n_R M).$$$
Lean4
/-- The image of `exteriorPower.ιMulti` spans `⋀[R]^n M`. -/
theorem ιMulti_span : Submodule.span R (Set.range (ιMulti R n)) = (⊤ : Submodule R (⋀[R]^n M)) :=
by
apply LinearMap.map_injective (Submodule.ker_subtype (⋀[R]^n M))
rw [LinearMap.map_span, ← Set.image_univ, Set.image_image]
simp only [Submodule.coe_subtype, ιMulti_apply_coe, Set.image_univ, Submodule.map_top, Submodule.range_subtype]
exact ExteriorAlgebra.ιMulti_span_fixedDegree R n
