Module

SmoothFiniteSchemeConstants.lean

Nyll.EtaleFundamentalGroups.FiniteEtale.GenericFiber.SmoothFiniteSchemeConstants

4 declarations indexed from sourceView source ↗

Module documentation

Constant fields of smooth finite arithmetic schemes

A finite affine cover and its inverse image supply the rings and maps in the arithmetic constants theorem. Normality extends integral constants on every chart, and the actual covering of Spec ℤ supplies faithful flatness.

Imports11

Nyll.EtaleFundamentalGroups.FiniteEtale.GenericFiber.SmoothFiniteCoverConstants
Nyll.EtaleFundamentalGroups.FiniteEtale.GenericFiber.ArithmeticFunctionField
Nyll.SchemeTheory.FunctionFields.Functoriality
Nyll.SchemeTheory.Normalization.Normal
Nyll.SchemeTheory.RingTheory.SeparableConstantsTensor
Mathlib.Algebra.CharZero.AddMonoidHom
Mathlib.AlgebraicGeometry.Limits
Mathlib.AlgebraicGeometry.Morphisms.Finite
Mathlib.AlgebraicGeometry.Morphisms.Smooth
Mathlib.AlgebraicGeometry.Morphisms.UnderlyingMap
Mathlib.RingTheory.Flat.TorsionFree

Imported by2

theorem

charZero_functionField_of_dominant_integers

L36 ↗

EtaleFundamentalGroups.charZero_functionField_of_dominant_integers

Documentation

A dominant arithmetic integral scheme has characteristic-zero function field, via the actual map from the fraction field of the integers.

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 NumberField
namespace EtaleFundamentalGroups

Lean source · statement

theorem charZero_functionField_of_dominant_integers
    {X : Scheme.{0}} [IsIntegral X]
    (p : X ⟶ Spec (CommRingCat.of ℤ)) [IsDominant p] :
    CharZero X.functionField

theorem

smooth_int_sections

L49 ↗

EtaleFundamentalGroups.smooth_int_sections

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 NumberField
namespace EtaleFundamentalGroups

Lean source · statement

theorem smooth_int_sections
    {X : Scheme.{0}} (p : X ⟶ Spec (CommRingCat.of ℤ)) [Smooth p]
    (U : X.Opens) (hU : IsAffineOpen U) : Algebra.Smooth ℤ Γ(X, U)

theorem

numberField_finrank_eq_one_of_smooth_finite_scheme_cover

L62 ↗

EtaleFundamentalGroups.numberField_finrank_eq_one_of_smooth_finite_scheme_cover

Documentation

A finite surjective arithmetic cover that is smooth and normal admits no nontrivial constant number field disjoint from the base function field.

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 NumberField
namespace EtaleFundamentalGroups

Lean source · statement

theorem numberField_finrank_eq_one_of_smooth_finite_scheme_cover
    {X Y : Scheme.{0}} [IsIntegral X] [IsIntegral Y] [IsNormalIntegral X]
    (f : X ⟶ Y) [IsFinite f] [Flat f] [Surjective f]
    (p : Y ⟶ Spec (CommRingCat.of ℤ)) [QuasiCompact p] [Surjective p]
    [Smooth (f ≫ p)] [CharZero Y.functionField] [CharZero X.functionField]
    (K : Type) [Field K] [NumberField K]
    [IsDomain (Y.functionField ⊗[ℚ] K)] (g : K →ₐ[ℚ] X.functionField) :
    Module.finrank ℚ K = 1

theorem

isField_tensor_algebraicClosure_of_smooth_finite_scheme_cover

L119 ↗

EtaleFundamentalGroups.isField_tensor_algebraicClosure_of_smooth_finite_scheme_cover

Documentation

After extension to the algebraic closure of the rational constants, the function field of the smooth finite arithmetic cover is still a field.

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 NumberField
namespace EtaleFundamentalGroups

Lean source · statement

theorem isField_tensor_algebraicClosure_of_smooth_finite_scheme_cover
    {X Y : Scheme.{0}} [IsIntegral X] [IsIntegral Y] [IsNormalIntegral X]
    (f : X ⟶ Y) [IsFinite f] [Flat f] [Surjective f]
    (p : Y ⟶ Spec (CommRingCat.of ℤ)) [QuasiCompact p] [Surjective p]
    [Smooth (f ≫ p)] [CharZero Y.functionField] [CharZero X.functionField]
    [GeometricallyIntegral
      (p.fiberToSpecResidueField (genericPoint (Spec (CommRingCat.of ℤ))))] :
    IsField (X.functionField ⊗[ℚ] AlgebraicClosure ℚ)

Module documentation

Constant fields of smooth finite arithmetic schemes

Declarations

charZero_functionField_of_dominant_integers

smooth_int_sections

numberField_finrank_eq_one_of_smooth_finite_scheme_cover

isField_tensor_algebraicClosure_of_smooth_finite_scheme_cover