English
If there exists a spanning set of localizations then surjectivity follows from surjectivity after localization.
Русский
Если существует множество локализаций, покрывающее модуль, суръективность следует из суръективности после локализации.
LaTeX
$$$$ \operatorname{OfLocalizationSpan}(\text{surjective}). $$$$
Lean4
/-- `R →+* S` is surjective if there exists a set `{ r }` that spans `R` such that
`Rᵣ →+* Sᵣ` is surjective. -/
theorem surjective_ofLocalizationSpan : OfLocalizationSpan surjective :=
by
introv R e H
rw [← Set.range_eq_univ, Set.eq_univ_iff_forall]
letI := f.toAlgebra
intro x
apply Submodule.mem_of_span_eq_top_of_smul_pow_mem (LinearMap.range (Algebra.linearMap R S)) s e
intro r
obtain ⟨a, e'⟩ := H r (algebraMap _ _ x)
obtain ⟨b, ⟨_, n, rfl⟩, rfl⟩ := IsLocalization.mk'_surjective (Submonoid.powers (r : R)) a
rw [Localization.awayMap, IsLocalization.Away.map, IsLocalization.map_mk', eq_comm, IsLocalization.eq_mk'_iff_mul_eq,
Subtype.coe_mk, Subtype.coe_mk, ← map_mul] at e'
obtain ⟨⟨_, n', rfl⟩, e''⟩ := (IsLocalization.eq_iff_exists (Submonoid.powers (f r)) _).mp e'
dsimp only at e''
rw [mul_comm x, ← mul_assoc, ← map_pow, ← map_mul, ← map_mul, ← pow_add] at e''
exact ⟨n' + n, _, e''.symm⟩
