NYLL
Module

Ideal_exists_isPrime_le_and_le_and_ringKrullDim_quotient_eq_one.lean

Nyll.AlgebraicCurves.Foundations.CommutativeAlgebra.Ideal_exists_isPrime_le_and_le_and_ringKrullDim_quotient_eq_one
14 declarations indexed from sourceView source ↗

Module documentation

Ideal exists is Prime le and le and ring Krull Dim quotient eq one

Imports1
Imported by3

Declarations

lemma

exists_ltSeries_comap_eq_last

L30 ↗
AlgebraicCurves.Foundations.CommutativeAlgebra.Proofs.Ideal_exists_isPrime_le_and_le_and_ringKrullDim_quotient_eq_one.P2mBertiniHyp.exists_ltSeries_comap_eq_last
Source context 6 commands

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

section ProofImplementation
namespace AlgebraicCurves.Foundations.CommutativeAlgebra.Proofs
namespace Ideal_exists_isPrime_le_and_le_and_ringKrullDim_quotient_eq_one
universe u v
namespace P2mBertiniHyp
open _root_.Ideal _root_.Polynomial
Lean source · statement
lemma exists_ltSeries_comap_eq_last {R S : Type*} [CommRing R] [CommRing S]
    [Algebra R S] [Algebra.IsIntegral R S] (hinj : Function.Injective (algebraMap R S))
    (l : LTSeries (PrimeSpectrum R)) :
    ∃ L : LTSeries (PrimeSpectrum S), L.length = l.length ∧
      PrimeSpectrum.comap (algebraMap R S) L.last = l.last
theorem

ringKrullDim_eq_of_isIntegral_of_injective

L59 ↗
AlgebraicCurves.Foundations.CommutativeAlgebra.Proofs.Ideal_exists_isPrime_le_and_le_and_ringKrullDim_quotient_eq_one.P2mBertiniHyp.ringKrullDim_eq_of_isIntegral_of_injective
Source context 6 commands

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

section ProofImplementation
namespace AlgebraicCurves.Foundations.CommutativeAlgebra.Proofs
namespace Ideal_exists_isPrime_le_and_le_and_ringKrullDim_quotient_eq_one
universe u v
namespace P2mBertiniHyp
open _root_.Ideal _root_.Polynomial
Lean source · statement
theorem ringKrullDim_eq_of_isIntegral_of_injective {R S : Type*} [CommRing R] [CommRing S]
    [Algebra R S] [Algebra.IsIntegral R S] (hinj : Function.Injective (algebraMap R S)) :
    ringKrullDim R = ringKrullDim S
theorem

ringKrullDim_mvPolynomial_fin

L78 ↗
AlgebraicCurves.Foundations.CommutativeAlgebra.Proofs.Ideal_exists_isPrime_le_and_le_and_ringKrullDim_quotient_eq_one.P2mBertiniHyp.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_isPrime_le_and_le_and_ringKrullDim_quotient_eq_one
universe u v
namespace P2mBertiniHyp
open _root_.Ideal _root_.Polynomial
Lean source · statement
theorem ringKrullDim_mvPolynomial_fin (k : Type u) [Field k] (s : ℕ) :
    ringKrullDim (MvPolynomial (Fin s) k) = s
theorem

height_eq_of_isMaximal_mvPolynomial

L84 ↗
AlgebraicCurves.Foundations.CommutativeAlgebra.Proofs.Ideal_exists_isPrime_le_and_le_and_ringKrullDim_quotient_eq_one.P2mBertiniHyp.height_eq_of_isMaximal_mvPolynomial
Source context 6 commands

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

section ProofImplementation
namespace AlgebraicCurves.Foundations.CommutativeAlgebra.Proofs
namespace Ideal_exists_isPrime_le_and_le_and_ringKrullDim_quotient_eq_one
universe u v
namespace P2mBertiniHyp
open _root_.Ideal _root_.Polynomial
Lean source · statement
theorem height_eq_of_isMaximal_mvPolynomial (k : Type u) [Field k] :
    ∀ (n : ℕ) (M : Ideal (MvPolynomial (Fin n) k)), M.IsMaximal → M.height = n
theorem

height_eq_ringKrullDim_of_isMaximal

L115 ↗
AlgebraicCurves.Foundations.CommutativeAlgebra.Proofs.Ideal_exists_isPrime_le_and_le_and_ringKrullDim_quotient_eq_one.P2mBertiniHyp.height_eq_ringKrullDim_of_isMaximal
Source context 6 commands

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

