English
There is an order isomorphism between the lattice of Submodules of the quotient R/(R a) acting on torsionBy(R,M,a) and the lattice of Submodules of R acting on torsionBy(R,M,a).
Русский
Между порядковыми решетками подмодулов существует изоморфизм, связывающий подмодули над квотиентом и подмодули над R внутри torsionBy.
LaTeX
$$Submodule (R/(R a)) (torsionBy(R,M,a)) ≃o Submodule R (torsionBy(R,M,a)).$$
Lean4
/-- Given an `R`-module `M` and an element `a` in `R`, submodules of the `a`-torsion submodule of
`M` do not depend on whether we take scalars to be `R` or `R ⧸ R ∙ a`. -/
def submodule_torsionBy_orderIso (a : R) : Submodule (R ⧸ R ∙ a) (torsionBy R M a) ≃o Submodule R (torsionBy R M a) :=
{
restrictScalarsEmbedding R (R ⧸ R ∙ a)
(torsionBy R M
a) with
invFun := fun p ↦
{ carrier := p
add_mem' := add_mem
zero_mem' := p.zero_mem
smul_mem' := by rintro ⟨b⟩; exact p.smul_mem b }
left_inv := by intro; ext; simp [restrictScalarsEmbedding]
right_inv := by intro; ext; simp [restrictScalarsEmbedding] }
