NYLL
Module

FiniteAbelianConstants.lean

Nyll.EtaleFundamentalGroups.Cohomology.FiniteAbelianConstants
11 declarations indexed from sourceView source ↗

Module documentation

Constant coefficients in finite abelian monodromy descent

For a trivial finite abelian representation, constant equivariant functions give sections of the descended finite étale group. These sections respect addition and define a map from the actual constant abelian sheaf.

Imports6
Imported by2

Declarations

abbrev

baseCover

L39 ↗
EtaleFundamentalGroups.Cohomology.baseCover
Source context 6 commands

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

noncomputable section
open AlgebraicGeometry CategoryTheory CategoryTheory.Limits Opposite EtaleCohomology
open scoped CategoryTheory.MonObj CategoryTheory.Obj FintypeCatDiscrete
universe u
namespace EtaleFundamentalGroups.Cohomology
variable {X : Scheme.{u}} [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]
  (hM : ∀ (g : Aut (FiniteEtale.fiber ξ)) (m : M), g • m = m)
Lean source · statement
abbrev baseCover : FiniteEtale X
def

constantEquivariant

L42 ↗
EtaleFundamentalGroups.Cohomology.constantEquivariant
Source context 6 commands

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

noncomputable section
open AlgebraicGeometry CategoryTheory CategoryTheory.Limits Opposite EtaleCohomology
open scoped CategoryTheory.MonObj CategoryTheory.Obj FintypeCatDiscrete
universe u
namespace EtaleFundamentalGroups.Cohomology
variable {X : Scheme.{u}} [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]
  (hM : ∀ (g : Aut (FiniteEtale.fiber ξ)) (m : M), g • m = m)
Lean source · full declaration
def constantEquivariant (m : M) :
    MulActionHom (id : Aut (FiniteEtale.fiber ξ) → _)
      ((FiniteEtale.fiber ξ).obj (baseCover (X := X))) M where
  toFun := fun _ => m
  map_smul' := fun g _ => (hM g m).symm
def

finiteAbelianConstantSection

L50 ↗
EtaleFundamentalGroups.Cohomology.finiteAbelianConstantSection
Documentation

A coefficient in a trivial representation determines a section of its actual descended finite étale cover.

Source context 6 commands

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

noncomputable section
open AlgebraicGeometry CategoryTheory CategoryTheory.Limits Opposite EtaleCohomology
open scoped CategoryTheory.MonObj CategoryTheory.Obj FintypeCatDiscrete
universe u
namespace EtaleFundamentalGroups.Cohomology
variable {X : Scheme.{u}} [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]
  (hM : ∀ (g : Aut (FiniteEtale.fiber ξ)) (m : M), g • m = m)
Lean source · statement
def finiteAbelianConstantSection (m : M) :
    baseCover (X := X) ⟶ finiteAbelianCover ξ M
theorem

finiteAbelianConstantSection_fiber

L55 ↗
EtaleFundamentalGroups.Cohomology.finiteAbelianConstantSection_fiber
Documentation

The section has the prescribed value in the actual geometric fiber.

Source context 6 commands

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

noncomputable section
open AlgebraicGeometry CategoryTheory CategoryTheory.Limits Opposite EtaleCohomology
open scoped CategoryTheory.MonObj CategoryTheory.Obj FintypeCatDiscrete
universe u
namespace EtaleFundamentalGroups.Cohomology
variable {X : Scheme.{u}} [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]
  (hM : ∀ (g : Aut (FiniteEtale.fiber ξ)) (m : M), g • m = m)
Lean source · statement
theorem finiteAbelianConstantSection_fiber (m : M)
    (x : (FiniteEtale.fiber ξ).obj (baseCover (X := X))) :
    finiteAbelianCoverFiberEquiv ξ M
      ((FiniteEtale.fiber ξ).map (finiteAbelianConstantSection ξ M hM m) x) = m
theorem

constantSection_add

L64 ↗
EtaleFundamentalGroups.Cohomology.constantSection_add
Source context 6 commands

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

noncomputable section
open AlgebraicGeometry CategoryTheory CategoryTheory.Limits Opposite EtaleCohomology
open scoped CategoryTheory.MonObj CategoryTheory.Obj FintypeCatDiscrete
universe u
namespace EtaleFundamentalGroups.Cohomology
variable {X : Scheme.{u}} [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]
  (hM : ∀ (g : Aut (FiniteEtale.fiber ξ)) (m : M), g • m = m)
