NYLL
Module

PuncturedSpectrumCompleteLocalDomainAlgebra.lean

Nyll.EtaleFundamentalGroups.Purity.PuncturedSpectrumCompleteLocalDomainAlgebra
4 declarations indexed from sourceView source ↗

Module documentation

Direct algebra on the complete-local connectedness frontier

This file extracts the consequences of the two radical component ideals produced by a disconnected punctured principal hypersurface. In a domain, the principal element is nonzero. The component ideals also determine two nonmaximal minimal primes over the principal ideal; Krull's principal ideal theorem bounds both of their heights by one.

Imports2
Imported by2

Declarations

theorem

ne_zero_of_radical_componentIntersection

L30 ↗
AlgebraicGeometry.FiniteEtale.ne_zero_of_radical_componentIntersection
Documentation

In a local domain, a radical component decomposition of a principal ideal into two nonmaximal pieces forces the principal element to be nonzero.

Source context 4 commands

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

noncomputable section
open IsLocalRing TopologicalSpace
namespace AlgebraicGeometry.FiniteEtale
universe u
Lean source · statement
theorem ne_zero_of_radical_componentIntersection
    {C : Type u} [CommRing C] [IsDomain C] [IsLocalRing C]
    {x : C} {a b : Ideal C}
    (haRadical : a.IsRadical) (hbRadical : b.IsRadical)
    (haMax : a ≠ maximalIdeal C) (hbMax : b ≠ maximalIdeal C)
    (hinf : a ⊓ b = (Ideal.span {x}).radical)
    (hsup : (a ⊔ b).radical = maximalIdeal C) :
    x ≠ 0
theorem

exists_nonmaximal_minimalPrime_pair_of_radical_componentIntersection

L54 ↗
AlgebraicGeometry.FiniteEtale.exists_nonmaximal_minimalPrime_pair_of_radical_componentIntersection
Documentation

Two radical nonmaximal components whose intersection is I.radical produce nonmaximal minimal primes over I, one containing each component. Their sum still has maximal radical.

Source context 4 commands

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

noncomputable section
open IsLocalRing TopologicalSpace
namespace AlgebraicGeometry.FiniteEtale
universe u
Lean source · statement
theorem exists_nonmaximal_minimalPrime_pair_of_radical_componentIntersection
    {C : Type u} [CommRing C] [IsLocalRing C]
    {I a b : Ideal C}
    (haRadical : a.IsRadical) (hbRadical : b.IsRadical)
    (haMax : a ≠ maximalIdeal C) (hbMax : b ≠ maximalIdeal C)
    (hinf : a ⊓ b = I.radical)
    (hsup : (a ⊔ b).radical = maximalIdeal C) :
    ∃ P Q : Ideal C,
      P ∈ I.minimalPrimes ∧ Q ∈ I.minimalPrimes ∧
      a ≤ P ∧ b ≤ Q ∧
      P ≠ maximalIdeal C ∧ Q ≠ maximalIdeal C ∧
      (P ⊔ Q).radical = maximalIdeal C
theorem

exists_height_le_one_minimalPrime_pair_of_radical_componentIntersection

L146 ↗
AlgebraicGeometry.FiniteEtale.exists_height_le_one_minimalPrime_pair_of_radical_componentIntersection
Documentation

For a principal intersection in a Noetherian local domain, the two minimal primes supplied by the radical components both have height at most one. The principal element is simultaneously certified to be nonzero.

Source context 4 commands

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

