NYLL
Module

FiniteAbelianSheaf.lean

Nyll.EtaleFundamentalGroups.Cohomology.FiniteAbelianSheaf
19 declarations indexed from sourceView source ↗

Module documentation

Abelian étale sheaves from finite monodromy

The abelian operations constructed on the finite étale representing cover give an actual sheaf of abelian groups on the small étale site. The underlying set sheaf is the represented sheaf of that cover. All group operations are transported through finite-product-preserving functors.

Imports8
Imported by2

Declarations

instance

finiteEtaleCartesian

L36 ↗
EtaleFundamentalGroups.Cohomology.finiteEtaleCartesian
Source context 6 commands

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

noncomputable section
open AlgebraicGeometry CategoryTheory CategoryTheory.Limits Opposite
open scoped CategoryTheory.MonObj FintypeCatDiscrete
universe u
namespace EtaleFundamentalGroups.Cohomology
variable (X : Scheme.{u})
Lean source · statement
instance finiteEtaleCartesian : CartesianMonoidalCategory (FiniteEtale X)
instance

finiteEtaleBraided

L39 ↗
EtaleFundamentalGroups.Cohomology.finiteEtaleBraided
Source context 6 commands

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

noncomputable section
open AlgebraicGeometry CategoryTheory CategoryTheory.Limits Opposite
open scoped CategoryTheory.MonObj FintypeCatDiscrete
universe u
namespace EtaleFundamentalGroups.Cohomology
variable (X : Scheme.{u})
Lean source · statement
instance finiteEtaleBraided : BraidedCategory (FiniteEtale X)
instance

etaleCartesian

L42 ↗
EtaleFundamentalGroups.Cohomology.etaleCartesian
Source context 6 commands

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

noncomputable section
open AlgebraicGeometry CategoryTheory CategoryTheory.Limits Opposite
open scoped CategoryTheory.MonObj FintypeCatDiscrete
universe u
namespace EtaleFundamentalGroups.Cohomology
variable (X : Scheme.{u})
Lean source · statement
instance etaleCartesian : CartesianMonoidalCategory X.Etale
instance

etaleBraided

L45 ↗
EtaleFundamentalGroups.Cohomology.etaleBraided
Source context 6 commands

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

noncomputable section
open AlgebraicGeometry CategoryTheory CategoryTheory.Limits Opposite
open scoped CategoryTheory.MonObj FintypeCatDiscrete
universe u
namespace EtaleFundamentalGroups.Cohomology
variable (X : Scheme.{u})
Lean source · statement
instance etaleBraided : BraidedCategory X.Etale
instance

finiteEtaleToEtalePreservesFiniteLimits

L48 ↗
EtaleFundamentalGroups.Cohomology.finiteEtaleToEtalePreservesFiniteLimits
Source context 6 commands

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

noncomputable section
open AlgebraicGeometry CategoryTheory CategoryTheory.Limits Opposite
open scoped CategoryTheory.MonObj FintypeCatDiscrete
universe u
namespace EtaleFundamentalGroups.Cohomology
variable (X : Scheme.{u})
Lean source · statement
instance finiteEtaleToEtalePreservesFiniteLimits :
    PreservesFiniteLimits (EtaleCohomology.finiteEtaleToEtale X)
instance

finiteEtaleToEtaleBraided

L57 ↗
EtaleFundamentalGroups.Cohomology.finiteEtaleToEtaleBraided
Source context 6 commands

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

noncomputable section
open AlgebraicGeometry CategoryTheory CategoryTheory.Limits Opposite
open scoped CategoryTheory.MonObj FintypeCatDiscrete
universe u
namespace EtaleFundamentalGroups.Cohomology
variable (X : Scheme.{u})
Lean source · statement
instance finiteEtaleToEtaleBraided :
    (EtaleCohomology.finiteEtaleToEtale X).Braided
def

abelianRepresentablePresheaf

L61 ↗
EtaleFundamentalGroups.Cohomology.abelianRepresentablePresheaf
Source context 6 commands

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

