PuncturedSpectrumCompleteRegularLocalPurity.lean

theorem hasPuncturedPurity_of_complete_regularLocal_quotient_span_singleton
    {R : Type u} [CommRing R] [IsDomain R] [IsRegularLocalRing R]
    [IsIntegrallyClosed R]
    [IsAdicComplete (maximalIdeal R) R]
    (hdim : ((3 : ℕ∞) : WithBot ℕ∞) ≤ ringKrullDim R)
    (x : R) (hx : x ∈ maximalIdeal R) (hx0 : x ≠ 0) :
    let I : Ideal R := Ideal.span {x}
    letI : Nontrivial (R ⧸ I) :=
      Ideal.Quotient.nontrivial_iff.mpr
        (ne_top_of_le_ne_top (maximalIdeal.isMaximal R).ne_top
          ((maximalIdeal R).span_singleton_le_iff_mem.mpr hx))
    letI : IsLocalRing (R ⧸ I) :=
      IsLocalRing.of_surjective' (Ideal.Quotient.mk I)
        Ideal.Quotient.mk_surjective
    AlgebraicGeometry.FiniteEtale.HasPuncturedPurity (R ⧸ I) →
      AlgebraicGeometry.FiniteEtale.HasPuncturedPurity R := by
  dsimp only
  let I : Ideal R := Ideal.span {x}
  have hI : I ≤ maximalIdeal R :=
    (maximalIdeal R).span_singleton_le_iff_mem.mpr hx
  have hIne : I ≠ ⊤ :=
    ne_top_of_le_ne_top (maximalIdeal.isMaximal R).ne_top hI
  let : Nontrivial (R ⧸ I) :=
    Ideal.Quotient.nontrivial_iff.mpr hIne
  let : IsLocalRing (R ⧸ I) :=
    IsLocalRing.of_surjective' (Ideal.Quotient.mk I)
      Ideal.Quotient.mk_surjective
  intro hquotient
  have hpos : (1 : WithBot ℕ∞) ≤ ringKrullDim R :=
    (by norm_num : (1 : WithBot ℕ∞) ≤ (3 : ℕ∞)).trans hdim
  have hconnectedR : ConnectedSpace
      (AlgebraicGeometry.Scheme.puncturedSpectrum R) := by
    let U := AlgebraicGeometry.Scheme.puncturedSpectrum R
    let j : U ⟶ AlgebraicGeometry.Spec (.of R) :=
      AlgebraicGeometry.Scheme.puncturedSpectrumInclusion R
    let : Nonempty U :=
      AlgebraicGeometry.Scheme.puncturedSpectrum_nonempty_of_one_le_ringKrullDim
        R hpos
    let : IsOpenImmersion j := by
      dsimp only [j, AlgebraicGeometry.Scheme.puncturedSpectrumInclusion]
      infer_instance
    let : IsIntegral U := isIntegral_of_isOpenImmersion j
    infer_instance
  have hconnectedQuotient : ConnectedSpace
      (AlgebraicGeometry.Scheme.puncturedSpectrum (R ⧸ I)) := by
    exact
      (open _root_.AlgebraicGeometry.FiniteEtale in
        connectedSpace_puncturedSpectrum_quotient_span_singleton_of_completeLocalDomain
          hdim x hx hx0)
  apply hasPuncturedPurity_of_complete_quotient_of_preserves_connected
    I hI hconnectedR hconnectedQuotient hquotient
  intro W hW
  let : IsConnected W := hW
  rw [AlgebraicGeometry.FiniteEtale.connectedPuncturedCoverQuotientRestriction_isConnected_iff
    R hpos W I hI]
  exact
    (open _root_.AlgebraicGeometry.FiniteEtale in
      connectedSpace_connectedPuncturedCoverNormalizationPuncturedFiber_span_singleton
        R hdim W x hx hx0)

theorem hasPuncturedPurity_of_complete_regularSystem_prefix_two
    {R : Type u} [CommRing R] [IsLocalRing R] [IsNoetherianRing R]
    [IsIntegrallyClosed R]
    [IsAdicComplete (maximalIdeal R) R]
    (xs : List R) (y z : R)
    (hreg : RingTheory.Sequence.IsRegular R (xs ++ [y, z]))
    (hgen : Ideal.ofList (xs ++ [y, z]) = maximalIdeal R) :
    AlgebraicGeometry.FiniteEtale.HasPuncturedPurity R

theorem hasPuncturedPurity_of_complete_regularSystem_of_two_le_length
    {R : Type u} [CommRing R] [IsLocalRing R] [IsNoetherianRing R]
    [IsIntegrallyClosed R]
    [IsAdicComplete (maximalIdeal R) R]
    (ps : List R) (hreg : RingTheory.Sequence.IsRegular R ps)
    (hgen : Ideal.ofList ps = maximalIdeal R)
    (hlen : 2 ≤ ps.length) :
    AlgebraicGeometry.FiniteEtale.HasPuncturedPurity R