generator_maximal_submoduleImage_dvd

English

Let N ≤ O be submodules of a module M, and ϕ: O → R a linear map whose image of N is principal with a generator a. If the submodule-image maximality condition holds, and y ∈ N with ϕ(y) = a, then for any ψ: O → R we have a | ψ(y).

Русский

Пусть N ⊆ O — подмодули модуля M и ϕ: O → R линейное. Пусть образ N через ϕ — главное, порождающее a, и выполнено максимум-подобное условие. Если y ∈ N и ϕ(y) = a, то для любого ψ: O → R имеет место делимость a | ψ(y).

LaTeX

$$$\\forall N \\le O \\le M, \\; ϕ: O \\to_R R,\\; (∀ ψ, \\neg (ϕ.submoduleImage N < ψ.submoduleImage N)) \n\\Rightarrow (∀ y \\in N, ϕ ⟨y, _⟩ = generator (ϕ.submoduleImage N) \n\\Rightarrow ∀ ψ, generator (ϕ.submoduleImage N) | ψ ⟨y, _⟩).$$$

Lean4

theorem generator_maximal_submoduleImage_dvd {N O : Submodule R M} (hNO : N ≤ O) {ϕ : O →ₗ[R] R}
    (hϕ : ∀ ψ : O →ₗ[R] R, ¬ϕ.submoduleImage N < ψ.submoduleImage N) [(ϕ.submoduleImage N).IsPrincipal] (y : M)
    (yN : y ∈ N) (ϕy_eq : ϕ ⟨y, hNO yN⟩ = generator (ϕ.submoduleImage N)) (ψ : O →ₗ[R] R) :
    generator (ϕ.submoduleImage N) ∣ ψ ⟨y, hNO yN⟩ :=
  by
  let a : R := generator (ϕ.submoduleImage N)
  let d : R := IsPrincipal.generator (Submodule.span R {a, ψ ⟨y, hNO yN⟩})
  have d_dvd_left : d ∣ a := (mem_iff_generator_dvd _).mp (subset_span (mem_insert _ _))
  have d_dvd_right : d ∣ ψ ⟨y, hNO yN⟩ :=
    (mem_iff_generator_dvd _).mp (subset_span (mem_insert_of_mem _ (mem_singleton _)))
  refine dvd_trans ?_ d_dvd_right
  rw [dvd_generator_iff, Ideal.span, ← span_singleton_generator (Submodule.span R {a, ψ ⟨y, hNO yN⟩})]
  · obtain ⟨r₁, r₂, d_eq⟩ : ∃ r₁ r₂ : R, d = r₁ * a + r₂ * ψ ⟨y, hNO yN⟩ :=
      by
      obtain ⟨r₁, r₂', hr₂', hr₁⟩ :=
        mem_span_insert.mp (IsPrincipal.generator_mem (Submodule.span R {a, ψ ⟨y, hNO yN⟩}))
      obtain ⟨r₂, rfl⟩ := mem_span_singleton.mp hr₂'
      exact ⟨r₁, r₂, hr₁⟩
    let ψ' : O →ₗ[R] R := r₁ • ϕ + r₂ • ψ
    have : span R { d } ≤ ψ'.submoduleImage N :=
      by
      rw [span_le, singleton_subset_iff, SetLike.mem_coe, LinearMap.mem_submoduleImage_of_le hNO]
      refine ⟨y, yN, ?_⟩
      change r₁ * ϕ ⟨y, hNO yN⟩ + r₂ * ψ ⟨y, hNO yN⟩ = d
      rw [d_eq, ϕy_eq]
    refine le_antisymm (this.trans (le_of_eq ?_)) (Ideal.span_singleton_le_span_singleton.mpr d_dvd_left)
    rw [span_singleton_generator]
    apply (le_trans _ this).eq_of_not_lt' (hϕ ψ')
    rw [← span_singleton_generator (ϕ.submoduleImage N)]
    exact Ideal.span_singleton_le_span_singleton.mpr d_dvd_left
  · exact subset_span (mem_insert _ _)

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