Module

GeometricStalkFractionTensor.lean

Nyll.EtaleFundamentalGroups.StrictHenselian.GeometricStalkFractionTensor

2 declarations indexed from sourceView source ↗

Module documentation

The actual fraction field of the geometric étale stalk

For a normal local domain, the generic tensor of its actual geometric stalk is a localization of a domain at nonzero elements. It is integral over the original fraction field, so every nonzero element is a unit. Thus it is the fraction ring of the actual stalk, with its canonical scalar map.

The resulting comparison uses the existing tensor and localization algebra structures. No field structure is installed on the tensor product, and no uniformizer or finite presentation of the original fraction field is used.

Imports7

Nyll.EtaleFundamentalGroups.StrictHenselian.GeometricStalkNormalDomain
Nyll.EtaleFundamentalGroups.StrictHenselian.GeometricStalkFlat
Nyll.EtaleFundamentalGroups.StrictHenselian.GeometricStalkGenericIntegral
Mathlib.RingTheory.IntegralClosure.IsIntegralClosure.Basic
Mathlib.RingTheory.Localization.BaseChange
Mathlib.RingTheory.Localization.FractionRing
Mathlib.RingTheory.TensorProduct.Maps

Imported by5

theorem

geometricStalk_genericTensor_isFractionRing

L43 ↗

EtaleFundamentalGroups.StrictHenselian.geometricStalk_genericTensor_isFractionRing

Documentation

The canonical generic tensor is a fraction ring of the actual geometric stalk: its integral elements over the base field are units when nonzero.

Source context 6 commands

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

noncomputable section
open AlgebraicGeometry CategoryTheory
open scoped TensorProduct nonZeroDivisors
namespace EtaleFundamentalGroups.StrictHenselian
universe u
variable {R Ω : Type u} [CommRing R] [IsDomain R] [IsIntegrallyClosed R]
  [IsLocalRing R] [Field Ω] (φ : R →+* Ω) [IsLocalHom φ]

Lean source · full declaration

theorem geometricStalk_genericTensor_isFractionRing :
    let : Algebra R (geometricStalk (Spec.map (CommRingCat.ofHom φ))) :=
      (geometricStalkStructureMap φ).toAlgebra
    let : Algebra (geometricStalk (Spec.map (CommRingCat.ofHom φ)))
        (FractionRing R ⊗[R] geometricStalk (Spec.map (CommRingCat.ofHom φ))) :=
      Algebra.TensorProduct.rightAlgebra
    IsFractionRing (geometricStalk (Spec.map (CommRingCat.ofHom φ)))
      (FractionRing R ⊗[R] geometricStalk (Spec.map (CommRingCat.ofHom φ))) := by
  let A := geometricStalk (Spec.map (CommRingCat.ofHom φ))
  let K := FractionRing R
  let : Algebra R A := (geometricStalkStructureMap φ).toAlgebra
  let T := K ⊗[R] A
  let : Algebra A T := Algebra.TensorProduct.rightAlgebra
  let M : Submonoid A := Algebra.algebraMapSubmonoid A R⁰
  have hM : M ≤ A⁰ := by
    rintro _ ⟨r, hr, rfl⟩
    apply mem_nonZeroDivisors_iff_ne_zero.mpr
    change geometricStalkStructureMap φ r ≠ 0
    exact (map_ne_zero_iff _ (geometricStalkStructureMap_injective φ)).mpr
      (nonZeroDivisors.ne_zero hr)
  have : IsLocalization M T := IsLocalization.tensorRight (R := R) (S := A) (A := K) R⁰
  have : IsDomain T := IsLocalization.isDomain_of_le_nonZeroDivisors T hM
  have : Algebra.IsIntegral K T := geometricStalk_tensor_isIntegral φ K
  apply IsLocalization.of_le M A⁰ hM
  intro a ha
  exact (Algebra.IsIntegral.isIntegral (R := K) (algebraMap A T a)).isUnit
    (IsLocalization.to_map_ne_zero_of_mem_nonZeroDivisors T hM ha)

def

geometricStalkFractionTensorEquiv

L73 ↗

EtaleFundamentalGroups.StrictHenselian.geometricStalkFractionTensorEquiv