NYLL
Module

ModuleMonodromy.lean

Nyll.EtaleCohomology.Constructible.ModuleMonodromy
18 declarations indexed from sourceView source ↗

Module documentation

Linear monodromy on actual geometric stalks

Over a finite commutative coefficient ring, finite type locally constant étale module sheaves carry a continuous linear action of the étale fundamental group on their actual geometric stalks. The underlying set action is naturally isomorphic to the finite continuous monodromy action of the underlying set sheaf.

Linearity is proved from naturality: the square of the sheaf is locally constant, the stalk preserves its product, and monodromy commutes with the projections, their sum, and scalar endomorphisms. Additivity and scalar compatibility of the stalk functor itself are checked using the canonical maps into its defining filtered colimit. No finite field assumption on the base is used.

Imports30
Imported by1

Declarations

abbrev

EtaleFiniteTypeLocallyConstantModuleSheaf

L60 ↗
EtaleCohomology.EtaleFiniteTypeLocallyConstantModuleSheaf
Documentation

The full category of finite type locally constant étale module sheaves.

Source context 5 commands

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

noncomputable section
open AlgebraicGeometry CategoryTheory Limits
open scoped FintypeCatDiscrete
universe u
namespace EtaleCohomology
Lean source · statement
abbrev EtaleFiniteTypeLocallyConstantModuleSheaf (X : Scheme.{u})
    (R : Type u) [CommRing R] : Type (u + 1)
def

finiteLocallyConstantModuleUnderlying

L67 ↗
EtaleCohomology.finiteLocallyConstantModuleUnderlying
Documentation

Forgetting a finite-ring local system gives a finite locally constant set sheaf.

Source context 6 commands

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

noncomputable section
open AlgebraicGeometry CategoryTheory Limits
open scoped FintypeCatDiscrete
universe u
namespace EtaleCohomology
variable {X : Scheme.{u}} {R : Type u} [CommRing R] [Finite R]
Lean source · statement
def finiteLocallyConstantModuleUnderlying :
    EtaleFiniteTypeLocallyConstantModuleSheaf X R ⥤ EtaleFiniteLocallyConstantSetSheaf X
abbrev

finiteLocallyConstantModuleSetMonodromy

L78 ↗
EtaleCohomology.finiteLocallyConstantModuleSetMonodromy
Documentation

The finite continuous set action underlying a finite-ring local system.

Source context 7 commands

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

noncomputable section
open AlgebraicGeometry CategoryTheory Limits
open scoped FintypeCatDiscrete
universe u
namespace EtaleCohomology
variable {X : Scheme.{u}} {R : Type u} [CommRing R] [Finite R]
variable [ConnectedSpace X] {Ω : Type u} [Field Ω] [IsSepClosed Ω]
  (ξ : Spec (.of Ω) ⟶ X)
Lean source · statement
abbrev finiteLocallyConstantModuleSetMonodromy :
    EtaleFiniteTypeLocallyConstantModuleSheaf X R ⥤
      ContAction FintypeCat.{u} (Aut (FiniteEtale.fiber ξ))
def

finiteLocallyConstantModuleStalkIso

L85 ↗
EtaleCohomology.finiteLocallyConstantModuleStalkIso
Documentation

The set-theoretic monodromy carrier is naturally the actual module stalk.

Source context 7 commands

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

noncomputable section
open AlgebraicGeometry CategoryTheory Limits
open scoped FintypeCatDiscrete
universe u
namespace EtaleCohomology
variable {X : Scheme.{u}} {R : Type u} [CommRing R] [Finite R]
variable [ConnectedSpace X] {Ω : Type u} [Field Ω] [IsSepClosed Ω]
  (ξ : Spec (.of Ω) ⟶ X)
Lean source · statement
def finiteLocallyConstantModuleStalkIso :
    finiteLocallyConstantModuleSetMonodromy (R := R) ξ ⋙
      forget₂ (ContAction FintypeCat.{u} (Aut (FiniteEtale.fiber ξ))) FintypeCat ⋙
      forget FintypeCat ≅
    ObjectProperty.ι (IsEtaleFiniteTypeLocallyConstant (X := X) R) ⋙
      (Scheme.pointSmallEtale ξ).sheafFiber (A := ModuleCat R) ⋙ forget (ModuleCat R)
abbrev

moduleStalkSetAction

