Module

ArithmeticGenericFiber.lean

Nyll.EtaleFundamentalGroups.FiniteEtale.GenericFiber.ArithmeticGenericFiber

2 declarations indexed from sourceView source ↗

Module documentation

Arithmetic generic fibers after characteristic-zero field extension

Every point of a characteristic-zero field maps to the generic point of Spec ℤ. The fiber base-change square therefore transports geometric integrality of the generic fiber to every such field extension.

Imports4

Mathlib.AlgebraicGeometry.Fiber
Mathlib.AlgebraicGeometry.Geometrically.Integral
Mathlib.AlgebraicGeometry.FunctionField
Mathlib.Data.Int.Cast.Lemmas

Imported by2

theorem

specMap_int_field_eq_genericPoint

L28 ↗

EtaleFundamentalGroups.specMap_int_field_eq_genericPoint

Documentation

A characteristic-zero field point of the integer scheme is its generic point.

Source context 3 commands

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

noncomputable section
open AlgebraicGeometry CategoryTheory CategoryTheory.Limits TopologicalSpace
namespace EtaleFundamentalGroups

Lean source · statement

theorem specMap_int_field_eq_genericPoint
    (K : Type) [Field K] [CharZero K] (x : Spec (CommRingCat.of K)) :
    (Spec.map (CommRingCat.ofHom (algebraMap ℤ K))) x =
      genericPoint (Spec (CommRingCat.of ℤ))

theorem

geometricallyIntegral_pullback_of_arithmetic_genericFiber

L40 ↗

EtaleFundamentalGroups.geometricallyIntegral_pullback_of_arithmetic_genericFiber