liftAlternating_ι — Mathlib

English

The action of liftAlternating on a product with ι_R(m) is equivalent to lifting with a shifted family, i.e., liftAlternating(f)(ι_R(m)·x) = liftAlternating(f(i+1) ∘ curryLeft m)(x).

Русский

Действие liftAlternating на произведение с ι_R(m) эквивалентно продолжению со сдвинутой семейством: liftAlternating(f)(ι_R(m)·x) = liftAlternating(f(i+1) с curryLeft m)(x).

LaTeX

$$$\text{liftAlternating}(f)(\iota_R(m)\cdot x) = \text{liftAlternating}(f_{\cdot}^{(m)})(x), \quad f_{\cdot}^{(m)}(i) = (f(i+1)).curryLeft(m)$$$

Lean4

@[simp]
theorem liftAlternating_ι (f : ∀ i, M [⋀^Fin i]→ₗ[R] N) (m : M) :
    liftAlternating (R := R) (M := M) (N := N) f (ι R m) = f 1 ![m] :=
  by
  dsimp [liftAlternating]
  rw [foldl_ι, LinearMap.mk₂_apply, AlternatingMap.curryLeft_apply_apply]
  congr!

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