English
There is a canonical symmetry between left-right tensor quotients, expressed via a commutative diagram of isomorphisms between various tensor-quotient constructions.
Русский
Существует каноническая симметрия между лево-правыми тензорными факторизациями, выраженная через каноническую диаграмму соответствующих изоморфизмов.
LaTeX
$$$$ \text{There exists a natural isomorphism between } M ⊗_R (N / n) \text{ and } (M ⊗_R N) / (M ⊗_R n). $$$$
Lean4
theorem lTensor_range : range (lTensor Q g) = range (lTensor Q (Submodule.subtype (range g))) :=
by
have : g = (Submodule.subtype _).comp g.rangeRestrict := rfl
nth_rewrite 1 [this]
rw [lTensor_comp]
apply range_comp_of_range_eq_top
rw [range_eq_top]
apply lTensor_surjective
rw [← range_eq_top, range_rangeRestrict]
