Module

ClosedZariskiComparison.lean

Nyll.EtaleCohomology.Sites.ClosedZariskiComparison

4 declarations indexed from sourceView source ↗

Module documentation

The closed-immersion Zariski comparison is a monomorphism

The module-valued closed adjunction unit is an isomorphism on geometric stalks inside the closed subscheme. The injective map from Zariski germs to geometric germs makes its underlying Zariski stalk map injective there. The actual mixed unit square and the topological inverse-image stalk formula then prove that the constructed comparison is a monomorphism.

Imports14

Nyll.EtaleCohomology.Sites.ZariskiGeometricStalks
Nyll.EtaleCohomology.Sites.ZariskiModuleBaseChange
Nyll.EtaleCohomology.Sites.ClosedAdjunction
Nyll.SchemeTheory.Topology.SheafPullbackStalks
Nyll.SchemeTheory.Topology.SheafPullbackGerms
Mathlib.Algebra.Category.ModuleCat.Adjunctions
Mathlib.Algebra.Category.ModuleCat.FilteredColimits
Mathlib.AlgebraicGeometry.ResidueField
Mathlib.CategoryTheory.Adjunction.Limits
Mathlib.CategoryTheory.Sites.Point.Basic
Mathlib.CategoryTheory.Sites.Whiskering
Mathlib.CategoryTheory.Types.Basic
Mathlib.FieldTheory.SeparableClosure
Mathlib.Topology.Sheaves.Stalks

Imported by2

lemma

zariskiStalkComparison_naturality

L41 ↗

EtaleCohomology.zariskiStalkComparison_naturality

Source context 4 commands

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

noncomputable section
universe u
open AlgebraicGeometry CategoryTheory Limits TopologicalSpace Opposite
namespace EtaleCohomology

Lean source · statement

lemma zariskiStalkComparison_naturality
    {X : Scheme.{u}} {Ω : Type u} [Field Ω] [IsSepClosed Ω]
    (s : Spec (CommRingCat.of Ω) ⟶ X) (ξ : Spec (CommRingCat.of Ω))
    {F G : Sheaf X.smallEtaleTopology (Type u)} (η : F ⟶ G) :
    (TopCat.Presheaf.stalkFunctor (Type u) (s ξ)).map
        ((etaleZariskiRestriction X (Type u)).map η).hom ≫
        etaleZariskiStalkToGeometricStalk s ξ G =
      etaleZariskiStalkToGeometricStalk s ξ F ≫
        (Scheme.pointSmallEtale s).presheafFiber.map η.hom

lemma

etaleZariski_stalk_map_mono_of_geometric

L88 ↗

EtaleCohomology.etaleZariski_stalk_map_mono_of_geometric

Documentation

Injectivity at a geometric stalk detects injectivity on the actual Zariski stalk.

Source context 4 commands

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

noncomputable section
universe u
open AlgebraicGeometry CategoryTheory Limits TopologicalSpace Opposite
namespace EtaleCohomology

Lean source · statement

lemma etaleZariski_stalk_map_mono_of_geometric
    {X : Scheme.{u}} {Ω : Type u} [Field Ω] [IsSepClosed Ω]
    (s : Spec (CommRingCat.of Ω) ⟶ X) (ξ : Spec (CommRingCat.of Ω))
    {F G : Sheaf X.smallEtaleTopology (Type u)} (η : F ⟶ G)
    [Mono ((Scheme.pointSmallEtale s).presheafFiber.map η.hom)] :
    Mono ((TopCat.Presheaf.stalkFunctor (Type u) (s ξ)).map
      ((etaleZariskiRestriction X (Type u)).map η).hom)

lemma

etaleClosedUnit_zariskiStalk_mono

L115 ↗

EtaleCohomology.etaleClosedUnit_zariskiStalk_mono

Documentation

The actual closed adjunction unit is injective on Zariski stalks along the closed subscheme, after forgetting the module structure.

Source context 4 commands

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

noncomputable section
universe u
open AlgebraicGeometry CategoryTheory Limits TopologicalSpace Opposite
namespace EtaleCohomology

Lean source · statement

lemma etaleClosedUnit_zariskiStalk_mono
    {X Z : Scheme.{u}} (i : Z ⟶ X) [IsClosedImmersion i]
    (Λ : Type u) [CommRing Λ] (F : Sheaf X.smallEtaleTopology (ModuleCat.{u} Λ))
    (z : Z) :
    Mono ((TopCat.Presheaf.stalkFunctor (Type u) (i z)).map
      ((etaleModuleZariskiRestriction X Λ).map
        ((etalePullbackPushforwardAdjunction i Λ).unit.app F)).hom)

theorem

etaleModuleZariskiPullbackComparison_mono

L149 ↗

EtaleCohomology.etaleModuleZariskiPullbackComparison_mono

Documentation

For a closed immersion, topological inverse image of the underlying Zariski sheaf embeds into the underlying actual étale inverse image.

Source context 4 commands

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

noncomputable section
universe u
open AlgebraicGeometry CategoryTheory Limits TopologicalSpace Opposite
namespace EtaleCohomology

Lean source · statement

theorem etaleModuleZariskiPullbackComparison_mono
    {X Z : Scheme.{u}} (i : Z ⟶ X) [IsClosedImmersion i]
    (Λ : Type u) [CommRing Λ] (F : Sheaf X.smallEtaleTopology (ModuleCat.{u} Λ)) :
    Mono ((etaleModuleZariskiPullbackComparison i Λ).app F)

Module documentation

The closed-immersion Zariski comparison is a monomorphism

Declarations

zariskiStalkComparison_naturality

etaleZariski_stalk_map_mono_of_geometric

etaleClosedUnit_zariskiStalk_mono

etaleModuleZariskiPullbackComparison_mono