English
If K over E over F is a tower of rings and L ⊆ K is a submonoid generated by S as an F-module (i.e., (L : Set K) = span_F S), then the E-submodule generated by L equals the span of S over E: toSubmodule(adjoin_E (L : Set K)) = span_E S.
Русский
Пусть K/ E/ F — структурный «стек» колец и L ⊆ K — подмоноид, порожденный S как F-модуль (то есть (L : Set K) = span_F S). Тогда E-модуль, порожденный L, равен span_E S: toSubmodule(adjoin_E (L : Set K)) = span_E S.
LaTeX
$$$ \operatorname{toSubmodule}(\operatorname{adjoin}_{E} (L : Set K)) = \operatorname{span}_{E} S $$$
Lean4
/-- If `K / E / F` is a ring extension tower, `L` is a submonoid of `K / F` which is generated by
`S` as an `F`-module, then `E[L]` is generated by `S` as an `E`-module. -/
theorem adjoin_eq_span_of_eq_span [Semiring F] [Module F K] [IsScalarTower F E K] (L : Submonoid K) {S : Set K}
(h : (L : Set K) = span F S) : toSubmodule (adjoin E (L : Set K)) = span E S :=
by
rw [adjoin_eq_span, L.closure_eq, h]
exact (span_le.mpr <| span_subset_span _ _ _).antisymm (span_mono subset_span)