section ProofImplementation
namespace AlgebraicCurves.Foundations.CommutativeAlgebra.Proofs
namespace Ideal_exists_isPrime_le_and_le_and_ringKrullDim_quotient_eq_one
universe u v
namespace P2mBertiniHyp
open _root_.Ideal _root_.Polynomial
Lean source · statement
theorem height_eq_ringKrullDim_of_isMaximal (k : Type u) {A : Type v} [Field k] [CommRing A]
    [IsDomain A] [Algebra k A] [Algebra.FiniteType k A] (m : Ideal A) [hm : m.IsMaximal] :
    (m.height : WithBot ℕ∞) = ringKrullDim A
theorem

ringKrullDim_quotient_radical

L137 ↗
AlgebraicCurves.Foundations.CommutativeAlgebra.Proofs.Ideal_exists_isPrime_le_and_le_and_ringKrullDim_quotient_eq_one.P2mBertiniHyp.ringKrullDim_quotient_radical
Source context 6 commands

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

section ProofImplementation
namespace AlgebraicCurves.Foundations.CommutativeAlgebra.Proofs
namespace Ideal_exists_isPrime_le_and_le_and_ringKrullDim_quotient_eq_one
universe u v
namespace P2mBertiniHyp
open _root_.Ideal _root_.Polynomial
Lean source · statement
theorem ringKrullDim_quotient_radical {A : Type v} [CommRing A] (I : Ideal A) :
    ringKrullDim (A ⧸ I.radical) = ringKrullDim (A ⧸ I)
theorem

ringKrullDim_quotient_radical_span_add_one

L141 ↗
AlgebraicCurves.Foundations.CommutativeAlgebra.Proofs.Ideal_exists_isPrime_le_and_le_and_ringKrullDim_quotient_eq_one.P2mBertiniHyp.ringKrullDim_quotient_radical_span_add_one
Source context 6 commands

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

section ProofImplementation
namespace AlgebraicCurves.Foundations.CommutativeAlgebra.Proofs
namespace Ideal_exists_isPrime_le_and_le_and_ringKrullDim_quotient_eq_one
universe u v
namespace P2mBertiniHyp
open _root_.Ideal _root_.Polynomial
Lean source · statement
theorem ringKrullDim_quotient_radical_span_add_one (k : Type u) {A : Type v} [Field k] [CommRing A]
    [IsDomain A] [Algebra k A] [Algebra.FiniteType k A] (m : Ideal A) [m.IsMaximal]
    {f : A} (hf : f ≠ 0) (hfm : f ∈ m) :
    ringKrullDim (A ⧸ (Ideal.span {f}).radical) + 1 = ringKrullDim A
theorem

exists_ringKrullDim_eq_natCast

L150 ↗
AlgebraicCurves.Foundations.CommutativeAlgebra.Proofs.Ideal_exists_isPrime_le_and_le_and_ringKrullDim_quotient_eq_one.P2mBertiniHyp.exists_ringKrullDim_eq_natCast
Source context 6 commands

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

section ProofImplementation
namespace AlgebraicCurves.Foundations.CommutativeAlgebra.Proofs
namespace Ideal_exists_isPrime_le_and_le_and_ringKrullDim_quotient_eq_one
universe u v
namespace P2mBertiniHyp
open _root_.Ideal _root_.Polynomial
Lean source · statement
theorem exists_ringKrullDim_eq_natCast (k : Type u) (A : Type v) [Field k] [CommRing A]
    [Nontrivial A] [Algebra k A] [Algebra.FiniteType k A] : ∃ n : ℕ, ringKrullDim A = n
theorem

exists_isMaximal_ne

L159 ↗
AlgebraicCurves.Foundations.CommutativeAlgebra.Proofs.Ideal_exists_isPrime_le_and_le_and_ringKrullDim_quotient_eq_one.P2mBertiniHyp.exists_isMaximal_ne
Source context 6 commands

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

section ProofImplementation
namespace AlgebraicCurves.Foundations.CommutativeAlgebra.Proofs
namespace Ideal_exists_isPrime_le_and_le_and_ringKrullDim_quotient_eq_one
universe u v
namespace P2mBertiniHyp
open _root_.Ideal _root_.Polynomial
Lean source · statement
theorem exists_isMaximal_ne (k : Type u) {A : Type v} [Field k] [CommRing A] [IsDomain A] [Algebra
  k A]
    [Algebra.FiniteType k A] (hA : 1 ≤ ringKrullDim A) (m : Ideal A) [hm : m.IsMaximal] :
    ∃ m' : Ideal A, m'.IsMaximal ∧ m' ≠ m
theorem

step

L180 ↗
AlgebraicCurves.Foundations.CommutativeAlgebra.Proofs.Ideal_exists_isPrime_le_and_le_and_ringKrullDim_quotient_eq_one.P2mBertiniHyp.step
Source context 8 commands

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

