English
There is a natural equivalence between the solutions of the relations that define the exterior power and the class of alternating multilinear maps M → N indexed by ι; i.e., the solution space (relations R ι M).Solution N is canonically isomorphic to AlternatingMap R M N ι.
Русский
Существует естественное эквивалентное соответствие между решениями системы отношений, определяющей внешнее произведение, и множеством чередующихся многочленов M → N с индексами ι; то есть пространство решений (relations R ι M).Solution N изоморфно AlternatingMap R M N ι.
LaTeX
$$$((\\text{relations }R\\ ι\\ M).\\text{Solution } N) \\cong \\operatorname{Alt}_R(M,N,ι).$$$
Lean4
/-- The solutions in a module `N` to the linear equations
given by `exteriorPower.relations R ι M` identify to alternating maps to `N`. -/
@[simps!]
noncomputable def relationsSolutionEquiv {ι : Type*} [DecidableEq ι] {M : Type*} [AddCommGroup M] [Module R M] :
(relations R ι M).Solution N ≃ AlternatingMap R M N ι
where
toFun
s :=
{ toFun := fun m ↦ s.var m
map_update_add' := fun m i x y ↦
by
have := s.linearCombination_var_relation (.add m i x y)
dsimp at this ⊢
rw [map_sub, map_add, Finsupp.linearCombination_single, one_smul, Finsupp.linearCombination_single, one_smul,
Finsupp.linearCombination_single, one_smul, sub_eq_zero] at this
convert this.symm
map_update_smul' := fun m i r x ↦
by
have := s.linearCombination_var_relation (.smul m i r x)
dsimp at this ⊢
rw [Finsupp.smul_single, smul_eq_mul, mul_one, map_sub, Finsupp.linearCombination_single, one_smul,
Finsupp.linearCombination_single, sub_eq_zero] at this
convert this
map_eq_zero_of_eq' := fun v i j hm hij ↦ by simpa using s.linearCombination_var_relation (.alt v i j hm hij) }
invFun
f :=
{ var := fun m ↦ f m
linearCombination_var_relation :=
by
rintro (⟨m, i, x, y⟩ | ⟨m, i, r, x⟩ | ⟨v, i, j, hm, hij⟩)
· simp
· simp
· simpa using f.map_eq_zero_of_eq v hm hij }
