English
Given a submodule p of M and q a submodule of the subtype p, there is a natural linear equivalence between q and q.map p.subtype, relating their inclusions.
Русский
Дано подмодуль p модуля M и подмодуль q подмодуля p; существует естественный линейный эквивалент между q и q.map p.subtype, связывающий их вложения.
LaTeX
$$$q \\simeq_{\\mathrm{lin}} q.map(p.subtype)$ with the forward map given by restriction to p.$$
Lean4
/-- Given `p` a submodule of the module `M` and `q` a submodule of `p`, `p.equivSubtypeMap q`
is the natural `LinearEquiv` between `q` and `q.map p.subtype`. -/
def equivSubtypeMap (p : Submodule R M) (q : Submodule R p) : q ≃ₗ[R] q.map p.subtype :=
{ (p.subtype.domRestrict q).codRestrict _ (by rintro ⟨x, hx⟩; exact ⟨x, hx, rfl⟩) with
invFun := by
rintro ⟨x, hx⟩
refine ⟨⟨x, ?_⟩, ?_⟩ <;> rcases hx with ⟨⟨_, h⟩, _, rfl⟩ <;> assumption }
