NYLL
Module

Ideal_exists_mem_and_mem_and_radical_span_singleton_isPrime.lean

Nyll.AlgebraicCurves.Foundations.CommutativeAlgebra.Ideal_exists_mem_and_mem_and_radical_span_singleton_isPrime
20 declarations indexed from sourceView source ↗

Module documentation

Ideal exists mem and mem and radical span singleton is Prime

Imports4
Imported by2

Declarations

theorem

sub_mem_span_of_algHom

L33 ↗
AlgebraicCurves.Foundations.CommutativeAlgebra.Proofs.Ideal_exists_mem_and_mem_and_radical_span_singleton_isPrime.P2mIrredHyp.sub_mem_span_of_algHom
Source context 6 commands

Surrounding namespaces, section variables, and local commands at this declaration.

section ProofImplementation
namespace AlgebraicCurves.Foundations.CommutativeAlgebra.Proofs
namespace Ideal_exists_mem_and_mem_and_radical_span_singleton_isPrime
universe u v
open MvPolynomial
namespace P2mIrredHyp
Lean source · full declaration
theorem sub_mem_span_of_algHom {R : Type*} [CommRing R] {σ : Type*}
    (φ : MvPolynomial σ R →ₐ[R] MvPolynomial σ R) (p : MvPolynomial σ R) :
    p - φ p ∈ Ideal.span (Set.range fun i : σ => (X i - φ (X i) : MvPolynomial σ R)) := by
  set I := Ideal.span (Set.range fun i : σ => (X i - φ (X i) : MvPolynomial σ R))
  induction p using MvPolynomial.induction_on with
  | C a =>
    have : φ (C a) = C a := by
      rw [← MvPolynomial.algebraMap_eq, AlgHom.commutes]
    rw [this, sub_self]; exact I.zero_mem
  | add p q hp hq =>
    have : p + q - φ (p + q) = (p - φ p) + (q - φ q) := by rw [map_add]; ring
    rw [this]; exact I.add_mem hp hq
  | mul_X p i hp =>
    have : p * X i - φ (p * X i) = (p - φ p) * X i + φ p * (X i - φ (X i)) := by
      rw [map_mul]; ring
    rw [this]
    exact I.add_mem (I.mul_mem_right _ hp) (I.mul_mem_left _ (Ideal.subset_span ⟨i, rfl⟩))
theorem

mem_span_X_sub_C_of_aeval_eq_zero

L51 ↗
AlgebraicCurves.Foundations.CommutativeAlgebra.Proofs.Ideal_exists_mem_and_mem_and_radical_span_singleton_isPrime.P2mIrredHyp.mem_span_X_sub_C_of_aeval_eq_zero
Source context 6 commands

Surrounding namespaces, section variables, and local commands at this declaration.

section ProofImplementation
namespace AlgebraicCurves.Foundations.CommutativeAlgebra.Proofs
namespace Ideal_exists_mem_and_mem_and_radical_span_singleton_isPrime
universe u v
open MvPolynomial
namespace P2mIrredHyp
Lean source · full declaration
theorem mem_span_X_sub_C_of_aeval_eq_zero {R : Type*} [CommRing R] {σ : Type*} (a : σ → R)
    {p : MvPolynomial σ R} (hp : MvPolynomial.aeval a p = 0) :
    p ∈ Ideal.span (Set.range fun i : σ => (X i - C (a i) : MvPolynomial σ R)) := by
  let φ : MvPolynomial σ R →ₐ[R] MvPolynomial σ R := MvPolynomial.aeval fun i => C (a i)
  have hφX : ∀ i, φ (X i) = C (a i) := fun i => by simp [φ]
  have hφ : ∀ q : MvPolynomial σ R, φ q = C (MvPolynomial.aeval a q) := by
    intro q
    have h1 : φ = (IsScalarTower.toAlgHom R R (MvPolynomial σ R)).comp (MvPolynomial.aeval a) := by
      apply MvPolynomial.algHom_ext
      intro i
      simp [φ]
    rw [h1]; rfl
  have hmem := sub_mem_span_of_algHom φ p
  simp only [hφX] at hmem
  rwa [hφ p, hp, map_zero, sub_zero] at hmem
