comap_prod_prod — Mathlib

English

The comap of the prodMap with respect to submodules equals the intersection of the comaps: comap (prod f g) (S.prod S') = comap f S ∩ comap g S'.

Русский

Предобразение по prodMap равно пересечению предобразований: comap (prod f g) (S.prod S') = comap f S ∩ comap g S'.

LaTeX

$$$ \\text{comap} (\\text{prodMap } f g) (S \\text{.prod } S') = \\text{comap } f S \\cap \\text{comap } g S'. $$$

Lean4

theorem comap_prod_prod (f : M →ₗ[R] M₂) (g : M →ₗ[R] M₃) (p : Submodule R M₂) (q : Submodule R M₃) :
    comap (prod f g) (p.prod q) = comap f p ⊓ comap g q :=
  Submodule.ext fun _x => Iff.rfl

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