NYLL
Module

ArithmeticGeometricIntegrality.lean

Nyll.SchemeTheory.FunctionFields.ArithmeticGeometricIntegrality
2 declarations indexed from sourceView source ↗

Module documentation

Arithmetic geometric integrality from the function field

A field tensor product with the algebraic closure of the rationals makes the corresponding base change of the generic point integral. Scheme-theoretic dominance transports this to the whole scheme. Smoothness and field descent then give geometric integrality of the arithmetic generic fiber.

Imports7
Imported by2

Declarations

theorem

integral_pullback_algebraicClosure_of_functionField_tensor_isField

L31 ↗
AlgebraicGeometry.integral_pullback_algebraicClosure_of_functionField_tensor_isField
Source context 4 commands

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

noncomputable section
open CategoryTheory Limits TopologicalSpace
open scoped TensorProduct
namespace AlgebraicGeometry
Lean source · statement
theorem integral_pullback_algebraicClosure_of_functionField_tensor_isField
    {X : Scheme} [IsIntegral X] [CharZero X.functionField]
    (p : X ⟶ Spec (CommRingCat.of ℤ))
    (h : IsField (X.functionField ⊗[ℚ] AlgebraicClosure ℚ)) :
    IsIntegral (pullback p
      (Spec.map (CommRingCat.ofHom (algebraMap ℤ (AlgebraicClosure ℚ)))))
theorem

geometricallyIntegral_arithmeticGenericFiber_of_functionField_tensor_isField

L80 ↗
AlgebraicGeometry.geometricallyIntegral_arithmeticGenericFiber_of_functionField_tensor_isField
Documentation

If the function field stays a field after tensoring with the algebraic closure of the rationals, a smooth integral arithmetic scheme has a geometrically integral generic fiber.

Source context 4 commands

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

noncomputable section
open CategoryTheory Limits TopologicalSpace
open scoped TensorProduct
namespace AlgebraicGeometry
Lean source · statement
theorem geometricallyIntegral_arithmeticGenericFiber_of_functionField_tensor_isField
    {X : Scheme} [IsIntegral X] [CharZero X.functionField]
    (p : X ⟶ Spec (CommRingCat.of ℤ)) [Smooth p]
    (h : IsField (X.functionField ⊗[ℚ] AlgebraicClosure ℚ)) :
    GeometricallyIntegral
      (p.fiberToSpecResidueField (genericPoint (Spec (CommRingCat.of ℤ))))

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