English
Equality expresses that FaithfullyFlat is equivalent to a predicate on f.
Русский
Равенство выражает эквивалентность FaithfullyFlat и соответствующего предиката на f.
LaTeX
$$$\\operatorname{eq\_and} : \\text{FaithfullyFlat} = (f \\mapsto f.Flat \\land \\text{Surjective}(f.specComap))$$$
Lean4
theorem of_isLocalization (R S) {Rₚ Sₚ : Type*} [CommSemiring R] [CommSemiring S] [CommSemiring Rₚ] [CommSemiring Sₚ]
[Algebra R S] [Algebra R Rₚ] [Algebra R Sₚ] [Algebra S Sₚ] [Algebra Rₚ Sₚ] [IsScalarTower R S Sₚ]
[IsScalarTower R Rₚ Sₚ] (M : Submonoid R) [IsLocalization M Rₚ]
[IsLocalization (Algebra.algebraMapSubmonoid S M) Sₚ] [hRS : Module.Finite R S] : Module.Finite Rₚ Sₚ := by
classical
have :
algebraMap Rₚ Sₚ =
IsLocalization.map (T := Algebra.algebraMapSubmonoid S M) Sₚ (algebraMap R S) (Submonoid.le_comap_map M) :=
by
apply IsLocalization.ringHom_ext M
simp only [IsLocalization.map_comp, ← IsScalarTower.algebraMap_eq]
-- We claim that if `S` is generated by `T` as an `R`-module,
-- then `S'` is generated by `T` as an `R'`-module.
obtain ⟨T, hT⟩ := hRS
use T.image (algebraMap S Sₚ)
rw [eq_top_iff]
rintro x
-
-- By the hypotheses, for each `x : S'`, we have `x = y / (f r)` for some `y : S` and `r : M`.
-- Since `S` is generated by `T`, the image of `y` should fall in the span of the image of `T`.
obtain ⟨y, ⟨_, ⟨r, hr, rfl⟩⟩, rfl⟩ := IsLocalization.mk'_surjective (Algebra.algebraMapSubmonoid S M) x
rw [IsLocalization.mk'_eq_mul_mk'_one, mul_comm, Finset.coe_image]
have hy : y ∈ Submodule.span R ↑T := by rw [hT]; trivial
replace hy :
algebraMap S Sₚ y ∈ Submodule.map (IsScalarTower.toAlgHom R S Sₚ).toLinearMap (Submodule.span R (T : Set S)) :=
Submodule.mem_map_of_mem (f := (IsScalarTower.toAlgHom R S Sₚ).toLinearMap) hy
rw [Submodule.map_span (IsScalarTower.toAlgHom R S Sₚ).toLinearMap T] at hy
have H : Submodule.span R (algebraMap S Sₚ '' T) ≤ (Submodule.span Rₚ (algebraMap S Sₚ '' T)).restrictScalars R := by
rw [Submodule.span_le]; exact Submodule.subset_span
convert (Submodule.span Rₚ (algebraMap S Sₚ '' T)).smul_mem (IsLocalization.mk' Rₚ (1 : R) ⟨r, hr⟩) (H hy) using 1
rw [Algebra.smul_def, this, IsLocalization.map_mk', map_one]
