chore(RingTheory/Ideal): add new file Ideal.IsPrincipal

Mathlib.lean

@@ -3476,6 +3476,7 @@ import Mathlib.RingTheory.Ideal.Colon
 import Mathlib.RingTheory.Ideal.Cotangent
 import Mathlib.RingTheory.Ideal.IdempotentFG
 import Mathlib.RingTheory.Ideal.IsPrimary
+import Mathlib.RingTheory.Ideal.IsPrincipal
 import Mathlib.RingTheory.Ideal.LocalRing
 import Mathlib.RingTheory.Ideal.Maps
 import Mathlib.RingTheory.Ideal.MinimalPrime

Mathlib/RingTheory/Ideal/Basic.lean

@@ -5,8 +5,8 @@
 -/
 import Mathlib.Tactic.FinCases
 import Mathlib.Data.Nat.Choose.Sum
 import Mathlib.LinearAlgebra.Finsupp
 import Mathlib.Algebra.Field.IsField
 
 #align_import ring_theory.ideal.basic from "leanprover-community/mathlib"@"dc6c365e751e34d100e80fe6e314c3c3e0fd2988"
 
@@ -172,20 +172,6 @@
   Submodule.mem_span_insert
 #align ideal.mem_span_insert Ideal.mem_span_insert
 
