Module

PuncturedHypersurfaceNeighborhoodDiagram.lean

Nyll.EtaleFundamentalGroups.Purity.PuncturedHypersurfaceNeighborhoodDiagram

14 declarations indexed from sourceView source ↗

Module documentation

The actual neighbourhood diagram of a punctured hypersurface

The indices are opens inside the punctured local spectrum that contain its hypersurface. Their order is reversed so that intersections are later stages. The cone vertex is the actual pullback of the hypersurface to the puncture. Its maps to every neighbourhood are constructed using the unique isomorphism between the corresponding open subschemes of the hypersurface.

Thus no comparison map, pullback identification, or limiting property is assumed in the neighbourhood system used in Stacks Project, Tag 0BLN.

Imports10

Nyll.SchemeTheory.LocalGeometry.PuncturedSpectrum
Mathlib.AlgebraicGeometry.Limits
Mathlib.AlgebraicGeometry.OpenImmersion
Mathlib.AlgebraicGeometry.Restrict
Mathlib.CategoryTheory.Category.Preorder
Mathlib.CategoryTheory.Limits.Cones
Mathlib.Order.Directed
Mathlib.Order.OrderDual
Mathlib.RingTheory.Ideal.Quotient.Basic
Mathlib.RingTheory.Spectrum.Prime.RingHom

Imported by3

def

hypersurfaceMap

L42 ↗

AlgebraicGeometry.FiniteEtale.PuncturedHypersurface.hypersurfaceMap

Documentation

The actual principal closed immersion into the local spectrum.

Source context 5 commands

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

noncomputable section
open CategoryTheory CategoryTheory.Limits Opposite
namespace AlgebraicGeometry.FiniteEtale.PuncturedHypersurface
universe u
variable (R : Type u) [CommRing R] [IsLocalRing R] (f : R)

Lean source · statement

def hypersurfaceMap : Spec (.of (R ⧸ Ideal.span {f})) ⟶ Spec (.of R)

abbrev

puncture

L46 ↗

AlgebraicGeometry.FiniteEtale.PuncturedHypersurface.puncture

Documentation

The hypersurface in the punctured spectrum, defined by its actual pullback.

Source context 5 commands

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

noncomputable section
open CategoryTheory CategoryTheory.Limits Opposite
namespace AlgebraicGeometry.FiniteEtale.PuncturedHypersurface
universe u
variable (R : Type u) [CommRing R] [IsLocalRing R] (f : R)

Lean source · statement

abbrev puncture : Scheme.{u}

def

Neighborhood

L50 ↗

AlgebraicGeometry.FiniteEtale.PuncturedHypersurface.Neighborhood

Documentation

The open neighbourhoods of the punctured hypersurface within the puncture.

Source context 5 commands

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

noncomputable section
open CategoryTheory CategoryTheory.Limits Opposite
namespace AlgebraicGeometry.FiniteEtale.PuncturedHypersurface
universe u
variable (R : Type u) [CommRing R] [IsLocalRing R] (f : R)

Lean source · statement

def Neighborhood : Type u

instance

(anonymous instance)

L56 ↗

Source context 5 commands

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

noncomputable section
open CategoryTheory CategoryTheory.Limits Opposite
namespace AlgebraicGeometry.FiniteEtale.PuncturedHypersurface
universe u
variable (R : Type u) [CommRing R] [IsLocalRing R] (f : R)

Lean source · statement

instance : PartialOrder (Neighborhood R f)

instance

(anonymous instance)

L58 ↗

Source context 5 commands

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

noncomputable section
open CategoryTheory CategoryTheory.Limits Opposite
namespace AlgebraicGeometry.FiniteEtale.PuncturedHypersurface
universe u
variable (R : Type u) [CommRing R] [IsLocalRing R] (f : R)

Lean source · statement

instance : Nonempty (Neighborhood R f)

instance

(anonymous instance)

L61 ↗

Source context 5 commands

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

noncomputable section
open CategoryTheory CategoryTheory.Limits Opposite
namespace AlgebraicGeometry.FiniteEtale.PuncturedHypersurface
universe u
variable (R : Type u) [CommRing R] [IsLocalRing R] (f : R)

Lean source · full declaration

instance : IsDirectedOrder (OrderDual (Neighborhood R f)) where
  directed W V := by
    let D : Neighborhood R f :=
      ⟨W.val ⊓ V.val, inf_le_left.trans W.property.1,
        fun p hp hfp ↦ ⟨W.property.2 p hp hfp, V.property.2 p hp hfp⟩⟩
    refine ⟨OrderDual.toDual D, ?_, ?_⟩
    · change W.val ⊓ V.val ≤ W.val
      exact inf_le_left
    · change W.val ⊓ V.val ≤ V.val
      exact inf_le_right

theorem

preimage_neighborhood_eq

L73 ↗

AlgebraicGeometry.FiniteEtale.PuncturedHypersurface.preimage_neighborhood_eq

Documentation

Pulling a neighbourhood back to the hypersurface gives exactly its puncture.

Source context 5 commands

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

noncomputable section
open CategoryTheory CategoryTheory.Limits Opposite
namespace AlgebraicGeometry.FiniteEtale.PuncturedHypersurface
universe u
variable (R : Type u) [CommRing R] [IsLocalRing R] (f : R)

Lean source · statement

theorem preimage_neighborhood_eq (W : Neighborhood R f) :
    hypersurfaceMap R f ⁻¹ᵁ W.val =
      hypersurfaceMap R f ⁻¹ᵁ Scheme.puncturedSpectrumOpen R

theorem

neighborhoodPullback_range_eq

L86 ↗

AlgebraicGeometry.FiniteEtale.PuncturedHypersurface.neighborhoodPullback_range_eq

