Module

Integers.lean

Nyll.EtaleFundamentalGroups.FiniteEtale.Integers

5 declarations indexed from sourceView source ↗

Module documentation

Finite étale algebras over the integers

Hermite–Minkowski excludes a nontrivial number field whose ring of integers is unramified over ℤ: no prime can divide its discriminant, whereas a number field of degree greater than one has absolute discriminant greater than two. Applying this to a component of the generic fibre shows that a connected finite étale ℤ-algebra is ℤ itself.

Imports16

Mathlib.NumberTheory.NumberField.Discriminant.Different
Mathlib.NumberTheory.NumberField.ExistsRamified
Mathlib.RingTheory.Smooth.Flat
Mathlib.RingTheory.Flat.TorsionFree
Mathlib.NumberTheory.NumberField.Discriminant.Basic
Mathlib.RingTheory.Algebraic.Basic
Mathlib.LinearAlgebra.FiniteDimensional.Basic
Mathlib.RingTheory.Unramified.Locus
Mathlib.Data.Int.Order.Units
Nyll.EtaleFundamentalGroups.FiniteEtale.GenericFiber.Connected
Nyll.EtaleFundamentalGroups.FiniteEtale.GenericFiber.Component
Nyll.EtaleFundamentalGroups.FiniteEtale.Connected
Mathlib.AlgebraicGeometry.Limits
Mathlib.AlgebraicGeometry.Morphisms.Finite
Mathlib.AlgebraicGeometry.Morphisms.Etale
Mathlib.CategoryTheory.Limits.Shapes.Pullback.Iso

Imported by2

theorem

numberField_finrank_eq_one_of_formallyUnramified

L41 ↗

EtaleFundamentalGroups.numberField_finrank_eq_one_of_formallyUnramified

Documentation

An everywhere unramified number field has degree one over ℚ.

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_formallyUnramified
    (K : Type*) [Field K] [NumberField K]
    [Algebra.FormallyUnramified ℤ (𝓞 K)] :
    Module.finrank ℚ K = 1

theorem

integerAlgebraMap_ringOfIntegers_bijective

L65 ↗

EtaleFundamentalGroups.integerAlgebraMap_ringOfIntegers_bijective

Documentation

For an everywhere unramified number field, every algebraic integer is an ordinary integer.

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 integerAlgebraMap_ringOfIntegers_bijective
    (K : Type*) [Field K] [NumberField K]
    [Algebra.FormallyUnramified ℤ (𝓞 K)] :
    Function.Bijective (algebraMap ℤ (𝓞 K))

theorem

integerAlgebraMap_bijective_of_connected_finiteEtale

L92 ↗

EtaleFundamentalGroups.integerAlgebraMap_bijective_of_connected_finiteEtale

Documentation

The structure map of a connected finite étale ℤ-algebra is bijective. Connectedness makes the algebra a domain; étaleness gives flatness, hence torsion-freeness. The number-field unramified theorem then applies.

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 integerAlgebraMap_bijective_of_connected_finiteEtale
    (T : Type*) [CommRing T]
    [Algebra.Etale ℤ T]
    [ConnectedSpace (PrimeSpectrum T)]
    (hfiniteT : RingHom.Finite (algebraMap ℤ T)) :
    Function.Bijective (algebraMap ℤ T)

theorem

isIso_hom_of_connected_over_integers

L116 ↗

AlgebraicGeometry.FiniteEtale.isIso_hom_of_connected_over_integers

Documentation

A connected finite étale cover of Spec ℤ has an invertible structure morphism. Its global-sections algebra is a connected finite étale ℤ-algebra, so the arithmetic theorem above applies.

Source context 4 commands

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

noncomputable section
open scoped TensorProduct NumberField
open AlgebraicGeometry CategoryTheory CategoryTheory.Limits
namespace AlgebraicGeometry.FiniteEtale

Lean source · statement

theorem isIso_hom_of_connected_over_integers
    (Y : FiniteEtale (Spec (CommRingCat.of ℤ)))
    [ConnectedSpace Y.left] : IsIso Y.hom

theorem

subsingleton_fiber_of_connected_over_integers

L158 ↗

AlgebraicGeometry.FiniteEtale.subsingleton_fiber_of_connected_over_integers

Documentation

The geometric fibre of a connected finite étale cover of Spec ℤ consists of exactly one point.

Source context 4 commands

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

noncomputable section
open scoped TensorProduct NumberField
open AlgebraicGeometry CategoryTheory CategoryTheory.Limits
namespace AlgebraicGeometry.FiniteEtale

Lean source · statement

theorem subsingleton_fiber_of_connected_over_integers
    (Ω : Type) [Field Ω]
    (ξ : Spec (CommRingCat.of Ω) ⟶ Spec (CommRingCat.of ℤ))
    (Y : FiniteEtale (Spec (CommRingCat.of ℤ)))
    [ConnectedSpace Y.left] : Subsingleton ((fiber ξ).obj Y)

Module documentation

Finite étale algebras over the integers

Declarations

numberField_finrank_eq_one_of_formallyUnramified

integerAlgebraMap_ringOfIntegers_bijective

integerAlgebraMap_bijective_of_connected_finiteEtale

isIso_hom_of_connected_over_integers

subsingleton_fiber_of_connected_over_integers