comap — Mathlib

English

For any f and p ≤ p', map f p ≤ map f p'.

Русский

Для любого отображения f и p ⊆ p' выполняется map f p ⊆ map f p'.

LaTeX

$$p \\subseteq p' \\Rightarrow map f p \\subseteq map f p'$$

Lean4

/-- The pullback of a submodule `p ⊆ M₂` along `f : M → M₂` -/
def comap [SemilinearMapClass F σ₁₂ M M₂] (f : F) (p : Submodule R₂ M₂) : Submodule R M :=
  { p.toAddSubmonoid.comap f with
    carrier := f ⁻¹' p
    smul_mem' := fun a x h => by simp [p.smul_mem (σ₁₂ a) h, map_smulₛₗ _] }

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