Module

PuncturedSpectrumFlat.lean

Nyll.SchemeTheory.LocalGeometry.PuncturedSpectrumFlat

1 declaration indexed from sourceView source ↗

Module documentation

Density of a punctured local spectrum after flat base change

The inverse image of a nonempty punctured local spectrum is dense under any flat morphism. For a point over the closed point, flat going-down lifts the generalization from a chosen puncture point. Every remaining point is already in the inverse image. No finite-presentation or quasi-compactness assumption on the flat morphism is needed.

Imports6

Nyll.SchemeTheory.LocalGeometry.PuncturedSpectrum
Mathlib.AlgebraicGeometry.Morphisms.Flat
Mathlib.AlgebraicGeometry.Morphisms.UnderlyingMap
Mathlib.AlgebraicGeometry.Morphisms.UniversallyOpen
Mathlib.RingTheory.Spectrum.Prime.Topology
Mathlib.Topology.Inseparable

Imported by3

theorem

dense_preimage_puncturedSpectrumOpen_of_flat

L32 ↗

AlgebraicGeometry.Scheme.dense_preimage_puncturedSpectrumOpen_of_flat

Documentation

A nonempty punctured local spectrum remains dense after arbitrary flat base change, including flat maps that are not locally of finite presentation.

Source context 3 commands

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

open CategoryTheory
namespace AlgebraicGeometry.Scheme
universe u

Lean source · statement

theorem dense_preimage_puncturedSpectrumOpen_of_flat
    (R : Type u) [CommRing R] [IsLocalRing R]
    [Nonempty (puncturedSpectrum R)]
    {X : Scheme.{u}} (f : X ⟶ Spec (.of R)) [Flat f] :
    Dense (f ⁻¹' (puncturedSpectrumOpen R : Set (Spec (.of R))))

Module documentation

Density of a punctured local spectrum after flat base change

Declarations

dense_preimage_puncturedSpectrumOpen_of_flat