3. Ringe und Ideale🔗

Dieses Kapitel übersetzt den Satz „ℤ ist ein Hauptidealring“ aus Kapitel 9 des Skripts. Es ist der klassische Beweis über Division mit Rest und zugleich unsere erste Begegnung mit dem Wohlordnungsprinzip in Lean.

3.1. Das Mathlib-Wörterbuch🔗

Ein Ideal in einem kommutativen Ring R ist ein Term I : Ideal R. Die beiden Bedingungen aus der Ideal-Definition des Skripts heißen I.add_mem (für alle a, b \in I ist a+b \in I) und I.mul_mem_left (für alle r \in R und a \in I ist r \cdot a \in I); außerdem ist I.zero_mem : 0 ∈ I.
Das von einer Menge s erzeugte Ideal ist Ideal.span s; ein Hauptideal (a) ist also Ideal.span {a}. Die Beobachtung „Hauptideale und Teilbarkeit“ des Skripts ist das Lemma Ideal.mem_span_singleton : b ∈ span {a} ↔ a ∣ b.
„Jedes Ideal ist endlich erzeugt / ein Hauptideal“ sind die Prädikate IsNoetherianRing R und IsPrincipalIdealRing R.

3.2. ℤ ist ein Hauptidealring🔗

Satz 9.3.7 des Skripts, mit Beweis:

Es sei I \subset \mathbb{Z} ein Ideal und I \neq \{0\}. Dann gibt es ein x \in I \setminus \{0\}. Beachte, dass dann auch -x = (-1) \cdot x in I ist. Also enthält I positive Elemente. Sei a \in I jetzt das kleinste positive Element. Wir werden zeigen, dass I = (a) ist. Die Inklusion (a) \subseteq I ist klar. Sei b \in I irgendein positives Element, dann teilen wir mit Rest: b = q \cdot a + r mit 0 \leq r < a. Die Zahl r ist jetzt aber in I, denn b und q \cdot a sind in I. Weiter muss wegen der Minimalität von a also r = 0 sein und somit b \in (a).

Zwei Anmerkungen zur Übersetzung. Das „kleinste positive Element“ liefert das Wohlordnungsprinzip, in Mathlib Int.exists_least_of_bdd. Und wo das Skript nur positive b behandelt (und den Rest dem Leser überlässt), nehmen wir gleich beliebige b; die Division mit Rest in Lean funktioniert für alle ganzen Zahlen.

