Module

GeometricFiberNeighborhood.lean

Nyll.SchemeTheory.Etale.GeometricFiberNeighborhood

3 declarations indexed from sourceView source ↗

Module documentation

Finite sets of geometric points persist on an open neighborhood

For a separated étale morphism, a finite set of distinct points in one geometric fiber gives equally many distinct points in every nearby geometric fiber. The conclusion is an actual injection; no finiteness or cardinality convention is needed for the surrounding fibers.

The construction uses the native finite product in the small étale category. It removes the inverse images of the actual relative diagonals, not the loci where projected underlying points coincide. Open-immersion lifting retains the actual maps from the chosen field, including their residue embeddings. This is the local geometric input for the degree-decrease step in Stacks Project, Tag 09Z0.

Imports14

Mathlib.AlgebraicGeometry.Limits
Mathlib.AlgebraicGeometry.Morphisms.Etale
Mathlib.AlgebraicGeometry.Morphisms.FlatMono
Mathlib.AlgebraicGeometry.Morphisms.FormallyUnramified
Mathlib.AlgebraicGeometry.Morphisms.Separated
Mathlib.AlgebraicGeometry.Morphisms.UniversallyOpen
Mathlib.AlgebraicGeometry.OpenImmersion
Mathlib.AlgebraicGeometry.Sites.EtalePoint
Mathlib.CategoryTheory.EpiMono
Mathlib.CategoryTheory.Limits.Preserves.Shapes.Products
Mathlib.CategoryTheory.Limits.Shapes.Diagonal
Mathlib.CategoryTheory.Limits.Shapes.Products
Mathlib.CategoryTheory.Limits.Shapes.Pullback.HasPullback
Mathlib.Topology.Basic

Imported by2

theorem

field_sections_eq_of_apply_eq

L47 ↗

AlgebraicGeometry.Etale.field_sections_eq_of_apply_eq

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 field_sections_eq_of_apply_eq
    {Ω : Type u} [Field Ω] {Z : Scheme.{u}}
    (p : Z ⟶ Spec (CommRingCat.of Ω)) [Etale p]
    (a b : Spec (CommRingCat.of Ω) ⟶ Z)
    (ha : a ≫ p = 𝟙 _) (hb : b ≫ p = 𝟙 _)
    (hab : a default = b default) : a = b

theorem

exists_etale_factor_finite_family

L76 ↗

AlgebraicGeometry.Etale.exists_etale_factor_finite_family

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_etale_factor_finite_family
    {U X : Scheme.{u}} (f : U ⟶ X) [Etale f]
    {Ω : Type u} [Field Ω] (s : Spec (CommRingCat.of Ω) ⟶ X)
    {n : ℕ} (a : Fin n → (Spec (CommRingCat.of Ω) ⟶ U))
    (ha : ∀ i, a i ≫ f = s) :
    ∃ (T : Scheme.{u}) (g : T ⟶ X), Etale g ∧
      ∃ (r : Spec (CommRingCat.of Ω) ⟶ T) (p : Fin n → (T ⟶ U)),
        r ≫ g = s ∧ (∀ i, p i ≫ f = g) ∧ (∀ i, r ≫ p i = a i)

theorem

exists_geometricFiber_injections_neighborhood

L104 ↗

AlgebraicGeometry.Etale.exists_geometricFiber_injections_neighborhood

Documentation

Finitely many distinct points in one geometric fiber of a separated étale morphism persist as distinct points in every geometric fiber over an open neighborhood of the given base point. The target fields and their actual maps to the base remain arbitrary.

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_geometricFiber_injections_neighborhood
    {U X : Scheme.{u}} (f : U ⟶ X) [Etale f] [IsSeparated f]
    {Ω : Type u} [Field Ω] [IsSepClosed Ω]
    (s : Spec (CommRingCat.of Ω) ⟶ X) {n : ℕ}
    (e : Fin n ↪ (pullback f s : Scheme.{u})) :
    ∃ V : X.Opens, s default ∈ V ∧
      ∀ (Ω' : Type u) [Field Ω'] [IsSepClosed Ω']
        (s' : Spec (CommRingCat.of Ω') ⟶ X), s' default ∈ V →
        Nonempty (Fin n ↪ (pullback f s' : Scheme.{u}))

Module documentation

Finite sets of geometric points persist on an open neighborhood

Declarations

field_sections_eq_of_apply_eq

exists_etale_factor_finite_family

exists_geometricFiber_injections_neighborhood