Module

ArithmeticConstantsFiniteDominance.lean

Nyll.EtaleFundamentalGroups.FiniteEtale.GenericFiber.ArithmeticConstantsFiniteDominance

3 declarations indexed from sourceView source ↗

Module documentation

Surjectivity over integral constant extensions

For a finite cover of integral affine schemes, a number field in the cover's function field gives an actual map to the integral constant extension. Geometric integrality of the base's function field makes this map dominant; finiteness then makes it surjective on prime spectra.

Imports4

Nyll.EtaleFundamentalGroups.FiniteEtale.GenericFiber.ArithmeticConstantsTensor
Mathlib.RingTheory.Finiteness.Basic
Mathlib.RingTheory.IntegralClosure.Algebra.Basic
Mathlib.RingTheory.Spectrum.Prime.Topology

Imported by2

def

arithmeticConstantsTensorToNormalDomain

L35 ↗

EtaleFundamentalGroups.arithmeticConstantsTensorToNormalDomain

Documentation

The actual morphism from an affine finite cover to the constant extension, specified contravariantly as a ring homomorphism.

Source context 4 commands

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

noncomputable section
open scoped TensorProduct NumberField
namespace EtaleFundamentalGroups
variable (B A F K L : Type) [CommRing B]
  [CommRing A] [IsDomain A] [IsIntegrallyClosed A] [Algebra B A]
  [Field F] [CharZero F] [Algebra B F] [IsFractionRing B F]
  [Field K] [NumberField K] [Field L] [CharZero L]
  [Algebra A L] [IsFractionRing A L]

Lean source · statement

def arithmeticConstantsTensorToNormalDomain (g : K →ₐ[ℚ] L) :
    B ⊗[ℤ] (𝓞 K) →ₐ[B] A

theorem

arithmeticConstantsTensorToNormalDomain_injective

L42 ↗

EtaleFundamentalGroups.arithmeticConstantsTensorToNormalDomain_injective

Documentation

The constant-extension map is dominant, as witnessed by injectivity of its coordinate ring homomorphism.

Source context 4 commands

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

noncomputable section
open scoped TensorProduct NumberField
namespace EtaleFundamentalGroups
variable (B A F K L : Type) [CommRing B]
  [CommRing A] [IsDomain A] [IsIntegrallyClosed A] [Algebra B A]
  [Field F] [CharZero F] [Algebra B F] [IsFractionRing B F]
  [Field K] [NumberField K] [Field L] [CharZero L]
  [Algebra A L] [IsFractionRing A L]

Lean source · statement

theorem arithmeticConstantsTensorToNormalDomain_injective
    [FaithfulSMul B A] [IsDomain (F ⊗[ℚ] K)]
    (g : K →ₐ[ℚ] L) :
    Function.Injective (arithmeticConstantsTensorToNormalDomain B A K L g)

theorem

arithmeticConstantsTensorToNormalDomain_comap_surjective

L80 ↗

EtaleFundamentalGroups.arithmeticConstantsTensorToNormalDomain_comap_surjective

Documentation

A finite cover is surjective onto its integral constant extension.

Source context 4 commands

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

noncomputable section
open scoped TensorProduct NumberField
namespace EtaleFundamentalGroups
variable (B A F K L : Type) [CommRing B]
  [CommRing A] [IsDomain A] [IsIntegrallyClosed A] [Algebra B A]
  [Field F] [CharZero F] [Algebra B F] [IsFractionRing B F]
  [Field K] [NumberField K] [Field L] [CharZero L]
  [Algebra A L] [IsFractionRing A L]

Lean source · statement

theorem arithmeticConstantsTensorToNormalDomain_comap_surjective
    [FaithfulSMul B A] [Module.Finite B A]
    [IsDomain (F ⊗[ℚ] K)] (g : K →ₐ[ℚ] L) :
    Function.Surjective (PrimeSpectrum.comap
      (arithmeticConstantsTensorToNormalDomain B A K L g).toRingHom)

Module documentation

Surjectivity over integral constant extensions

Declarations

arithmeticConstantsTensorToNormalDomain

arithmeticConstantsTensorToNormalDomain_injective

arithmeticConstantsTensorToNormalDomain_comap_surjective