Module

ClosedNeighborhoods.lean

Nyll.EtaleCohomology.Sites.ClosedNeighborhoods

2 declarations indexed from sourceView source ↗

Module documentation

Closed-subscheme neighborhoods and geometric points

The geometric neighborhood lifting theorem supplies an ambient étale neighborhood and a map from its restriction to any prescribed pointed étale neighborhood of the closed subscheme. We construct the corresponding costructured arrow for base change on categories of elements.

The equalizing refinement theorem supplies the second part of the initiality criterion for a functor with cofiltered domain. Thus the costructured arrow categories are connected and the neighborhood functor is initial, allowing stalks to be computed on ambient neighborhoods.

Imports11

Nyll.SchemeTheory.Etale.ClosedNeighborhoodLift
Nyll.SchemeTheory.Etale.ClosedNeighborhoodEqualizer
Mathlib.CategoryTheory.Filtered.Final
Mathlib.CategoryTheory.Functor.Flat
Mathlib.CategoryTheory.Limits.Shapes.Pullback.Pasting
Nyll.EtaleCohomology.Sites.BaseChange
Mathlib.AlgebraicGeometry.Sites.EtalePoint
Mathlib.CategoryTheory.MorphismProperty.Comma
Mathlib.CategoryTheory.Limits.Shapes.Pullback.HasPullback
Mathlib.CategoryTheory.Elements
Mathlib.CategoryTheory.Comma.StructuredArrow.Basic

Imported by3

lemma

closedNeighborhoodBaseChange_nonempty

L47 ↗

EtaleCohomology.closedNeighborhoodBaseChange_nonempty

Documentation

Every pointed étale neighborhood of the closed subscheme receives a pointed map from the restriction of an ambient étale neighborhood.

Source context 5 commands

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

noncomputable section
universe u
open AlgebraicGeometry CategoryTheory Limits EtaleCohomology
namespace EtaleCohomology
variable {X Z : Scheme.{u}} (i : Z ⟶ X) [IsClosedImmersion i]
  {Ω : Type u} [Field Ω] [IsSepClosed Ω] (s : Spec (.of Ω) ⟶ Z)

Lean source · statement

lemma closedNeighborhoodBaseChange_nonempty (N : (Scheme.pointSmallEtale s).fiber.Elements) :
    Nonempty (CostructuredArrow
      (Functor.Elements.precomp (etaleBaseChange i) (Scheme.pointSmallEtale s).fiber) N)

theorem

closedNeighborhoodBaseChange_initial

L72 ↗

EtaleCohomology.closedNeighborhoodBaseChange_initial