English
There is an IsLocalizedModule instance for Submodule.toLocalizedQuotient, i.e., the localization of a quotient submodule is integrally localized.
Русский
Существует экземпляр IsLocalizedModule для Submodule.toLocalizedQuotient, т.е. локализация частичного модуля в виде квартины локализуется.
LaTeX
$$$\text{IsLocalizedModule } p\, (\text{Submodule}.\mathrm{toLocalizedQuotient}(p M'))$$$
Lean4
instance toLocalizedQuotient' (M' : Submodule R M) : IsLocalizedModule p (M'.toLocalizedQuotient' S p f)
where
map_units
x :=
by
refine
(Module.End.isUnit_iff _).mpr
⟨fun m n e ↦ ?_, fun m ↦
⟨(IsLocalization.mk' S 1 x) • m, by
rw [Module.algebraMap_end_apply, ← smul_assoc, smul_mk'_one, mk'_self', one_smul]⟩⟩
obtain ⟨⟨m, rfl⟩, n, rfl⟩ := PProd.mk (mk_surjective _ m) (mk_surjective _ n)
simp only [Module.algebraMap_end_apply, ← mk_smul, Submodule.Quotient.eq, ← smul_sub] at e
replace e := Submodule.smul_mem _ (IsLocalization.mk' S 1 x) e
rwa [smul_comm, ← smul_assoc, smul_mk'_one, mk'_self', one_smul, ← Submodule.Quotient.eq] at e
surj
y := by
obtain ⟨y, rfl⟩ := mk_surjective _ y
obtain ⟨⟨y, s⟩, rfl⟩ := IsLocalizedModule.mk'_surjective p f y
exact
⟨⟨Submodule.Quotient.mk y, s⟩, by
simp only [Function.uncurry_apply_pair, toLocalizedQuotient'_mk, ← mk_smul, mk'_cancel']⟩
exists_of_eq {m n}
e := by
obtain ⟨⟨m, rfl⟩, n, rfl⟩ := PProd.mk (mk_surjective _ m) (mk_surjective _ n)
obtain ⟨x, hx, s, hs⟩ : f (m - n) ∈ _ := by simpa [Submodule.Quotient.eq] using e
obtain ⟨c, hc⟩ := exists_of_eq (S := p) (show f (s • (m - n)) = f x by simp [-map_sub, ← hs])
exact
⟨c * s, by
simpa only [← Quotient.mk_smul, Submodule.Quotient.eq, ← smul_sub, mul_smul, hc] using M'.smul_mem c hx⟩
