isPrincipal_iff_exists_isGreatest

English

For hv, an ideal I of O is principal iff there exists x such that x equals the greatest element of the image of I under v∘algebraMap.

Русский

Пусть hv. для идеала I кольца O справедливо: I порожденный ⇔ существует x такое, что x является наибольшим элементом образа I под v∘algebraMap.

LaTeX

$$I.IsPrincipal \iff \exists x, IsGreatest (v \circ algebraMap(O,F) '' I) x$$

Lean4

theorem isPrincipal_iff_exists_isGreatest (hv : Integers v O) {I : Ideal O} :
    I.IsPrincipal ↔ ∃ x, IsGreatest (v ∘ algebraMap O F '' I) x :=
  by
  constructor <;> rintro ⟨x, hx⟩
  · refine ⟨(v ∘ algebraMap O F) x, ?_, ?_⟩
    · refine Set.mem_image_of_mem _ ?_
      simp [hx, Ideal.mem_span_singleton_self]
    · intro y hy
      simp only [Function.comp_apply, hx, Ideal.submodule_span_eq, Set.mem_image, SetLike.mem_coe,
        Ideal.mem_span_singleton] at hy
      obtain ⟨y, hy, rfl⟩ := hy
      exact le_of_dvd hv hy
  · obtain ⟨a, ha, rfl⟩ : ∃ a ∈ I, (v ∘ algebraMap O F) a = x := by simpa using hx.left
    refine ⟨a, ?_⟩
    ext b
    simp only [Ideal.submodule_span_eq, Ideal.mem_span_singleton]
    exact ⟨fun hb ↦ dvd_of_le hv (hx.2 <| mem_image_of_mem _ hb), fun hb ↦ I.mem_of_dvd hb ha⟩

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