prod_eq_inf_comap — Mathlib

English

For submodules p ⊆ M and q ⊆ M₂, p × q equals the infimum of the pulled-back submodules via fst and snd: p.prod q = comap fst p ∩ comap snd q.

Русский

Для подмодулей p ⊆ M и q ⊆ M₂ произведение p × q равно пересечению предобразов: p.prod q = comap fst p ∩ comap snd q.

LaTeX

$$$ p \\text{.prod } q = \\text{comap }(\\text{fst } R M M_2) p \\cap \\text{comap }(\\text{snd } R M M_2) q $$$

Lean4

theorem prod_eq_inf_comap (p : Submodule R M) (q : Submodule R M₂) :
    p.prod q = p.comap (LinearMap.fst R M M₂) ⊓ q.comap (LinearMap.snd R M M₂) :=
  Submodule.ext fun _x => Iff.rfl

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