English
The congruence lemmas ensure that lifting is compatible with equality of maps; if two maps are equal, their lifts coincide.
Русский
Леммы сопряжения обеспечивают совместимость подъёмов с равенством отображений; если две карты равны, их подъёмы совпадают.
LaTeX
$$$g = g_1 \\Rightarrow \\mathrm{lift}'(g,h) = \\mathrm{lift}'(g_1,h).$$$
Lean4
theorem of_restrictScalars (S : Submonoid R) {N : Type*} [AddCommMonoid N] [Module R N] [Module A M] [Module A N]
[IsScalarTower R A M] [IsScalarTower R A N] (f : M →ₗ[A] N) [IsLocalizedModule S (f.restrictScalars R)] :
IsLocalizedModule (Algebra.algebraMapSubmonoid A S) f
where
map_units
x := by
obtain ⟨_, x, hx, rfl⟩ := x
have := IsLocalizedModule.map_units (f.restrictScalars R) ⟨x, hx⟩
simp only [← IsScalarTower.algebraMap_apply, Module.End.isUnit_iff] at this ⊢
exact this
surj
y := by
obtain ⟨⟨x, t⟩, e⟩ := IsLocalizedModule.surj S (f.restrictScalars R) y
exact ⟨⟨x, ⟨_, t, t.2, rfl⟩⟩, by simpa [Submonoid.smul_def] using e⟩
exists_of_eq {x₁ x₂}
e := by
obtain ⟨c, hc⟩ := IsLocalizedModule.exists_of_eq (S := S) (f := f.restrictScalars R) e
refine ⟨⟨_, c, c.2, rfl⟩, by simpa [Submonoid.smul_def]⟩
