Module

ProperHenselianSections.lean

Nyll.SchemeTheory.FiniteEtale.ProperHenselianSections

6 declarations indexed from sourceView source ↗

Module documentation

Finite etale sections over an arbitrary proper Henselian family

The clopen image of a section on the closed fibre lifts to a clopen subscheme of the finite etale cover. Its projection is an isomorphism because it is an isomorphism on the closed fibre. The original FLT section construction is adapted here to the unrestricted Henselian clopen-lifting theorem, removing the Noetherian hypothesis on the base.

Imports3

Mathlib.AlgebraicGeometry.Morphisms.FlatMono
Nyll.SchemeTheory.FiniteEtale.isIso_of_isIso_pullback_closedFibre_of_isFinite_of_etale_of_isProper
Nyll.SchemeTheory.Morphisms.ProperHenselianClopenLift

Imported by3

theorem

etale_of_section

L36 ↗

AlgebraicGeometry.etale_of_section

Source context 4 commands

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

noncomputable section
universe u
open CategoryTheory CategoryTheory.Limits
namespace AlgebraicGeometry

Lean source · statement

theorem etale_of_section {X Y : Scheme.{u}} (π : Y ⟶ X) [Etale π] (s : X ⟶ Y) (hs : s ≫ π =
  𝟙 X) :
    Etale s

theorem

isClosedImmersion_of_section

L42 ↗

AlgebraicGeometry.isClosedImmersion_of_section

Source context 4 commands

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

noncomputable section
universe u
open CategoryTheory CategoryTheory.Limits
namespace AlgebraicGeometry

Lean source · statement

theorem isClosedImmersion_of_section {X Y : Scheme.{u}} (π : Y ⟶ X) [IsSeparated π] (s : X
  ⟶ Y)
    (hs : s ≫ π = 𝟙 X) : IsClosedImmersion s

theorem

isOpenImmersion_of_section

L48 ↗

AlgebraicGeometry.isOpenImmersion_of_section

Source context 4 commands

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

noncomputable section
universe u
open CategoryTheory CategoryTheory.Limits
namespace AlgebraicGeometry

Lean source · statement

theorem isOpenImmersion_of_section {X Y : Scheme.{u}} (π : Y ⟶ X) [Etale π] (s : X ⟶ Y)
    (hs : s ≫ π = 𝟙 X) : IsOpenImmersion s

theorem

isClosedImmersion_ι_of_isClosed

L54 ↗

AlgebraicGeometry.isClosedImmersion_ι_of_isClosed

Source context 4 commands

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

noncomputable section
universe u
open CategoryTheory CategoryTheory.Limits
namespace AlgebraicGeometry

Lean source · statement

theorem isClosedImmersion_ι_of_isClosed {Y : Scheme.{u}} (U : Y.Opens) (hU : IsClosed (U :
  Set Y)) :
    IsClosedImmersion U.ι

theorem

isIso_pullback_snd_of_preimage_eq

L59 ↗

AlgebraicGeometry.isIso_pullback_snd_of_preimage_eq

Source context 4 commands

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

noncomputable section
universe u
open CategoryTheory CategoryTheory.Limits
namespace AlgebraicGeometry

Lean source · statement

theorem isIso_pullback_snd_of_preimage_eq
    {Xk X Y : Scheme.{u}} (ι : Xk ⟶ X) (π : Y ⟶ X) (U : Y.Opens) (V₀ : (pullback π ι).Opens)
    (hV₀ : IsIso (V₀.ι ≫ pullback.snd π ι)) (hUV : (pullback.fst π ι) ⁻¹ᵁ U = V₀) :
    IsIso (pullback.snd (U.ι ≫ π) ι)

theorem

exists_section_of_isFinite_of_etale_of_isProper_of_henselianLocalRing

L83 ↗

AlgebraicGeometry.exists_section_of_isFinite_of_etale_of_isProper_of_henselianLocalRing

Documentation

A section on the actual closed fibre of a finite etale cover of a proper scheme over any Henselian local ring extends to a section of the cover.

Source context 4 commands

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

noncomputable section
universe u
open CategoryTheory CategoryTheory.Limits
namespace AlgebraicGeometry

Lean source · statement

theorem exists_section_of_isFinite_of_etale_of_isProper_of_henselianLocalRing
    {R : Type u} [CommRing R] [HenselianLocalRing R]
    {X Y : Scheme.{u}} (f : X ⟶ Spec (CommRingCat.of R)) [IsProper f]
    (π : Y ⟶ X) [IsFinite π] [AlgebraicGeometry.Etale π]
    (s₀ : pullback f (Spec.map (CommRingCat.ofHom (IsLocalRing.residue R))) ⟶ Y)
    (hs₀ : s₀ ≫ π = pullback.fst f (Spec.map (CommRingCat.ofHom (IsLocalRing.residue R)))) :
    ∃ s : X ⟶ Y, s ≫ π = 𝟙 X ∧
      pullback.fst f (Spec.map (CommRingCat.ofHom (IsLocalRing.residue R))) ≫ s = s₀

Module documentation

Finite etale sections over an arbitrary proper Henselian family

Declarations

etale_of_section

isClosedImmersion_of_section

isOpenImmersion_of_section

isClosedImmersion_ι_of_isClosed

isIso_pullback_snd_of_preimage_eq

exists_section_of_isFinite_of_etale_of_isProper_of_henselianLocalRing