English
The Kronecker product–type map intertwines the Kronecker TMul with the linear version as expected by the canonical isomorphism.
Русский
Отображение типа Кронекер сопряжено с линейным эквивалентом через каноническое изоморфное отображение.
LaTeX
$$kroneckerTMulAlgEquiv_apply (x) = kroneckerTMulLinearEquiv x$$
Lean4
theorem localization_localization_surj [IsLocalization N T] (x : T) :
∃ y : R × localizationLocalizationSubmodule M N, x * algebraMap R T y.2 = algebraMap R T y.1 :=
by
rcases IsLocalization.surj N x with
⟨⟨y, s⟩, eq₁⟩
-- x = y / s
rcases IsLocalization.surj M y with
⟨⟨z, t⟩, eq₂⟩
-- y = z / t
rcases IsLocalization.surj M (s : S) with
⟨⟨z', t'⟩, eq₃⟩
-- s = z' / t'
dsimp only at eq₁ eq₂ eq₃
refine
⟨⟨z * t', z' * t, ?_⟩, ?_⟩ -- x = y / s = (z * t') / (z' * t)
· rw [mem_localizationLocalizationSubmodule]
refine ⟨s, t * t', ?_⟩
rw [RingHom.map_mul, ← eq₃, mul_assoc, ← RingHom.map_mul, mul_comm t, Submonoid.coe_mul]
· simp only [RingHom.map_mul, IsScalarTower.algebraMap_apply R S T, ← eq₃, ← eq₂, ← eq₁]
ring