theorem int_hauptidealring (I : Ideal ℤ) :
    ∃ a : ℤ, I = Ideal.span {a} := byI:Ideal ℤ⊢ ∃ a, I = Ideal.span {a}
  -- „… und I ≠ {0}.“  Das Nullideal erledigt a = 0:
  by_cases hI : I = ⊥posI:Ideal ℤhI:I = ⊥⊢ ∃ a, I = Ideal.span {a}negI:Ideal ℤhI:¬I = ⊥⊢ ∃ a, I = Ideal.span {a}
  ·posI:Ideal ℤhI:I = ⊥⊢ ∃ a, I = Ideal.span {a} exact ⟨0, byI:Ideal ℤhI:I = ⊥⊢ I = Ideal.span {0} simp [hI]All goals completed! 🐙⟩
  -- „Dann gibt es ein x ∈ I∖{0}.“
  ·negI:Ideal ℤhI:¬I = ⊥⊢ ∃ a, I = Ideal.span {a} obtain ⟨x, hxI, hx0⟩ :=
      Submodule.exists_mem_ne_zero_of_ne_bot hInegI:Ideal ℤhI:¬I = ⊥x:ℤhxI:x ∈ Ihx0:x ≠ 0⊢ ∃ a, I = Ideal.span {a}
    -- „Beachte, dass dann auch −x = (−1)·x in I ist.  Also
    --  enthält I positive Elemente.“
    have hmx : -x ∈ I := by
      have h := I.mul_mem_left (-1) hxII:Ideal ℤhI:¬I = ⊥x:ℤhxI:x ∈ Ihx0:x ≠ 0h:-1 * x ∈ I⊢ -x ∈ I
      simpa using hnegI:Ideal ℤhI:¬I = ⊥x:ℤhxI:x ∈ Ihx0:x ≠ 0hmx:-x ∈ I⊢ ∃ a, I = Ideal.span {a}
    have hpos : ∃ y, y ∈ I ∧ 0 < y := by
      rcases lt_or_gt_of_ne hx0 with h | hinlI:Ideal ℤhI:¬I = ⊥x:ℤhxI:x ∈ Ihx0:x ≠ 0hmx:-x ∈ Ih:x < 0⊢ ∃ y ∈ I, 0 < yinrI:Ideal ℤhI:¬I = ⊥x:ℤhxI:x ∈ Ihx0:x ≠ 0hmx:-x ∈ Ih:0 < x⊢ ∃ y ∈ I, 0 < y
      ·inlI:Ideal ℤhI:¬I = ⊥x:ℤhxI:x ∈ Ihx0:x ≠ 0hmx:-x ∈ Ih:x < 0⊢ ∃ y ∈ I, 0 < y exact ⟨-x, hmx, byI:Ideal ℤhI:¬I = ⊥x:ℤhxI:x ∈ Ihx0:x ≠ 0hmx:-x ∈ Ih:x < 0⊢ 0 < -x omegaAll goals completed! 🐙⟩
      ·inrI:Ideal ℤhI:¬I = ⊥x:ℤhxI:x ∈ Ihx0:x ≠ 0hmx:-x ∈ Ih:0 < x⊢ ∃ y ∈ I, 0 < y exact ⟨x, hxI, h⟩negI:Ideal ℤhI:¬I = ⊥x:ℤhxI:x ∈ Ihx0:x ≠ 0hmx:-x ∈ Ihpos:∃ y ∈ I, 0 < y⊢ ∃ a, I = Ideal.span {a}
    -- „Sei a ∈ I jetzt das kleinste positive Element.“
    obtain ⟨a, ⟨haI, ha⟩, hmin⟩ :=
      Int.exists_least_of_bdd
        (P := fun y => y ∈ I ∧ 0 < y)
        ⟨1, fun z hz => byI:Ideal ℤhI:¬I = ⊥x:ℤhxI:x ∈ Ihx0:x ≠ 0hmx:-x ∈ Ihpos:∃ y ∈ I, 0 < yz:ℤhz:z ∈ I ∧ 0 < z⊢ 1 ≤ z have := hz.2I:Ideal ℤhI:¬I = ⊥x:ℤhxI:x ∈ Ihx0:x ≠ 0hmx:-x ∈ Ihpos:∃ y ∈ I, 0 < yz:ℤhz:z ∈ I ∧ 0 < zthis:0 < z⊢ 1 ≤ z; omegaAll goals completed! 🐙⟩ hposnegI:Ideal ℤhI:¬I = ⊥x:ℤhxI:x ∈ Ihx0:x ≠ 0hmx:-x ∈ Ihpos:∃ y ∈ I, 0 < ya:ℤhmin:∀ (z : ℤ), z ∈ I ∧ 0 < z → a ≤ zhaI:a ∈ Iha:0 < a⊢ ∃ a, I = Ideal.span {a}
    -- „Wir werden zeigen, dass I = (a) ist.“
    refine ⟨a, le_antisymm ?_ ?_⟩neg.refine_1I:Ideal ℤhI:¬I = ⊥x:ℤhxI:x ∈ Ihx0:x ≠ 0hmx:-x ∈ Ihpos:∃ y ∈ I, 0 < ya:ℤhmin:∀ (z : ℤ), z ∈ I ∧ 0 < z → a ≤ zhaI:a ∈ Iha:0 < a⊢ I ≤ Ideal.span {a}neg.refine_2I:Ideal ℤhI:¬I = ⊥x:ℤhxI:x ∈ Ihx0:x ≠ 0hmx:-x ∈ Ihpos:∃ y ∈ I, 0 < ya:ℤhmin:∀ (z : ℤ), z ∈ I ∧ 0 < z → a ≤ zhaI:a ∈ Iha:0 < a⊢ Ideal.span {a} ≤ I
    ·neg.refine_1I:Ideal ℤhI:¬I = ⊥x:ℤhxI:x ∈ Ihx0:x ≠ 0hmx:-x ∈ Ihpos:∃ y ∈ I, 0 < ya:ℤhmin:∀ (z : ℤ), z ∈ I ∧ 0 < z → a ≤ zhaI:a ∈ Iha:0 < a⊢ I ≤ Ideal.span {a} -- „Sei b ∈ I irgendein Element, dann teilen wir mit
      --  Rest: b = q·a + r mit 0 ≤ r < a.“
      intro b hbneg.refine_1I:Ideal ℤhI:¬I = ⊥x:ℤhxI:x ∈ Ihx0:x ≠ 0hmx:-x ∈ Ihpos:∃ y ∈ I, 0 < ya:ℤhmin:∀ (z : ℤ), z ∈ I ∧ 0 < z → a ≤ zhaI:a ∈ Iha:0 < ab:ℤhb:b ∈ I⊢ b ∈ Ideal.span {a}
      set q := b / a with hq_defneg.refine_1I:Ideal ℤhI:¬I = ⊥x:ℤhxI:x ∈ Ihx0:x ≠ 0hmx:-x ∈ Ihpos:∃ y ∈ I, 0 < ya:ℤhmin:∀ (z : ℤ), z ∈ I ∧ 0 < z → a ≤ zhaI:a ∈ Iha:0 < ab:ℤhb:b ∈ Iq:ℤ := b / ahq_def:q = b / a⊢ b ∈ Ideal.span {a}
      set r := b % a with hr_defneg.refine_1I:Ideal ℤhI:¬I = ⊥x:ℤhxI:x ∈ Ihx0:x ≠ 0hmx:-x ∈ Ihpos:∃ y ∈ I, 0 < ya:ℤhmin:∀ (z : ℤ), z ∈ I ∧ 0 < z → a ≤ zhaI:a ∈ Iha:0 < ab:ℤhb:b ∈ Iq:ℤ := b / ahq_def:q = b / ar:ℤ := b % ahr_def:r = b % a⊢ b ∈ Ideal.span {a}
      have hdiv : b = a * q + r := byI:Ideal ℤ⊢ ∃ a, I = Ideal.span {a}
        rw [hq_def,I:Ideal ℤhI:¬I = ⊥x:ℤhxI:x ∈ Ihx0:x ≠ 0hmx:-x ∈ Ihpos:∃ y ∈ I, 0 < ya:ℤhmin:∀ (z : ℤ), z ∈ I ∧ 0 < z → a ≤ zhaI:a ∈ Iha:0 < ab:ℤhb:b ∈ Iq:ℤ := b / ahq_def:q = b / ar:ℤ := b % ahr_def:r = b % a⊢ b = a * (b / a) + r hr_defI:Ideal ℤhI:¬I = ⊥x:ℤhxI:x ∈ Ihx0:x ≠ 0hmx:-x ∈ Ihpos:∃ y ∈ I, 0 < ya:ℤhmin:∀ (z : ℤ), z ∈ I ∧ 0 < z → a ≤ zhaI:a ∈ Iha:0 < ab:ℤhb:b ∈ Iq:ℤ := b / ahq_def:q = b / ar:ℤ := b % ahr_def:r = b % a⊢ b = a * (b / a) + b % a]I:Ideal ℤhI:¬I = ⊥x:ℤhxI:x ∈ Ihx0:x ≠ 0hmx:-x ∈ Ihpos:∃ y ∈ I, 0 < ya:ℤhmin:∀ (z : ℤ), z ∈ I ∧ 0 < z → a ≤ zhaI:a ∈ Iha:0 < ab:ℤhb:b ∈ Iq:ℤ := b / ahq_def:q = b / ar:ℤ := b % ahr_def:r = b % a⊢ b = a * (b / a) + b % a
        exact (Int.mul_ediv_add_emod b a).symmneg.refine_1I:Ideal ℤhI:¬I = ⊥x:ℤhxI:x ∈ Ihx0:x ≠ 0hmx:-x ∈ Ihpos:∃ y ∈ I, 0 < ya:ℤhmin:∀ (z : ℤ), z ∈ I ∧ 0 < z → a ≤ zhaI:a ∈ Iha:0 < ab:ℤhb:b ∈ Iq:ℤ := b / ahq_def:q = b / ar:ℤ := b % ahr_def:r = b % ahdiv:b = a * q + r⊢ b ∈ Ideal.span {a}
      have hr0 : 0 ≤ r := Int.emod_nonneg b (byI:Ideal ℤhI:¬I = ⊥x:ℤhxI:x ∈ Ihx0:x ≠ 0hmx:-x ∈ Ihpos:∃ y ∈ I, 0 < ya:ℤhmin:∀ (z : ℤ), z ∈ I ∧ 0 < z → a ≤ zhaI:a ∈ Iha:0 < ab:ℤhb:b ∈ Iq:ℤ := b / ahq_def:q = b / ar:ℤ := b % ahr_def:r = b % ahdiv:b = a * q + r⊢ a ≠ 0 omegaAll goals completed! 🐙)neg.refine_1I:Ideal ℤhI:¬I = ⊥x:ℤhxI:x ∈ Ihx0:x ≠ 0hmx:-x ∈ Ihpos:∃ y ∈ I, 0 < ya:ℤhmin:∀ (z : ℤ), z ∈ I ∧ 0 < z → a ≤ zhaI:a ∈ Iha:0 < ab:ℤhb:b ∈ Iq:ℤ := b / ahq_def:q = b / ar:ℤ := b % ahr_def:r = b % ahdiv:b = a * q + rhr0:0 ≤ r⊢ b ∈ Ideal.span {a}
      have hra : r < a := Int.emod_lt_of_pos b haneg.refine_1I:Ideal ℤhI:¬I = ⊥x:ℤhxI:x ∈ Ihx0:x ≠ 0hmx:-x ∈ Ihpos:∃ y ∈ I, 0 < ya:ℤhmin:∀ (z : ℤ), z ∈ I ∧ 0 < z → a ≤ zhaI:a ∈ Iha:0 < ab:ℤhb:b ∈ Iq:ℤ := b / ahq_def:q = b / ar:ℤ := b % ahr_def:r = b % ahdiv:b = a * q + rhr0:0 ≤ rhra:r < a⊢ b ∈ Ideal.span {a}
      -- „Die Zahl r ist jetzt aber in I, denn b und q·a
      --  sind in I.“
      have hqaI : a * q ∈ I := I.mul_mem_right q haIneg.refine_1I:Ideal ℤhI:¬I = ⊥x:ℤhxI:x ∈ Ihx0:x ≠ 0hmx:-x ∈ Ihpos:∃ y ∈ I, 0 < ya:ℤhmin:∀ (z : ℤ), z ∈ I ∧ 0 < z → a ≤ zhaI:a ∈ Iha:0 < ab:ℤhb:b ∈ Iq:ℤ := b / ahq_def:q = b / ar:ℤ := b % ahr_def:r = b % ahdiv:b = a * q + rhr0:0 ≤ rhra:r < ahqaI:a * q ∈ I⊢ b ∈ Ideal.span {a}
      have hrI : r ∈ I := byI:Ideal ℤ⊢ ∃ a, I = Ideal.span {a}
        have hr_eq : r = b - a * q := byI:Ideal ℤ⊢ ∃ a, I = Ideal.span {a} rw [hdivI:Ideal ℤhI:¬I = ⊥x:ℤhxI:x ∈ Ihx0:x ≠ 0hmx:-x ∈ Ihpos:∃ y ∈ I, 0 < ya:ℤhmin:∀ (z : ℤ), z ∈ I ∧ 0 < z → a ≤ zhaI:a ∈ Iha:0 < ab:ℤhb:b ∈ Iq:ℤ := b / ahq_def:q = b / ar:ℤ := b % ahr_def:r = b % ahdiv:b = a * q + rhr0:0 ≤ rhra:r < ahqaI:a * q ∈ I⊢ r = a * q + r - a * q]I:Ideal ℤhI:¬I = ⊥x:ℤhxI:x ∈ Ihx0:x ≠ 0hmx:-x ∈ Ihpos:∃ y ∈ I, 0 < ya:ℤhmin:∀ (z : ℤ), z ∈ I ∧ 0 < z → a ≤ zhaI:a ∈ Iha:0 < ab:ℤhb:b ∈ Iq:ℤ := b / ahq_def:q = b / ar:ℤ := b % ahr_def:r = b % ahdiv:b = a * q + rhr0:0 ≤ rhra:r < ahqaI:a * q ∈ I⊢ r = a * q + r - a * q; ringI:Ideal ℤhI:¬I = ⊥x:ℤhxI:x ∈ Ihx0:x ≠ 0hmx:-x ∈ Ihpos:∃ y ∈ I, 0 < ya:ℤhmin:∀ (z : ℤ), z ∈ I ∧ 0 < z → a ≤ zhaI:a ∈ Iha:0 < ab:ℤhb:b ∈ Iq:ℤ := b / ahq_def:q = b / ar:ℤ := b % ahr_def:r = b % ahdiv:b = a * q + rhr0:0 ≤ rhra:r < ahqaI:a * q ∈ Ihr_eq:r = b - a * q⊢ r ∈ I
        rw [hr_eqI:Ideal ℤhI:¬I = ⊥x:ℤhxI:x ∈ Ihx0:x ≠ 0hmx:-x ∈ Ihpos:∃ y ∈ I, 0 < ya:ℤhmin:∀ (z : ℤ), z ∈ I ∧ 0 < z → a ≤ zhaI:a ∈ Iha:0 < ab:ℤhb:b ∈ Iq:ℤ := b / ahq_def:q = b / ar:ℤ := b % ahr_def:r = b % ahdiv:b = a * q + rhr0:0 ≤ rhra:r < ahqaI:a * q ∈ Ihr_eq:r = b - a * q⊢ b - a * q ∈ I]I:Ideal ℤhI:¬I = ⊥x:ℤhxI:x ∈ Ihx0:x ≠ 0hmx:-x ∈ Ihpos:∃ y ∈ I, 0 < ya:ℤhmin:∀ (z : ℤ), z ∈ I ∧ 0 < z → a ≤ zhaI:a ∈ Iha:0 < ab:ℤhb:b ∈ Iq:ℤ := b / ahq_def:q = b / ar:ℤ := b % ahr_def:r = b % ahdiv:b = a * q + rhr0:0 ≤ rhra:r < ahqaI:a * q ∈ Ihr_eq:r = b - a * q⊢ b - a * q ∈ I
        exact I.sub_mem hb hqaIneg.refine_1I:Ideal ℤhI:¬I = ⊥x:ℤhxI:x ∈ Ihx0:x ≠ 0hmx:-x ∈ Ihpos:∃ y ∈ I, 0 < ya:ℤhmin:∀ (z : ℤ), z ∈ I ∧ 0 < z → a ≤ zhaI:a ∈ Iha:0 < ab:ℤhb:b ∈ Iq:ℤ := b / ahq_def:q = b / ar:ℤ := b % ahr_def:r = b % ahdiv:b = a * q + rhr0:0 ≤ rhra:r < ahqaI:a * q ∈ IhrI:r ∈ I⊢ b ∈ Ideal.span {a}
      -- „Weiter muss wegen der Minimalität von a also r = 0
      --  sein …“
      have hr : r = 0 := byI:Ideal ℤ⊢ ∃ a, I = Ideal.span {a}
        by_contra hrI:Ideal ℤhI:¬I = ⊥x:ℤhxI:x ∈ Ihx0:x ≠ 0hmx:-x ∈ Ihpos:∃ y ∈ I, 0 < ya:ℤhmin:∀ (z : ℤ), z ∈ I ∧ 0 < z → a ≤ zhaI:a ∈ Iha:0 < ab:ℤhb:b ∈ Iq:ℤ := b / ahq_def:q = b / ar:ℤ := b % ahr_def:r = b % ahdiv:b = a * q + rhr0:0 ≤ rhra:r < ahqaI:a * q ∈ IhrI:r ∈ Ihr:¬r = 0⊢ False
        have : a ≤ r := hmin r ⟨hrI, byI:Ideal ℤhI:¬I = ⊥x:ℤhxI:x ∈ Ihx0:x ≠ 0hmx:-x ∈ Ihpos:∃ y ∈ I, 0 < ya:ℤhmin:∀ (z : ℤ), z ∈ I ∧ 0 < z → a ≤ zhaI:a ∈ Iha:0 < ab:ℤhb:b ∈ Iq:ℤ := b / ahq_def:q = b / ar:ℤ := b % ahr_def:r = b % ahdiv:b = a * q + rhr0:0 ≤ rhra:r < ahqaI:a * q ∈ IhrI:r ∈ Ihr:¬r = 0⊢ 0 < r omegaAll goals completed! 🐙⟩I:Ideal ℤhI:¬I = ⊥x:ℤhxI:x ∈ Ihx0:x ≠ 0hmx:-x ∈ Ihpos:∃ y ∈ I, 0 < ya:ℤhmin:∀ (z : ℤ), z ∈ I ∧ 0 < z → a ≤ zhaI:a ∈ Iha:0 < ab:ℤhb:b ∈ Iq:ℤ := b / ahq_def:q = b / ar:ℤ := b % ahr_def:r = b % ahdiv:b = a * q + rhr0:0 ≤ rhra:r < ahqaI:a * q ∈ IhrI:r ∈ Ihr:¬r = 0this:a ≤ r⊢ False
        omeganeg.refine_1I:Ideal ℤhI:¬I = ⊥x:ℤhxI:x ∈ Ihx0:x ≠ 0hmx:-x ∈ Ihpos:∃ y ∈ I, 0 < ya:ℤhmin:∀ (z : ℤ), z ∈ I ∧ 0 < z → a ≤ zhaI:a ∈ Iha:0 < ab:ℤhb:b ∈ Iq:ℤ := b / ahq_def:q = b / ar:ℤ := b % ahr_def:r = b % ahdiv:b = a * q + rhr0:0 ≤ rhra:r < ahqaI:a * q ∈ IhrI:r ∈ Ihr:r = 0⊢ b ∈ Ideal.span {a}
      -- „… und somit b ∈ (a).“
      rw [Ideal.mem_span_singletonneg.refine_1I:Ideal ℤhI:¬I = ⊥x:ℤhxI:x ∈ Ihx0:x ≠ 0hmx:-x ∈ Ihpos:∃ y ∈ I, 0 < ya:ℤhmin:∀ (z : ℤ), z ∈ I ∧ 0 < z → a ≤ zhaI:a ∈ Iha:0 < ab:ℤhb:b ∈ Iq:ℤ := b / ahq_def:q = b / ar:ℤ := b % ahr_def:r = b % ahdiv:b = a * q + rhr0:0 ≤ rhra:r < ahqaI:a * q ∈ IhrI:r ∈ Ihr:r = 0⊢ a ∣ b]neg.refine_1I:Ideal ℤhI:¬I = ⊥x:ℤhxI:x ∈ Ihx0:x ≠ 0hmx:-x ∈ Ihpos:∃ y ∈ I, 0 < ya:ℤhmin:∀ (z : ℤ), z ∈ I ∧ 0 < z → a ≤ zhaI:a ∈ Iha:0 < ab:ℤhb:b ∈ Iq:ℤ := b / ahq_def:q = b / ar:ℤ := b % ahr_def:r = b % ahdiv:b = a * q + rhr0:0 ≤ rhra:r < ahqaI:a * q ∈ IhrI:r ∈ Ihr:r = 0⊢ a ∣ b
      exact ⟨q, byI:Ideal ℤhI:¬I = ⊥x:ℤhxI:x ∈ Ihx0:x ≠ 0hmx:-x ∈ Ihpos:∃ y ∈ I, 0 < ya:ℤhmin:∀ (z : ℤ), z ∈ I ∧ 0 < z → a ≤ zhaI:a ∈ Iha:0 < ab:ℤhb:b ∈ Iq:ℤ := b / ahq_def:q = b / ar:ℤ := b % ahr_def:r = b % ahdiv:b = a * q + rhr0:0 ≤ rhra:r < ahqaI:a * q ∈ IhrI:r ∈ Ihr:r = 0⊢ b = a * q rw [hdiv,I:Ideal ℤhI:¬I = ⊥x:ℤhxI:x ∈ Ihx0:x ≠ 0hmx:-x ∈ Ihpos:∃ y ∈ I, 0 < ya:ℤhmin:∀ (z : ℤ), z ∈ I ∧ 0 < z → a ≤ zhaI:a ∈ Iha:0 < ab:ℤhb:b ∈ Iq:ℤ := b / ahq_def:q = b / ar:ℤ := b % ahr_def:r = b % ahdiv:b = a * q + rhr0:0 ≤ rhra:r < ahqaI:a * q ∈ IhrI:r ∈ Ihr:r = 0⊢ a * q + r = a * q hrI:Ideal ℤhI:¬I = ⊥x:ℤhxI:x ∈ Ihx0:x ≠ 0hmx:-x ∈ Ihpos:∃ y ∈ I, 0 < ya:ℤhmin:∀ (z : ℤ), z ∈ I ∧ 0 < z → a ≤ zhaI:a ∈ Iha:0 < ab:ℤhb:b ∈ Iq:ℤ := b / ahq_def:q = b / ar:ℤ := b % ahr_def:r = b % ahdiv:b = a * q + rhr0:0 ≤ rhra:r < ahqaI:a * q ∈ IhrI:r ∈ Ihr:r = 0⊢ a * q + 0 = a * q]I:Ideal ℤhI:¬I = ⊥x:ℤhxI:x ∈ Ihx0:x ≠ 0hmx:-x ∈ Ihpos:∃ y ∈ I, 0 < ya:ℤhmin:∀ (z : ℤ), z ∈ I ∧ 0 < z → a ≤ zhaI:a ∈ Iha:0 < ab:ℤhb:b ∈ Iq:ℤ := b / ahq_def:q = b / ar:ℤ := b % ahr_def:r = b % ahdiv:b = a * q + rhr0:0 ≤ rhra:r < ahqaI:a * q ∈ IhrI:r ∈ Ihr:r = 0⊢ a * q + 0 = a * q; ringAll goals completed! 🐙⟩
    ·neg.refine_2I:Ideal ℤhI:¬I = ⊥x:ℤhxI:x ∈ Ihx0:x ≠ 0hmx:-x ∈ Ihpos:∃ y ∈ I, 0 < ya:ℤhmin:∀ (z : ℤ), z ∈ I ∧ 0 < z → a ≤ zhaI:a ∈ Iha:0 < a⊢ Ideal.span {a} ≤ I -- „Die Inklusion (a) ⊆ I ist klar.“
      rw [Ideal.span_le,neg.refine_2I:Ideal ℤhI:¬I = ⊥x:ℤhxI:x ∈ Ihx0:x ≠ 0hmx:-x ∈ Ihpos:∃ y ∈ I, 0 < ya:ℤhmin:∀ (z : ℤ), z ∈ I ∧ 0 < z → a ≤ zhaI:a ∈ Iha:0 < a⊢ {a} ⊆ ↑I Set.singleton_subset_iffneg.refine_2I:Ideal ℤhI:¬I = ⊥x:ℤhxI:x ∈ Ihx0:x ≠ 0hmx:-x ∈ Ihpos:∃ y ∈ I, 0 < ya:ℤhmin:∀ (z : ℤ), z ∈ I ∧ 0 < z → a ≤ zhaI:a ∈ Iha:0 < a⊢ a ∈ ↑I]neg.refine_2I:Ideal ℤhI:¬I = ⊥x:ℤhxI:x ∈ Ihx0:x ≠ 0hmx:-x ∈ Ihpos:∃ y ∈ I, 0 < ya:ℤhmin:∀ (z : ℤ), z ∈ I ∧ 0 < z → a ≤ zhaI:a ∈ Iha:0 < a⊢ a ∈ ↑I
      exact haIAll goals completed! 🐙