L101 ↗
EtaleCohomology.moduleStalkSetAction
Documentation

Transport the finite set action onto the underlying set of the actual module stalk.

Source context 7 commands

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

noncomputable section
open AlgebraicGeometry CategoryTheory Limits
open scoped FintypeCatDiscrete
universe u
namespace EtaleCohomology
variable {X : Scheme.{u}} {R : Type u} [CommRing R] [Finite R]
variable [ConnectedSpace X] {Ω : Type u} [Field Ω] [IsSepClosed Ω]
  (ξ : Spec (.of Ω) ⟶ X)
Lean source · full declaration
abbrev moduleStalkSetAction (G : EtaleFiniteTypeLocallyConstantModuleSheaf X R) :
    Action (Type u) (Aut (FiniteEtale.fiber ξ)) where
  V := ↥((Scheme.pointSmallEtale ξ).sheafFiber (A := ModuleCat R) |>.obj G.obj)
  ρ := ((finiteLocallyConstantModuleStalkIso ξ).app G).conj.toMonoidHom.comp
    ((Functor.mapEnd (((finiteLocallyConstantModuleSetMonodromy ξ).obj G).obj.V)
      (forget FintypeCat)).comp
      (((finiteLocallyConstantModuleSetMonodromy ξ).obj G).obj.ρ))
def

moduleStalkSetActionIso

L110 ↗
EtaleCohomology.moduleStalkSetActionIso
Documentation

The transported set action agrees with the finite continuous set action.

Source context 7 commands

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

noncomputable section
open AlgebraicGeometry CategoryTheory Limits
open scoped FintypeCatDiscrete
universe u
namespace EtaleCohomology
variable {X : Scheme.{u}} {R : Type u} [CommRing R] [Finite R]
variable [ConnectedSpace X] {Ω : Type u} [Field Ω] [IsSepClosed Ω]
  (ξ : Spec (.of Ω) ⟶ X)
Lean source · statement
def moduleStalkSetActionIso (G : EtaleFiniteTypeLocallyConstantModuleSheaf X R) :
    ((forget FintypeCat).mapAction (Aut (FiniteEtale.fiber ξ))).obj
      ((finiteLocallyConstantModuleSetMonodromy ξ).obj G).obj ≅ moduleStalkSetAction ξ G
def

moduleStalkSetActionMap

L121 ↗
EtaleCohomology.moduleStalkSetActionMap
Source context 7 commands

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

noncomputable section
open AlgebraicGeometry CategoryTheory Limits
open scoped FintypeCatDiscrete
universe u
namespace EtaleCohomology
variable {X : Scheme.{u}} {R : Type u} [CommRing R] [Finite R]
variable [ConnectedSpace X] {Ω : Type u} [Field Ω] [IsSepClosed Ω]
  (ξ : Spec (.of Ω) ⟶ X)
Lean source · statement
def moduleStalkSetActionMap {G H : EtaleFiniteTypeLocallyConstantModuleSheaf X R}
    (f : G ⟶ H) : moduleStalkSetAction ξ G ⟶ moduleStalkSetAction ξ H
lemma

moduleStalkSetActionMap_hom

L127 ↗
EtaleCohomology.moduleStalkSetActionMap_hom
Source context 7 commands

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

noncomputable section
open AlgebraicGeometry CategoryTheory Limits
open scoped FintypeCatDiscrete
universe u
namespace EtaleCohomology
variable {X : Scheme.{u}} {R : Type u} [CommRing R] [Finite R]
variable [ConnectedSpace X] {Ω : Type u} [Field Ω] [IsSepClosed Ω]
  (ξ : Spec (.of Ω) ⟶ X)
Lean source · statement
lemma moduleStalkSetActionMap_hom {G H : EtaleFiniteTypeLocallyConstantModuleSheaf X R}
    (f : G ⟶ H) : (moduleStalkSetActionMap ξ f).hom =
      (forget (ModuleCat R)).map ((Scheme.pointSmallEtale ξ).sheafFiber.map f.hom)
theorem

moduleStalkSetAction_naturality

L141 ↗
EtaleCohomology.moduleStalkSetAction_naturality
Documentation

Every actual stalk map of module sheaves is equivariant.

Source context 7 commands

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

