Module

FiniteAbelianExact.lean

Nyll.EtaleFundamentalGroups.Cohomology.FiniteAbelianExact

4 declarations indexed from sourceView source ↗

Module documentation

Descent of exact sequences of finite abelian representations

The finite étale representing covers and their abelian sheaves carry the original maps on actual geometric stalks. Consequently an exact sequence of finite continuous representations descends to an exact sequence of actual étale sheaves, with no extra descent or comparison assumption.

Imports3

Imported by2

theorem

finiteAbelianMonodromySheafMap_comp_zero

L48 ↗

EtaleFundamentalGroups.Cohomology.finiteAbelianMonodromySheafMap_comp_zero

Documentation

A zero composite of equivariant homomorphisms remains zero on the actual descended abelian sheaves.

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}} [ConnectedSpace X]
  {Ω : Type u} [Field Ω] [IsSepClosed Ω] (ξ : Spec (.of Ω) ⟶ X)
  (M N P : Type u) [AddCommGroup M] [AddCommGroup N] [AddCommGroup P]
  [Fintype M] [Fintype N] [Fintype P]
  [DistribMulAction (Aut (FiniteEtale.fiber ξ)) M]
  [DistribMulAction (Aut (FiniteEtale.fiber ξ)) N]
  [DistribMulAction (Aut (FiniteEtale.fiber ξ)) P]
  [TopologicalSpace M] [TopologicalSpace N] [TopologicalSpace P]
  [DiscreteTopology M] [DiscreteTopology N] [DiscreteTopology P]
  [ContinuousSMul (Aut (FiniteEtale.fiber ξ)) M]
  [ContinuousSMul (Aut (FiniteEtale.fiber ξ)) N]
  [ContinuousSMul (Aut (FiniteEtale.fiber ξ)) P]
  (α : M →+ N) (β : N →+ P)
  (hα : ∀ (g : Aut (FiniteEtale.fiber ξ)) (x : M), α (g • x) = g • α x)
  (hβ : ∀ (g : Aut (FiniteEtale.fiber ξ)) (x : N), β (g • x) = g • β x)
  (w : (AddCommGrpCat.ofHom α) ≫ AddCommGrpCat.ofHom β = 0)
include w in

Lean source · statement

theorem finiteAbelianMonodromySheafMap_comp_zero :
    finiteAbelianMonodromySheafMap ξ M N α hα ≫
      finiteAbelianMonodromySheafMap ξ N P β hβ = 0

def

finiteAbelianMonodromyComplex

L66 ↗

EtaleFundamentalGroups.Cohomology.finiteAbelianMonodromyComplex

Documentation

The actual short complex obtained by descending finite abelian representations and their two equivariant maps.

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}} [ConnectedSpace X]
  {Ω : Type u} [Field Ω] [IsSepClosed Ω] (ξ : Spec (.of Ω) ⟶ X)
  (M N P : Type u) [AddCommGroup M] [AddCommGroup N] [AddCommGroup P]
  [Fintype M] [Fintype N] [Fintype P]
  [DistribMulAction (Aut (FiniteEtale.fiber ξ)) M]
  [DistribMulAction (Aut (FiniteEtale.fiber ξ)) N]
  [DistribMulAction (Aut (FiniteEtale.fiber ξ)) P]
  [TopologicalSpace M] [TopologicalSpace N] [TopologicalSpace P]
  [DiscreteTopology M] [DiscreteTopology N] [DiscreteTopology P]
  [ContinuousSMul (Aut (FiniteEtale.fiber ξ)) M]
  [ContinuousSMul (Aut (FiniteEtale.fiber ξ)) N]
  [ContinuousSMul (Aut (FiniteEtale.fiber ξ)) P]
  (α : M →+ N) (β : N →+ P)
  (hα : ∀ (g : Aut (FiniteEtale.fiber ξ)) (x : M), α (g • x) = g • α x)
  (hβ : ∀ (g : Aut (FiniteEtale.fiber ξ)) (x : N), β (g • x) = g • β x)
  (w : (AddCommGrpCat.ofHom α) ≫ AddCommGrpCat.ofHom β = 0)

Lean source · statement

def finiteAbelianMonodromyComplex :
    ShortComplex (Sheaf X.smallEtaleTopology AddCommGrpCat.{u})

def

finiteAbelianMonodromyComplex_stalkIso

