English
Two alternating maps are equal if they agree after evaluating on all distinct basis vectors, formalized via a basis-extensional principle.
Русский
Две чередующиеся отображения равны, если они совпадают на всех независимых базисных векторах, формализуется через эквивалентность по базису.
LaTeX
$$Theorem ext_alternating: equality follows from basis-vector testing$$
Lean4
/-- Given an alternating map `f` in `n+1` variables, split the first variable to obtain
a linear map into alternating maps in `n` variables, given by `x ↦ (m ↦ f (Matrix.vecCons x m))`.
It can be thought of as a map $Hom(\bigwedge^{n+1} M, N) \to Hom(M, Hom(\bigwedge^n M, N))$.
This is `MultilinearMap.curryLeft` for `AlternatingMap`. See also
`AlternatingMap.curryLeftLinearMap`. -/
@[simps apply_toMultilinearMap]
def curryLeft (f : M [⋀^Fin n.succ]→ₗ[R] N) : M →ₗ[R] M [⋀^Fin n]→ₗ[R] N
where
toFun
m :=
{ f.toMultilinearMap.curryLeft m with
map_eq_zero_of_eq' v i j hv hij := f.map_eq_zero_of_eq _ (by simpa) ((Fin.succ_injective _).ne hij) }
map_add' _ _ := ext fun _ => f.map_vecCons_add _ _ _
map_smul' _ _ := ext fun _ => f.map_vecCons_smul _ _ _