noncomputable section
open AlgebraicGeometry CategoryTheory CategoryTheory.Limits Opposite
open scoped CategoryTheory.MonObj FintypeCatDiscrete
universe u
namespace EtaleFundamentalGroups.Cohomology
variable (X : Scheme.{u})
Lean source · full declaration
def abelianRepresentablePresheaf (G : CommGrp X.Etale) :
    X.Etaleᵒᵖ ⥤ AddCommGrpCat.{u} where
  obj U := AddCommGrpCat.of (Additive (U.unop ⟶ G.X))
  map f := AddCommGrpCat.ofHom (((yonedaGrpObj G.X).map f).hom.toAdditive)
  map_id U := by
    apply AddCommGrpCat.hom_ext
    apply AddMonoidHom.ext
    intro f
    exact Category.id_comp f
  map_comp f g := by
    apply AddCommGrpCat.hom_ext
    apply AddMonoidHom.ext
    intro h
    exact Category.assoc g.unop f.unop h
def

abelianRepresentableSheaf

L76 ↗
EtaleFundamentalGroups.Cohomology.abelianRepresentableSheaf
Source context 6 commands

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

noncomputable section
open AlgebraicGeometry CategoryTheory CategoryTheory.Limits Opposite
open scoped CategoryTheory.MonObj FintypeCatDiscrete
universe u
namespace EtaleFundamentalGroups.Cohomology
variable (X : Scheme.{u})
Lean source · statement
def abelianRepresentableSheaf (G : CommGrp X.Etale) :
    Sheaf X.smallEtaleTopology AddCommGrpCat.{u}
def

abelianRepresentableSheafMap

L83 ↗
EtaleFundamentalGroups.Cohomology.abelianRepresentableSheafMap
Source context 6 commands

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

noncomputable section
open AlgebraicGeometry CategoryTheory CategoryTheory.Limits Opposite
open scoped CategoryTheory.MonObj FintypeCatDiscrete
universe u
namespace EtaleFundamentalGroups.Cohomology
variable (X : Scheme.{u})
Lean source · full declaration
def abelianRepresentableSheafMap {G H : CommGrp X.Etale} (f : G ⟶ H) :
    abelianRepresentableSheaf X G ⟶ abelianRepresentableSheaf X H where
  hom :=
    { app U := AddCommGrpCat.ofHom (((yonedaGrp.map f.hom).app U).hom.toAdditive)
      naturality U V g := by
        apply AddCommGrpCat.hom_ext
        apply AddMonoidHom.ext
        intro h
        exact Category.assoc g.unop h f.hom.hom.hom }
def

finiteAbelianGroupOnEtale

L100 ↗
EtaleFundamentalGroups.Cohomology.finiteAbelianGroupOnEtale
Source context 7 commands

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

