adjoin_nonUnitalSubalgebra_eq_span

English

For a non-unital subalgebra s of R-algebra A, the subalgebra adjoin_R (s) has underlying submodule equal to span_R{1} ⊔ s.toSubmodule.

Русский

Для неполного порождения подалгебры s в A над R, подалгебра adjoin_R(s) имеет как подмодуль: span_R{1} ⊔ s.toSubmodule.

LaTeX

$$$\\operatorname{toSubmodule}(\\operatorname{adjoin}_R(s:Set A)) = \\operatorname{span}_R\\{1\\} \\;\\sqcup\\; s.toSubmodule$$

Lean4

theorem adjoin_nonUnitalSubalgebra_eq_span (s : NonUnitalSubalgebra R A) :
    Subalgebra.toSubmodule (adjoin R (s : Set A)) = span R { 1 } ⊔ s.toSubmodule := by
  rw [adjoin_eq_span, Submonoid.closure_eq_one_union, span_union, ← NonUnitalAlgebra.adjoin_eq_span,
    NonUnitalAlgebra.adjoin_eq]

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