submoduleOf — Mathlib

English

For submodules p and q of M, the intersection p ⊓ q can be viewed as a submodule of q, obtained by pulling back along the inclusion q ↪ M.

Русский

Для подмодулей p и q модуля M пересечение p ∩ q можно рассматривать как подмодуль q, полученный обратным образом через включение q в M.

LaTeX

$$$p \cap q \text{ as a submodule of } q \;=\; \operatorname{Submodule}.comap_{\text{inclusion}}(p)$$$

Lean4

/-- For any `R` submodules `p` and `q`, `p ⊓ q` as a submodule of `q`. -/
def submoduleOf (p q : Submodule R M) : Submodule R q :=
  Submodule.comap q.subtype p

Похожие утверждения