noncomputable section
open AlgebraicGeometry CategoryTheory Limits
open scoped FintypeCatDiscrete
universe u
namespace EtaleCohomology
variable {X : Scheme.{u}} {R : Type u} [CommRing R] [Finite R]
variable [ConnectedSpace X] {Ω : Type u} [Field Ω] [IsSepClosed Ω]
  (ξ : Spec (.of Ω) ⟶ X)
Lean source · statement
theorem moduleStalkSetAction_naturality
    {G H : EtaleFiniteTypeLocallyConstantModuleSheaf X R} (f : G ⟶ H)
    (γ : Aut (FiniteEtale.fiber ξ))
    (x : (Scheme.pointSmallEtale ξ).sheafFiber (A := ModuleCat R) |>.obj G.obj) :
    (Scheme.pointSmallEtale ξ).sheafFiber.map f.hom ((moduleStalkSetAction ξ G).ρ γ x) =
      (moduleStalkSetAction ξ H).ρ γ ((Scheme.pointSmallEtale ξ).sheafFiber.map f.hom x)
lemma

moduleStalk_map_add

L153 ↗
EtaleCohomology.moduleStalk_map_add
Source context 8 commands

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

noncomputable section
open AlgebraicGeometry CategoryTheory Limits
open scoped FintypeCatDiscrete
universe u
namespace EtaleCohomology
variable {X : Scheme.{u}} {R : Type u} [CommRing R] [Finite R]
variable [ConnectedSpace X] {Ω : Type u} [Field Ω] [IsSepClosed Ω]
  (ξ : Spec (.of Ω) ⟶ X)
omit [Finite R] [ConnectedSpace X] in
Lean source · statement
lemma moduleStalk_map_add
    {G H : Sheaf X.smallEtaleTopology (ModuleCat R)} (f g : G ⟶ H) :
    (Scheme.pointSmallEtale ξ).sheafFiber.map (f + g) =
      (Scheme.pointSmallEtale ξ).sheafFiber.map f +
        (Scheme.pointSmallEtale ξ).sheafFiber.map g
lemma

moduleStalk_map_smul

L169 ↗
EtaleCohomology.moduleStalk_map_smul
Source context 8 commands

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

noncomputable section
open AlgebraicGeometry CategoryTheory Limits
open scoped FintypeCatDiscrete
universe u
namespace EtaleCohomology
variable {X : Scheme.{u}} {R : Type u} [CommRing R] [Finite R]
variable [ConnectedSpace X] {Ω : Type u} [Field Ω] [IsSepClosed Ω]
  (ξ : Spec (.of Ω) ⟶ X)
omit [Finite R] [ConnectedSpace X] in
Lean source · statement
lemma moduleStalk_map_smul
    {G H : Sheaf X.smallEtaleTopology (ModuleCat R)} (r : R) (f : G ⟶ H) :
    (Scheme.pointSmallEtale ξ).sheafFiber.map (r • f) =
      r • (Scheme.pointSmallEtale ξ).sheafFiber.map f
theorem

moduleStalkSetAction_map_add

L183 ↗
EtaleCohomology.moduleStalkSetAction_map_add
Documentation

Naturality for the two projections and their sum gives additivity of monodromy.

Source context 7 commands

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

noncomputable section
open AlgebraicGeometry CategoryTheory Limits
open scoped FintypeCatDiscrete
universe u
namespace EtaleCohomology
variable {X : Scheme.{u}} {R : Type u} [CommRing R] [Finite R]
variable [ConnectedSpace X] {Ω : Type u} [Field Ω] [IsSepClosed Ω]
  (ξ : Spec (.of Ω) ⟶ X)
Lean source · statement
theorem moduleStalkSetAction_map_add (G : EtaleFiniteTypeLocallyConstantModuleSheaf X R)
    (γ : Aut (FiniteEtale.fiber ξ))
    (x y : (Scheme.pointSmallEtale ξ).sheafFiber (A := ModuleCat R) |>.obj G.obj) :
    (moduleStalkSetAction ξ G).ρ γ (x + y) =
      (moduleStalkSetAction ξ G).ρ γ x + (moduleStalkSetAction ξ G).ρ γ y
theorem

moduleStalkSetAction_map_smul

L228 ↗
EtaleCohomology.moduleStalkSetAction_map_smul
Documentation

Naturality for scalar endomorphisms gives compatibility with the coefficient ring.

Source context 7 commands

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

