English
Two isomorphisms between localized modules commute with the localization maps, yielding a natural commutativity relation between the two sides of the diagram.
Русский
Два изоморфизма между локализованными модулями коммутируют с локализационными отображениями, образуя естественную связь на диаграмме.
LaTeX
$$$$ (\\text{iso } S f_0) \\circ (\\text{map } S (mkLinearMap S M_0) (LocalizedModule.mkLinearMap S M_1) g) = \\dots $$$$
Lean4
theorem map_iso_commute (g : M₀ →ₗ[R] M₁) :
(map S f₀ f₁) g ∘ₗ (iso S f₀) = (iso S f₁) ∘ₗ (map S (mkLinearMap S M₀) (mkLinearMap S M₁)) g :=
by
ext x
induction x using induction_on with
| _ m s
refine ((Module.End.isUnit_iff _).1 (map_units f₁ s)).1 ?_
rw [Module.algebraMap_end_apply, Module.algebraMap_end_apply, ← CompatibleSMul.map_smul, ← CompatibleSMul.map_smul,
smul'_mk, ← mk_smul _ s.2, mk_cancel]
simp [map, lift, iso_localizedModule_eq_refl, lift_mk]
