proj_recompose — Mathlib

English

The zero-degree projection map from a graded ring onto its 0-th component is surjective onto that component.

Русский

Проекция нулевой степени из градуированного кольца на компоненту 0 сюрьективна на 𝒜(0).

LaTeX

$$$\mathrm{projZeroRingHom}' 𝒜: A \twoheadrightarrow 𝒜(0)$ is surjective.$$

Lean4

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

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