NYLL
Module

StrictGenericSplittingEtale.lean

Nyll.EtaleFundamentalGroups.StrictHenselian.StrictGenericSplittingEtale
2 declarations indexed from sourceView source ↗

Module documentation

Strict generic splitting implies étale normalization

A splitting into copies of the actual fraction field of the actual geometric stalk descends to an actual pointed affine étale neighborhood. Its sections are faithfully flat over the original local ring. The descended splitting and smooth base change of integral closure then prove that the original normalization is étale. No normalization comparison for the infinite strict-henselization map is assumed.

Imports9
Imported by1

Declarations

theorem

integralClosure_etale_of_geometricStalk_generic_split

L40 ↗
EtaleFundamentalGroups.StrictHenselian.integralClosure_etale_of_geometricStalk_generic_split
Documentation

An actual strict generic splitting of a finitely presented algebra over a DVR forces its actual integral closure to be étale over that DVR.

Source context 5 commands

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

noncomputable section
open AlgebraicGeometry CategoryTheory
open scoped TensorProduct
namespace EtaleFundamentalGroups.StrictHenselian
universe u
Lean source · full declaration
theorem integralClosure_etale_of_geometricStalk_generic_split
    {R Ω B : Type u} [CommRing R] [IsDomain R] [IsDiscreteValuationRing R]
    [Field Ω] [IsSepClosed Ω] [CommRing B] [Algebra R B]
    [Algebra.FinitePresentation R B]
    (φ : R →+* Ω) [IsLocalHom φ] (ι : Type u) [Finite ι] :
    letI : Algebra R (geometricStalk (Spec.map (CommRingCat.ofHom φ))) :=
      (geometricStalkStructureMap φ).toAlgebra
    Nonempty ((geometricStalk (Spec.map (CommRingCat.ofHom φ)) ⊗[R] B) ≃ₐ[
      geometricStalk (Spec.map (CommRingCat.ofHom φ))]
      (ι → FractionRing (geometricStalk (Spec.map (CommRingCat.ofHom φ))))) →
    Algebra.Etale R (integralClosure R B) := by
  classical
  let : Fintype ι := Fintype.ofFinite ι
  let A := geometricStalk (Spec.map (CommRingCat.ofHom φ))
  let : Algebra R A := (geometricStalkStructureMap φ).toAlgebra
  rintro ⟨e⟩
  obtain ⟨π, hπ⟩ := IsDiscreteValuationRing.exists_irreducible R
  let : IsLocalization.Away π (FractionRing R) :=
    SchemeTheory.isLocalizationAway_fractionField_of_isDiscreteValuationRing
      R (FractionRing R) π hπ.ne_zero hπ.not_isUnit
  let : Algebra.FinitePresentation R (FractionRing R) :=
    IsLocalization.Away.finitePresentation π
  let : Algebra.FinitePresentation R (ι → FractionRing R) :=
    Algebra.FinitePresentation.of_finiteType.mp inferInstance
  let eD : (A ⊗[R] (ι → FractionRing R)) ≃ₐ[A] (ι → FractionRing A) :=
    (Algebra.TensorProduct.piRight R A A (fun _ : ι => FractionRing R)).trans
      (AlgEquiv.piCongrRight (fun _ : ι => geometricStalkFractionTensorEquiv φ))
  obtain ⟨V, v, hV, heV⟩ := geometricStalk_exists_affine_tensorProduct_algEquiv
    (B := B) (D := ι → FractionRing R) φ ⟨e.trans eD.symm⟩
  let : IsAffine V.left := hV
  let S := Γ(V.left, ⊤)
  let β : R →+* S :=
    ((Scheme.ΓSpecIso (CommRingCat.of R)).inv ≫ V.hom.appTop).hom
  let : Algebra R S := β.toAlgebra
  obtain ⟨hβ, hβfaithful⟩ := affineNeighborhood_structure_etale_faithfullyFlat φ V v
  let : Algebra.Etale R S := hβ
  let : Module.FaithfullyFlat R S := hβfaithful
  obtain ⟨eV⟩ := heV
  let eSplit : (S ⊗[R] B) ≃ₐ[S] (ι → S ⊗[R] FractionRing R) :=
    eV.trans (Algebra.TensorProduct.piRight R S S (fun _ : ι => FractionRing R))
  exact SchemeTheory.integralClosure_etale_of_split_after_faithfullyFlat_etale
    R S B (S ⊗[R] FractionRing R) ι π hπ.ne_zero eSplit
theorem

integralClosure_etale_of_finite_fractionAlgebra_geometricStalk_generic_split

L85 ↗
EtaleFundamentalGroups.StrictHenselian.integralClosure_etale_of_finite_fractionAlgebra_geometricStalk_generic_split
Documentation

For an actual finite algebra over the fraction field of the DVR, finite presentation over the original DVR is constructed by inverting a uniformizer.

Source context 5 commands

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

noncomputable section
open AlgebraicGeometry CategoryTheory
open scoped TensorProduct
namespace EtaleFundamentalGroups.StrictHenselian
universe u
Lean source · full declaration
theorem integralClosure_etale_of_finite_fractionAlgebra_geometricStalk_generic_split
    {R Ω K B : Type u} [CommRing R] [IsDomain R] [IsDiscreteValuationRing R]
    [Field Ω] [IsSepClosed Ω] [Field K] [Algebra R K] [IsFractionRing R K]
    [CommRing B] [Algebra R B] [Algebra K B] [IsScalarTower R K B] [Module.Finite K B]
    (φ : R →+* Ω) [IsLocalHom φ] (ι : Type u) [Finite ι] :
    letI : Algebra R (geometricStalk (Spec.map (CommRingCat.ofHom φ))) :=
      (geometricStalkStructureMap φ).toAlgebra
    Nonempty ((geometricStalk (Spec.map (CommRingCat.ofHom φ)) ⊗[R] B) ≃ₐ[
      geometricStalk (Spec.map (CommRingCat.ofHom φ))]
      (ι → FractionRing (geometricStalk (Spec.map (CommRingCat.ofHom φ))))) →
    Algebra.Etale R (integralClosure R B) := by
  obtain ⟨π, hπ⟩ := IsDiscreteValuationRing.exists_irreducible R
  let : IsLocalization.Away π K :=
    SchemeTheory.isLocalizationAway_fractionField_of_isDiscreteValuationRing
      R K π hπ.ne_zero hπ.not_isUnit
  let : Algebra.FinitePresentation R K := IsLocalization.Away.finitePresentation π
  let : Algebra.FinitePresentation K B :=
    Algebra.FinitePresentation.of_finiteType.mp inferInstance
  let : Algebra.FinitePresentation R B := Algebra.FinitePresentation.trans R K B
  exact integralClosure_etale_of_geometricStalk_generic_split φ ι

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