English
For any function f: X → A into an R-algebra A, the smallest subalgebra of A containing the image of f equals the range of the lifted map FreeAlgebra.lift R f.
Русский
Для любой функции f: X → A в R-алгебру A наименьшая подалгебра A, содержащая образ f, равна образу отображения, полученного поднятием FreeAlgebra.lift R f.
LaTeX
$$$ \\operatorname{Algebra.adjoin}_R (\\operatorname{Set.range} f) = (\\mathrm{FreeAlgebra.lift}\\, R\\, f).\\mathrm{range} $$$
Lean4
@[simp]
theorem adjoin_range_ι : Algebra.adjoin R (Set.range (ι R : X → FreeAlgebra R X)) = ⊤ :=
by
set S := Algebra.adjoin R (Set.range (ι R : X → FreeAlgebra R X))
refine top_unique fun x hx => ?_; clear hx
induction x with
| grade0 => exact S.algebraMap_mem _
| add x y hx hy => exact S.add_mem hx hy
| mul x y hx hy => exact S.mul_mem hx hy
| grade1 x => exact Algebra.subset_adjoin (Set.mem_range_self _)
