generator_map_dvd_of_mem — Mathlib

English

Let N,O be submodules and φ a linear map between appropriate domains; if the image is principal, certain divisibility relations hold between the image generator and φ of elements.

Русский

Пусть N,O — подподмодули и φ линейное отображение между соответствующими пространствами; если образ является главным, то выполняются определённые делимости между генератором образа и φ(const).

LaTeX

$$generator (ϕ.submoduleImage N) ∣ ϕ ⟨x, hNO hx⟩$$

Lean4

theorem generator_map_dvd_of_mem {N : Submodule R M} (ϕ : M →ₗ[R] R) [(N.map ϕ).IsPrincipal] {x : M} (hx : x ∈ N) :
    generator (N.map ϕ) ∣ ϕ x := by
  rw [← mem_iff_generator_dvd, Submodule.mem_map]
  exact
    ⟨x, hx, rfl⟩
      -- Note that the converse may not hold if `ϕ` is not injective.

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