Module

StalkDominantNeighborhood.lean

Nyll.SchemeTheory.LocalGeometry.StalkDominantNeighborhood

1 declaration indexed from sourceView source ↗

Module documentation

+# A neighborhood dominated by the actual local spectrum

When a scheme has finitely many irreducible components, deleting the components which miss a given point gives an open neighborhood dominated by its actual stalk spectrum. The generic point of each remaining component is in the range of the stalk map.

This provides compatible shrinking in the local connectedness criteria without imposing normality or Noetherianity on the local rings.

Imports4

Mathlib.AlgebraicGeometry.Stalk
Mathlib.AlgebraicGeometry.Properties
Mathlib.AlgebraicGeometry.Morphisms.UnderlyingMap
Mathlib.Topology.Sober

Imported by2

theorem

exists_open_fromSpecStalkOfMem_isDominant

L33 ↗

AlgebraicGeometry.Scheme.exists_open_fromSpecStalkOfMem_isDominant

Documentation

Finite irreducible components suffice for the actual stalk spectrum to dominate some open neighborhood of its center.

Source context 4 commands

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

noncomputable section
universe u
open CategoryTheory TopologicalSpace
namespace AlgebraicGeometry.Scheme

Lean source · statement

theorem exists_open_fromSpecStalkOfMem_isDominant
    (X : Scheme.{u}) (hfin : (irreducibleComponents X).Finite) (x : X) :
    ∃ (U : X.Opens) (hxU : x ∈ U), IsDominant (U.fromSpecStalkOfMem x hxU)

Module documentation

Declarations

exists_open_fromSpecStalkOfMem_isDominant