proj — Mathlib

English

The projection maps proj 𝒜 i form a graded projection system extracting the i-th homogeneous component of an element of a graded algebra.

Русский

Проекции proj 𝒜 i образуют систему проекций, извлекающую i-ю однородную компоненту элемента градуированной алгебры.

LaTeX

$$$\mathrm{proj} 𝒜 i: A \to A, \; r \mapsto (\mathrm{decompose} 𝒜 r)_i.$$$

Lean4

/-- The projection maps of graded algebra -/
def proj (𝒜 : ι → Submodule R A) [GradedAlgebra 𝒜] (i : ι) : A →ₗ[R] A :=
  (𝒜 i).subtype.comp <| (DFinsupp.lapply i).comp <| (decomposeAlgEquiv 𝒜).toAlgHom.toLinearMap

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