English
The LiftOfLE construction provides the natural map between LocalizedModule S1 M and LocalizedModule S2 M under the assumption S1 ≤ S2, via a pair of localized linear maps and a commutativity constraint.
Русский
Конструкция LiftOfLE задаёт естественное отображение между \nLocalizedModule S1 M и LocalizedModule S2 M при S1 ⊆ S2 через пару локализованных линейных отображений и условие коммутативности.
LaTeX
$$$$ \\text{LiftOfLE}: \\text{LocalizedModule } S_1 M \\to \\text{LocalizedModule } S_2 M \\; \\text{с удовлетворением свойств совместимости} $$$$
Lean4
/-- The natural map `Mₛ →ₗ[R] Mₜ` if `s ≤ t` (in `Submonoid R`). -/
noncomputable abbrev _root_.LocalizedModule.liftOfLE : LocalizedModule S₁ M →ₗ[R] LocalizedModule S₂ M :=
IsLocalizedModule.liftOfLE S₁ S₂ h (LocalizedModule.mkLinearMap S₁ M) (LocalizedModule.mkLinearMap S₂ M)
