Module

SmoothArithmeticConstants.lean

Nyll.EtaleFundamentalGroups.FiniteEtale.GenericFiber.SmoothArithmeticConstants

3 declarations indexed from sourceView source ↗

Module documentation

Smooth arithmetic schemes and fields of constants

A number field admitting a faithfully flat algebra which is smooth over the integers is unramified at every finite prime. Smoothness gives reduced special fibers; faithful flatness descends this reducedness to the ring of integers. The local unramified criterion and Minkowski then force degree one.

Imports15

Nyll.SchemeTheory.RingTheory.SmoothReduced
Mathlib.Data.Int.Order.Units
Mathlib.LinearAlgebra.FiniteDimensional.Basic
Mathlib.NumberTheory.NumberField.Discriminant.Basic
Mathlib.NumberTheory.NumberField.Discriminant.Different
Mathlib.NumberTheory.NumberField.ExistsRamified
Mathlib.RingTheory.Artinian.Module
Mathlib.RingTheory.Flat.FaithfullyFlat.Algebra
Mathlib.RingTheory.Finiteness.Quotient
Mathlib.RingTheory.Ideal.Quotient.Nilpotent
Mathlib.RingTheory.Ideal.Quotient.HasFiniteQuotients.Basic
Mathlib.RingTheory.Ideal.MinimalPrime.Localization
Mathlib.RingTheory.LocalRing.ResidueField.Separable
Mathlib.RingTheory.TensorProduct.Quotient
Mathlib.RingTheory.Unramified.LocalRing

Imported by2

theorem

unramifiedAt_of_radical_specialFiber

L38 ↗

EtaleFundamentalGroups.unramifiedAt_of_radical_specialFiber

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 unramifiedAt_of_radical_specialFiber
    {R S : Type} [CommRing R] [CommRing S] [Algebra R S]
    [Module.Finite R S] (p : Ideal R) [p.IsMaximal]
    [PerfectField p.ResidueField] (q : Ideal S) [q.IsPrime] [q.LiesOver p]
    (hred : (p.map (algebraMap R S)).IsRadical) :
    Algebra.IsUnramifiedAt R q

theorem

ringOfIntegers_unramifiedAt_of_smooth_faithfullyFlat

L79 ↗

EtaleFundamentalGroups.ringOfIntegers_unramifiedAt_of_smooth_faithfullyFlat

Documentation

Smoothness over the integers and faithful flatness over the ring of integers force every finite prime of that ring of integers to be unramified.

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 ringOfIntegers_unramifiedAt_of_smooth_faithfullyFlat
    (K A : Type) [Field K] [NumberField K] [CommRing A]
    [Algebra (𝓞 K) A] [Module.FaithfullyFlat (𝓞 K) A] [Algebra.Smooth ℤ A]
    (p : Ideal ℤ) [p.IsMaximal]
    (q : Ideal (𝓞 K)) [q.IsPrime] [q.LiesOver p] :
    Algebra.IsUnramifiedAt ℤ q

theorem

numberField_finrank_eq_one_of_smooth_faithfullyFlat_ringOfIntegers

L104 ↗

EtaleFundamentalGroups.numberField_finrank_eq_one_of_smooth_faithfullyFlat_ringOfIntegers

Documentation

A number field with a faithfully flat algebra smooth over ℤ is ℚ in degree. In the geometric application the algebra comes from a finite affine cover of the smooth arithmetic covering scheme.

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_faithfullyFlat_ringOfIntegers
    (K A : Type) [Field K] [NumberField K] [CommRing A]
    [Algebra (𝓞 K) A] [Module.FaithfullyFlat (𝓞 K) A] [Algebra.Smooth ℤ A] :
    Module.finrank ℚ K = 1

Module documentation

Smooth arithmetic schemes and fields of constants

Declarations

unramifiedAt_of_radical_specialFiber

ringOfIntegers_unramifiedAt_of_smooth_faithfullyFlat

numberField_finrank_eq_one_of_smooth_faithfullyFlat_ringOfIntegers