Module

ProperLocalSections.lean

Nyll.EtaleCohomology.Sites.ProperLocalSections

3 declarations indexed from sourceView source ↗

Module documentation

Injectivity of proper-local restriction on global sections

The actual inverse-image/direct-image unit is an isomorphism on geometric stalks along a closed immersion. Equal images of two global sections therefore give equal germs at the closed fiber, and the filtered-colimit description supplies étale neighborhoods on which the sections agree.

Choose one such neighborhood for each point of the closed fiber. This is a family in the original universe. Proper-local covering detection makes its disjoint union surjective, and the sheaf separation axiom proves equality of the original sections. Only universally closedness of the structure morphism is needed. Surjectivity of restriction and positive-degree proper base change are not asserted.

Imports28

Nyll.EtaleCohomology.Sites.ClosedAdjunction
Nyll.EtaleCohomology.Sites.SheafFunctors
Nyll.SchemeTheory.Etale.ProperLocalCover
Mathlib.Algebra.Category.ModuleCat.Adjunctions
Mathlib.Algebra.Category.ModuleCat.Colimits
Mathlib.Algebra.Category.ModuleCat.EpiMono
Mathlib.Algebra.Category.ModuleCat.FilteredColimits
Mathlib.AlgebraicGeometry.Limits
Mathlib.AlgebraicGeometry.Morphisms.Basic
Mathlib.AlgebraicGeometry.Morphisms.ClosedImmersion
Mathlib.AlgebraicGeometry.Morphisms.Etale
Mathlib.AlgebraicGeometry.PullbackCarrier
Mathlib.AlgebraicGeometry.ResidueField
Mathlib.AlgebraicGeometry.Scheme
Mathlib.AlgebraicGeometry.Sites.Etale
Mathlib.AlgebraicGeometry.Sites.EtalePoint
Mathlib.CategoryTheory.Adjunction.Limits
Mathlib.CategoryTheory.Comma.Over.Basic
Mathlib.CategoryTheory.Limits.Shapes.Products
Mathlib.CategoryTheory.MorphismProperty.Comma
Mathlib.CategoryTheory.Sites.Grothendieck
Mathlib.CategoryTheory.Sites.LocallyInjective
Mathlib.CategoryTheory.Sites.Point.Basic
Mathlib.CategoryTheory.Sites.Sheaf
Mathlib.CategoryTheory.Sites.Sieves.Basic
Mathlib.CategoryTheory.Sites.Whiskering
Mathlib.FieldTheory.SeparableClosure
Mathlib.RingTheory.LocalRing.ResidueField.Basic

Imported by2

theorem

covering_sieve_of_closedFiber

L61 ↗

EtaleCohomology.covering_sieve_of_closedFiber

Source context 4 commands

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

noncomputable section
universe u
open AlgebraicGeometry CategoryTheory Limits Opposite
namespace EtaleCohomology

Lean source · statement

theorem covering_sieve_of_closedFiber
    (R : Type u) [CommRing R] [IsLocalRing R]
    {X : Scheme.{u}} (f : X ⟶ Spec (CommRingCat.of R)) [UniversallyClosed f]
    (S : Sieve (Scheme.Etale.mk (𝟙 X)))
    (hS : ∀ x : X, f x = IsLocalRing.closedPoint R →
      ∃ (V : X.Etale) (g : V ⟶ Scheme.Etale.mk (𝟙 X)) (v : V.left),
        S g ∧ g.left v = x) :
    S ∈ X.smallEtaleTopology (Scheme.Etale.mk (𝟙 X))

theorem

exists_neighborhood_unit_sections_eq

L101 ↗

EtaleCohomology.exists_neighborhood_unit_sections_eq

Source context 4 commands

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

noncomputable section
universe u
open AlgebraicGeometry CategoryTheory Limits Opposite
namespace EtaleCohomology

Lean source · statement

theorem exists_neighborhood_unit_sections_eq
    {X Z : Scheme.{u}} (i : Z ⟶ X) [IsClosedImmersion i]
    (Λ : Type u) [CommRing Λ] (F : Sheaf X.smallEtaleTopology (ModuleCat.{u} Λ))
    (a b : F.obj.obj (op (Scheme.Etale.mk (𝟙 X))))
    (hab : (((etalePullbackPushforwardAdjunction i Λ).unit.app F).hom.app
      (op (Scheme.Etale.mk (𝟙 X)))) a =
      (((etalePullbackPushforwardAdjunction i Λ).unit.app F).hom.app
        (op (Scheme.Etale.mk (𝟙 X)))) b)
    (z : Z) :
    ∃ (V : X.Etale) (g : V ⟶ Scheme.Etale.mk (𝟙 X)) (v : V.left),
      F.obj.map g.op a = F.obj.map g.op b ∧ g.left v = i z

theorem

etaleClosedFiber_unit_globalSections_injective

L150 ↗

EtaleCohomology.etaleClosedFiber_unit_globalSections_injective

Documentation

For a universally closed scheme over a local ring, restriction to the actual closed fiber is injective on global sections of every coefficient sheaf. The map is the existing inverse-image/direct-image unit evaluated on the identity object of the small étale site. In particular it applies to proper schemes, with no henselian, noetherian or torsion requirement.

Source context 4 commands

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

noncomputable section
universe u
open AlgebraicGeometry CategoryTheory Limits Opposite
namespace EtaleCohomology

Lean source · statement

theorem etaleClosedFiber_unit_globalSections_injective
    (R : Type u) [CommRing R] [IsLocalRing R]
    {X : Scheme.{u}} (f : X ⟶ Spec (CommRingCat.of R)) [UniversallyClosed f]
    (Λ : Type u) [CommRing Λ] (F : Sheaf X.smallEtaleTopology (ModuleCat.{u} Λ)) :
    Function.Injective
      (((etalePullbackPushforwardAdjunction
        (pullback.fst f (Spec.map (CommRingCat.ofHom (IsLocalRing.residue R))))
          Λ).unit.app F).hom.app
          (op (Scheme.Etale.mk (𝟙 X))))

Module documentation

Injectivity of proper-local restriction on global sections

Declarations

covering_sieve_of_closedFiber

exists_neighborhood_unit_sections_eq

etaleClosedFiber_unit_globalSections_injective