proj_recompose — Mathlib

English

The i-th projection of the graded piece equals the i-th coordinate of the decompose representation.

Русский

i-я проекция градуированной части равна i-й координате представления в разложении.

LaTeX

$$$ GradedRing.proj 𝒜 i \; r = (decompose 𝒜 r)_i. $$$

Lean4

theorem proj_recompose (a : ⨁ i, 𝒜 i) (i : ι) :
    GradedRing.proj 𝒜 i ((decompose 𝒜).symm a) = (decompose 𝒜).symm (DirectSum.of _ i (a i)) := by
  rw [GradedRing.proj_apply, decompose_symm_of, Equiv.apply_symm_apply]

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