English
For every natural number n, the n-fold exterior product map that sends (m1, ..., mn) in M^n to the product ι_R(m1) · ι_R(m2) · ... · ι_R(mn) in ExteriorAlgebra_R M is an alternating multilinear map M^n → ExteriorAlgebra_R M.
Русский
Для любого натурального числа n отображение n-сложного внешнего произведения, отправляющее (m1, ..., mn) из M^n в произведение ι_R(m1) · ι_R(m2) · ... · ι_R(mn) в ExteriorAlgebra_R M, является чередующейся мультилайновой картой M^n → ExteriorAlgebra_R M.
LaTeX
$$$ (m_1, \\dots, m_n) \\mapsto \\iota_R(m_1)\\iota_R(m_2)\\cdots\\iota_R(m_n) \\in \\operatorname{ExteriorAlgebra}_R M, \\quad \\Phi_n \\in \\operatorname{Alt}_R^n(M, \\operatorname{ExteriorAlgebra}_R M). $$$
Lean4
/-- The product of `n` terms of the form `ι R m` is an alternating map.
This is a special case of `MultilinearMap.mkPiAlgebraFin`, and the exterior algebra version of
`TensorAlgebra.tprod`. -/
def ιMulti (n : ℕ) : M [⋀^Fin n]→ₗ[R] ExteriorAlgebra R M :=
let F := (MultilinearMap.mkPiAlgebraFin R n (ExteriorAlgebra R M)).compLinearMap fun _ => ι R
{
F with
map_eq_zero_of_eq' := fun f x y hfxy hxy => by
dsimp [F]
clear F
wlog h : x < y
· exact this R n f y x hfxy.symm hxy.symm (hxy.lt_or_gt.resolve_left h)
clear hxy
induction n with
| zero => exact x.elim0
| succ n hn =>
rw [List.ofFn_succ, List.prod_cons]
by_cases hx :
x =
0
-- one of the repeated terms is on the left
· rw [hx] at hfxy h
rw [hfxy, ← Fin.succ_pred y (ne_of_lt h).symm]
exact
ι_mul_prod_list (f ∘ Fin.succ)
_
-- ignore the left-most term and induct on the remaining ones, decrementing indices
· convert mul_zero (ι R (f 0))
refine
hn (fun i => f <| Fin.succ i) (x.pred hx) (y.pred (ne_of_lt <| lt_of_le_of_lt x.zero_le h).symm) ?_
(Fin.pred_lt_pred_iff.mpr h)
simp only [Fin.succ_pred]
exact hfxy
toFun := F }