Lean source · full declaration
theorem constantSection_add (m n : M) :
    let : CartesianMonoidalCategory (FiniteEtale X) := .ofHasFiniteProducts
    let : BraidedCategory (FiniteEtale X) := .ofCartesianMonoidalCategory
    let : CommGrpObj (finiteAbelianCover ξ M) := finiteAbelianCoverGroup ξ M
    finiteAbelianConstantSection ξ M hM (m + n) =
      finiteAbelianConstantSection ξ M hM m * finiteAbelianConstantSection ξ M hM n := by
  let : CartesianMonoidalCategory (FiniteEtale X) := .ofHasFiniteProducts
  let : BraidedCategory (FiniteEtale X) := .ofCartesianMonoidalCategory
  let : CommGrpObj (finiteAbelianCover ξ M) := finiteAbelianCoverGroup ξ M
  let r := finiteAbelianRepresentableBy ξ M
  let e := yonedaGrpObjIsoOfRepresentableBy _
    (finiteAbelianEquivariantPresheaf ξ M ⋙ forget₂ CommGrpCat GrpCat) r
  apply r.homEquiv.injective
  have hm := (e.hom.app (op (baseCover (X := X)))).hom.map_mul
    (finiteAbelianConstantSection ξ M hM m) (finiteAbelianConstantSection ξ M hM n)
  change r.homEquiv (_ * _) = r.homEquiv _ * r.homEquiv _ at hm
  have hs := r.homEquiv.apply_symm_apply (constantEquivariant ξ M hM (m + n))
  have hmn := congrArg₂ (· * ·)
    (r.homEquiv.apply_symm_apply (constantEquivariant ξ M hM m))
    (r.homEquiv.apply_symm_apply (constantEquivariant ξ M hM n))
  exact hs.trans (hmn.symm.trans hm.symm)
def

toBaseCover

L86 ↗
EtaleFundamentalGroups.Cohomology.toBaseCover
Source context 6 commands

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

noncomputable section
open AlgebraicGeometry CategoryTheory CategoryTheory.Limits Opposite EtaleCohomology
open scoped CategoryTheory.MonObj CategoryTheory.Obj FintypeCatDiscrete
universe u
namespace EtaleFundamentalGroups.Cohomology
variable {X : Scheme.{u}} [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]
  (hM : ∀ (g : Aut (FiniteEtale.fiber ξ)) (m : M), g • m = m)
Lean source · statement
def toBaseCover (U : X.Etale) :
    U ⟶ (finiteEtaleToEtale X).obj (baseCover (X := X))
def

constantSectionsPresheaf

L90 ↗
EtaleFundamentalGroups.Cohomology.constantSectionsPresheaf
Source context 6 commands

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

noncomputable section
open AlgebraicGeometry CategoryTheory CategoryTheory.Limits Opposite EtaleCohomology
open scoped CategoryTheory.MonObj CategoryTheory.Obj FintypeCatDiscrete
universe u
namespace EtaleFundamentalGroups.Cohomology
variable {X : Scheme.{u}} [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]
  (hM : ∀ (g : Aut (FiniteEtale.fiber ξ)) (m : M), g • m = m)
Lean source · full declaration
def constantSectionsPresheaf :
    (Functor.const X.Etaleᵒᵖ).obj (AddCommGrpCat.of M) ⟶
      (finiteAbelianMonodromySheaf ξ M).obj where
  app U := AddCommGrpCat.ofHom
    (AddMonoidHom.mk'
      (fun m => Additive.ofMul
        (toBaseCover U.unop ≫ (finiteEtaleToEtale X).map
          (finiteAbelianConstantSection ξ M hM m)))
      (fun m n => by
        let : CartesianMonoidalCategory (FiniteEtale X) := .ofHasFiniteProducts
        let : BraidedCategory (FiniteEtale X) := .ofCartesianMonoidalCategory
        let : CommGrpObj (finiteAbelianCover ξ M) := finiteAbelianCoverGroup ξ M
        let F := finiteEtaleToEtale X
        have h := congrArg F.map (constantSection_add ξ M hM m n)
        have hm := F.map_mul (finiteAbelianConstantSection ξ M hM m)
          (finiteAbelianConstantSection ξ M hM n)
        exact (congrArg (toBaseCover U.unop ≫ ·) (h.trans hm)).trans
          (MonObj.comp_mul (toBaseCover U.unop)
            (F.map (finiteAbelianConstantSection ξ M hM m))
            (F.map (finiteAbelianConstantSection ξ M hM n)))))
  naturality U V f := by
    apply AddCommGrpCat.hom_ext
    apply AddMonoidHom.ext
    intro m
    have hw : toBaseCover V.unop = f.unop ≫ toBaseCover U.unop := by
      apply MorphismProperty.Over.Hom.ext
      exact f.unop.w.symm
    exact (congrArg (· ≫ (finiteEtaleToEtale X).map
      (finiteAbelianConstantSection ξ M hM m)) hw).trans
        (Category.assoc f.unop (toBaseCover U.unop)
          ((finiteEtaleToEtale X).map (finiteAbelianConstantSection ξ M hM m)))
