English
Analogous to the previous isLocalization_of_is_exists_mul_mem, but stated for the alternative setting of M ≤ N with the equivalence of localizations via a witness predicate on multiplications.
Русский
Аналогично предыдущему утверждению о локализации через существование умножения, но в альтернативной постановке через N и M.
LaTeX
$$IsLocalization N S$$
Lean4
theorem span_eq_top_of_isLocalizedModule {v : Set M} (hv : span R v = ⊤) : span Rₛ (f '' v) = ⊤ :=
top_unique fun x _ ↦ by
obtain ⟨⟨m, s⟩, h⟩ := IsLocalizedModule.surj S f x
rw [Submonoid.smul_def, ← algebraMap_smul Rₛ, ← Units.smul_isUnit (IsLocalization.map_units Rₛ s), eq_comm, ←
inv_smul_eq_iff] at h
refine h ▸ smul_mem _ _ (span_subset_span R Rₛ _ ?_)
rw [← LinearMap.coe_restrictScalars R, ← LinearMap.map_span, hv]
exact mem_map_of_mem mem_top
