English
For any submodule P of M over R and any scalar extension S acting on M with a compatible tower, the quotient of M by P.restrictScalars S is naturally isomorphic (as an S-module) to the quotient M / P.
Русский
Для любого подпространства P ⊆ M над R и любого расширения скаляров S, действующего на M с совместной тектонной структурой, фактор-модуль M / P.restrictScalars S естественно изоморфен фактор-модулю M / P как S-модуль.
LaTeX
$$$$ (M \\! / P_{\\text{restrictScalars } S}) \\cong_S (M \\! / P). $$$$
Lean4
/-- The quotient of `P` as an `S`-submodule is the same as the quotient of `P` as an `R`-submodule,
where `P : Submodule R M`.
-/
def restrictScalarsEquiv [Ring S] [SMul S R] [Module S M] [IsScalarTower S R M] (P : Submodule R M) :
(M ⧸ P.restrictScalars S) ≃ₗ[S] M ⧸ P :=
{
Quotient.congrRight fun _ _ =>
Iff.rfl with
map_add' := fun x y => Quotient.inductionOn₂' x y fun _x' _y' => rfl
map_smul' := fun _c x => Submodule.Quotient.induction_on _ x fun _x' => rfl }
