liftAlternating_algebraMap — Mathlib

English

For any f, liftAlternating applied to the algebra map algebraMap_R (ExteriorAlgebra R M) r equals r times f 0 0; i.e., liftAlternating(algebraMap r) = r • f 0 0.

Русский

Для любого f, liftAlternating применяется к алгебраическому отображению algebraMap и даёт r • f 0 0.

LaTeX

$$$liftAlternating(f)(algebraMap_{ExteriorAlgebra} r) = r \cdot f 0 0$$$

Lean4

@[simp]
theorem liftAlternating_algebraMap (f : ∀ i, M [⋀^Fin i]→ₗ[R] N) (r : R) :
    liftAlternating (R := R) (M := M) (N := N) f (algebraMap _ (ExteriorAlgebra R M) r) = r • f 0 0 := by
  rw [Algebra.algebraMap_eq_smul_one, map_smul, liftAlternating_one]

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