Module

AffineGeometricFiberBound.lean

Nyll.SchemeTheory.Etale.AffineGeometricFiberBound

1 declaration indexed from sourceView source ↗

Module documentation

Uniform bounds for affine étale geometric fibers

For an étale map between spectra, one natural number bounds the actual carrier of every pullback to the spectrum of a separably closed field. The field and its map to the base are chosen after the bound.

The proof uses the existing uniform bound on field-valued algebra maps. Every point of the étale pullback has a rational section through it, and its first projection corresponds to an algebra map by Spec.homEquivAlgHom. The evaluation map is therefore surjective onto the actual pullback. No tensor-product presentation or assumed point comparison is used.

This is the affine geometric-fiber supplier for the finite-refinement argument of Stacks Project, Tag 09Z0; the refinement itself remains open.

Imports9

Nyll.SchemeTheory.RingTheory.EtaleFieldPointGlobalBound
Mathlib.AlgebraicGeometry.GammaSpecAdjunction
Mathlib.AlgebraicGeometry.Limits
Mathlib.AlgebraicGeometry.Morphisms.Etale
Mathlib.AlgebraicGeometry.Morphisms.RingHomProperties
Mathlib.AlgebraicGeometry.Sites.EtalePoint
Mathlib.CategoryTheory.Limits.Shapes.Pullback.HasPullback
Mathlib.RingTheory.RingHom.Etale
Mathlib.SetTheory.Cardinal.Finite

Imported by3

theorem

exists_uniform_geometricFiber_bound_spec

L46 ↗

AlgebraicGeometry.Etale.exists_uniform_geometricFiber_bound_spec

Documentation

All geometric fibers of an étale morphism between affine spectra have one finite bound, independent of the separably closed field and its actual map to the base. Finiteness is asserted as well as the Nat.card inequality.

Source context 4 commands

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

noncomputable section
universe u
open CategoryTheory Limits
namespace AlgebraicGeometry.Etale

Lean source · statement

theorem exists_uniform_geometricFiber_bound_spec
    {R S : CommRingCat.{u}} (f : Spec S ⟶ Spec R) [Etale f] :
    ∃ N : ℕ, ∀ (Ω : Type u) [Field Ω] [IsSepClosed Ω]
      (s : Spec (CommRingCat.of Ω) ⟶ Spec R),
      Finite (pullback f s : Scheme.{u}) ∧
        Nat.card (pullback f s : Scheme.{u}) ≤ N

Module documentation

Uniform bounds for affine étale geometric fibers

Declarations

exists_uniform_geometricFiber_bound_spec