English
There is a natural linear map from compatible maps p → q to linear maps M/p → M₂/q, defined by sending a representative m to its image under f, modulo q.
Русский
Существует естественное линейное отображение от совместимых отображений p → q к линейным отображениям M/p → M₂/q, задаваемое отображением [m] ↦ [f(m)].
LaTeX
$$$mapQLinear: \operatorname{compatibleMaps}(p,q) \to_L[R] M/p \to_L[R] M_2/q, \quad toFun(f,[m]) = [f(m)].$$$
Lean4
/-- Given modules `M`, `M₂` over a commutative ring, together with submodules `p ⊆ M`, `q ⊆ M₂`,
the natural map $\{f ∈ Hom(M, M₂) | f(p) ⊆ q \} \to Hom(M/p, M₂/q)$ is linear. -/
def mapQLinear : compatibleMaps p q →ₗ[R] M ⧸ p →ₗ[R] M₂ ⧸ q
where
toFun f := mapQ _ _ f.val f.property
map_add' x
y := by
ext
rfl
map_smul' c
f := by
ext
rfl
