Module

ArithmeticFunctionField.lean

Nyll.EtaleFundamentalGroups.FiniteEtale.GenericFiber.ArithmeticFunctionField

1 declaration indexed from sourceView source ↗

Module documentation

Geometric integrality of arithmetic function fields

An affine open of an integral arithmetic scheme stays nonempty after a characteristic-zero field extension: its coordinate ring embeds in the tensor product. Geometric integrality of the generic fiber then makes this tensor product a domain. Passing to the fraction field gives the corresponding rational tensor product of function fields.

Imports5

Nyll.EtaleFundamentalGroups.FiniteEtale.GenericFiber.ArithmeticGenericFiber
Nyll.SchemeTheory.RingTheory.FractionFieldTensorDomain
Mathlib.AlgebraicGeometry.Limits
Mathlib.AlgebraicGeometry.OpenImmersion
Mathlib.RingTheory.Flat.TorsionFree

Imported by2

theorem

isDomain_functionField_ratTensor_of_arithmetic_genericFiber

L33 ↗

EtaleFundamentalGroups.isDomain_functionField_ratTensor_of_arithmetic_genericFiber

Documentation

The function field of an integral arithmetic scheme with geometrically integral generic fiber remains a domain after every characteristic-zero field extension of its rational constants.

Source context 4 commands

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

noncomputable section
open AlgebraicGeometry CategoryTheory CategoryTheory.Limits TopologicalSpace
open scoped TensorProduct
namespace EtaleFundamentalGroups

Lean source · statement

theorem isDomain_functionField_ratTensor_of_arithmetic_genericFiber
    {X : Scheme} [IsIntegral X] [CharZero X.functionField]
    (f : X ⟶ Spec (.of ℤ))
    [GeometricallyIntegral
      (f.fiberToSpecResidueField (genericPoint (Spec (.of ℤ))))]
    (K : Type) [Field K] [CharZero K] :
    IsDomain (X.functionField ⊗[ℚ] K)

Module documentation

Geometric integrality of arithmetic function fields

Declarations

isDomain_functionField_ratTensor_of_arithmetic_genericFiber