NYLL
Module

ProperHenselianClopenLift.lean

Nyll.SchemeTheory.Morphisms.ProperHenselianClopenLift
1 declaration indexed from sourceView source ↗

Module documentation

Clopen lifting from the closed fibre over an arbitrary Henselian local ring

The scheme-theoretic closed fibre is identified with its actual closed subset in the proper total space. The spectral closed-restriction theorem then lifts each clopen subset. No Noetherian hypothesis is required.

Imports4
Imported by2

Declarations

theorem

exists_isClopen_closedFiber_preimage_eq_of_isProper_of_henselianLocalRing

L30 ↗
AlgebraicGeometry.exists_isClopen_closedFiber_preimage_eq_of_isProper_of_henselianLocalRing
Documentation

Every clopen subset of the scheme-theoretic closed fibre of a proper scheme over a Henselian local ring extends to a clopen subset of that scheme.

Source context 4 commands

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

noncomputable section
open CategoryTheory CategoryTheory.Limits TopologicalSpace
namespace AlgebraicGeometry
universe u
Lean source · statement
theorem exists_isClopen_closedFiber_preimage_eq_of_isProper_of_henselianLocalRing
    {R : Type u} [CommRing R] [HenselianLocalRing R]
    {X : Scheme.{u}} (f : X ⟶ Spec (CommRingCat.of R)) [IsProper f]
    (V : Set ↥(pullback f (Spec.map (CommRingCat.ofHom (IsLocalRing.residue R)))))
    (hV : IsClopen V) :
    ∃ U : Set X, IsClopen U ∧
      pullback.fst f (Spec.map (CommRingCat.ofHom (IsLocalRing.residue R))) ⁻¹' U = V

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