zero_prime_not_maximaltheoremProved here from basic factspropext, Classical.choice, Quot.sound
zero_prime_not_maximalLean 4Proved here from basic factsFormally verified
/-- **A prime ideal need not be maximal.** In `ℤ` the zero ideal is prime (because `ℤ` is anintegral domain: `ab = 0` forces `a = 0` or `b = 0`), but it is not maximal, since`(0) ⊊ (2) ⊊ ℤ`. In a PID every *non-zero* prime ideal is maximal, so `(0)` is the onlyexception in `ℤ`. -/theorem zero_prime_not_maximal : (⊥ : Ideal ℤ).IsPrime ∧ ¬ (⊥ : Ideal ℤ).IsMaximal := by refine ⟨Ideal.isPrime_bot, fun hmax => ?_⟩ -- `(2)` lies strictly between `(0)` and `ℤ` have h2 : (⊥ : Ideal ℤ) < Ideal.span {2} := by rw [bot_lt_iff_ne_bot, Ne, Ideal.span_singleton_eq_bot] norm_num have htop : Ideal.span {(2 : ℤ)} = ⊤ := hmax.1.2 _ h2 rw [Ideal.span_singleton_eq_top] at htop exact absurd (Int.isUnit_iff.mp htop) (by norm_num)
hilbert_basistheoremApplies a library theorempropext, Classical.choice, Quot.sound
hilbert_basisLean 4Applies a library theoremFormally verified
/-- **Hilbert's basis theorem**: if `R` is Noetherian, so is `R[X]`. Mathlib:`Polynomial.isNoetherianRing`, proved via ideals of leading coefficients, as in the lesson. -/theorem hilbert_basis (R : Type*) [CommRing R] [IsNoetherianRing R] : IsNoetherianRing (Polynomial R) := Polynomial.isNoetherianRing
infinitely_many_variables_not_noetheriantheoremProved here from basic factspropext, Classical.choice, Quot.sound
infinitely_many_variables_not_noetherianLean 4Proved here from basic factsFormally verified
/-- **`k[x₀, x₁, x₂, …]` is not Noetherian.** Human proof: let `Iₙ = (x₀, …, xₙ₋₁)`. The chain`I₀ ⊆ I₁ ⊆ ⋯` is increasing; if it stabilised at `n`, then `xₙ ∈ Iₙ₊₁ = Iₙ`. But the evaluationhomomorphism sending `xᵢ ↦ 0` for `i < n` and `xᵢ ↦ 1` otherwise kills `Iₙ` and sends `xₙ ↦ 1`. -/theorem infinitely_many_variables_not_noetherian (k : Type*) [Field k] : ¬ IsNoetherianRing (MvPolynomial ℕ k) := by intro hnoeth let I : ℕ →o Ideal (MvPolynomial ℕ k) := ⟨fun n => Ideal.span (MvPolynomial.X '' {i | i < n}), fun a b hab => Ideal.span_mono (Set.image_mono fun i (hi : i < a) => lt_of_lt_of_le hi hab)⟩ obtain ⟨n, hn⟩ := (monotone_stabilizes_iff_noetherian).mpr hnoeth I -- evaluation killing the first `n` variables let φ : MvPolynomial ℕ k →+* k := MvPolynomial.eval fun i => if i < n then 0 else 1 have hker : I n ≤ RingHom.ker φ := by show Ideal.span _ ≤ _ rw [Ideal.span_le] rintro _ ⟨i, hi, rfl⟩ simp only [SetLike.mem_coe, RingHom.mem_ker, φ, MvPolynomial.eval_X] exact (ite_eq_left_iff.mpr fun h => absurd hi h) have hmem : (MvPolynomial.X n : MvPolynomial ℕ k) ∈ I n := by rw [hn (n + 1) (Nat.le_succ n)] exact Ideal.subset_span ⟨n, Nat.lt_succ_self n, rfl⟩ have h1 : φ (MvPolynomial.X n) = 0 := hker hmem simp [φ] at h1
nakayamatheoremProved here from basic factspropext, Classical.choice, Quot.sound
nakayamaLean 4Proved here from basic factsFormally verified
/-- **Nakayama's lemma.** Let `N` be a finitely generated module and `I` an ideal contained inthe Jacobson radical. If `N ⊆ I N` then `N = 0`. Human proof: the determinant trick(Cayley–Hamilton applied to a matrix expressing the generators in terms of themselves withcoefficients in `I`) gives `r ∈ R` with `r - 1 ∈ I` and `r N = 0`. Since `r - 1` lies in theJacobson radical, `r = 1 + (r - 1)` is a unit, so `N = r⁻¹ r N = 0`. (Mathlib's version is`Submodule.eq_bot_of_le_smul_of_le_jacobson_bot`.) -/theorem nakayama {R M : Type*} [CommRing R] [AddCommGroup M] [Module R M] (I : Ideal R) (N : Submodule R M) (hN : N.FG) (hIN : N ≤ I • N) (hjac : I ≤ Ideal.jacobson ⊥) : N = ⊥ := by obtain ⟨r, hr, hrN⟩ := Submodule.exists_sub_one_mem_and_smul_eq_zero_of_fg_of_le_smul I N hN hIN -- `r = 1 + (r - 1)` is a unit, because `r - 1` lies in the Jacobson radical have hunit : IsUnit r := by have h := (Ideal.mem_jacobson_bot.mp (hjac hr)) 1 simpa using h rw [eq_bot_iff] intro n hn have h0 : r • n = 0 := hrN n hn rw [Submodule.mem_bot] calc n = (1 : R) • n := (one_smul R n).symm _ = ((hunit.unit⁻¹ : Rˣ) * r : R) • n := by rw [hunit.val_inv_mul] _ = (hunit.unit⁻¹ : Rˣ) • (r • n) := mul_smul _ _ _ _ = 0 := by rw [h0, smul_zero]
nakayama_librarytheoremApplies a library theorempropext, Classical.choice, Quot.sound
nakayama_libraryLean 4Applies a library theoremFormally verified
/-- **Nakayama's lemma, Mathlib's version** (`Submodule.eq_bot_of_le_smul_of_le_jacobson_bot`). For alocal ring, `I = 𝔪` lies in the Jacobson radical, giving the familiar form: if `M` is finitelygenerated and `𝔪 M = M` then `M = 0`. -/theorem nakayama_library {R M : Type*} [CommRing R] [AddCommGroup M] [Module R M] (I : Ideal R) (N : Submodule R M) (hN : N.FG) (hIN : N ≤ I • N) (hjac : I ≤ Ideal.jacobson ⊥) : N = ⊥ := Submodule.eq_bot_of_le_smul_of_le_jacobson_bot I N hN hIN hjac
localization_primesdefApplies a library theorempropext, Classical.choice, Quot.sound
localization_primesLean 4Applies a library theoremFormally verified
/-- **Primes of a localisation.** If `S` is the localisation of `R` at the complement of a prime`𝔭`, the prime ideals of `S` correspond, preserving inclusion, to the prime ideals of `R`contained in `𝔭`. Mathlib: `IsLocalization.AtPrime.orderIsoOfPrime`. In particular `R_𝔭` has aunique maximal ideal: it is local. -/noncomputable def localization_primes {R : Type*} [CommRing R] (p : Ideal R) [p.IsPrime] (S : Type*) [CommRing S] [Algebra R S] [IsLocalization.AtPrime S p] : { q : Ideal S // q.IsPrime } ≃o { q : Ideal R // q.IsPrime ∧ q ≤ p } := IsLocalization.AtPrime.orderIsoOfPrime S p
x_sq_not_radicaltheoremProved here from basic factspropext, Classical.choice, Quot.sound
x_sq_not_radicalLean 4Proved here from basic factsFormally verified
/-- **`(x²)` is not a radical ideal of `k[x]`.** Its zero set is the single point `0`, whosevanishing ideal is `(x)`; and indeed `x ∉ (x²)` although `x² ∈ (x²)`. So the Nullstellensatzmust return the radical `√I`, not `I`. Proof: `x² ∣ x` would force the coefficient of `x` in`x` to vanish. -/theorem x_sq_not_radical (k : Type*) [Field k] : (Polynomial.X : Polynomial k) ^ 2 ∈ Ideal.span {Polynomial.X ^ 2} ∧ (Polynomial.X : Polynomial k) ∉ Ideal.span {Polynomial.X ^ 2} := by refine ⟨Ideal.subset_span rfl, fun h => ?_⟩ rw [Ideal.mem_span_singleton, Polynomial.X_pow_dvd_iff] at h have := h 1 (by norm_num) simp at this
nullstellensatztheoremApplies a library theorempropext, Classical.choice, Quot.sound
nullstellensatzLean 4Applies a library theoremFormally verified
/-- **Hilbert's Nullstellensatz** (strong form): over an algebraically closed field `k`, apolynomial vanishes on the zero set of an ideal `I ⊆ k[x₁, …, xₙ]` exactly when some power of itlies in `I`: `I(V(I)) = √I`. Mathlib: `MvPolynomial.vanishingIdeal_zeroLocus_eq_radical`. -/theorem nullstellensatz {k : Type*} [Field k] [IsAlgClosed k] {n : ℕ} (I : Ideal (MvPolynomial (Fin n) k)) : MvPolynomial.vanishingIdeal k (MvPolynomial.zeroLocus k I) = I.radical := MvPolynomial.vanishingIdeal_zeroLocus_eq_radical I
/-- The zero ideal of `ℤ` is prime but not maximal.Hint: `Ideal.isPrime_bot` gives primality. For non-maximality, show `⊥ < Ideal.span {2}`(`bot_lt_iff_ne_bot`, `Ideal.span_singleton_eq_bot`), deduce `Ideal.span {2} = ⊤` frommaximality (`hmax.1.2`), and contradict `Ideal.span_singleton_eq_top` with `Int.isUnit_iff`. -/theorem zero_prime_not_maximal : (⊥ : Ideal ℤ).IsPrime ∧ ¬ (⊥ : Ideal ℤ).IsMaximal := by sorry
Show the compiled solution
zero_prime_not_maximalLean 4Proved here from basic factsFormally verified
/-- **A prime ideal need not be maximal.** In `ℤ` the zero ideal is prime (because `ℤ` is anintegral domain: `ab = 0` forces `a = 0` or `b = 0`), but it is not maximal, since`(0) ⊊ (2) ⊊ ℤ`. In a PID every *non-zero* prime ideal is maximal, so `(0)` is the onlyexception in `ℤ`. -/theorem zero_prime_not_maximal : (⊥ : Ideal ℤ).IsPrime ∧ ¬ (⊥ : Ideal ℤ).IsMaximal := by refine ⟨Ideal.isPrime_bot, fun hmax => ?_⟩ -- `(2)` lies strictly between `(0)` and `ℤ` have h2 : (⊥ : Ideal ℤ) < Ideal.span {2} := by rw [bot_lt_iff_ne_bot, Ne, Ideal.span_singleton_eq_bot] norm_num have htop : Ideal.span {(2 : ℤ)} = ⊤ := hmax.1.2 _ h2 rw [Ideal.span_singleton_eq_top] at htop exact absurd (Int.isUnit_iff.mp htop) (by norm_num)
/-- `x² ∈ (x²)` but `x ∉ (x²)` in `k[x]`.Hint: `Ideal.mem_span_singleton` turns membership into divisibility, and`Polynomial.X_pow_dvd_iff` turns `X ^ 2 ∣ p` into the vanishing of the coefficients of `p` indegrees `0` and `1`. -/theorem x_sq_not_radical (k : Type*) [Field k] : (Polynomial.X : Polynomial k) ^ 2 ∈ Ideal.span {Polynomial.X ^ 2} ∧ (Polynomial.X : Polynomial k) ∉ Ideal.span {Polynomial.X ^ 2} := by sorry
Show the compiled solution
x_sq_not_radicalLean 4Proved here from basic factsFormally verified
/-- **`(x²)` is not a radical ideal of `k[x]`.** Its zero set is the single point `0`, whosevanishing ideal is `(x)`; and indeed `x ∉ (x²)` although `x² ∈ (x²)`. So the Nullstellensatzmust return the radical `√I`, not `I`. Proof: `x² ∣ x` would force the coefficient of `x` in`x` to vanish. -/theorem x_sq_not_radical (k : Type*) [Field k] : (Polynomial.X : Polynomial k) ^ 2 ∈ Ideal.span {Polynomial.X ^ 2} ∧ (Polynomial.X : Polynomial k) ∉ Ideal.span {Polynomial.X ^ 2} := by refine ⟨Ideal.subset_span rfl, fun h => ?_⟩ rw [Ideal.mem_span_singleton, Polynomial.X_pow_dvd_iff] at h have := h 1 (by norm_num) simp at this