NYLL
Module

HenselianLocalSection.lean

Nyll.SchemeTheory.Etale.HenselianLocalSection
5 declarations indexed from sourceView source ↗

Module documentation

Sections of étale morphisms over Henselian local spectra

A rational point of the closed fiber of an arbitrary étale scheme over a Henselian local ring lifts to a section. An affine open neighborhood of the point reduces this statement to étale algebra section lifting over a Henselian pair. The étale scheme need not be affine or finite over the base.

For a separably closed residue field, a point over the closed point supplies the rational point, so every étale cover of a strictly local spectrum splits.

Imports11
  • Nyll.SchemeTheory.FiniteEtale.Algebra.HenselianEtaleSection
  • Mathlib.AlgebraicGeometry.GammaSpecAdjunction
  • Mathlib.AlgebraicGeometry.Morphisms.Etale
  • Mathlib.AlgebraicGeometry.Morphisms.FormallyUnramified
  • Mathlib.AlgebraicGeometry.Pullbacks
  • Mathlib.AlgebraicGeometry.Morphisms.RingHomProperties
  • Mathlib.AlgebraicGeometry.OpenImmersion
  • Mathlib.AlgebraicGeometry.Sites.EtalePoint
  • Mathlib.RingTheory.Henselian
  • Mathlib.RingTheory.RingHom.Etale
  • Mathlib.RingTheory.Spectrum.Prime.Topology
Imported by8

Declarations

theorem

exists_affine_section_of_henselian

L40 ↗
AlgebraicGeometry.Etale.exists_affine_section_of_henselian
Source context 4 commands

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

noncomputable section
universe u
open AlgebraicGeometry CategoryTheory CategoryTheory.Limits
namespace AlgebraicGeometry.Etale
Lean source · statement
theorem exists_affine_section_of_henselian
    (R B : Type u) [CommRing R] [CommRing B]
    (I : Ideal R) [HenselianRing R I]
    (f : Spec (.of B) ⟶ Spec (.of R)) [Etale f]
    (p : Spec (.of (R ⧸ I)) ⟶ Spec (.of B))
    (hp : p ≫ f = Spec.map (CommRingCat.ofHom (Ideal.Quotient.mk I))) :
    ∃ s : Spec (.of R) ⟶ Spec (.of B), s ≫ f = 𝟙 _ ∧
      Spec.map (CommRingCat.ofHom (Ideal.Quotient.mk I)) ≫ s = p
theorem

exists_section_of_henselianLocalRing

L75 ↗
AlgebraicGeometry.Etale.exists_section_of_henselianLocalRing
Documentation

Every residue-field point of an étale scheme over a Henselian local ring lifts to an actual section, with its closed-fiber restriction prescribed.

Source context 4 commands

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

noncomputable section
universe u
open AlgebraicGeometry CategoryTheory CategoryTheory.Limits
namespace AlgebraicGeometry.Etale
Lean source · statement
theorem exists_section_of_henselianLocalRing
    (R : Type u) [CommRing R] [HenselianLocalRing R]
    {X : Scheme.{u}} (f : X ⟶ Spec (.of R)) [Etale f]
    (p : Spec (.of (IsLocalRing.ResidueField R)) ⟶ X)
    (hp : p ≫ f = Spec.map (CommRingCat.ofHom (IsLocalRing.residue R))) :
    ∃ s : Spec (.of R) ⟶ X, s ≫ f = 𝟙 _ ∧
      Spec.map (CommRingCat.ofHom (IsLocalRing.residue R)) ≫ s = p
theorem

exists_section_of_isSepClosed_residueField

L107 ↗
AlgebraicGeometry.Etale.exists_section_of_isSepClosed_residueField
Documentation

An étale morphism to a strictly local spectrum has a section whenever its image contains the closed point. Neither module-finiteness nor affineness of the source is required.

Source context 4 commands

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

noncomputable section
universe u
open AlgebraicGeometry CategoryTheory CategoryTheory.Limits
namespace AlgebraicGeometry.Etale
Lean source · statement
theorem exists_section_of_isSepClosed_residueField
    (R : Type u) [CommRing R] [HenselianLocalRing R]
    [IsSepClosed (IsLocalRing.ResidueField R)]
    {X : Scheme.{u}} (f : X ⟶ Spec (.of R)) [Etale f]
    (x : X) (hx : f x =
      Spec.map (CommRingCat.ofHom (IsLocalRing.residue R)) default) :
    ∃ s : Spec (.of R) ⟶ X, s ≫ f = 𝟙 _
theorem

localSource_hom_ext_of_residue

L120 ↗
AlgebraicGeometry.Etale.localSource_hom_ext_of_residue
Source context 4 commands

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

noncomputable section
universe u
open AlgebraicGeometry CategoryTheory CategoryTheory.Limits
namespace AlgebraicGeometry.Etale
Lean source · statement
theorem localSource_hom_ext_of_residue
    (R : Type u) [CommRing R] [IsLocalRing R]
    {X Y : Scheme.{u}} (f : X ⟶ Y) [FormallyUnramified f] [LocallyOfFiniteType f]
    (a b : Spec (.of R) ⟶ X) (hab : a ≫ f = b ≫ f)
    (hresidue : Spec.map (CommRingCat.ofHom (IsLocalRing.residue R)) ≫ a =
      Spec.map (CommRingCat.ofHom (IsLocalRing.residue R)) ≫ b) : a = b
theorem

existsUnique_lift_of_henselianLocalRing

L167 ↗
AlgebraicGeometry.Etale.existsUnique_lift_of_henselianLocalRing
Documentation

A prescribed residue-field point of an étale scheme lifts uniquely over any map from a Henselian local spectrum. The source of the étale morphism need not be affine: existence uses the existing section theorem after base change, and uniqueness uses its open diagonal over the local spectrum.

Source context 4 commands

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

noncomputable section
universe u
open AlgebraicGeometry CategoryTheory CategoryTheory.Limits
namespace AlgebraicGeometry.Etale
Lean source · statement
theorem existsUnique_lift_of_henselianLocalRing
    (R : Type u) [CommRing R] [HenselianLocalRing R]
    {X Y : Scheme.{u}} (f : X ⟶ Y) [Etale f]
    (b : Spec (.of R) ⟶ Y)
    (p : Spec (.of (IsLocalRing.ResidueField R)) ⟶ X)
    (hp : p ≫ f = Spec.map (CommRingCat.ofHom (IsLocalRing.residue R)) ≫ b) :
    ∃! s : Spec (.of R) ⟶ X,
      s ≫ f = b ∧ Spec.map (CommRingCat.ofHom (IsLocalRing.residue R)) ≫ s = p

Statements and documentation are read from the Lean source at the revision shown. Source entries are not a measure of mathematical completeness.