NYLL
Module

exists_section_of_isFinite_of_etale_of_isProper_of_henselianLocalRing_of_isNoetherianRing.lean

Nyll.AlgebraicCurves.Geometry.Schemes.exists_section_of_isFinite_of_etale_of_isProper_of_henselianLocalRing_of_isNoetherianRing
1 declaration indexed from sourceView source ↗

Module documentation

Lifting finite etale sections over a Noetherian Henselian base

The existing public statement is retained as a specialization of the unrestricted Henselian section-lifting theorem in SchemeTheory.

Imports1
Imported by1

Declarations

theorem

exists_section_of_isFinite_of_etale_of_isProper_of_henselianLocalRing_of_isNoetherianRing

L29 ↗
AlgebraicGeometry.exists_section_of_isFinite_of_etale_of_isProper_of_henselianLocalRing_of_isNoetherianRing
Source context 3 commands

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

namespace AlgebraicGeometry
universe u
open CategoryTheory CategoryTheory.Limits
Lean source · statement
theorem exists_section_of_isFinite_of_etale_of_isProper_of_henselianLocalRing_of_isNoetherianRing
    {R : Type u} [CommRing R] [IsNoetherianRing 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₀

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