section ProofImplementation
namespace AlgebraicCurves.Foundations.CommutativeAlgebra.Proofs
namespace Ideal_exists_isPrime_le_and_le_and_ringKrullDim_quotient_eq_one
universe u v
namespace P2mBertiniHyp
open _root_.Ideal _root_.Polynomial
section Main
variable (k : Type u) [Field k] [IsAlgClosed k]
Lean source · statement
theorem step {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₁) :
    ∃ P : Ideal A, P.IsPrime ∧ P ≤ m₀ ∧ P ≤ m₁ ∧ ringKrullDim (A ⧸ P) + 1 = ringKrullDim A
theorem

comap_mk_le

L192 ↗
AlgebraicCurves.Foundations.CommutativeAlgebra.Proofs.Ideal_exists_isPrime_le_and_le_and_ringKrullDim_quotient_eq_one.P2mBertiniHyp.comap_mk_le
Source context 8 commands

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

section ProofImplementation
namespace AlgebraicCurves.Foundations.CommutativeAlgebra.Proofs
namespace Ideal_exists_isPrime_le_and_le_and_ringKrullDim_quotient_eq_one
universe u v
namespace P2mBertiniHyp
open _root_.Ideal _root_.Polynomial
section Main
variable (k : Type u) [Field k] [IsAlgClosed k]
Lean source · statement
theorem comap_mk_le {A : Type v} [CommRing A] {P' n : Ideal A} (h : P' ≤ n)
    {Q : Ideal (A ⧸ P')} (hQ : Q ≤ n.map (Ideal.Quotient.mk P')) :
    Q.comap (Ideal.Quotient.mk P') ≤ n
theorem

ringKrullDim_quotient_comap_mk

L204 ↗
AlgebraicCurves.Foundations.CommutativeAlgebra.Proofs.Ideal_exists_isPrime_le_and_le_and_ringKrullDim_quotient_eq_one.P2mBertiniHyp.ringKrullDim_quotient_comap_mk
Source context 8 commands

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

section ProofImplementation
namespace AlgebraicCurves.Foundations.CommutativeAlgebra.Proofs
namespace Ideal_exists_isPrime_le_and_le_and_ringKrullDim_quotient_eq_one
universe u v
namespace P2mBertiniHyp
open _root_.Ideal _root_.Polynomial
section Main
variable (k : Type u) [Field k] [IsAlgClosed k]
Lean source · statement
theorem ringKrullDim_quotient_comap_mk {A : Type v} [CommRing A] (P' : Ideal A)
    (Q : Ideal (A ⧸ P')) :
    ringKrullDim (A ⧸ Q.comap (Ideal.Quotient.mk P')) = ringKrullDim ((A ⧸ P') ⧸ Q)
theorem

main

L215 ↗
AlgebraicCurves.Foundations.CommutativeAlgebra.Proofs.Ideal_exists_isPrime_le_and_le_and_ringKrullDim_quotient_eq_one.P2mBertiniHyp.main
Source context 8 commands

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

section ProofImplementation
namespace AlgebraicCurves.Foundations.CommutativeAlgebra.Proofs
namespace Ideal_exists_isPrime_le_and_le_and_ringKrullDim_quotient_eq_one
universe u v
namespace P2mBertiniHyp
open _root_.Ideal _root_.Polynomial
section Main
variable (k : Type u) [Field k] [IsAlgClosed k]
Lean source · statement
theorem main : ∀ (n : ℕ) {A : Type v} [CommRing A] [IsDomain A] [Algebra k A] [Algebra.FiniteType k
  A],
    ringKrullDim A = n → 1 ≤ n → ∀ (m₀ m₁ : Ideal A) [m₀.IsMaximal] [m₁.IsMaximal],
      ∃ P : Ideal A, P.IsPrime ∧ P ≤ m₀ ∧ P ≤ m₁ ∧ ringKrullDim (A ⧸ P) = 1
theorem

exists_isPrime_le_and_le_and_ringKrullDim_quotient_eq_one

L267 ↗
Ideal.exists_isPrime_le_and_le_and_ringKrullDim_quotient_eq_one
Source context 4 commands

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

section ProofImplementation
namespace AlgebraicCurves.Foundations.CommutativeAlgebra.Proofs
namespace Ideal_exists_isPrime_le_and_le_and_ringKrullDim_quotient_eq_one
universe u v
Lean source · statement
theorem _root_.Ideal.exists_isPrime_le_and_le_and_ringKrullDim_quotient_eq_one
    (k : Type u) [Field k] [IsAlgClosed k] {A : Type v} [CommRing A] [IsDomain A] [Algebra k A]
    [Algebra.FiniteType k A] (hA : 1 ≤ ringKrullDim A)
    (m₀ m₁ : Ideal A) [m₀.IsMaximal] [m₁.IsMaximal] :
    ∃ P : Ideal A, P.IsPrime ∧ P ≤ m₀ ∧ P ≤ m₁ ∧ ringKrullDim (A ⧸ P) = 1

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