Module

ConstantStalk.lean

Nyll.EtaleFundamentalGroups.Cohomology.ConstantStalk

4 declarations indexed from sourceView source ↗

Module documentation

Constant coefficients in actual geometric stalks

The stalk of a constant abelian étale sheaf is canonically its coefficient group. This follows from the connectedness of the filtered neighborhood category and the fact that sheafification does not change stalks. The comparison is compatible with the original constant local sections.

Imports7

Mathlib.Algebra.Category.Grp.AB
Mathlib.Algebra.Category.Grp.Limits
Mathlib.AlgebraicGeometry.Sites.AffineEtale
Mathlib.AlgebraicGeometry.Sites.EtalePoint
Mathlib.CategoryTheory.Limits.Connected
Mathlib.CategoryTheory.Sites.ConstantSheaf
Mathlib.CategoryTheory.Sites.Point.Skyscraper

Imported by3

def

constantAbelianPresheafStalkIso

L36 ↗

EtaleFundamentalGroups.Cohomology.constantAbelianPresheafStalkIso

Documentation

A filtered colimit of the constant abelian presheaf is its original group.

Source context 5 commands

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

noncomputable section
open AlgebraicGeometry CategoryTheory CategoryTheory.Limits Opposite
universe u
namespace EtaleFundamentalGroups.Cohomology
variable {X : Scheme.{u}} {Ω : Type u} [Field Ω] [IsSepClosed Ω]
  (ξ : Spec (.of Ω) ⟶ X)

Lean source · statement

def constantAbelianPresheafStalkIso (A : AddCommGrpCat.{u}) :
    (Scheme.pointSmallEtale ξ).presheafFiber.obj ((Functor.const X.Etaleᵒᵖ).obj A) ≅ A

theorem

constantAbelianPresheafStalkIso_toFiber

L42 ↗

EtaleFundamentalGroups.Cohomology.constantAbelianPresheafStalkIso_toFiber

Documentation

Constant local sections retain their value in the constant presheaf stalk.

Source context 5 commands

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

noncomputable section
open AlgebraicGeometry CategoryTheory CategoryTheory.Limits Opposite
universe u
namespace EtaleFundamentalGroups.Cohomology
variable {X : Scheme.{u}} {Ω : Type u} [Field Ω] [IsSepClosed Ω]
  (ξ : Spec (.of Ω) ⟶ X)

Lean source · statement

theorem constantAbelianPresheafStalkIso_toFiber (A : AddCommGrpCat.{u})
    (U : X.Etale) (x : (Scheme.pointSmallEtale ξ).fiber.obj U) :
    (Scheme.pointSmallEtale ξ).toPresheafFiber U x ((Functor.const X.Etaleᵒᵖ).obj A) ≫
      (constantAbelianPresheafStalkIso ξ A).hom = 𝟙 A

abbrev

constantAbelianStalkIso

L51 ↗

EtaleFundamentalGroups.Cohomology.constantAbelianStalkIso

Documentation

Sheafification and the connected constant colimit identify the actual geometric stalk of the constant sheaf with its coefficient group.

Source context 5 commands

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

noncomputable section
open AlgebraicGeometry CategoryTheory CategoryTheory.Limits Opposite
universe u
namespace EtaleFundamentalGroups.Cohomology
variable {X : Scheme.{u}} {Ω : Type u} [Field Ω] [IsSepClosed Ω]
  (ξ : Spec (.of Ω) ⟶ X)

Lean source · statement

abbrev constantAbelianStalkIso (A : AddCommGrpCat.{u}) :
    (Scheme.pointSmallEtale ξ).sheafFiber.obj
      ((constantSheaf X.smallEtaleTopology AddCommGrpCat.{u}).obj A) ≅ A

theorem

constantAbelianStalkIso_unit

L59 ↗

EtaleFundamentalGroups.Cohomology.constantAbelianStalkIso_unit

Documentation

The comparison sends a constant local section to that very coefficient.

Source context 5 commands

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

noncomputable section
open AlgebraicGeometry CategoryTheory CategoryTheory.Limits Opposite
universe u
namespace EtaleFundamentalGroups.Cohomology
variable {X : Scheme.{u}} {Ω : Type u} [Field Ω] [IsSepClosed Ω]
  (ξ : Spec (.of Ω) ⟶ X)

Lean source · statement

theorem constantAbelianStalkIso_unit (A : AddCommGrpCat.{u})
    (U : X.Etale) (x : (Scheme.pointSmallEtale ξ).fiber.obj U) :
    (toSheafify X.smallEtaleTopology ((Functor.const X.Etaleᵒᵖ).obj A)).app (op U) ≫
      (Scheme.pointSmallEtale ξ).toPresheafFiber U x
        ((constantSheaf X.smallEtaleTopology AddCommGrpCat.{u}).obj A).obj ≫
      (constantAbelianStalkIso ξ A).hom = 𝟙 A

Module documentation

Constant coefficients in actual geometric stalks

Declarations

constantAbelianPresheafStalkIso

constantAbelianPresheafStalkIso_toFiber

constantAbelianStalkIso

constantAbelianStalkIso_unit