Module

ProperHenselianClosedRestriction.lean

Nyll.SchemeTheory.Morphisms.ProperHenselianClosedRestriction

3 declarations indexed from sourceView source ↗

Module documentation

Closed-fiber intersections and constant sections of arbitrary proper schemes

For every irreducible closed subset, its actual reduced induced subscheme is integral and proper over the base. Applying connectedness to that scheme supplies the point-closure condition in Stacks 09ZG. The existing spectral restriction theorem then extends every locally constant function from the closed fiber of an arbitrary proper scheme. No integrality assumption is made on the ambient proper scheme, including finite refinements of it.

Imports8

Nyll.SchemeTheory.Morphisms.ProperIntegralHenselianConnectedFiber
Nyll.SchemeTheory.Divisors.Reduced
Nyll.SchemeTheory.Topology.SpectralClosedRestriction
Mathlib.AlgebraicGeometry.IdealSheaf.Subscheme
Mathlib.AlgebraicGeometry.Morphisms.QuasiCompact
Mathlib.AlgebraicGeometry.Morphisms.QuasiSeparated
Mathlib.AlgebraicGeometry.Properties
Mathlib.Topology.Irreducible

Imported by4

theorem

isConnected_closedFiber_inter_of_isIrreducible

L41 ↗

AlgebraicGeometry.isConnected_closedFiber_inter_of_isIrreducible

Documentation

Every nonempty irreducible closed subset of an arbitrary proper scheme meets the henselian closed fiber in a connected nonempty subset.

Source context 6 commands

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

noncomputable section
open CategoryTheory TopologicalSpace
namespace AlgebraicGeometry
universe u
variable {R : Type u} [CommRing R] [HenselianLocalRing R]
variable {X : Scheme.{u}} (f : X ⟶ Spec (CommRingCat.of R)) [IsProper f]

Lean source · statement

theorem isConnected_closedFiber_inter_of_isIrreducible
    (C : Set X) (hC : IsClosed C) (hIrreducible : IsIrreducible C) :
    _root_.IsConnected ((f ⁻¹' {IsLocalRing.closedPoint R}) ∩ C)

theorem

isConnected_closedFiber_inter_closure

L65 ↗

AlgebraicGeometry.isConnected_closedFiber_inter_closure

Documentation

The actual point-closure condition needed in the spectral restriction theorem is supplied for every point of the original proper scheme.

Source context 6 commands

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

noncomputable section
open CategoryTheory TopologicalSpace
namespace AlgebraicGeometry
universe u
variable {R : Type u} [CommRing R] [HenselianLocalRing R]
variable {X : Scheme.{u}} (f : X ⟶ Spec (CommRingCat.of R)) [IsProper f]

Lean source · statement

theorem isConnected_closedFiber_inter_closure (x : X) :
    _root_.IsConnected
      ((f ⁻¹' {IsLocalRing.closedPoint R}) ∩ closure ({x} : Set X))

theorem

locallyConstant_closedFiber_restriction_bijective

L73 ↗

AlgebraicGeometry.locallyConstant_closedFiber_restriction_bijective

Documentation

Every locally constant function on the actual closed fiber extends uniquely to the arbitrary proper scheme. The value type need not be finite.

Source context 6 commands

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

noncomputable section
open CategoryTheory TopologicalSpace
namespace AlgebraicGeometry
universe u
variable {R : Type u} [CommRing R] [HenselianLocalRing R]
variable {X : Scheme.{u}} (f : X ⟶ Spec (CommRingCat.of R)) [IsProper f]

Lean source · statement

theorem locallyConstant_closedFiber_restriction_bijective (S : Type*) :
    Function.Bijective (LocallyConstant.comap
      (⟨Subtype.val, continuous_subtype_val⟩ : C(f ⁻¹' {IsLocalRing.closedPoint R}, X)) :
        LocallyConstant X S → LocallyConstant (f ⁻¹' {IsLocalRing.closedPoint R}) S)

Module documentation

Closed-fiber intersections and constant sections of arbitrary proper schemes

Declarations

isConnected_closedFiber_inter_of_isIrreducible

isConnected_closedFiber_inter_closure

locallyConstant_closedFiber_restriction_bijective