def

finiteAbelianConstantSheafMap

L124 ↗
EtaleFundamentalGroups.Cohomology.finiteAbelianConstantSheafMap
Documentation

Constant equivariant sections extend uniquely through sheafification to a homomorphism from the actual constant abelian sheaf.

Source context 6 commands

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

noncomputable section
open AlgebraicGeometry CategoryTheory CategoryTheory.Limits Opposite EtaleCohomology
open scoped CategoryTheory.MonObj CategoryTheory.Obj FintypeCatDiscrete
universe u
namespace EtaleFundamentalGroups.Cohomology
variable {X : Scheme.{u}} [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]
  (hM : ∀ (g : Aut (FiniteEtale.fiber ξ)) (m : M), g • m = m)
Lean source · statement
def finiteAbelianConstantSheafMap :
    (constantSheaf X.smallEtaleTopology AddCommGrpCat.{u}).obj (AddCommGrpCat.of M) ⟶
      finiteAbelianMonodromySheaf ξ M
theorem

constantSection_stalk

L130 ↗
EtaleFundamentalGroups.Cohomology.constantSection_stalk
Source context 6 commands

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

noncomputable section
open AlgebraicGeometry CategoryTheory CategoryTheory.Limits Opposite EtaleCohomology
open scoped CategoryTheory.MonObj CategoryTheory.Obj FintypeCatDiscrete
universe u
namespace EtaleFundamentalGroups.Cohomology
variable {X : Scheme.{u}} [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]
  (hM : ∀ (g : Aut (FiniteEtale.fiber ξ)) (m : M), g • m = m)
Lean source · statement
theorem constantSection_stalk (U : X.Etale)
    (x : (Scheme.pointSmallEtale ξ).fiber.obj U) (m : M) :
    finiteAbelianMonodromyStalkEquiv ξ M
      ((Scheme.pointSmallEtale ξ).toPresheafFiber U x
        (finiteAbelianMonodromySheaf ξ M).obj
          ((constantSectionsPresheaf ξ M hM).app (op U) m)) = m
theorem

finiteAbelianConstantSheafMap_stalk

L167 ↗
EtaleFundamentalGroups.Cohomology.finiteAbelianConstantSheafMap_stalk
Documentation

The map from the constant sheaf has the prescribed coefficient map on the actual geometric stalk.

Source context 6 commands

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

noncomputable section
open AlgebraicGeometry CategoryTheory CategoryTheory.Limits Opposite EtaleCohomology
open scoped CategoryTheory.MonObj CategoryTheory.Obj FintypeCatDiscrete
universe u
namespace EtaleFundamentalGroups.Cohomology
variable {X : Scheme.{u}} [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]
  (hM : ∀ (g : Aut (FiniteEtale.fiber ξ)) (m : M), g • m = m)
Lean source · statement
theorem finiteAbelianConstantSheafMap_stalk
    (z : (Scheme.pointSmallEtale ξ).sheafFiber (A := AddCommGrpCat.{u}) |>.obj
      ((constantSheaf X.smallEtaleTopology AddCommGrpCat.{u}).obj (AddCommGrpCat.of M))) :
    finiteAbelianMonodromyStalkAddEquiv ξ M
      ((Scheme.pointSmallEtale ξ).sheafFiber.map (finiteAbelianConstantSheafMap ξ M hM) z) =
        (constantAbelianStalkIso ξ (AddCommGrpCat.of M)).hom z
def

finiteAbelianConstantSheafIso

L206 ↗
EtaleFundamentalGroups.Cohomology.finiteAbelianConstantSheafIso
Documentation

A trivial finite abelian representation descends to the actual constant abelian sheaf with those coefficients.

Source context 6 commands

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

noncomputable section
open AlgebraicGeometry CategoryTheory CategoryTheory.Limits Opposite EtaleCohomology
open scoped CategoryTheory.MonObj CategoryTheory.Obj FintypeCatDiscrete
universe u
namespace EtaleFundamentalGroups.Cohomology
variable {X : Scheme.{u}} [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]
  (hM : ∀ (g : Aut (FiniteEtale.fiber ξ)) (m : M), g • m = m)
Lean source · statement
def finiteAbelianConstantSheafIso :
    (constantSheaf X.smallEtaleTopology AddCommGrpCat.{u}).obj (AddCommGrpCat.of M) ≅
      finiteAbelianMonodromySheaf ξ M

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