NYLL
Module

HenselianLocalGeometricSection.lean

Nyll.SchemeTheory.Etale.HenselianLocalGeometricSection
2 declarations indexed from sourceView source ↗

Module documentation

Étale sections through arbitrary closed field points

An arbitrary field-valued point over the closed point of a strictly local spectrum extends uniquely to an étale section. The residue-field point lifts by Henselianity. Its section is an open immersion; its image contains the given field-valued point and determines the section uniquely.

The open-section argument is adapted from SchemeTheory/FiniteEtale/StrictLocalSections.lean by the same authors. Here the closed-point hypothesis removes the need for the étale morphism to be finite, and no change of field or algebraization is needed.

Imports6
  • Nyll.SchemeTheory.Etale.HenselianLocalSection
  • Mathlib.AlgebraicGeometry.Morphisms.Etale
  • Mathlib.AlgebraicGeometry.OpenImmersion
  • Mathlib.AlgebraicGeometry.Sites.EtalePoint
  • Mathlib.CategoryTheory.MorphismProperty.Limits
  • Mathlib.RingTheory.Spectrum.Prime.Topology
Imported by1

Declarations

theorem

comp_section_eq_of_range_subset

L36 ↗
AlgebraicGeometry.Etale.comp_section_eq_of_range_subset
Source context 4 commands

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

noncomputable section
universe u
open AlgebraicGeometry CategoryTheory
namespace AlgebraicGeometry.Etale
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_closedFieldPoint

L52 ↗
AlgebraicGeometry.Etale.existsUnique_section_of_closedFieldPoint
Documentation

Every field-valued point over the closed point of a strictly local spectrum lies on exactly one global section of an arbitrary étale scheme.

Source context 4 commands

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

noncomputable section
universe u
open AlgebraicGeometry CategoryTheory
namespace AlgebraicGeometry.Etale
Lean source · statement
theorem existsUnique_section_of_closedFieldPoint
    (R : Type u) [CommRing R] [HenselianLocalRing R]
    [IsSepClosed (IsLocalRing.ResidueField R)]
    {X : Scheme.{u}} (f : X ⟶ Spec (.of R)) [Etale f]
    {Ω : Type u} [Field Ω] (j : Spec (.of Ω) ⟶ Spec (.of R))
    (hj : j default = IsLocalRing.closedPoint R)
    (s : Spec (.of Ω) ⟶ X) (hs : s ≫ f = j) :
    ∃! σ : Spec (.of R) ⟶ X, σ ≫ f = 𝟙 _ ∧ j ≫ σ = s

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