Module

GeometricFiberBound.lean

Nyll.SchemeTheory.Etale.GeometricFiberBound

3 declarations indexed from sourceView source ↗

Module documentation

Uniform geometric-fiber bounds from a compact étale source

An étale morphism with quasi-compact source has a uniform finite bound on all actual geometric fibers. The target is arbitrary. The proof uses the native affine refinement of the pullback of an affine target cover, then compactness selects finitely many of those source charts.

Each selected chart maps to an affine target chart, where the existing affine bound applies. A field-valued point either misses that target chart or lifts through its open immersion; the existing pullback universal property compares the actual fibers. Finally the pulled-back source charts cover each geometric fiber, so the sum of their bounds is a uniform bound.

This supplies the initial bound required by the degree induction in Stacks Project, Tag 09Z0, after its existing affine-source reduction.

Imports17

Nyll.SchemeTheory.Etale.AffineGeometricFiberBound
Mathlib.AlgebraicGeometry.AffineScheme
Mathlib.AlgebraicGeometry.Cover.MorphismProperty
Mathlib.AlgebraicGeometry.Cover.Open
Mathlib.AlgebraicGeometry.Morphisms.Etale
Mathlib.AlgebraicGeometry.Morphisms.RingHomProperties
Mathlib.AlgebraicGeometry.Morphisms.UniversallyInjective
Mathlib.AlgebraicGeometry.OpenImmersion
Mathlib.AlgebraicGeometry.PullbackCarrier
Mathlib.AlgebraicGeometry.Pullbacks
Mathlib.AlgebraicGeometry.Scheme
Mathlib.CategoryTheory.Limits.Shapes.Pullback.HasPullback
Mathlib.CategoryTheory.Limits.Shapes.Pullback.Mono
Mathlib.CategoryTheory.Limits.Shapes.Pullback.Pasting
Mathlib.Algebra.Order.BigOperators.Group.Finset
Mathlib.SetTheory.Cardinal.Finite
Mathlib.Topology.Compactness.Compact

Imported by2

theorem

exists_uniform_geometricFiber_bound_affine

L52 ↗

AlgebraicGeometry.Etale.exists_uniform_geometricFiber_bound_affine

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_affine
    {U X : Scheme.{u}} [IsAffine U] [IsAffine X] (f : U ⟶ X) [Etale f] :
    ∃ N : ℕ, ∀ (Ω : Type u) [Field Ω] [IsSepClosed Ω]
      (s : Spec (CommRingCat.of Ω) ⟶ X),
      Finite (pullback f s : Scheme.{u}) ∧ Nat.card (pullback f s : Scheme.{u}) ≤ N

theorem

geometricFiber_bound_postcomp_open

L76 ↗

AlgebraicGeometry.Etale.geometricFiber_bound_postcomp_open

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 geometricFiber_bound_postcomp_open
    {A V X : Scheme.{u}} (h : A ⟶ V) (j : V ⟶ X) [IsOpenImmersion j]
    (N : ℕ)
    (hN : ∀ (Ω : Type u) [Field Ω] [IsSepClosed Ω]
      (s : Spec (CommRingCat.of Ω) ⟶ V),
      Finite (pullback h s : Scheme.{u}) ∧ Nat.card (pullback h s : Scheme.{u}) ≤ N)
    (Ω : Type u) [Field Ω] [IsSepClosed Ω] (s : Spec (CommRingCat.of Ω) ⟶ X) :
    Finite (pullback (h ≫ j) s : Scheme.{u}) ∧
      Nat.card (pullback (h ≫ j) s : Scheme.{u}) ≤ N

theorem

exists_uniform_geometricFiber_bound

L117 ↗

AlgebraicGeometry.Etale.exists_uniform_geometricFiber_bound

Documentation

A quasi-compact source supplies one finite bound on every geometric fiber of an étale morphism, independently of the separably closed field and its actual map to the arbitrary target.

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
    {U X : Scheme.{u}} [CompactSpace U] (f : U ⟶ X) [Etale f] :
    ∃ N : ℕ, ∀ (Ω : Type u) [Field Ω] [IsSepClosed Ω]
      (s : Spec (CommRingCat.of Ω) ⟶ X),
      Finite (pullback f s : Scheme.{u}) ∧ Nat.card (pullback f s : Scheme.{u}) ≤ N

Module documentation

Uniform geometric-fiber bounds from a compact étale source

Declarations

exists_uniform_geometricFiber_bound_affine

geometricFiber_bound_postcomp_open

exists_uniform_geometricFiber_bound