English
The simp lemma for isLocalizedModule_id states that the identity map is localized and behaves trivially under the localization, i.e., equality with itself holds by reflexivity.
Русский
Симп-лемма для isLocalizedModule_id утверждает локализуемость тождественного отображения и тривиальность поведения локализации (рефлексивность).
LaTeX
$$$[isLocalizedModule_id].$$$
Lean4
instance localizedModuleIsLocalizedModule : IsLocalizedModule S (LocalizedModule.mkLinearMap S M)
where
map_units
s :=
⟨⟨algebraMap R (Module.End R (LocalizedModule S M)) s, LocalizedModule.divBy s,
DFunLike.ext _ _ <| LocalizedModule.mul_by_divBy s, DFunLike.ext _ _ <| LocalizedModule.divBy_mul_by s⟩,
DFunLike.ext _ _ fun p =>
p.induction_on <| by
intros
rfl⟩
surj
p :=
p.induction_on fun m t => by
refine ⟨⟨m, t⟩, ?_⟩
rw [Submonoid.smul_def, LocalizedModule.smul'_mk, LocalizedModule.mkLinearMap_apply, ← Submonoid.smul_def,
LocalizedModule.mk_cancel t]
exists_of_eq eq1 := by simpa only [eq_comm, one_smul] using LocalizedModule.mk_eq.mp eq1
