liftι — Mathlib

English

For each i and x in ∧^i_R M, the lifted map liftι sends x to the i-th summand of the direct sum, i.e., liftι(R,M)x = DirectSum.of (fun i => ∧^i_R M) i x.

Русский

Для каждого i и x в ∧^i_R M отображение liftι отправляет x в i-ю составляющую прямого суммы.

LaTeX

$$$\operatorname{liftι}(R,M)x = \operatorname{DirectSum}.of(\!\,i\mapsto \bigwedge^i_R M)\, i\, x$$$

Lean4

/-- `ExteriorAlgebra.GradedAlgebra.ι` lifted to exterior algebra. This is
primarily an auxiliary construction used to provide `ExteriorAlgebra.gradedAlgebra`. -/
def liftι : ExteriorAlgebra R M →ₐ[R] ⨁ i : ℕ, ⋀[R]^i M :=
  lift R ⟨by apply GradedAlgebra.ι R M, GradedAlgebra.ι_sq_zero R M⟩

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