NYLL
Module

StrictGenericSplittingNormal.lean

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

Module documentation

Strict generic splitting and normalization over a normal local domain

A splitting over the actual strict generic field descends to an actual pointed affine étale neighborhood. Its actual section algebra is faithfully flat. The concrete tensor cancellation and commutation comparison then supplies the generic-fiber splitting used by normal-localization and integral-closure descent. No finite presentation of the original fraction field over its base is used.

Imports11
Imported by4

Declarations

def

mkUnderTensorSplit

L42 ↗
EtaleFundamentalGroups.StrictHenselian.mkUnderTensorSplit
Documentation

Restore the original scalar dictionary after the canonical Under construction. The scalar-map identity, including its induced tensor action, is supplied by toAlgebra_algebraMap.

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 · statement
def mkUnderTensorSplit
    {K : CommRingCat.{u}} {A B : Type u} [CommRing A] [CommRing B]
    [Algebra K A] [Algebra K B] (ι : Type u)
    (e : ((CommRingCat.mkUnder K A) ⊗[K] B) ≃ₐ[CommRingCat.mkUnder K A]
      (ι → CommRingCat.mkUnder K A)) :
    (A ⊗[K] B) ≃ₐ[A] (ι → A)
theorem

integralClosure_etale_of_normal_strictGeneric_tensor_split

L56 ↗
EtaleFundamentalGroups.StrictHenselian.integralClosure_etale_of_normal_strictGeneric_tensor_split
Documentation

An actual strict-generic splitting of a finite fraction-field algebra makes its actual integral closure étale over the original normal local domain.

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_normal_strictGeneric_tensor_split
    {R Ω B : Type u} [CommRing R] [IsDomain R] [IsIntegrallyClosed R] [IsLocalRing R]
    [Field Ω] [IsSepClosed Ω] [CommRing B]
    [Algebra R B] [Algebra (FractionRing R) B]
    [IsScalarTower R (FractionRing R) B] [Module.Finite (FractionRing R) B]
    (φ : R →+* Ω) [IsLocalHom φ] (ι : Type u) [Finite ι] :
    let : Algebra (FractionRing R)
        (FractionRing (geometricStalk (Spec.map (CommRingCat.ofHom φ)))) :=
      (geometricStalkFractionFieldMap φ).toAlgebra
    Nonempty ((FractionRing (geometricStalk (Spec.map (CommRingCat.ofHom φ))) ⊗[FractionRing R] B)
      ≃ₐ[FractionRing (geometricStalk (Spec.map (CommRingCat.ofHom φ)))]
        (ι → FractionRing (geometricStalk (Spec.map (CommRingCat.ofHom φ))))) →
    Algebra.Etale R (integralClosure R B) := by
  intro scalarAction he
  obtain ⟨e⟩ := he
  obtain ⟨V, v, hV, eV, -⟩ := geometricStalk_exists_affine_generic_split φ ι e
  have : IsAffine V.left := hV
  let S := Γ(V.left, ⊤)
  let : Algebra R S :=
    ((Scheme.ΓSpecIso (CommRingCat.of R)).inv ≫ V.hom.appTop).hom.toAlgebra
  obtain ⟨hEtale, hFlat⟩ := affineNeighborhood_structure_etale_faithfullyFlat φ V v
  have : Algebra.Etale R S := hEtale
  have : Module.FaithfullyFlat R S := hFlat
  apply SchemeTheory.integralClosure_etale_of_generic_split_after_faithfullyFlat_etale R S B ι
  exact SchemeTheory.genericTensorSplitEquiv R (FractionRing R) S B ι
    (mkUnderTensorSplit (K := CommRingCat.of (FractionRing R))
      (A := FractionRing R ⊗[R] S) (B := B) ι eV)

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