noncomputable section
open IsLocalRing TopologicalSpace
namespace AlgebraicGeometry.FiniteEtale
universe u
Lean source · statement
theorem exists_height_le_one_minimalPrime_pair_of_radical_componentIntersection
    {C : Type u} [CommRing C] [IsDomain C] [IsLocalRing C]
    [IsNoetherianRing C]
    {x : C} {a b : Ideal C}
    (haRadical : a.IsRadical) (hbRadical : b.IsRadical)
    (haMax : a ≠ maximalIdeal C) (hbMax : b ≠ maximalIdeal C)
    (hinf : a ⊓ b = (Ideal.span {x}).radical)
    (hsup : (a ⊔ b).radical = maximalIdeal C) :
    x ≠ 0 ∧
      ∃ P Q : Ideal C,
        P ∈ (Ideal.span {x}).minimalPrimes ∧
        Q ∈ (Ideal.span {x}).minimalPrimes ∧
        a ≤ P ∧ b ≤ Q ∧
        P ≠ maximalIdeal C ∧ Q ≠ maximalIdeal C ∧
        P.height ≤ 1 ∧ Q.height ≤ 1 ∧
        (P ⊔ Q).radical = maximalIdeal C
theorem

exists_height_le_one_minimalPrime_pair_of_not_connectedSpace

L174 ↗
AlgebraicGeometry.FiniteEtale.exists_height_le_one_minimalPrime_pair_of_not_connectedSpace
Documentation

A disconnected punctured principal hypersurface in a Noetherian local domain supplies a nonzero equation and a pair of nonmaximal height-at-most-one minimal primes whose sum has maximal radical.

Source context 4 commands

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

noncomputable section
open IsLocalRing TopologicalSpace
namespace AlgebraicGeometry.FiniteEtale
universe u
Lean source · full declaration
theorem exists_height_le_one_minimalPrime_pair_of_not_connectedSpace
    {C : Type u} [CommRing C] [IsDomain C] [IsLocalRing C]
    [IsNoetherianRing C]
    (hdim : ((3 : ℕ∞) : WithBot ℕ∞) ≤ ringKrullDim C)
    (x : C) (hx : x ∈ maximalIdeal C) :
    letI : Nontrivial (C ⧸ Ideal.span {x}) :=
      Ideal.Quotient.nontrivial_iff.mpr <|
        ne_top_of_le_ne_top (maximalIdeal.isMaximal C).ne_top <|
          (maximalIdeal C).span_singleton_le_iff_mem.mpr hx
    letI : IsLocalRing (C ⧸ Ideal.span {x}) :=
      IsLocalRing.of_surjective' (Ideal.Quotient.mk (Ideal.span {x}))
        Ideal.Quotient.mk_surjective
    ¬ ConnectedSpace (Scheme.puncturedSpectrum (C ⧸ Ideal.span {x})) →
      x ≠ 0 ∧
        ∃ P Q : Ideal C,
          P ∈ (Ideal.span {x}).minimalPrimes ∧
          Q ∈ (Ideal.span {x}).minimalPrimes ∧
          P ≠ maximalIdeal C ∧ Q ≠ maximalIdeal C ∧
          P.height ≤ 1 ∧ Q.height ≤ 1 ∧
          (P ⊔ Q).radical = maximalIdeal C := by
  let D := C ⧸ Ideal.span {x}
  let : Nontrivial D :=
    Ideal.Quotient.nontrivial_iff.mpr <|
      ne_top_of_le_ne_top (maximalIdeal.isMaximal C).ne_top <|
        (maximalIdeal C).span_singleton_le_iff_mem.mpr hx
  let : IsLocalRing D :=
    IsLocalRing.of_surjective'
      (Ideal.Quotient.mk (Ideal.span {x})) Ideal.Quotient.mk_surjective
  intro hnot
  obtain ⟨a, b, _hxa, _hxb, _haTop, _hbTop, haMax, hbMax,
      haRadical, hbRadical, hinf, hsup⟩ :=
    exists_radical_nonmaximal_ambient_componentIntersectionIdeals_of_not_connectedSpace
      hdim x hx hnot
  obtain ⟨hx0, P, Q, hP, hQ, _haP, _hbQ, hPMax, hQMax,
      hPheight, hQheight, hPQ⟩ :=
    exists_height_le_one_minimalPrime_pair_of_radical_componentIntersection
      haRadical hbRadical haMax hbMax hinf hsup
  exact ⟨hx0, P, Q, hP, hQ, hPMax, hQMax, hPheight, hQheight, hPQ⟩

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