English
Linear map from p to p ⊔ p' representing the inclusion as quotient modules.
Русский
Линейное отображение из p в p ⊔ p' как включение между соответствующими модулями-частями.
LaTeX
$$$\text{abbrev } \text{subToSupQuotient}(p,p') : {x\in p} o {x\mod (p\sqcup p')}$$$
Lean4
/-- Canonical linear map from the quotient `p/(p ∩ p')` to `(p+p')/p'`, mapping `x + (p ∩ p')`
to `x + p'`, where `p` and `p'` are submodules of an ambient module.
Note that in the following declaration the type of the domain is expressed using
``comap p.subtype p ⊓ comap p.subtype p'`
instead of
`comap p.subtype (p ⊓ p')`
because the former is the simp normal form (see also `Submodule.comap_inf`). -/
def quotientInfToSupQuotient (p p' : Submodule R M) :
(↥p) ⧸ (comap p.subtype p ⊓ comap p.subtype p') →ₗ[R] (↥(p ⊔ p')) ⧸ (comap (p ⊔ p').subtype p') :=
(comap p.subtype (p ⊓ p')).liftQ (subToSupQuotient p p') (comap_leq_ker_subToSupQuotient p p')
