decompose_algebraMap — Mathlib

English

The direct-sum decomposition map commutes with the algebra map from R to A, i.e., applying decompose to algebraMap R A r equals algebraMap R (⨁ᵢ 𝒜 i) r.

Русский

Прямой разложение мапа и алгебраическое отображение совместны: разложение(decompose 𝒜) (algebraMap R A r) = algebraMap R (⨁ᵢ 𝒜 i) r.

LaTeX

$$$\\forall r \\in R:\\ decompose \\mathcal{A} (\\operatorname{algebraMap}_R^A (r)) = \\operatorname{algebraMap}_R^{\\bigoplus_i 𝒜(i)}(r).$$$

Lean4

@[simp]
theorem decompose_algebraMap (r : R) : decompose 𝒜 (algebraMap R A r) = algebraMap R (⨁ i, 𝒜 i) r :=
  (decomposeAlgEquiv 𝒜).commutes r

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