proj_apply — Mathlib

English

Applying proj to the inverse decomposition recovers the corresponding summand of the inverse decomposition map.

Русский

Применение proj к обратному разложению восстанавливает соответствующую долю обратного разложения.

LaTeX

$$$\mathrm{proj}_{𝒜,i}((\mathrm{decompose} 𝒜)^{-1}(a)) = (\mathrm{decompose} 𝒜)^{-1}(\mathrm{of} _i(a_i)).$$$

Lean4

@[simp]
theorem proj_apply (i : ι) (r : A) : GradedAlgebra.proj 𝒜 i r = (decompose 𝒜 r : ⨁ i, 𝒜 i) i :=
  rfl

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