noncomputable section
open AlgebraicGeometry CategoryTheory CategoryTheory.Limits Opposite
open scoped CategoryTheory.MonObj FintypeCatDiscrete
universe u
namespace EtaleFundamentalGroups.Cohomology
variable (X : Scheme.{u})
variable {X} [ConnectedSpace X]
  {Ω : Type u} [Field Ω] [IsSepClosed Ω] (ξ : Spec (.of Ω) ⟶ 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
def finiteAbelianGroupOnEtale : CommGrp X.Etale
def

finiteAbelianMonodromySheaf

L106 ↗
EtaleFundamentalGroups.Cohomology.finiteAbelianMonodromySheaf
Documentation

The actual abelian sheaf obtained by descending a finite continuous abelian representation of the étale fundamental group.

Source context 7 commands

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

noncomputable section
open AlgebraicGeometry CategoryTheory CategoryTheory.Limits Opposite
open scoped CategoryTheory.MonObj FintypeCatDiscrete
universe u
namespace EtaleFundamentalGroups.Cohomology
variable (X : Scheme.{u})
variable {X} [ConnectedSpace X]
  {Ω : Type u} [Field Ω] [IsSepClosed Ω] (ξ : Spec (.of Ω) ⟶ 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
def finiteAbelianMonodromySheaf : Sheaf X.smallEtaleTopology AddCommGrpCat.{u}
def

finiteAbelianMonodromySheafUnderlyingIso

L111 ↗
EtaleFundamentalGroups.Cohomology.finiteAbelianMonodromySheafUnderlyingIso
Documentation

Forgetting the abelian structure recovers the sheaf represented by the finite étale cover constructed from the given representation.

Source context 7 commands

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

noncomputable section
open AlgebraicGeometry CategoryTheory CategoryTheory.Limits Opposite
open scoped CategoryTheory.MonObj FintypeCatDiscrete
universe u
namespace EtaleFundamentalGroups.Cohomology
variable (X : Scheme.{u})
variable {X} [ConnectedSpace X]
  {Ω : Type u} [Field Ω] [IsSepClosed Ω] (ξ : Spec (.of Ω) ⟶ 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
def finiteAbelianMonodromySheafUnderlyingIso :
    (sheafCompose X.smallEtaleTopology (forget AddCommGrpCat.{u})).obj
        (finiteAbelianMonodromySheaf ξ M) ≅
      (EtaleCohomology.finiteEtaleSheaf X).obj (finiteAbelianCover ξ M)
theorem

finiteAbelianMonodromySheaf_isFiniteLocallyConstant

L118 ↗
EtaleFundamentalGroups.Cohomology.finiteAbelianMonodromySheaf_isFiniteLocallyConstant
Documentation

The descended abelian sheaf has a finite locally constant underlying set sheaf.

Source context 7 commands

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

noncomputable section
open AlgebraicGeometry CategoryTheory CategoryTheory.Limits Opposite
open scoped CategoryTheory.MonObj FintypeCatDiscrete
universe u
namespace EtaleFundamentalGroups.Cohomology
variable (X : Scheme.{u})
variable {X} [ConnectedSpace X]
  {Ω : Type u} [Field Ω] [IsSepClosed Ω] (ξ : Spec (.of Ω) ⟶ 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 finiteAbelianMonodromySheaf_isFiniteLocallyConstant :
    EtaleCohomology.IsEtaleFiniteLocallyConstantSet
      ((sheafCompose X.smallEtaleTopology (forget AddCommGrpCat.{u})).obj
        (finiteAbelianMonodromySheaf ξ M))
def

finiteAbelianMonodromyFiberIso

L127 ↗
EtaleFundamentalGroups.Cohomology.finiteAbelianMonodromyFiberIso
Documentation

The underlying actual abelian stalk is the geometric fiber of its finite étale representing cover.

Source context 7 commands

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

noncomputable section
open AlgebraicGeometry CategoryTheory CategoryTheory.Limits Opposite
open scoped CategoryTheory.MonObj FintypeCatDiscrete
universe u
namespace EtaleFundamentalGroups.Cohomology
variable (X : Scheme.{u})
variable {X} [ConnectedSpace X]
  {Ω : Type u} [Field Ω] [IsSepClosed Ω] (ξ : Spec (.of Ω) ⟶ 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
def finiteAbelianMonodromyFiberIso :
    ↥((Scheme.pointSmallEtale ξ).sheafFiber (A := AddCommGrpCat.{u}) |>.obj
      (finiteAbelianMonodromySheaf ξ M)) ≅
      ↥((FiniteEtale.fiber ξ).obj (finiteAbelianCover ξ M))
def

finiteAbelianMonodromyStalkEquiv

L139 ↗
EtaleFundamentalGroups.Cohomology.finiteAbelianMonodromyStalkEquiv
Documentation

The actual geometric stalk of the descended sheaf has the given underlying finite set, via the represented-sheaf comparison and the Galois counit.

Source context 7 commands

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

noncomputable section
open AlgebraicGeometry CategoryTheory CategoryTheory.Limits Opposite
open scoped CategoryTheory.MonObj FintypeCatDiscrete
universe u
namespace EtaleFundamentalGroups.Cohomology
variable (X : Scheme.{u})
variable {X} [ConnectedSpace X]
  {Ω : Type u} [Field Ω] [IsSepClosed Ω] (ξ : Spec (.of Ω) ⟶ 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
def finiteAbelianMonodromyStalkEquiv :
    ↥((Scheme.pointSmallEtale ξ).sheafFiber (A := AddCommGrpCat.{u}) |>.obj
      (finiteAbelianMonodromySheaf ξ M)) ≃ M
def

finiteAbelianMonodromySheafMap

L151 ↗
EtaleFundamentalGroups.Cohomology.finiteAbelianMonodromySheafMap
Documentation

An equivariant additive map descends to a morphism of the actual abelian étale sheaves constructed from the two representations.

Source context 8 commands

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

noncomputable section
open AlgebraicGeometry CategoryTheory CategoryTheory.Limits Opposite
open scoped CategoryTheory.MonObj FintypeCatDiscrete
universe u
namespace EtaleFundamentalGroups.Cohomology
variable (X : Scheme.{u})
variable {X} [ConnectedSpace X]
  {Ω : Type u} [Field Ω] [IsSepClosed Ω] (ξ : Spec (.of Ω) ⟶ X)
  (M : Type u) [AddCommGroup M] [Fintype M]
  [DistribMulAction (Aut (FiniteEtale.fiber ξ)) M]
  [TopologicalSpace M] [DiscreteTopology M]
  [ContinuousSMul (Aut (FiniteEtale.fiber ξ)) M]
variable (N : Type u) [AddCommGroup N] [Fintype N]
  [DistribMulAction (Aut (FiniteEtale.fiber ξ)) N]
  [TopologicalSpace N] [DiscreteTopology N]
  [ContinuousSMul (Aut (FiniteEtale.fiber ξ)) N]
Lean source · statement
def finiteAbelianMonodromySheafMap (α : M →+ N)
    (hα : ∀ (g : Aut (FiniteEtale.fiber ξ)) (x : M), α (g • x) = g • α x) :
    finiteAbelianMonodromySheaf ξ M ⟶ finiteAbelianMonodromySheaf ξ N
theorem

finiteAbelianMonodromySheafMap_underlying

L160 ↗
EtaleFundamentalGroups.Cohomology.finiteAbelianMonodromySheafMap_underlying
Documentation

The underlying morphism of sheaves is induced by the actual map between the finite étale representing covers.

Source context 8 commands

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

noncomputable section
open AlgebraicGeometry CategoryTheory CategoryTheory.Limits Opposite
open scoped CategoryTheory.MonObj FintypeCatDiscrete
universe u
namespace EtaleFundamentalGroups.Cohomology
variable (X : Scheme.{u})
variable {X} [ConnectedSpace X]
  {Ω : Type u} [Field Ω] [IsSepClosed Ω] (ξ : Spec (.of Ω) ⟶ X)
  (M : Type u) [AddCommGroup M] [Fintype M]
  [DistribMulAction (Aut (FiniteEtale.fiber ξ)) M]
  [TopologicalSpace M] [DiscreteTopology M]
  [ContinuousSMul (Aut (FiniteEtale.fiber ξ)) M]
variable (N : Type u) [AddCommGroup N] [Fintype N]
  [DistribMulAction (Aut (FiniteEtale.fiber ξ)) N]
  [TopologicalSpace N] [DiscreteTopology N]
  [ContinuousSMul (Aut (FiniteEtale.fiber ξ)) N]
Lean source · statement
theorem finiteAbelianMonodromySheafMap_underlying (α : M →+ N)
    (hα : ∀ (g : Aut (FiniteEtale.fiber ξ)) (x : M), α (g • x) = g • α x) :
    (sheafCompose X.smallEtaleTopology (forget AddCommGrpCat.{u})).map
        (finiteAbelianMonodromySheafMap ξ M N α hα) =
      (EtaleCohomology.finiteEtaleSheaf X).map
        (finiteAbelianGroupMap ξ M N α hα).hom.hom.hom
theorem

finiteAbelianMonodromySheafMap_add

L169 ↗
EtaleFundamentalGroups.Cohomology.finiteAbelianMonodromySheafMap_add
Documentation

Descent to abelian sheaves preserves addition of equivariant maps.

Source context 9 commands

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

noncomputable section
open AlgebraicGeometry CategoryTheory CategoryTheory.Limits Opposite
open scoped CategoryTheory.MonObj FintypeCatDiscrete
universe u
namespace EtaleFundamentalGroups.Cohomology
variable (X : Scheme.{u})
variable {X} [ConnectedSpace X]
  {Ω : Type u} [Field Ω] [IsSepClosed Ω] (ξ : Spec (.of Ω) ⟶ X)
  (M : Type u) [AddCommGroup M] [Fintype M]
  [DistribMulAction (Aut (FiniteEtale.fiber ξ)) M]
  [TopologicalSpace M] [DiscreteTopology M]
  [ContinuousSMul (Aut (FiniteEtale.fiber ξ)) M]
variable (N : Type u) [AddCommGroup N] [Fintype N]
  [DistribMulAction (Aut (FiniteEtale.fiber ξ)) N]
  [TopologicalSpace N] [DiscreteTopology N]
  [ContinuousSMul (Aut (FiniteEtale.fiber ξ)) N]
open scoped CategoryTheory.Obj in
Lean source · full declaration
theorem finiteAbelianMonodromySheafMap_add (α β : M →+ N)
    (hα : ∀ (g : Aut (FiniteEtale.fiber ξ)) (x : M), α (g • x) = g • α x)
    (hβ : ∀ (g : Aut (FiniteEtale.fiber ξ)) (x : M), β (g • x) = g • β x) :
    finiteAbelianMonodromySheafMap ξ M N (α + β) (fun g x =>
      (congrArg₂ (· + ·) (hα g x) (hβ g x)).trans (smul_add g (α x) (β x)).symm) =
        finiteAbelianMonodromySheafMap ξ M N α hα +
          finiteAbelianMonodromySheafMap ξ M N β hβ := by
  let : CommGrpObj (finiteAbelianCover ξ N) := finiteAbelianCoverGroup ξ N
  let F := EtaleCohomology.finiteEtaleToEtale X
  let f := (finiteAbelianGroupMap ξ M N α hα).hom.hom.hom
  let g := (finiteAbelianGroupMap ξ M N β hβ).hom.hom.hom
  have h := congrArg F.map (finiteAbelianGroupMap_add ξ M N α β hα hβ)
  have hm := F.map_mul f g
  apply Sheaf.hom_ext
  apply NatTrans.ext
  funext U
  apply AddCommGrpCat.hom_ext
  apply AddMonoidHom.ext
  intro s
  exact (congrArg (s.toMul ≫ ·) (h.trans hm)).trans
    (MonObj.comp_mul s.toMul (F.map f) (F.map g))
theorem

finiteAbelianMonodromyStalkEquiv_map

L193 ↗
EtaleFundamentalGroups.Cohomology.finiteAbelianMonodromyStalkEquiv_map
Documentation

Under the actual stalk comparisons, the descended morphism induces the original additive equivariant map on the given finite groups.

Source context 8 commands

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

noncomputable section
open AlgebraicGeometry CategoryTheory CategoryTheory.Limits Opposite
open scoped CategoryTheory.MonObj FintypeCatDiscrete
universe u
namespace EtaleFundamentalGroups.Cohomology
variable (X : Scheme.{u})
variable {X} [ConnectedSpace X]
  {Ω : Type u} [Field Ω] [IsSepClosed Ω] (ξ : Spec (.of Ω) ⟶ X)
  (M : Type u) [AddCommGroup M] [Fintype M]
  [DistribMulAction (Aut (FiniteEtale.fiber ξ)) M]
  [TopologicalSpace M] [DiscreteTopology M]
  [ContinuousSMul (Aut (FiniteEtale.fiber ξ)) M]
variable (N : Type u) [AddCommGroup N] [Fintype N]
  [DistribMulAction (Aut (FiniteEtale.fiber ξ)) N]
  [TopologicalSpace N] [DiscreteTopology N]
  [ContinuousSMul (Aut (FiniteEtale.fiber ξ)) N]
Lean source · statement
theorem finiteAbelianMonodromyStalkEquiv_map (α : M →+ N)
    (hα : ∀ (g : Aut (FiniteEtale.fiber ξ)) (x : M), α (g • x) = g • α x)
    (x : (Scheme.pointSmallEtale ξ).sheafFiber (A := AddCommGrpCat.{u}) |>.obj
      (finiteAbelianMonodromySheaf ξ M)) :
    finiteAbelianMonodromyStalkEquiv ξ N
        ((Scheme.pointSmallEtale ξ).sheafFiber.map
          (finiteAbelianMonodromySheafMap ξ M N α hα) x) =
      α (finiteAbelianMonodromyStalkEquiv ξ M x)

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