liftAlternating_apply_ιMulti — Mathlib

English

For any n and vector v, liftAlternating applied to ιMulti R n on v yields f n v, i.e., the action on the nth multi-argument aligns with the nth alternating map.

Русский

Для любого n и вектора v, liftAlternating на ιMulti_R n(v) даёт f n v.

LaTeX

$$$liftAlternating (R := R) (M := M) (N := N) f (ιMulti R n v) = f n v$$$

Lean4

@[simp]
theorem liftAlternating_apply_ιMulti {n : ℕ} (f : ∀ i, M [⋀^Fin i]→ₗ[R] N) (v : Fin n → M) :
    liftAlternating (R := R) (M := M) (N := N) f (ιMulti R n v) = f n v :=
  by
  rw [ιMulti_apply]
  induction n generalizing f with
  | zero => rw [List.ofFn_zero, List.prod_nil, liftAlternating_one, Subsingleton.elim 0 v]
  | succ n
    ih =>
    rw [List.ofFn_succ, List.prod_cons, liftAlternating_ι_mul, ih, AlternatingMap.curryLeft_apply_apply]
    congr
    exact Matrix.cons_head_tail _

Похожие утверждения