noncomputable section
open AlgebraicGeometry CategoryTheory Limits
open scoped FintypeCatDiscrete
universe u
namespace EtaleCohomology
variable {X : Scheme.{u}} {R : Type u} [CommRing R] [Finite R]
variable [ConnectedSpace X] {Ω : Type u} [Field Ω] [IsSepClosed Ω]
  (ξ : Spec (.of Ω) ⟶ X)
Lean source · statement
theorem moduleStalkSetAction_map_smul (G : EtaleFiniteTypeLocallyConstantModuleSheaf X R)
    (γ : Aut (FiniteEtale.fiber ξ)) (r : R)
    (x : (Scheme.pointSmallEtale ξ).sheafFiber (A := ModuleCat R) |>.obj G.obj) :
    (moduleStalkSetAction ξ G).ρ γ (r • x) = r • (moduleStalkSetAction ξ G).ρ γ x
abbrev

moduleStalkMonodromy

L241 ↗
EtaleCohomology.moduleStalkMonodromy
Documentation

Linear monodromy on the actual geometric stalk, with its original module structure.

Source context 7 commands

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

noncomputable section
open AlgebraicGeometry CategoryTheory Limits
open scoped FintypeCatDiscrete
universe u
namespace EtaleCohomology
variable {X : Scheme.{u}} {R : Type u} [CommRing R] [Finite R]
variable [ConnectedSpace X] {Ω : Type u} [Field Ω] [IsSepClosed Ω]
  (ξ : Spec (.of Ω) ⟶ X)
