English
The isLocalizedModule_iff_isLocalization' proof provides the intricate structure of the adjunction and the commuting of algebra maps inside the scalar tower.
Русский
Доказательство isLocalizedModule_iff_isLocalization' раскрывает сложную структуру сопряжений и совместность алгебраических отображений внутри башни скаляров.
LaTeX
$$$\\text{theorem isLocalizedModule_iff_isLocalization' ...}$$$
Lean4
/-- The Galois insertion between `Submodule R M` and `Submodule S N`,
where `S` is the localization of `R` at `p` and `N` is the localization of `M` at `p`. -/
def localized'gi : GaloisInsertion (localized' S p f) (comap f <| ·.restrictScalars R)
where
gc M'
N' :=
⟨fun h m hm ↦ h ⟨m, hm, 1, by simp⟩, fun h ↦ by rw [localized'_eq_span, span_le]; apply map_le_iff_le_comap.mpr h⟩
le_l_u N' n
hn := by
obtain ⟨⟨m, s⟩, rfl⟩ := IsLocalizedModule.mk'_surjective p f n
refine ⟨m, ?_, s, rfl⟩
rw [mem_comap, restrictScalars_mem, ← IsLocalizedModule.mk'_cancel' _ _ s, Submonoid.smul_def, ← algebraMap_smul S]
exact smul_mem _ _ hn
choice x _ := localized' S p f x
choice_eq _ _ := rfl