Source context 5 commands

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

noncomputable section
open CategoryTheory CategoryTheory.Limits Opposite
namespace AlgebraicGeometry.FiniteEtale.PuncturedHypersurface
universe u
variable (R : Type u) [CommRing R] [IsLocalRing R] (f : R)

Lean source · statement

theorem neighborhoodPullback_range_eq (W : Neighborhood R f) :
    Set.range (Limits.pullback.snd
      (Scheme.puncturedSpectrumOpen R).ι (hypersurfaceMap R f)) =
        Set.range (Limits.pullback.snd W.val.ι (hypersurfaceMap R f))

def

neighborhoodPullbackIso

L98 ↗

AlgebraicGeometry.FiniteEtale.PuncturedHypersurface.neighborhoodPullbackIso

Documentation

The actual hypersurface pullback over each neighbourhood is the same open subscheme of the hypersurface as the original puncture.

Source context 5 commands

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

noncomputable section
open CategoryTheory CategoryTheory.Limits Opposite
namespace AlgebraicGeometry.FiniteEtale.PuncturedHypersurface
universe u
variable (R : Type u) [CommRing R] [IsLocalRing R] (f : R)

Lean source · statement

def neighborhoodPullbackIso (W : Neighborhood R f) :
    puncture R f ≅ Limits.pullback W.val.ι (hypersurfaceMap R f)

theorem

neighborhoodPullbackIso_hom_snd

L106 ↗

AlgebraicGeometry.FiniteEtale.PuncturedHypersurface.neighborhoodPullbackIso_hom_snd

Documentation

The hypersurface comparison preserves its map to the closed hypersurface.

Source context 5 commands

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

noncomputable section
open CategoryTheory CategoryTheory.Limits Opposite
namespace AlgebraicGeometry.FiniteEtale.PuncturedHypersurface
universe u
variable (R : Type u) [CommRing R] [IsLocalRing R] (f : R)

Lean source · statement

theorem neighborhoodPullbackIso_hom_snd (W : Neighborhood R f) :
    (neighborhoodPullbackIso R f W).hom ≫
        Limits.pullback.snd W.val.ι (hypersurfaceMap R f) =
      Limits.pullback.snd (Scheme.puncturedSpectrumOpen R).ι (hypersurfaceMap R f)

def

projection

L116 ↗

AlgebraicGeometry.FiniteEtale.PuncturedHypersurface.projection

Documentation

The punctured hypersurface maps canonically into every neighbourhood.

Source context 5 commands

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

noncomputable section
open CategoryTheory CategoryTheory.Limits Opposite
namespace AlgebraicGeometry.FiniteEtale.PuncturedHypersurface
universe u
variable (R : Type u) [CommRing R] [IsLocalRing R] (f : R)

Lean source · statement

def projection (W : Neighborhood R f) : puncture R f ⟶ W.val.toScheme

theorem

projection_comp_ι

L121 ↗

AlgebraicGeometry.FiniteEtale.PuncturedHypersurface.projection_comp_ι

Documentation

Each projection is over the original local spectrum.

Source context 5 commands

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

noncomputable section
open CategoryTheory CategoryTheory.Limits Opposite
namespace AlgebraicGeometry.FiniteEtale.PuncturedHypersurface
universe u
variable (R : Type u) [CommRing R] [IsLocalRing R] (f : R)

Lean source · statement

theorem projection_comp_ι (W : Neighborhood R f) :
    projection R f W ≫ W.val.ι =
      Limits.pullback.fst (Scheme.puncturedSpectrumOpen R).ι (hypersurfaceMap R f) ≫
        (Scheme.puncturedSpectrumOpen R).ι

def

diagram

L132 ↗

AlgebraicGeometry.FiniteEtale.PuncturedHypersurface.diagram

Documentation

The inverse diagram consists of the actual open subschemes and inclusions.

Source context 5 commands

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

noncomputable section
open CategoryTheory CategoryTheory.Limits Opposite
namespace AlgebraicGeometry.FiniteEtale.PuncturedHypersurface
universe u
variable (R : Type u) [CommRing R] [IsLocalRing R] (f : R)

Lean source · full declaration

def diagram : (OrderDual (Neighborhood R f))ᵒᵖ ⥤ Scheme.{u} where
  obj W := W.unop.val.toScheme
  map h := (Spec (.of R)).homOfLE (leOfHom h.unop)
  map_id W := (Spec (.of R)).homOfLE_rfl W.unop.val
  map_comp h k := ((Spec (.of R)).homOfLE_homOfLE
    (leOfHom h.unop) (leOfHom k.unop)).symm

def

cone

L140 ↗

AlgebraicGeometry.FiniteEtale.PuncturedHypersurface.cone

Documentation

The canonical cone with vertex the actual punctured hypersurface.

Source context 5 commands

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

noncomputable section
open CategoryTheory CategoryTheory.Limits Opposite
namespace AlgebraicGeometry.FiniteEtale.PuncturedHypersurface
universe u
variable (R : Type u) [CommRing R] [IsLocalRing R] (f : R)

Lean source · full declaration

def cone : Cone (diagram R f) where
  pt := puncture R f
  π :=
    { app W := projection R f W.unop
      naturality {W V} h := by
        change 𝟙 (puncture R f) ≫ projection R f V.unop =
          projection R f W.unop ≫ (Spec (.of R)).homOfLE (leOfHom h.unop)
        rw [Category.id_comp]
        apply (cancel_mono V.unop.val.ι).1
        rw [Category.assoc, Scheme.homOfLE_ι]
        exact (projection_comp_ι R f V.unop).trans
          (projection_comp_ι R f W.unop).symm }

Module documentation

The actual neighbourhood diagram of a punctured hypersurface

Declarations