Nyll.EtaleFundamentalGroups.FiniteEtale.GenericFiber.SmoothFiniteCoverConstants

Module documentation

Constants of smooth finite arithmetic covers

The coordinate rings of a finite affine cover are assembled into a faithfully flat algebra over the ring of integers of a constant field. The resulting smooth arithmetic algebra forces that field to have degree one. All maps to the integer ring are constructed from normality.

theorem

numberField_finrank_eq_one_of_smooth_finite_arithmetic_cover

L32 ↗

EtaleFundamentalGroups.numberField_finrank_eq_one_of_smooth_finite_arithmetic_cover

Documentation

A constant number field in a smooth finite arithmetic cover has degree one. The base charts cover Spec ℤ, while their common function field is geometrically disjoint from the constant number field.

Source context 3 commands

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

noncomputable section
open scoped TensorProduct NumberField
namespace EtaleFundamentalGroups

Lean source · statement

theorem numberField_finrank_eq_one_of_smooth_finite_arithmetic_cover
    {ι : Type} [Finite ι] (B A : ι → Type)
    [∀ i, CommRing (B i)] [∀ i, CommRing (A i)] [∀ i, IsDomain (A i)]
    [∀ i, IsIntegrallyClosed (A i)] [∀ i, Algebra (B i) (A i)]
    [∀ i, FaithfulSMul (B i) (A i)] [∀ i, Module.Finite (B i) (A i)]
    [∀ i, Algebra.Smooth ℤ (A i)]
    (F K L : Type) [Field F] [CharZero F] [Field K] [NumberField K]
    [Field L] [CharZero L]
    [∀ i, Algebra (B i) F] [∀ i, IsFractionRing (B i) F]
    [∀ i, Algebra (A i) L] [∀ i, IsFractionRing (A i) L]
    [IsDomain (F ⊗[ℚ] K)] (g : K →ₐ[ℚ] L)
    (hcover : ∀ p : PrimeSpectrum ℤ, ∃ (i : ι) (q : PrimeSpectrum (B i)),
      PrimeSpectrum.comap (algebraMap ℤ (B i)) q = p) :
    Module.finrank ℚ K = 1

Module documentation

Constants of smooth finite arithmetic covers

Declarations

numberField_finrank_eq_one_of_smooth_finite_arithmetic_cover