Module

FiniteAbelianStalk.lean

Nyll.EtaleFundamentalGroups.Cohomology.FiniteAbelianStalk

3 declarations indexed from sourceView source ↗

Module documentation

Additive stalk comparison for finite abelian monodromy

The actual geometric stalk of the descended abelian sheaf is additively isomorphic to the original finite representation. Naturality for both projections and their sum proves compatibility with addition.

Imports5

Nyll.EtaleFundamentalGroups.Cohomology.FiniteAbelianSheaf
Mathlib.CategoryTheory.Sites.Point.Basic
Mathlib.Algebra.Category.Grp.FilteredColimits
Mathlib.Algebra.Group.Hom.Instances
Mathlib.Topology.Algebra.MulAction

Imported by4

lemma

abelianStalk_map_add

L32 ↗

EtaleFundamentalGroups.Cohomology.abelianStalk_map_add

Source context 5 commands

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

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

Lean source · statement

lemma abelianStalk_map_add
    {F H : Sheaf X.smallEtaleTopology AddCommGrpCat.{u}} (f g : F ⟶ H) :
    (Scheme.pointSmallEtale ξ).sheafFiber.map (f + g) =
      (Scheme.pointSmallEtale ξ).sheafFiber.map f +
        (Scheme.pointSmallEtale ξ).sheafFiber.map g

theorem

finiteAbelianMonodromyStalkEquiv_add

L54 ↗

EtaleFundamentalGroups.Cohomology.finiteAbelianMonodromyStalkEquiv_add

Documentation

The actual stalk comparison respects addition in the finite representation.

Source context 6 commands

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

noncomputable section
open AlgebraicGeometry CategoryTheory CategoryTheory.Limits
universe u
namespace EtaleFundamentalGroups.Cohomology
variable {X : Scheme.{u}} {Ω : Type u} [Field Ω] [IsSepClosed Ω]
  (ξ : Spec (.of Ω) ⟶ X)
variable [ConnectedSpace X]
  (M : Type u) [AddCommGroup M] [Fintype M]
  [DistribMulAction (Aut (FiniteEtale.fiber ξ)) M]
  [TopologicalSpace M] [DiscreteTopology M]
  [ContinuousSMul (Aut (FiniteEtale.fiber ξ)) M]

Lean source · statement

theorem finiteAbelianMonodromyStalkEquiv_add
    (x y : (Scheme.pointSmallEtale ξ).sheafFiber (A := AddCommGrpCat.{u}) |>.obj
      (finiteAbelianMonodromySheaf ξ M)) :
    finiteAbelianMonodromyStalkEquiv ξ M (x + y) =
      finiteAbelianMonodromyStalkEquiv ξ M x +
        finiteAbelianMonodromyStalkEquiv ξ M y

def

finiteAbelianMonodromyStalkAddEquiv

L93 ↗

EtaleFundamentalGroups.Cohomology.finiteAbelianMonodromyStalkAddEquiv

Documentation

The actual geometric stalk is the original finite abelian representation, as an abelian group rather than merely as a finite set.

Source context 6 commands

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

noncomputable section
open AlgebraicGeometry CategoryTheory CategoryTheory.Limits
universe u
namespace EtaleFundamentalGroups.Cohomology
variable {X : Scheme.{u}} {Ω : Type u} [Field Ω] [IsSepClosed Ω]
  (ξ : Spec (.of Ω) ⟶ X)
variable [ConnectedSpace X]
  (M : Type u) [AddCommGroup M] [Fintype M]
  [DistribMulAction (Aut (FiniteEtale.fiber ξ)) M]
  [TopologicalSpace M] [DiscreteTopology M]
  [ContinuousSMul (Aut (FiniteEtale.fiber ξ)) M]

Lean source · full declaration

def finiteAbelianMonodromyStalkAddEquiv :
    ((Scheme.pointSmallEtale ξ).sheafFiber (A := AddCommGrpCat.{u}) |>.obj
      (finiteAbelianMonodromySheaf ξ M)) ≃+ M where
  __ := finiteAbelianMonodromyStalkEquiv ξ M
  map_add' := finiteAbelianMonodromyStalkEquiv_add ξ M

Module documentation

Additive stalk comparison for finite abelian monodromy

Declarations

abelianStalk_map_add

finiteAbelianMonodromyStalkEquiv_add

finiteAbelianMonodromyStalkAddEquiv