adjoin_eq_range_freeAlgebra_lift — Mathlib

English

For any set s ⊆ A, the subalgebra of A generated by s equals the range of the lift FreeAlgebra.lift R ((↑) : s → A).

Русский

Для любого подмножества s ⊆ A подалгебра A, порождаемая s, равна образу отображения lift R ((↑) : s → A).

LaTeX

$$$ \\operatorname{Algebra.adjoin}_R s = (\\mathrm{FreeAlgebra.lift}\\, R\\ ((\\uparrow) : s \\to A)).\\mathrm{range} $$$

Lean4

/-- Noncommutative version of `Algebra.adjoin_range_eq_range`. -/
theorem _root_.Algebra.adjoin_eq_range_freeAlgebra_lift (s : Set A) :
    Algebra.adjoin R s = (FreeAlgebra.lift R ((↑) : s → A)).range := by
  rw [← Algebra.adjoin_range_eq_range_freeAlgebra_lift, Subtype.range_coe]

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