Module

StrictLocalSections.lean

Nyll.SchemeTheory.FiniteEtale.StrictLocalSections

2 declarations indexed from sourceView source ↗

Module documentation

Extending finite étale sections over a strictly local spectrum

A morphism from a nonempty connected scheme into a finite étale scheme over a strictly Henselian local ring factors uniquely through a global section. In particular a section on a connected punctured spectrum extends uniquely.

Starting from one point of the connected source, finiteness lifts its specialization to the closed point of the base. The existing Henselian lifting theorem supplies a section through this closed-fiber point. The section has clopen image; connectedness puts the whole source in that image. No assumption on the dimension, normality, or Noetherianity of the ring is used, and the source need not be quasi-compact or an open subscheme.

Imports12

Nyll.SchemeTheory.Etale.HenselianLocalSection
Mathlib.AlgebraicGeometry.Morphisms.Etale
Mathlib.AlgebraicGeometry.Morphisms.Finite
Mathlib.AlgebraicGeometry.Morphisms.Proper
Mathlib.AlgebraicGeometry.Morphisms.Separated
Mathlib.AlgebraicGeometry.Morphisms.UniversallyClosed
Mathlib.AlgebraicGeometry.OpenImmersion
Mathlib.AlgebraicGeometry.Sites.EtalePoint
Mathlib.CategoryTheory.MorphismProperty.Limits
Mathlib.RingTheory.Spectrum.Prime.Topology
Mathlib.Topology.Connected.Clopen
Mathlib.Topology.Inseparable

Imported by2

theorem

comp_section_eq_of_range_subset

L43 ↗

AlgebraicGeometry.FiniteEtale.comp_section_eq_of_range_subset

Source context 4 commands

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

noncomputable section
open CategoryTheory
namespace AlgebraicGeometry.FiniteEtale
universe u

Lean source · statement

theorem comp_section_eq_of_range_subset
    {S X T : Scheme.{u}} (f : X ⟶ S) (σ : S ⟶ X) [IsOpenImmersion σ]
    (hσ : σ ≫ f = 𝟙 S) (j : T ⟶ S) (s : T ⟶ X) (hs : s ≫ f = j)
    (hrange : Set.range s ⊆ Set.range σ) : j ≫ σ = s

theorem

existsUnique_section_of_connected_of_strictHenselian

L61 ↗

AlgebraicGeometry.FiniteEtale.existsUnique_section_of_connected_of_strictHenselian

Documentation

Every finite étale section over a nonempty connected scheme mapping to a strictly local spectrum is the restriction of exactly one global section. This applies to the actual punctured spectrum without a quasi-compactness assumption.