NYLL
Module

PuncturedSpectrumCompleteIntersectionInputs.lean

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

Module documentation

Power data from a disconnected punctured hypersurface

This file converts the ideal-theoretic separation attached to a disconnected punctured hypersurface into the two power containments used by complete-local intersection arguments.

Imports1
Imported by2

Declarations

theorem

exists_maximalIdeal_pow_le_of_radical_eq

L27 ↗
AlgebraicGeometry.FiniteEtale.exists_maximalIdeal_pow_le_of_radical_eq
Documentation

If the radical of an ideal is the maximal ideal of a Noetherian local ring, then a power of the maximal ideal is contained in it.

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_maximalIdeal_pow_le_of_radical_eq
    {C : Type u} [CommRing C] [IsLocalRing C] [IsNoetherianRing C]
    {I : Ideal C} (hI : I.radical = maximalIdeal C) :
    ∃ n : ℕ, (maximalIdeal C) ^ n ≤ I
theorem

exists_product_pow_le_of_inf_eq_radical

L37 ↗
AlgebraicGeometry.FiniteEtale.exists_product_pow_le_of_inf_eq_radical
Documentation

If the intersection of two ideals is the radical of I, then a power of their product is contained in I.

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_product_pow_le_of_inf_eq_radical
    {C : Type u} [CommRing C] [IsNoetherianRing C]
    {I a b : Ideal C} (hab : a ⊓ b = I.radical) :
    ∃ n : ℕ, (a * b) ^ n ≤ I
theorem

exists_radical_completeIntersectionPowerData_of_not_connectedSpace

L48 ↗
AlgebraicGeometry.FiniteEtale.exists_radical_completeIntersectionPowerData_of_not_connectedSpace
Documentation

Strengthened power data retaining that both component ideals are radical and nonmaximal.

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 · full declaration
theorem exists_radical_completeIntersectionPowerData_of_not_connectedSpace
    {C : Type u} [CommRing 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})) →
      ∃ a b : Ideal C, ∃ n k : ℕ,
        Ideal.span {x} ≤ a ∧ Ideal.span {x} ≤ b ∧
        a ≠ ⊤ ∧ b ≠ ⊤ ∧
        a ≠ maximalIdeal C ∧ b ≠ maximalIdeal C ∧
        a.IsRadical ∧ b.IsRadical ∧
        a ⊓ b = (Ideal.span {x}).radical ∧
        (a ⊔ b).radical = maximalIdeal C ∧
        (maximalIdeal C) ^ n ≤ a ⊔ b ∧
        (a * b) ^ k ≤ Ideal.span {x} := 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, ha, hb, ham, hbm, haRadical, hbRadical,
      hinf, hsup⟩ :=
    exists_radical_nonmaximal_ambient_componentIntersectionIdeals_of_not_connectedSpace
      hdim x hx hnot
  obtain ⟨n, hn⟩ := exists_maximalIdeal_pow_le_of_radical_eq hsup
  obtain ⟨k, hk⟩ := exists_product_pow_le_of_inf_eq_radical hinf
  exact
    ⟨a, b, n, k, hxa, hxb, ha, hb, ham, hbm, haRadical, hbRadical,
      hinf, hsup, hn, hk⟩
theorem

exists_completeIntersectionPowerData_of_not_connectedSpace

L92 ↗
AlgebraicGeometry.FiniteEtale.exists_completeIntersectionPowerData_of_not_connectedSpace
Documentation

A disconnected punctured principal hypersurface produces ambient proper ideals together with the two power containments that a complete-local intersection theorem must exclude.

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 · full declaration
theorem exists_completeIntersectionPowerData_of_not_connectedSpace
    {C : Type u} [CommRing 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})) →
      ∃ a b : Ideal C, ∃ n k : ℕ,
        Ideal.span {x} ≤ a ∧ Ideal.span {x} ≤ b ∧
        a ≠ ⊤ ∧ b ≠ ⊤ ∧
        a ≠ maximalIdeal C ∧ b ≠ maximalIdeal C ∧
        a ⊓ b = (Ideal.span {x}).radical ∧
        (a ⊔ b).radical = maximalIdeal C ∧
        (maximalIdeal C) ^ n ≤ a ⊔ b ∧
        (a * b) ^ k ≤ Ideal.span {x} := 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, n, k, hxa, hxb, ha, hb, ham, hbm, _haRadical,
      _hbRadical, hinf, hsup, hn, hk⟩ :=
    exists_radical_completeIntersectionPowerData_of_not_connectedSpace
      hdim x hx hnot
  exact
    ⟨a, b, n, k, hxa, hxb, ha, hb, ham, hbm, hinf, hsup, hn, hk⟩

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