theorem

exists_sub_algebraMap_mem

L67 ↗
AlgebraicCurves.Foundations.CommutativeAlgebra.Proofs.Ideal_exists_mem_and_mem_and_radical_span_singleton_isPrime.P2mIrredHyp.exists_sub_algebraMap_mem
Source context 6 commands

Surrounding namespaces, section variables, and local commands at this declaration.

section ProofImplementation
namespace AlgebraicCurves.Foundations.CommutativeAlgebra.Proofs
namespace Ideal_exists_mem_and_mem_and_radical_span_singleton_isPrime
universe u v
open MvPolynomial
namespace P2mIrredHyp
Lean source · statement
theorem exists_sub_algebraMap_mem (k : Type u) [Field k] [IsAlgClosed k] {A : Type v} [CommRing A]
    [Algebra k A] [Algebra.FiniteType k A] (m : Ideal A) [hm : m.IsMaximal] (t : A) :
    ∃ c : k, t - algebraMap k A c ∈ m
theorem

mem_bot_of_isSeparable

L79 ↗
AlgebraicCurves.Foundations.CommutativeAlgebra.Proofs.Ideal_exists_mem_and_mem_and_radical_span_singleton_isPrime.P2mIrredHyp.mem_bot_of_isSeparable
Source context 6 commands

Surrounding namespaces, section variables, and local commands at this declaration.

section ProofImplementation
namespace AlgebraicCurves.Foundations.CommutativeAlgebra.Proofs
namespace Ideal_exists_mem_and_mem_and_radical_span_singleton_isPrime
universe u v
open MvPolynomial
namespace P2mIrredHyp
Lean source · statement
theorem mem_bot_of_isSeparable (k : Type u) [Field k] [IsAlgClosed k] {K : Type*} [Field K]
    [Algebra k K] (θ : K) (hθ : IsSeparable k θ) : θ ∈ (⊥ : IntermediateField k K)
theorem

isSeparable_transport

L87 ↗
AlgebraicCurves.Foundations.CommutativeAlgebra.Proofs.Ideal_exists_mem_and_mem_and_radical_span_singleton_isPrime.P2mIrredHyp.isSeparable_transport
Source context 6 commands

Surrounding namespaces, section variables, and local commands at this declaration.