3.3. Bemerkungen🔗

In Mathlib ist IsPrincipalIdealRing ℤ eine Instanz: ℤ ist ein euklidischer Ring, und EuclideanDomain.to_principal_ideal_domain führt genau unser Argument für beliebige euklidische Ringe. Damit ist auch der zweite Satz des Skript-Abschnitts abgedeckt: K[x] ist euklidisch (Division mit Rest, wobei der Grad die Rolle des Betrags übernimmt), also ein Hauptidealring. Auch der Hilbertsche Basissatz aus diesem Kapitel steht in Mathlib: Polynomial.isNoetherianRing.

3.4. Übungsaufgabe🔗

Das Beispiel „Triviale Ideale“ des Skripts:

Wenn R ein Körper und I \subset R ein Ideal ist und a \in I \setminus \{0\}, dann ist auch jedes andere Körperelement in I. Sei nämlich irgendein Element r \in R gegeben. Nach Definition ist r = (r \cdot a^{-1}) \cdot a \in I. Also ist I = R.

Übersetzen Sie dieses Argument: Öffnen Sie AlgebraInLean/Ideals.lean und ersetzen Sie das sorry durch einen Beweis. Tipp: Die Taktik field_simp räumt Brüche auf; sie benutzt dabei die Hypothese ha0 automatisch.

theorem declaration uses `sorry`ideal_im_koerper {K : Type*} [Field K]
    (I : Ideal K) {a : K} (haI : a ∈ I) (ha0 : a ≠ 0)
    (r : K) : r ∈ I := byK:Type u_1inst✝:Field KI:Ideal Ka:KhaI:a ∈ Iha0:a ≠ 0r:K⊢ r ∈ I
  sorryAll goals completed! 🐙