liftAlternating_comp_ιMulti — Mathlib

English

There exists an equality that identifies liftAlternating with the identity on ExteriorAlgebra when composed with ιMulti on appropriate inputs.

Русский

Существуют равенства, идентифицирующие liftAlternating с тождественным отображением после композиции с ιMulti на соответствующих входах.

LaTeX

$$$liftAlternating (R := R) (M := M) (N := ExteriorAlgebra R M) (ιMulti R) = id$$$

Lean4

@[simp]
theorem liftAlternating_comp_ιMulti {n : ℕ} (f : ∀ i, M [⋀^Fin i]→ₗ[R] N) :
    (liftAlternating (R := R) (M := M) (N := N) f).compAlternatingMap (ιMulti R n) = f n :=
  AlternatingMap.ext <| liftAlternating_apply_ιMulti f

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