section ProofImplementation
namespace AlgebraicCurves.Foundations.CommutativeAlgebra.Proofs
namespace Ideal_exists_mem_and_mem_and_radical_span_singleton_isPrime
universe u v
open MvPolynomial
namespace P2mIrredHyp
Lean source · statement
theorem isSeparable_transport {R₁ R₂ L L' : Type*} [Field R₁] [Field R₂] [Field L] [Field L']
    [Algebra R₁ L] [Algebra R₂ L'] (e : R₁ ≃+* R₂) (σ : L →+* L')
    (he : ∀ r, algebraMap R₂ L' (e r) = σ (algebraMap R₁ L r)) {y : L}
    (h : IsSeparable R₁ y) : IsSeparable R₂ (σ y)
theorem

fg_top_fractionRing

L100 ↗
AlgebraicCurves.Foundations.CommutativeAlgebra.Proofs.Ideal_exists_mem_and_mem_and_radical_span_singleton_isPrime.P2mIrredHyp.fg_top_fractionRing
Source context 6 commands

Surrounding namespaces, section variables, and local commands at this declaration.

section ProofImplementation
namespace AlgebraicCurves.Foundations.CommutativeAlgebra.Proofs
namespace Ideal_exists_mem_and_mem_and_radical_span_singleton_isPrime
universe u v
open MvPolynomial
namespace P2mIrredHyp
Lean source · statement
theorem fg_top_fractionRing (k : Type u) [Field k] (B : Type*) [CommRing B] [IsDomain B]
    [Algebra k B] [Algebra.FiniteType k B] :
    (⊤ : IntermediateField k (FractionRing B)).FG
theorem

adjoin_algebra_adjoin

L120 ↗
AlgebraicCurves.Foundations.CommutativeAlgebra.Proofs.Ideal_exists_mem_and_mem_and_radical_span_singleton_isPrime.P2mIrredHyp.adjoin_algebra_adjoin
Source context 6 commands

Surrounding namespaces, section variables, and local commands at this declaration.

section ProofImplementation
namespace AlgebraicCurves.Foundations.CommutativeAlgebra.Proofs
namespace Ideal_exists_mem_and_mem_and_radical_span_singleton_isPrime
universe u v
open MvPolynomial
namespace P2mIrredHyp
Lean source · statement
theorem adjoin_algebra_adjoin (k : Type u) [Field k] {L : Type*} [Field L] [Algebra k L]
    (S : Set L) :
    IntermediateField.adjoin k (↑(Algebra.adjoin k S) : Set L) = IntermediateField.adjoin k S
theorem

transcendental_add_mul

L128 ↗
AlgebraicCurves.Foundations.CommutativeAlgebra.Proofs.Ideal_exists_mem_and_mem_and_radical_span_singleton_isPrime.P2mIrredHyp.transcendental_add_mul
Source context 6 commands

Surrounding namespaces, section variables, and local commands at this declaration.

section ProofImplementation
namespace AlgebraicCurves.Foundations.CommutativeAlgebra.Proofs
namespace Ideal_exists_mem_and_mem_and_radical_span_singleton_isPrime
universe u v
open MvPolynomial
namespace P2mIrredHyp
Lean source · statement
theorem transcendental_add_mul {S L : Type*} [CommRing S] [IsDomain S] [Field L] [Algebra S L]
    {v : L} (hv : Transcendental S v) (c d : S) (hd : algebraMap S L d ≠ 0) :
    Transcendental S (algebraMap S L c + v * algebraMap S L d)
theorem

two_le_height_of_mem_of_mem

L139 ↗
AlgebraicCurves.Foundations.CommutativeAlgebra.Proofs.Ideal_exists_mem_and_mem_and_radical_span_singleton_isPrime.P2mIrredHyp.two_le_height_of_mem_of_mem
Source context 6 commands

Surrounding namespaces, section variables, and local commands at this declaration.

section ProofImplementation
namespace AlgebraicCurves.Foundations.CommutativeAlgebra.Proofs
namespace Ideal_exists_mem_and_mem_and_radical_span_singleton_isPrime
universe u v
open MvPolynomial
namespace P2mIrredHyp
Lean source · statement
theorem two_le_height_of_mem_of_mem (k : Type u) [Field k] {σ : Type*}
    {i j : σ} (hij : i ≠ j) (a b : k) (q : Ideal (MvPolynomial σ k)) [q.IsPrime]
    (hi : (X i - C a : MvPolynomial σ k) ∈ q) (hj : (X j - C b : MvPolynomial σ k) ∈ q) :
    (2 : ℕ∞) ≤ q.height
theorem

ringKrullDim_le_of_isIntegral

L217 ↗
AlgebraicCurves.Foundations.CommutativeAlgebra.Proofs.Ideal_exists_mem_and_mem_and_radical_span_singleton_isPrime.P2mIrredHyp.ringKrullDim_le_of_isIntegral
Source context 6 commands

Surrounding namespaces, section variables, and local commands at this declaration.

section ProofImplementation
namespace AlgebraicCurves.Foundations.CommutativeAlgebra.Proofs
namespace Ideal_exists_mem_and_mem_and_radical_span_singleton_isPrime
universe u v
open MvPolynomial
namespace P2mIrredHyp
Lean source · statement
theorem ringKrullDim_le_of_isIntegral {R S : Type*} [CommRing R] [CommRing S]
    [Algebra R S] [Algebra.IsIntegral R S] : ringKrullDim S ≤ ringKrullDim R
theorem

ringKrullDim_mvPolynomial_fin

L228 ↗
AlgebraicCurves.Foundations.CommutativeAlgebra.Proofs.Ideal_exists_mem_and_mem_and_radical_span_singleton_isPrime.P2mIrredHyp.ringKrullDim_mvPolynomial_fin
Source context 6 commands

Surrounding namespaces, section variables, and local commands at this declaration.

section ProofImplementation
namespace AlgebraicCurves.Foundations.CommutativeAlgebra.Proofs
namespace Ideal_exists_mem_and_mem_and_radical_span_singleton_isPrime
universe u v
open MvPolynomial
namespace P2mIrredHyp
Lean source · statement
theorem ringKrullDim_mvPolynomial_fin (k : Type u) [Field k] (s : ℕ) :
    ringKrullDim (MvPolynomial (Fin s) k) = s
theorem

exists_noether_two_le

L234 ↗
AlgebraicCurves.Foundations.CommutativeAlgebra.Proofs.Ideal_exists_mem_and_mem_and_radical_span_singleton_isPrime.P2mIrredHyp.exists_noether_two_le
Source context 6 commands

Surrounding namespaces, section variables, and local commands at this declaration.

section ProofImplementation
namespace AlgebraicCurves.Foundations.CommutativeAlgebra.Proofs
namespace Ideal_exists_mem_and_mem_and_radical_span_singleton_isPrime
universe u v
open MvPolynomial
namespace P2mIrredHyp
Lean source · statement
theorem exists_noether_two_le (k : Type u) [Field k] {A : Type v} [CommRing A] [IsDomain A]
    [Algebra k A] [Algebra.FiniteType k A] (hA : 2 ≤ ringKrullDim A) :
    ∃ s : ℕ, ∃ g : MvPolynomial (Fin s) k →ₐ[k] A, Function.Injective g ∧ g.Finite ∧ 2 ≤ s
theorem

not_mem_of_mem_minimalPrimes

L252 ↗
AlgebraicCurves.Foundations.CommutativeAlgebra.Proofs.Ideal_exists_mem_and_mem_and_radical_span_singleton_isPrime.P2mIrredHyp.not_mem_of_mem_minimalPrimes
Source context 8 commands

Surrounding namespaces, section variables, and local commands at this declaration.

section ProofImplementation
namespace AlgebraicCurves.Foundations.CommutativeAlgebra.Proofs
namespace Ideal_exists_mem_and_mem_and_radical_span_singleton_isPrime
universe u v
open MvPolynomial
namespace P2mIrredHyp
section AvoidMinimalPrimes
variable (k : Type u) [Field k] {A : Type v} [CommRing A] [IsDomain A] [Algebra k A]
  [Algebra.FiniteType k A]
Lean source · statement
theorem not_mem_of_mem_minimalPrimes {s : ℕ} (g : MvPolynomial (Fin s) k →ₐ[k] A)
    (hg : Function.Injective g) (hfin : g.Finite) {i j : Fin s} (hij : i ≠ j) (a a' b b' : k)
    (Q : Ideal A)
    (hQ : Q ∈ (Ideal.span {(g (X i) - algebraMap k A a) * (g (X i) - algebraMap k A
      a')}).minimalPrimes) :
    (g (X j) - algebraMap k A b) * (g (X j) - algebraMap k A b') ∉ Q
def

rhoVec

L305 ↗
AlgebraicCurves.Foundations.CommutativeAlgebra.Proofs.Ideal_exists_mem_and_mem_and_radical_span_singleton_isPrime.P2mIrredHyp.rhoVec
Documentation

The three polynomial coordinates given by u * X₀ + w * X₁, X₀, and X₁.

Source context 13 commands

Surrounding namespaces, section variables, and local commands at this declaration.

section ProofImplementation
namespace AlgebraicCurves.Foundations.CommutativeAlgebra.Proofs
namespace Ideal_exists_mem_and_mem_and_radical_span_singleton_isPrime
universe u v
open MvPolynomial
namespace P2mIrredHyp
section Fields
variable (k : Type u) [Field k] [IsAlgClosed k] (A' : Type v) [CommRing A'] [IsDomain A']
  [Algebra k A'] [Algebra.FiniteType k A'] (u w : A')
local notation "Kf" => FractionRing A'
local notation "C2" => MvPolynomial (Fin 2) A'
local notation "KX" => MvPolynomial (Fin 2) (FractionRing A')
local notation "Ω" => FractionRing (MvPolynomial (Fin 2) (FractionRing A'))
local notation "R3" => MvPolynomial (Fin 3) k
Lean source · statement
def rhoVec : Fin 3 → C2
def

rho

L308 ↗
AlgebraicCurves.Foundations.CommutativeAlgebra.Proofs.Ideal_exists_mem_and_mem_and_radical_span_singleton_isPrime.P2mIrredHyp.rho
Documentation

The algebra map evaluating three variables at the coordinates of rhoVec.

Source context 13 commands

Surrounding namespaces, section variables, and local commands at this declaration.

section ProofImplementation
namespace AlgebraicCurves.Foundations.CommutativeAlgebra.Proofs
namespace Ideal_exists_mem_and_mem_and_radical_span_singleton_isPrime
universe u v
open MvPolynomial
namespace P2mIrredHyp
section Fields
variable (k : Type u) [Field k] [IsAlgClosed k] (A' : Type v) [CommRing A'] [IsDomain A']
  [Algebra k A'] [Algebra.FiniteType k A'] (u w : A')
local notation "Kf" => FractionRing A'
local notation "C2" => MvPolynomial (Fin 2) A'
local notation "KX" => MvPolynomial (Fin 2) (FractionRing A')
local notation "Ω" => FractionRing (MvPolynomial (Fin 2) (FractionRing A'))
local notation "R3" => MvPolynomial (Fin 3) k
Lean source · statement
def rho : R3 →ₐ[k] C2
theorem

exists_ne_zero_forall_fibre

L310 ↗
AlgebraicCurves.Foundations.CommutativeAlgebra.Proofs.Ideal_exists_mem_and_mem_and_radical_span_singleton_isPrime.P2mIrredHyp.exists_ne_zero_forall_fibre
Source context 13 commands

Surrounding namespaces, section variables, and local commands at this declaration.

section ProofImplementation
namespace AlgebraicCurves.Foundations.CommutativeAlgebra.Proofs
namespace Ideal_exists_mem_and_mem_and_radical_span_singleton_isPrime
universe u v
open MvPolynomial
namespace P2mIrredHyp
section Fields
variable (k : Type u) [Field k] [IsAlgClosed k] (A' : Type v) [CommRing A'] [IsDomain A']
  [Algebra k A'] [Algebra.FiniteType k A'] (u w : A')
local notation "Kf" => FractionRing A'
local notation "C2" => MvPolynomial (Fin 2) A'
local notation "KX" => MvPolynomial (Fin 2) (FractionRing A')
local notation "Ω" => FractionRing (MvPolynomial (Fin 2) (FractionRing A'))
local notation "R3" => MvPolynomial (Fin 3) k
Lean source · statement
theorem exists_ne_zero_forall_fibre
    (huw : AlgebraicIndependent k ![algebraMap A' Kf u, algebraMap A' Kf w]) :
    ∃ r : R3, r ≠ 0 ∧ ∀ n : Ideal R3, n.IsMaximal → r ∉ n →
      n.map (rho k A' u w).toRingHom = ⊤ ∨ (n.map (rho k A' u w).toRingHom).radical.IsPrime
theorem

algebraicIndependent_ratio

L499 ↗
AlgebraicCurves.Foundations.CommutativeAlgebra.Proofs.Ideal_exists_mem_and_mem_and_radical_span_singleton_isPrime.P2mIrredHyp.algebraicIndependent_ratio
Source context 6 commands

Surrounding namespaces, section variables, and local commands at this declaration.

section ProofImplementation
namespace AlgebraicCurves.Foundations.CommutativeAlgebra.Proofs
namespace Ideal_exists_mem_and_mem_and_radical_span_singleton_isPrime
universe u v
open MvPolynomial
namespace P2mIrredHyp
Lean source · statement
theorem algebraicIndependent_ratio (k : Type u) [Field k] {L : Type*} [Field L] [Algebra k L]
    (τ : Fin 2 → L) (hτ : AlgebraicIndependent k τ) (a₁ b₁ a₂ b₂ : k) (v : L)
    (hv : v * ((τ 0 - algebraMap k L a₁) * (τ 0 - algebraMap k L b₁)) =
      (τ 1 - algebraMap k L a₂) * (τ 1 - algebraMap k L b₂)) :
    AlgebraicIndependent k ![τ 1, v]
theorem

radical_span_isPrime_of_away

L562 ↗
AlgebraicCurves.Foundations.CommutativeAlgebra.Proofs.Ideal_exists_mem_and_mem_and_radical_span_singleton_isPrime.P2mIrredHyp.radical_span_isPrime_of_away
Source context 6 commands

Surrounding namespaces, section variables, and local commands at this declaration.

section ProofImplementation
namespace AlgebraicCurves.Foundations.CommutativeAlgebra.Proofs
namespace Ideal_exists_mem_and_mem_and_radical_span_singleton_isPrime
universe u v
open MvPolynomial
namespace P2mIrredHyp
Lean source · statement
theorem radical_span_isPrime_of_away {A : Type v} [CommRing A] (f₀ F : A)
    (A' : Type*) [CommRing A'] [Algebra A A'] [IsLocalization.Away f₀ A']
    (hex : ((Ideal.span {F}).minimalPrimes).Nonempty)
    (havoid : ∀ P ∈ (Ideal.span {F}).minimalPrimes, f₀ ∉ P)
    (h : (Ideal.span {F}).map (algebraMap A A') = ⊤ ∨
      (((Ideal.span {F}).map (algebraMap A A')).radical).IsPrime) :
    (Ideal.span {F}).radical.IsPrime
theorem

irredHyp

L606 ↗
AlgebraicCurves.Foundations.CommutativeAlgebra.Proofs.Ideal_exists_mem_and_mem_and_radical_span_singleton_isPrime.P2mIrredHyp.irredHyp
Source context 6 commands

Surrounding namespaces, section variables, and local commands at this declaration.

section ProofImplementation
namespace AlgebraicCurves.Foundations.CommutativeAlgebra.Proofs
namespace Ideal_exists_mem_and_mem_and_radical_span_singleton_isPrime
universe u v
open MvPolynomial
namespace P2mIrredHyp
Lean source · statement
theorem irredHyp
    (k : Type u) [Field k] [IsAlgClosed k] {A : Type v} [CommRing A] [IsDomain A] [Algebra k A]
    [Algebra.FiniteType k A] (hA : 2 ≤ ringKrullDim A)
    (m₀ m₁ : Ideal A) [m₀.IsMaximal] [m₁.IsMaximal] (_hne : m₀ ≠ m₁) :
    ∃ f : A, f ∈ m₀ ∧ f ∈ m₁ ∧ f ≠ 0 ∧ (Ideal.span {f}).radical.IsPrime
theorem

exists_mem_and_mem_and_radical_span_singleton_isPrime

L834 ↗
Ideal.exists_mem_and_mem_and_radical_span_singleton_isPrime
Source context 5 commands

Surrounding namespaces, section variables, and local commands at this declaration.

section ProofImplementation
namespace AlgebraicCurves.Foundations.CommutativeAlgebra.Proofs
namespace Ideal_exists_mem_and_mem_and_radical_span_singleton_isPrime
universe u v
open MvPolynomial
Lean source · statement
theorem _root_.Ideal.exists_mem_and_mem_and_radical_span_singleton_isPrime
    (k : Type u) [Field k] [IsAlgClosed k] {A : Type v} [CommRing A] [IsDomain A] [Algebra k A]
    [Algebra.FiniteType k A] (hA : 2 ≤ ringKrullDim A)
    (m₀ m₁ : Ideal A) [m₀.IsMaximal] [m₁.IsMaximal] (hne : m₀ ≠ m₁) :
    ∃ f : A, f ∈ m₀ ∧ f ∈ m₁ ∧ f ≠ 0 ∧ (Ideal.span {f}).radical.IsPrime

Statements and documentation are read from the Lean source at the revision shown. Source entries are not a measure of mathematical completeness.