English
If a localized module structure exists for a map f: M → M' over a submonoid S of R, then f exhibits the base-change property with respect to the localization A of R; i.e., IsLocalizedModule S f implies IsBaseChange A f.
Русский
Если для отображения $f:M\to M'$ имеется структура локализации над подмоноидом $S$ кольца $R$, то эта локализация реализуется как базовое изменение вдоль локализации $A$; то есть IsLocalizedModule S f ⇒ IsBaseChange A f.
LaTeX
$$$(\text{IsLocalizedModule } S f) \Rightarrow (\text{IsBaseChange } A f)$$
Lean4
/-- The forward direction of `isLocalizedModule_iff_isBaseChange`. It is also used to prove the
other direction. -/
theorem isBaseChange [IsLocalizedModule S f] : IsBaseChange A f :=
.of_lift_unique _ fun Q _ _ _ _ g ↦
by
obtain ⟨ℓ, rfl, h₂⟩ :=
IsLocalizedModule.is_universal S f g fun s ↦ by rw [← (Algebra.lsmul R (A := A) R Q).commutes];
exact (IsLocalization.map_units A s).map _
refine ⟨ℓ.extendScalarsOfIsLocalization S A, by simp, fun g'' h ↦ ?_⟩
cases h₂ (LinearMap.restrictScalars R g'') h; rfl