L73 ↗

EtaleFundamentalGroups.Cohomology.finiteAbelianMonodromyComplex_stalkIso

Documentation

Its geometric stalk is the original short complex of finite abelian groups.

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}} [ConnectedSpace X]
  {Ω : Type u} [Field Ω] [IsSepClosed Ω] (ξ : Spec (.of Ω) ⟶ X)
  (M N P : Type u) [AddCommGroup M] [AddCommGroup N] [AddCommGroup P]
  [Fintype M] [Fintype N] [Fintype P]
  [DistribMulAction (Aut (FiniteEtale.fiber ξ)) M]
  [DistribMulAction (Aut (FiniteEtale.fiber ξ)) N]
  [DistribMulAction (Aut (FiniteEtale.fiber ξ)) P]
  [TopologicalSpace M] [TopologicalSpace N] [TopologicalSpace P]
  [DiscreteTopology M] [DiscreteTopology N] [DiscreteTopology P]
  [ContinuousSMul (Aut (FiniteEtale.fiber ξ)) M]
  [ContinuousSMul (Aut (FiniteEtale.fiber ξ)) N]
  [ContinuousSMul (Aut (FiniteEtale.fiber ξ)) P]
  (α : M →+ N) (β : N →+ P)
  (hα : ∀ (g : Aut (FiniteEtale.fiber ξ)) (x : M), α (g • x) = g • α x)
  (hβ : ∀ (g : Aut (FiniteEtale.fiber ξ)) (x : N), β (g • x) = g • β x)
  (w : (AddCommGrpCat.ofHom α) ≫ AddCommGrpCat.ofHom β = 0)

Lean source · statement

def finiteAbelianMonodromyComplex_stalkIso :
    (finiteAbelianMonodromyComplex ξ M N P α β hα hβ w).map
        (Scheme.pointSmallEtale ξ).sheafFiber ≅
      ShortComplex.mk (AddCommGrpCat.ofHom α) (AddCommGrpCat.ofHom β) w

theorem

finiteAbelianMonodromyComplex_shortExact

L92 ↗

EtaleFundamentalGroups.Cohomology.finiteAbelianMonodromyComplex_shortExact

Documentation

Descent of a short exact sequence of finite continuous abelian representations is short exact in the ambient category of étale abelian sheaves.

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}} [ConnectedSpace X]
  {Ω : Type u} [Field Ω] [IsSepClosed Ω] (ξ : Spec (.of Ω) ⟶ X)
  (M N P : Type u) [AddCommGroup M] [AddCommGroup N] [AddCommGroup P]
  [Fintype M] [Fintype N] [Fintype P]
  [DistribMulAction (Aut (FiniteEtale.fiber ξ)) M]
  [DistribMulAction (Aut (FiniteEtale.fiber ξ)) N]
  [DistribMulAction (Aut (FiniteEtale.fiber ξ)) P]
  [TopologicalSpace M] [TopologicalSpace N] [TopologicalSpace P]
  [DiscreteTopology M] [DiscreteTopology N] [DiscreteTopology P]
  [ContinuousSMul (Aut (FiniteEtale.fiber ξ)) M]
  [ContinuousSMul (Aut (FiniteEtale.fiber ξ)) N]
  [ContinuousSMul (Aut (FiniteEtale.fiber ξ)) P]
  (α : M →+ N) (β : N →+ P)
  (hα : ∀ (g : Aut (FiniteEtale.fiber ξ)) (x : M), α (g • x) = g • α x)
  (hβ : ∀ (g : Aut (FiniteEtale.fiber ξ)) (x : N), β (g • x) = g • β x)
  (w : (AddCommGrpCat.ofHom α) ≫ AddCommGrpCat.ofHom β = 0)

Lean source · statement

theorem finiteAbelianMonodromyComplex_shortExact
    (h : (ShortComplex.mk (AddCommGrpCat.ofHom α) (AddCommGrpCat.ofHom β) w).ShortExact) :
    (finiteAbelianMonodromyComplex ξ M N P α β hα hβ w).ShortExact

Module documentation

Descent of exact sequences of finite abelian representations

Declarations

finiteAbelianMonodromySheafMap_comp_zero

finiteAbelianMonodromyComplex

finiteAbelianMonodromyComplex_stalkIso

finiteAbelianMonodromyComplex_shortExact