NYLL
Module

ProperIntegralHenselianConnectedFiber.lean

Nyll.SchemeTheory.Morphisms.ProperIntegralHenselianConnectedFiber
3 declarations indexed from sourceView source ↗

Module documentation

Connected closed fibers of proper integral henselian families

The actual integral projective Chow cover embeds in the base change of projective space over the integers. Its closed-fiber idempotents descend to the actual Noetherian image stages and lift to global sections. The global section ring of the projective cover is local, so every such idempotent is zero or one. Connectedness then descends through the actual surjective Chow morphism. No Noetherian or finite-presentation assumption is made on the original henselian base or proper family.

Imports9
Imported by2

Declarations

theorem

isPreconnected_preimage_closedPoint

L46 ↗
AlgebraicGeometry.NoetherianImageApproximation.isPreconnected_preimage_closedPoint
Documentation

The actual closed fiber of an integral closed subscheme in the fixed proper ambient model is preconnected.

Source context 9 commands

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

noncomputable section
open CategoryTheory CategoryTheory.Limits TopologicalSpace
namespace AlgebraicGeometry.NoetherianImageApproximation
universe u
variable (A₀ A : Type u) [CommRing A₀] [CommRing A] [Algebra A₀ A]
variable [IsNoetherianRing A₀] [HenselianLocalRing A]
variable {X₀ : Scheme.{u}} (f₀ : X₀ ⟶ Spec (CommRingCat.of A₀)) [IsProper f₀]
variable {Z : Scheme.{u}} [IsIntegral Z]
variable (j : Z ⟶ (ambientCone A₀ A f₀).pt) [IsClosedImmersion j]
Lean source · statement
theorem isPreconnected_preimage_closedPoint :
    _root_.IsPreconnected ((originalBaseMap A₀ A f₀ j) ⁻¹' {IsLocalRing.closedPoint A})
theorem

isPreconnected_preimage_closedPoint_of_isProper_of_isIntegral

L90 ↗
AlgebraicGeometry.isPreconnected_preimage_closedPoint_of_isProper_of_isIntegral
Documentation

The closed fiber of a proper integral scheme over an arbitrary henselian local ring is preconnected. The projective model and all approximation data are constructed from the original morphism.

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 isPreconnected_preimage_closedPoint_of_isProper_of_isIntegral
    {R : Type u} [CommRing R] [HenselianLocalRing R]
    {Y : Scheme.{u}} [IsIntegral Y]
    (f : Y ⟶ Spec (CommRingCat.of R)) [IsProper f] :
    _root_.IsPreconnected (f ⁻¹' {IsLocalRing.closedPoint R})
theorem

isConnected_preimage_closedPoint_of_isProper_of_isIntegral

L131 ↗
AlgebraicGeometry.isConnected_preimage_closedPoint_of_isProper_of_isIntegral
Documentation

The same closed fiber is nonempty and connected. Properness sends the nonempty total space to a closed subset containing the base closed point.

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 isConnected_preimage_closedPoint_of_isProper_of_isIntegral
    {R : Type u} [CommRing R] [HenselianLocalRing R]
    {Y : Scheme.{u}} [IsIntegral Y]
    (f : Y ⟶ Spec (CommRingCat.of R)) [IsProper f] :
    _root_.IsConnected (f ⁻¹' {IsLocalRing.closedPoint R})

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