-theorem mem_span_singleton' {x y : α} : x ∈ span ({y} : Set α) ↔ ∃ a, a * y = x :=
-  Submodule.mem_span_singleton
-#align ideal.mem_span_singleton' Ideal.mem_span_singleton'
-
-theorem span_singleton_le_iff_mem {x : α} : span {x} ≤ I ↔ x ∈ I :=
-  Submodule.span_singleton_le_iff_mem _ _
-#align ideal.span_singleton_le_iff_mem Ideal.span_singleton_le_iff_mem
-
-theorem span_singleton_mul_left_unit {a : α} (h2 : IsUnit a) (x : α) :
-    span ({a * x} : Set α) = span {x} := by
-  apply le_antisymm <;> rw [span_singleton_le_iff_mem, mem_span_singleton']
-  exacts [⟨a, rfl⟩, ⟨_, h2.unit.inv_mul_cancel_left x⟩]
-#align ideal.span_singleton_mul_left_unit Ideal.span_singleton_mul_left_unit
-
 theorem span_insert (x) (s : Set α) : span (insert x s) = span ({x} : Set α) ⊔ span s :=
   Submodule.span_insert x s
 #align ideal.span_insert Ideal.span_insert
@@ -199,13 +185,6 @@
   Submodule.span_singleton_eq_bot
 #align ideal.span_singleton_eq_bot Ideal.span_singleton_eq_bot
 
-theorem span_singleton_ne_top {α : Type*} [CommSemiring α] {x : α} (hx : ¬IsUnit x) :
-    Ideal.span ({x} : Set α) ≠ ⊤ :=
-  (Ideal.ne_top_iff_one _).mpr fun h1 =>
-    let ⟨y, hy⟩ := Ideal.mem_span_singleton'.mp h1
-    hx ⟨⟨x, y, mul_comm y x ▸ hy, hy⟩, rfl⟩
-#align ideal.span_singleton_ne_top Ideal.span_singleton_ne_top
-
 @[simp]
 theorem span_zero : span (0 : Set α) = ⊥ := by rw [← Set.singleton_zero, span_singleton_eq_bot]
 #align ideal.span_zero Ideal.span_zero
@@ -220,17 +199,6 @@
   exact ⟨Submodule.mem_span_finite_of_mem_span, fun ⟨s', h₁, h₂⟩ => span_mono h₁ h₂⟩
 #align ideal.span_eq_top_iff_finite Ideal.span_eq_top_iff_finite
 
-theorem mem_span_singleton_sup {S : Type*} [CommSemiring S] {x y : S} {I : Ideal S} :
-    x ∈ Ideal.span {y} ⊔ I ↔ ∃ a : S, ∃ b ∈ I, a * y + b = x := by
-  rw [Submodule.mem_sup]
-  constructor
-  · rintro ⟨ya, hya, b, hb, rfl⟩
-    obtain ⟨a, rfl⟩ := mem_span_singleton'.mp hya
-    exact ⟨a, b, hb, rfl⟩
-  · rintro ⟨a, b, hb, rfl⟩
-    exact ⟨a * y, Ideal.mem_span_singleton'.mpr ⟨a, rfl⟩, b, hb, rfl⟩
-#align ideal.mem_span_singleton_sup Ideal.mem_span_singleton_sup
-
 /-- The ideal generated by an arbitrary binary relation.
 -/
 def ofRel (r : α → α → Prop) : Ideal α :=
@@ -499,57 +467,6 @@
   mul_comm y x ▸ unit_mul_mem_iff_mem I hy
 #align ideal.mul_unit_mem_iff_mem Ideal.mul_unit_mem_iff_mem
 
-theorem mem_span_singleton {x y : α} : x ∈ span ({y} : Set α) ↔ y ∣ x :=
-  mem_span_singleton'.trans <| exists_congr fun _ => by rw [eq_comm, mul_comm]
-#align ideal.mem_span_singleton Ideal.mem_span_singleton
-
-theorem mem_span_singleton_self (x : α) : x ∈ span ({x} : Set α) :=
-  mem_span_singleton.mpr dvd_rfl
-#align ideal.mem_span_singleton_self Ideal.mem_span_singleton_self
-
-theorem span_singleton_le_span_singleton {x y : α} :
-    span ({x} : Set α) ≤ span ({y} : Set α) ↔ y ∣ x :=
-  span_le.trans <| singleton_subset_iff.trans mem_span_singleton
-#align ideal.span_singleton_le_span_singleton Ideal.span_singleton_le_span_singleton
-
-theorem span_singleton_eq_span_singleton {α : Type u} [CommRing α] [IsDomain α] {x y : α} :
-    span ({x} : Set α) = span ({y} : Set α) ↔ Associated x y := by
-  rw [← dvd_dvd_iff_associated, le_antisymm_iff, and_comm]
-  apply and_congr <;> rw [span_singleton_le_span_singleton]
-#align ideal.span_singleton_eq_span_singleton Ideal.span_singleton_eq_span_singleton
-
-/-- The equivalence between `Associates R` and the principal ideals of `R` defined by sending the
-class of `x` to the principal ideal generated by `x`. -/
-noncomputable def associatesEquivIsPrincipal (R : Type*) [CommRing R] [IsDomain R] :
-    Associates R ≃ {I : Ideal R // Submodule.IsPrincipal I} := by
-  refine Equiv.ofBijective (fun x ↦ ⟨Ideal.span {Quot.out x}, ⟨Quot.out x, rfl⟩⟩)
-    ⟨fun  _ _ h ↦ ?_, fun ⟨I, hI⟩ ↦ ?_⟩
-  · rw [Subtype.mk_eq_mk, span_singleton_eq_span_singleton] at h
-    exact Quotient.out_equiv_out.mp h
-  · obtain ⟨x, hx⟩ := hI
-    refine ⟨⟦x⟧, ?_⟩
-    rw [Subtype.mk_eq_mk, hx, submodule_span_eq, span_singleton_eq_span_singleton]
-    exact Associates.mk_quot_out x
-
-@[simp]
-theorem associatesEquivIsPrincipal_apply (R : Type*) [CommRing R] [IsDomain R] (x : R) :
-    associatesEquivIsPrincipal R ⟦x⟧ = Ideal.span {x} := by
-  rw [associatesEquivIsPrincipal, Equiv.ofBijective_apply, span_singleton_eq_span_singleton]
-  exact Associates.mk_quot_out x
-
-theorem span_singleton_mul_right_unit {a : α} (h2 : IsUnit a) (x : α) :
-    span ({x * a} : Set α) = span {x} := by rw [mul_comm, span_singleton_mul_left_unit h2]
-#align ideal.span_singleton_mul_right_unit Ideal.span_singleton_mul_right_unit
-
-@[simp]
-theorem span_singleton_eq_top {x} : span ({x} : Set α) = ⊤ ↔ IsUnit x := by
-  rw [isUnit_iff_dvd_one, ← span_singleton_le_span_singleton, span_singleton_one, eq_top_iff]
-#align ideal.span_singleton_eq_top Ideal.span_singleton_eq_top
-
-theorem span_singleton_prime {p : α} (hp : p ≠ 0) : IsPrime (span ({p} : Set α)) ↔ Prime p := by
-  simp [isPrime_iff, Prime, span_singleton_eq_top, hp, mem_span_singleton]
-#align ideal.span_singleton_prime Ideal.span_singleton_prime
-
 theorem IsMaximal.isPrime {I : Ideal α} (H : I.IsMaximal) : I.IsPrime :=
   ⟨H.1.1, @fun x y hxy =>
     or_iff_not_imp_left.2 fun hx => by
@@ -570,20 +487,6 @@
   @IsMaximal.isPrime _ _ _
 #align ideal.is_maximal.is_prime' Ideal.IsMaximal.isPrime'
 
-theorem span_singleton_lt_span_singleton [IsDomain α] {x y : α} :
-    span ({x} : Set α) < span ({y} : Set α) ↔ DvdNotUnit y x := by
-  rw [lt_iff_le_not_le, span_singleton_le_span_singleton, span_singleton_le_span_singleton,
-    dvd_and_not_dvd_iff]
-#align ideal.span_singleton_lt_span_singleton Ideal.span_singleton_lt_span_singleton
-
-theorem factors_decreasing [IsDomain α] (b₁ b₂ : α) (h₁ : b₁ ≠ 0) (h₂ : ¬IsUnit b₂) :
-    span ({b₁ * b₂} : Set α) < span {b₁} :=
-  lt_of_le_not_le
-    (Ideal.span_le.2 <| singleton_subset_iff.2 <| Ideal.mem_span_singleton.2 ⟨b₂, rfl⟩) fun h =>
-    h₂ <| isUnit_of_dvd_one <|
-        (mul_dvd_mul_iff_left h₁).1 <| by rwa [mul_one, ← Ideal.span_singleton_le_span_singleton]
-#align ideal.factors_decreasing Ideal.factors_decreasing
-
 variable (b)
 
 theorem mul_mem_right (h : a ∈ I) : a * b ∈ I :=
@@ -669,55 +572,6 @@
     Finset.coe_image, Finset.val_toFinset] using pow_multiset_sum_mem_span_pow (s.1.map f) n
 #align ideal.sum_pow_mem_span_pow Ideal.sum_pow_mem_span_pow
 
-theorem span_pow_eq_top (s : Set α) (hs : span s = ⊤) (n : ℕ) :
-    span ((fun (x : α) => x ^ n) '' s) = ⊤ := by
-  rw [eq_top_iff_one]
-  cases' n with n
-  · obtain rfl | ⟨x, hx⟩ := eq_empty_or_nonempty s
-    · rw [Set.image_empty, hs]
-      trivial
-    · exact subset_span ⟨_, hx, pow_zero _⟩
-  rw [eq_top_iff_one, span, Finsupp.mem_span_iff_total] at hs
-  rcases hs with ⟨f, hf⟩
-  have hf : (f.support.sum fun a => f a * a) = 1 := hf -- Porting note: was `change ... at hf`
-  have := sum_pow_mem_span_pow f.support (fun a => f a * a) n
-  rw [hf, one_pow] at this
-  refine' span_le.mpr _ this
-  rintro _ hx
-  simp_rw [Set.mem_image] at hx
-  rcases hx with ⟨x, _, rfl⟩
-  have : span ({(x:α) ^ (n + 1)} : Set α) ≤ span ((fun x : α => x ^ (n + 1)) '' s) := by
-    rw [span_le, Set.singleton_subset_iff]
-    exact subset_span ⟨x, x.prop, rfl⟩
-  refine this ?_
-  rw [mul_pow, mem_span_singleton]
-  exact ⟨f x ^ (n + 1), mul_comm _ _⟩
-#align ideal.span_pow_eq_top Ideal.span_pow_eq_top
-
-lemma isPrime_of_maximally_disjoint (I : Ideal α)
-    (S : Submonoid α)
-    (disjoint : Disjoint (I : Set α) S)
-    (maximally_disjoint : ∀ (J : Ideal α), I < J → ¬ Disjoint (J : Set α) S) :
-    I.IsPrime where
-  ne_top' := by
-    rintro rfl
-    have : 1 ∈ (S : Set α) := S.one_mem
-    aesop
-  mem_or_mem' {x y} hxy := by
-    by_contra! rid
-    have hx := maximally_disjoint (I ⊔ span {x}) (Submodule.lt_sup_iff_not_mem.mpr rid.1)
-    have hy := maximally_disjoint (I ⊔ span {y}) (Submodule.lt_sup_iff_not_mem.mpr rid.2)
-    simp only [Set.not_disjoint_iff, mem_inter_iff, SetLike.mem_coe, Submodule.mem_sup,
-      mem_span_singleton] at hx hy
-    obtain ⟨s₁, ⟨i₁, hi₁, ⟨_, ⟨r₁, rfl⟩, hr₁⟩⟩, hs₁⟩ := hx
-    obtain ⟨s₂, ⟨i₂, hi₂, ⟨_, ⟨r₂, rfl⟩, hr₂⟩⟩, hs₂⟩ := hy
-    refine disjoint.ne_of_mem
-      (I.add_mem (I.mul_mem_left (i₁ + x * r₁) hi₂) <| I.add_mem (I.mul_mem_right (y * r₂) hi₁) <|
-        I.mul_mem_right (r₁ * r₂) hxy)
-      (S.mul_mem hs₁ hs₂) ?_
-    rw [← hr₁, ← hr₂]
-    ring
-
 end Ideal
 
 end CommSemiring
@@ -748,13 +602,6 @@
   Submodule.mem_span_insert'
 #align ideal.mem_span_insert' Ideal.mem_span_insert'
 
-@[simp]
-theorem span_singleton_neg (x : α) : (span {-x} : Ideal α) = span {x} := by
-  ext
-  simp only [mem_span_singleton']
-  exact ⟨fun ⟨y, h⟩ => ⟨-y, h ▸ neg_mul_comm y x⟩, fun ⟨y, h⟩ => ⟨-y, h ▸ neg_mul_neg y x⟩⟩
-#align ideal.span_singleton_neg Ideal.span_singleton_neg
-
 end Ideal
 
 end Ring
@@ -836,74 +683,8 @@
   exact ⟨x, hx, not_unit⟩
 #align ring.exists_not_is_unit_of_not_is_field Ring.exists_not_isUnit_of_not_isField
 
-theorem not_isField_iff_exists_ideal_bot_lt_and_lt_top [Nontrivial R] :
-    ¬IsField R ↔ ∃ I : Ideal R, ⊥ < I ∧ I < ⊤ := by
-  constructor
-  · intro h
-    obtain ⟨x, nz, nu⟩ := exists_not_isUnit_of_not_isField h
-    use Ideal.span {x}
-    rw [bot_lt_iff_ne_bot, lt_top_iff_ne_top]
-    exact ⟨mt Ideal.span_singleton_eq_bot.mp nz, mt Ideal.span_singleton_eq_top.mp nu⟩
-  · rintro ⟨I, bot_lt, lt_top⟩ hf
-    obtain ⟨x, mem, ne_zero⟩ := SetLike.exists_of_lt bot_lt
-    rw [Submodule.mem_bot] at ne_zero
-    obtain ⟨y, hy⟩ := hf.mul_inv_cancel ne_zero
-    rw [lt_top_iff_ne_top, Ne, Ideal.eq_top_iff_one, ← hy] at lt_top
-    exact lt_top (I.mul_mem_right _ mem)
-#align ring.not_is_field_iff_exists_ideal_bot_lt_and_lt_top Ring.not_isField_iff_exists_ideal_bot_lt_and_lt_top
-
-theorem not_isField_iff_exists_prime [Nontrivial R] :
-    ¬IsField R ↔ ∃ p : Ideal R, p ≠ ⊥ ∧ p.IsPrime :=
-  not_isField_iff_exists_ideal_bot_lt_and_lt_top.trans
-    ⟨fun ⟨I, bot_lt, lt_top⟩ =>
-      let ⟨p, hp, le_p⟩ := I.exists_le_maximal (lt_top_iff_ne_top.mp lt_top)
-      ⟨p, bot_lt_iff_ne_bot.mp (lt_of_lt_of_le bot_lt le_p), hp.isPrime⟩,
-      fun ⟨p, ne_bot, Prime⟩ => ⟨p, bot_lt_iff_ne_bot.mpr ne_bot, lt_top_iff_ne_top.mpr Prime.1⟩⟩
-#align ring.not_is_field_iff_exists_prime Ring.not_isField_iff_exists_prime
-
-/-- Also see `Ideal.isSimpleOrder` for the forward direction as an instance when `R` is a
-division (semi)ring.
-
-This result actually holds for all division semirings, but we lack the predicate to state it. -/
-theorem isField_iff_isSimpleOrder_ideal : IsField R ↔ IsSimpleOrder (Ideal R) := by
-  cases subsingleton_or_nontrivial R
-  · exact
-      ⟨fun h => (not_isField_of_subsingleton _ h).elim, fun h =>
-        (false_of_nontrivial_of_subsingleton <| Ideal R).elim⟩
-  rw [← not_iff_not, Ring.not_isField_iff_exists_ideal_bot_lt_and_lt_top, ← not_iff_not]
-  push_neg
-  simp_rw [lt_top_iff_ne_top, bot_lt_iff_ne_bot, ← or_iff_not_imp_left, not_ne_iff]
-  exact ⟨fun h => ⟨h⟩, fun h => h.2⟩
-#align ring.is_field_iff_is_simple_order_ideal Ring.isField_iff_isSimpleOrder_ideal
-
-/-- When a ring is not a field, the maximal ideals are nontrivial. -/
-theorem ne_bot_of_isMaximal_of_not_isField [Nontrivial R] {M : Ideal R} (max : M.IsMaximal)
-    (not_field : ¬IsField R) : M ≠ ⊥ := by
-  rintro h
-  rw [h] at max
-  rcases max with ⟨⟨_h1, h2⟩⟩
-  obtain ⟨I, hIbot, hItop⟩ := not_isField_iff_exists_ideal_bot_lt_and_lt_top.mp not_field
-  exact ne_of_lt hItop (h2 I hIbot)
-#align ring.ne_bot_of_is_maximal_of_not_is_field Ring.ne_bot_of_isMaximal_of_not_isField
-
 end Ring
 
-namespace Ideal
-
-variable {R : Type u} [CommSemiring R] [Nontrivial R]
-
-theorem bot_lt_of_maximal (M : Ideal R) [hm : M.IsMaximal] (non_field : ¬IsField R) : ⊥ < M := by
-  rcases Ring.not_isField_iff_exists_ideal_bot_lt_and_lt_top.1 non_field with ⟨I, Ibot, Itop⟩
-  constructor; · simp
-  intro mle
-  apply lt_irrefl (⊤ : Ideal R)
-  have : M = ⊥ := eq_bot_iff.mpr mle
-  rw [← this] at Ibot
-  rwa [hm.1.2 I Ibot] at Itop
-#align ideal.bot_lt_of_maximal Ideal.bot_lt_of_maximal
-
-end Ideal
-
 variable {a b : α}
 
 /-- The set of non-invertible elements of a monoid. -/
@@ -936,16 +717,3 @@
 theorem coe_subset_nonunits [Semiring α] {I : Ideal α} (h : I ≠ ⊤) : (I : Set α) ⊆ nonunits α :=
   fun _x hx hu => h <| I.eq_top_of_isUnit_mem hx hu
 #align coe_subset_nonunits coe_subset_nonunits
-
-theorem exists_max_ideal_of_mem_nonunits [CommSemiring α] (h : a ∈ nonunits α) :
-    ∃ I : Ideal α, I.IsMaximal ∧ a ∈ I := by
-  have : Ideal.span ({a} : Set α) ≠ ⊤ := by
-    intro H
-    rw [Ideal.span_singleton_eq_top] at H
-    contradiction
-  rcases Ideal.exists_le_maximal _ this with ⟨I, Imax, H⟩
-  use I, Imax
-  apply H
-  apply Ideal.subset_span
-  exact Set.mem_singleton a
-#align exists_max_ideal_of_mem_nonunits exists_max_ideal_of_mem_nonunits

Mathlib/RingTheory/Ideal/Basis.lean

@@ -5,7 +5,7 @@ Authors: Anne Baanen
 -/
 import Mathlib.Algebra.Algebra.Bilinear
 import Mathlib.LinearAlgebra.Basis
-import Mathlib.RingTheory.Ideal.Basic
+import Mathlib.RingTheory.Ideal.IsPrincipal
 
 #align_import ring_theory.ideal.operations from "leanprover-community/mathlib"@"e7f0ddbf65bd7181a85edb74b64bdc35ba4bdc74"