The subalgebra generated by a subring

Adjoining a subring R of an S-algebra A creates nothing beyond the S-span of R: a subring is already closed under multiplication and contains 1, so the products that Algebra.adjoin forms are again elements of R.

Main results

• Subring.toSubmodule_adjoin_coe: Algebra.adjoin S (R : Set A), as a submodule, is Submodule.span S (R : Set A).

theorem Subring.toSubmodule_adjoin_coe {S : Type u_1} {A : Type u_2} [CommSemiring S] [Ring A] [Algebra S A] (R : Subring A) : Subalgebra.toSubmodule (Algebra.adjoin S ↑R) = Submodule.span S ↑R

The S-subalgebra generated by a subring is its S-span. A subring is already closed under multiplication and contains 1, so adjoining it creates no products that its span misses.