Module

RepresentedMonodromy.lean

Nyll.EtaleFundamentalGroups.Cohomology.RepresentedMonodromy

3 declarations indexed from sourceView source ↗

Module documentation

The actual monodromy of a descended finite representation

The unit of finite étale representability identifies the monodromy of a represented sheaf with the original geometric fiber. Its comparison with the actual stalk is the existing represented-sheaf stalk comparison.

Imports2

Imported by2

def

representedMonodromyIso

L32 ↗

EtaleFundamentalGroups.Cohomology.representedMonodromyIso

Documentation

Monodromy of the sheaf represented by a finite étale cover is the actual geometric fiber action of that cover.

Source context 6 commands

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

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

Lean source · statement

def representedMonodromyIso (V : FiniteEtale X) :
    (finiteLocallyConstantSetMonodromy ξ).functor.obj
        ((finiteEtaleEquivFiniteLocallyConstantSetSheaf X).functor.obj V) ≅
      (functorToContAction (FiniteEtale.fiber ξ)).obj V

theorem

representedMonodromyIso_stalk

L41 ↗

EtaleFundamentalGroups.Cohomology.representedMonodromyIso_stalk

Documentation

The monodromy isomorphism agrees with the actual geometric stalk comparison, by naturality and the unit-counit identity.

Source context 6 commands

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

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

Lean source · statement

theorem representedMonodromyIso_stalk (V : FiniteEtale X)
    (q : ((finiteLocallyConstantSetMonodromy ξ).functor.obj
      ((finiteEtaleEquivFiniteLocallyConstantSetSheaf X).functor.obj V)).obj.V) :
    (finiteEtaleSheafFiberIso ξ).hom.app V
      ((finiteLocallyConstantSetMonodromyStalkIso ξ).hom.app
        ((finiteEtaleEquivFiniteLocallyConstantSetSheaf X).functor.obj V) q) =
      (representedMonodromyIso ξ V).hom.hom.hom q

theorem

finiteAbelianCoverFiberEquiv_smul

L72 ↗

EtaleFundamentalGroups.Cohomology.finiteAbelianCoverFiberEquiv_smul

Documentation

The geometric fiber comparison of the descended cover is equivariant for the original fundamental-group action.

Source context 7 commands

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

noncomputable section
open AlgebraicGeometry CategoryTheory CategoryTheory.PreGaloisCategory EtaleCohomology
open scoped FintypeCatDiscrete
universe u
namespace EtaleFundamentalGroups.Cohomology
variable {X : Scheme.{u}} [ConnectedSpace X]
  {Ω : Type u} [Field Ω] [IsSepClosed Ω] (ξ : Spec (.of Ω) ⟶ X)
variable (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 finiteAbelianCoverFiberEquiv_smul (g : Aut (FiniteEtale.fiber ξ))
    (x : (FiniteEtale.fiber ξ).obj (finiteAbelianCover ξ M)) :
    finiteAbelianCoverFiberEquiv ξ M (g • x) =
      g • finiteAbelianCoverFiberEquiv ξ M x

Module documentation

The actual monodromy of a descended finite representation

Declarations

representedMonodromyIso

representedMonodromyIso_stalk

finiteAbelianCoverFiberEquiv_smul