English
There is a canonical equivalence between the solution space of the presentation and the space of alternating maps from M to N indexed by ι: a solution corresponds to an alternating map and vice versa.
Русский
Существует каноническое эквивалентность между пространством решений презентa и пространством чередующихся отображений от M в N с индексами ι: решение соответствует чередующемуся отображению и наоборот.
LaTeX
$$$\\text{RelationsSolutionEquiv} : (\\text{relations } R ι M).\\text{Solution } N \\simeq \\operatorname{Alt}_R(M,N,ι).$$$
Lean4
/-- Two linear maps on `⋀[R]^n M` that agree on the image of `exteriorPower.ιMulti`
are equal. -/
@[ext]
theorem linearMap_ext {f : ⋀[R]^n M →ₗ[R] N} {g : ⋀[R]^n M →ₗ[R] N}
(heq : f.compAlternatingMap (ιMulti R n) = g.compAlternatingMap (ιMulti R n)) : f = g :=
(presentation R n M).postcomp_injective (by ext f; apply DFunLike.congr_fun heq)
