Module

PuncturedSpectrumHypersurfaceIntersectionReduction.lean

Nyll.EtaleFundamentalGroups.Purity.PuncturedSpectrumHypersurfaceIntersectionReduction

3 declarations indexed from sourceView source ↗

Module documentation

Ideal-theoretic reduction for punctured hypersurface connectedness

A finite partition of the irreducible components of a principal hypersurface gives two finite families of minimal primes. If every component from one family meets every component from the other only at the closed point, the radical of the sum of the two component intersections is the maximal ideal. This is the exact ideal-theoretic configuration to which the missing complete-local intersection inequality applies.

Imports1

Nyll.EtaleFundamentalGroups.Purity.PuncturedSpectrumHypersurfaceComponents

Imported by2

theorem

exists_mem_le_of_sInf_le_prime_of_finite

L30 ↗

AlgebraicGeometry.FiniteEtale.exists_mem_le_of_sInf_le_prime_of_finite

Documentation

A prime containing the intersection of a finite family of ideals contains one member of that family.

Source context 4 commands

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

noncomputable section
open IsLocalRing
namespace AlgebraicGeometry.FiniteEtale
universe u

Lean source · statement

theorem exists_mem_le_of_sInf_le_prime_of_finite
    {C : Type u} [CommRing C]
    {S : Set (Ideal C)} (hS : S.Finite)
    {P : Ideal C} [P.IsPrime] (h : sInf S ≤ P) :
    ∃ I ∈ S, I ≤ P

theorem

radical_sup_sInf_eq_maximalIdeal_of_cross_zeroLocus

L44 ↗

AlgebraicGeometry.FiniteEtale.radical_sup_sInf_eq_maximalIdeal_of_cross_zeroLocus

Documentation

If two nonempty finite families of prime ideals have all cross-component intersections supported at the closed point, then the radical of the sum of their intersections is the maximal ideal.

Source context 4 commands

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

noncomputable section
open IsLocalRing
namespace AlgebraicGeometry.FiniteEtale
universe u

Lean source · statement

theorem radical_sup_sInf_eq_maximalIdeal_of_cross_zeroLocus
    {C : Type u} [CommRing C] [IsLocalRing C]
    {S T : Set (Ideal C)}
    (hSfinite : S.Finite) (hTfinite : T.Finite)
    (hSnonempty : S.Nonempty) (hTnonempty : T.Nonempty)
    (hSprime : ∀ P ∈ S, P.IsPrime)
    (hTprime : ∀ Q ∈ T, Q.IsPrime)
    (hcross : ∀ P ∈ S, ∀ Q ∈ T,
      PrimeSpectrum.zeroLocus P ∩ PrimeSpectrum.zeroLocus Q ⊆
        ({closedPoint C} : Set (PrimeSpectrum C))) :
    (sInf S ⊔ sInf T).radical = maximalIdeal C

theorem

radical_sup_sInf_eq_maximalIdeal_of_minimalPrime_cross_zeroLocus

L85 ↗

AlgebraicGeometry.FiniteEtale.radical_sup_sInf_eq_maximalIdeal_of_minimalPrime_cross_zeroLocus

Documentation

The previous reduction specialized to two finite subfamilies of the minimal primes of an ideal in a Noetherian local ring.

Source context 4 commands

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

noncomputable section
open IsLocalRing
namespace AlgebraicGeometry.FiniteEtale
universe u

Lean source · statement

theorem radical_sup_sInf_eq_maximalIdeal_of_minimalPrime_cross_zeroLocus
    {C : Type u} [CommRing C] [IsLocalRing C] [IsNoetherianRing C]
    (I : Ideal C) {S T : Set (Ideal C)}
    (hS : S ⊆ I.minimalPrimes) (hT : T ⊆ I.minimalPrimes)
    (hSnonempty : S.Nonempty) (hTnonempty : T.Nonempty)
    (hcross : ∀ P ∈ S, ∀ Q ∈ T,
      PrimeSpectrum.zeroLocus P ∩ PrimeSpectrum.zeroLocus Q ⊆
        ({closedPoint C} : Set (PrimeSpectrum C))) :
    (sInf S ⊔ sInf T).radical = maximalIdeal C

Module documentation

Ideal-theoretic reduction for punctured hypersurface connectedness

Declarations

exists_mem_le_of_sInf_le_prime_of_finite

radical_sup_sInf_eq_maximalIdeal_of_cross_zeroLocus

radical_sup_sInf_eq_maximalIdeal_of_minimalPrime_cross_zeroLocus