liftAlternating_ι_mul — Mathlib

English

For every n, liftAlternating composed with ιMulti_R n equals the identity on ExteriorAlgebra R M; i.e., the action on the nth exterior power recovers the original map.

Русский

Для каждого n композиция liftAlternating с ιMulti_R n равна тождественному отображению на ExteriorAlgebra R M.

LaTeX

$$$liftAlternating(f) \circ ιMulti_R n = f_n$ and in particular $liftAlternating(ιMulti_R n) = id$ on ExteriorAlgebra$$

Lean4

theorem liftAlternating_ι_mul (f : ∀ i, M [⋀^Fin i]→ₗ[R] N) (m : M) (x : ExteriorAlgebra R M) :
    liftAlternating (R := R) (M := M) (N := N) f (ι R m * x) =
      liftAlternating (R := R) (M := M) (N := N) (fun i => (f i.succ).curryLeft m) x :=
  by
  dsimp [liftAlternating]
  rw [foldl_mul, foldl_ι]
  rfl

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