Lean source · full declaration
abbrev moduleStalkMonodromy (G : EtaleFiniteTypeLocallyConstantModuleSheaf X R) :
    Action (ModuleCat R) (Aut (FiniteEtale.fiber ξ)) where
  V := (Scheme.pointSmallEtale ξ).sheafFiber.obj G.obj
  ρ :=
    { toFun := fun γ => ModuleCat.ofHom
        { toFun := (moduleStalkSetAction ξ G).ρ γ
          map_add' := moduleStalkSetAction_map_add ξ G γ
          map_smul' := moduleStalkSetAction_map_smul ξ G γ }
      map_one' := by
        apply (forget (ModuleCat R)).map_injective
        exact (moduleStalkSetAction ξ G).ρ.map_one
      map_mul' := fun γ δ => by
        apply (forget (ModuleCat R)).map_injective
        exact (moduleStalkSetAction ξ G).ρ.map_mul γ δ }
def

finiteLocallyConstantModuleMonodromy

L257 ↗
EtaleCohomology.finiteLocallyConstantModuleMonodromy
Documentation

Taking the geometric stalk as a linear representation is functorial.

Source context 7 commands

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

noncomputable section
open AlgebraicGeometry CategoryTheory Limits
open scoped FintypeCatDiscrete
universe u
namespace EtaleCohomology
variable {X : Scheme.{u}} {R : Type u} [CommRing R] [Finite R]
variable [ConnectedSpace X] {Ω : Type u} [Field Ω] [IsSepClosed Ω]
  (ξ : Spec (.of Ω) ⟶ X)
Lean source · full declaration
def finiteLocallyConstantModuleMonodromy :
    EtaleFiniteTypeLocallyConstantModuleSheaf X R ⥤
      Action (ModuleCat R) (Aut (FiniteEtale.fiber ξ)) where
  obj := moduleStalkMonodromy ξ
  map f :=
    { hom := (Scheme.pointSmallEtale ξ).sheafFiber.map f.hom
      comm := fun γ => by
        ext x
        exact moduleStalkSetAction_naturality ξ f γ x }
  map_id G := Action.Hom.ext ((Scheme.pointSmallEtale ξ).sheafFiber.map_id G.obj)
  map_comp f g := Action.Hom.ext ((Scheme.pointSmallEtale ξ).sheafFiber.map_comp f.hom g.hom)
def

finiteLocallyConstantModuleMonodromyUnderlyingIso

L270 ↗
EtaleCohomology.finiteLocallyConstantModuleMonodromyUnderlyingIso
Documentation

Forgetting the linear structure recovers finite-set monodromy, naturally.

Source context 7 commands

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

noncomputable section
open AlgebraicGeometry CategoryTheory Limits
open scoped FintypeCatDiscrete
universe u
namespace EtaleCohomology
variable {X : Scheme.{u}} {R : Type u} [CommRing R] [Finite R]
variable [ConnectedSpace X] {Ω : Type u} [Field Ω] [IsSepClosed Ω]
  (ξ : Spec (.of Ω) ⟶ X)
Lean source · statement
def finiteLocallyConstantModuleMonodromyUnderlyingIso :
    finiteLocallyConstantModuleSetMonodromy (R := R) ξ ⋙
      ObjectProperty.ι (Action.isContinuous FintypeCat.{u} (Aut (FiniteEtale.fiber ξ))) ⋙
      (forget FintypeCat).mapAction (Aut (FiniteEtale.fiber ξ)) ≅
    finiteLocallyConstantModuleMonodromy (R := R) ξ ⋙
      (forget (ModuleCat R)).mapAction (Aut (FiniteEtale.fiber ξ))
theorem

finite_moduleStalk

L280 ↗
EtaleCohomology.finite_moduleStalk
Documentation

The actual geometric stalk of a finite-ring local system is a finite module.

Source context 7 commands

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

noncomputable section
open AlgebraicGeometry CategoryTheory Limits
open scoped FintypeCatDiscrete
universe u
namespace EtaleCohomology
variable {X : Scheme.{u}} {R : Type u} [CommRing R] [Finite R]
variable [ConnectedSpace X] {Ω : Type u} [Field Ω] [IsSepClosed Ω]
  (ξ : Spec (.of Ω) ⟶ X)
Lean source · statement
theorem finite_moduleStalk (G : EtaleFiniteTypeLocallyConstantModuleSheaf X R) :
    Finite ((Scheme.pointSmallEtale ξ).sheafFiber (A := ModuleCat R) |>.obj G.obj)
theorem

moduleStalkMonodromy_continuous

L287 ↗
EtaleCohomology.moduleStalkMonodromy_continuous
Documentation

The linear action is continuous when the finite geometric stalk is discrete.

Source context 7 commands

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

noncomputable section
open AlgebraicGeometry CategoryTheory Limits
open scoped FintypeCatDiscrete
universe u
namespace EtaleCohomology
variable {X : Scheme.{u}} {R : Type u} [CommRing R] [Finite R]
variable [ConnectedSpace X] {Ω : Type u} [Field Ω] [IsSepClosed Ω]
  (ξ : Spec (.of Ω) ⟶ X)
Lean source · full declaration
theorem moduleStalkMonodromy_continuous
    (G : EtaleFiniteTypeLocallyConstantModuleSheaf X R) :
    letI : TopologicalSpace ((Scheme.pointSmallEtale ξ).sheafFiber
      (A := ModuleCat R) |>.obj G.obj) := ⊥
    Continuous (fun p : Aut (FiniteEtale.fiber ξ) ×
        ((Scheme.pointSmallEtale ξ).sheafFiber (A := ModuleCat R) |>.obj G.obj) =>
      ((moduleStalkMonodromy ξ G).ρ p.1).hom p.2) := by
  let : TopologicalSpace ((Scheme.pointSmallEtale ξ).sheafFiber
    (A := ModuleCat R) |>.obj G.obj) := ⊥
  have : DiscreteTopology ((Scheme.pointSmallEtale ξ).sheafFiber
    (A := ModuleCat R) |>.obj G.obj) := ⟨rfl⟩
  let A := (finiteLocallyConstantModuleSetMonodromy ξ).obj G
  let e : ↥A.obj.V ≅ ↥((Scheme.pointSmallEtale ξ).sheafFiber
      (A := ModuleCat R) |>.obj G.obj) := (finiteLocallyConstantModuleStalkIso ξ).app G
  have hA : Continuous (fun p : Aut (FiniteEtale.fiber ξ) × A.obj.V =>
      ((forget FintypeCat).map (A.obj.ρ p.1)) p.2) := A.property.continuous_smul
  have hi : Continuous (fun p : Aut (FiniteEtale.fiber ξ) ×
      ((Scheme.pointSmallEtale ξ).sheafFiber (A := ModuleCat R) |>.obj G.obj) =>
      (p.1, e.inv p.2)) :=
    continuous_fst.prodMk (continuous_of_discreteTopology.comp continuous_snd)
  have he : Continuous (fun x : A.obj.V => e.hom x) := continuous_of_discreteTopology
  exact he.comp (hA.comp hi)

Statements and documentation are read from the Lean source at the revision shown. Source entries are not a measure of mathematical completeness.