NYLL
Module

ExtensionMonodromyEvaluation.lean

Nyll.EtaleFundamentalGroups.Cohomology.ExtensionMonodromyEvaluation
8 declarations indexed from sourceView source ↗

Module documentation

Evaluating extension monodromy in a represented abelian sheaf

The actual sheaf of lifts maps to the middle term of the extension. A map from that middle term to a descended finite representation therefore gives an equivariant map on geometric monodromy. Its value is computed in the original abelian stalk, retaining the original inclusion and coefficient.

Imports2
Imported by2

Declarations

abbrev

lifts

L35 ↗
EtaleFundamentalGroups.Cohomology.lifts
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 FintypeCatDiscrete
universe u
namespace EtaleFundamentalGroups.Cohomology
variable {X : Scheme.{u}} [ConnectedSpace X] (A : AddCommGrpCat.{u}) [Finite A]
  {E Q : Sheaf X.smallEtaleTopology AddCommGrpCat.{u}}
  (i : (constantSheaf X.smallEtaleTopology AddCommGrpCat.{u}).obj A ⟶ E)
  (p : E ⟶ Q) (h : i ≫ p = 0) (hs : (ShortComplex.mk i p h).ShortExact)
  (t : (Functor.const X.Etaleᵒᵖ).obj PUnit ⟶ Q.obj ⋙ forget AddCommGrpCat.{u})
  {Ω : Type u} [Field Ω] [IsSepClosed Ω] (ξ : Spec (.of Ω) ⟶ X)
Lean source · statement
abbrev lifts : EtaleFiniteLocallyConstantSetSheaf X
def

extensionMonodromyEvaluation

L41 ↗
EtaleFundamentalGroups.Cohomology.extensionMonodromyEvaluation
Documentation

A monodromy point of the lift sheaf, evaluated in the original middle 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 FintypeCatDiscrete
universe u
namespace EtaleFundamentalGroups.Cohomology
variable {X : Scheme.{u}} [ConnectedSpace X] (A : AddCommGrpCat.{u}) [Finite A]
  {E Q : Sheaf X.smallEtaleTopology AddCommGrpCat.{u}}
  (i : (constantSheaf X.smallEtaleTopology AddCommGrpCat.{u}).obj A ⟶ E)
  (p : E ⟶ Q) (h : i ≫ p = 0) (hs : (ShortComplex.mk i p h).ShortExact)
  (t : (Functor.const X.Etaleᵒᵖ).obj PUnit ⟶ Q.obj ⋙ forget AddCommGrpCat.{u})
  {Ω : Type u} [Field Ω] [IsSepClosed Ω] (ξ : Spec (.of Ω) ⟶ X)
Lean source · full declaration
def extensionMonodromyEvaluation
    (q : (extensionMonodromy A i p h hs t ξ).obj.V) :
    (Scheme.pointSmallEtale ξ).sheafFiber (A := AddCommGrpCat.{u}) |>.obj E :=
  (extensionFiberStalkEquiv (ShortComplex.mk i p h) t ξ
    ((finiteLocallyConstantSetMonodromyStalkIso ξ).hom.app (lifts A i p h hs t) q)).val
theorem

extensionMonodromyEvaluation_exists_germ

L49 ↗
EtaleFundamentalGroups.Cohomology.extensionMonodromyEvaluation_exists_germ
Documentation

An evaluated monodromy point is represented by an actual local lift of the specified quotient section.

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 FintypeCatDiscrete
universe u
namespace EtaleFundamentalGroups.Cohomology
variable {X : Scheme.{u}} [ConnectedSpace X] (A : AddCommGrpCat.{u}) [Finite A]
  {E Q : Sheaf X.smallEtaleTopology AddCommGrpCat.{u}}
  (i : (constantSheaf X.smallEtaleTopology AddCommGrpCat.{u}).obj A ⟶ E)
  (p : E ⟶ Q) (h : i ≫ p = 0) (hs : (ShortComplex.mk i p h).ShortExact)
  (t : (Functor.const X.Etaleᵒᵖ).obj PUnit ⟶ Q.obj ⋙ forget AddCommGrpCat.{u})
  {Ω : Type u} [Field Ω] [IsSepClosed Ω] (ξ : Spec (.of Ω) ⟶ X)
Lean source · statement
theorem extensionMonodromyEvaluation_exists_germ
    (q : (extensionMonodromy A i p h hs t ξ).obj.V) :
    ∃ (U : X.Etale) (x : (Scheme.pointSmallEtale ξ).fiber.obj U)
      (a : E.obj.obj (op U)),
      extensionMonodromyEvaluation A i p h hs t ξ q =
        (Scheme.pointSmallEtale ξ).toPresheafFiber U x E.obj a ∧
      p.hom.app (op U) a = t.app (op U) PUnit.unit
theorem

extensionMonodromyEvaluation_translation

L66 ↗
EtaleFundamentalGroups.Cohomology.extensionMonodromyEvaluation_translation
Documentation

Evaluation preserves translation by the actual constant coefficient.

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 FintypeCatDiscrete
universe u
namespace EtaleFundamentalGroups.Cohomology
variable {X : Scheme.{u}} [ConnectedSpace X] (A : AddCommGrpCat.{u}) [Finite A]
  {E Q : Sheaf X.smallEtaleTopology AddCommGrpCat.{u}}
  (i : (constantSheaf X.smallEtaleTopology AddCommGrpCat.{u}).obj A ⟶ E)
  (p : E ⟶ Q) (h : i ≫ p = 0) (hs : (ShortComplex.mk i p h).ShortExact)
  (t : (Functor.const X.Etaleᵒᵖ).obj PUnit ⟶ Q.obj ⋙ forget AddCommGrpCat.{u})
  {Ω : Type u} [Field Ω] [IsSepClosed Ω] (ξ : Spec (.of Ω) ⟶ X)
Lean source · full declaration
theorem extensionMonodromyEvaluation_translation (a : Multiplicative A)
    (q : (extensionMonodromy A i p h hs t ξ).obj.V) :
    let := extensionMonodromyTorsor A i p h hs t ξ
    extensionMonodromyEvaluation A i p h hs t ξ (a • q) =
      (Scheme.pointSmallEtale ξ).sheafFiber.map i
        ((constantAbelianStalkIso ξ A).inv a.toAdd) +
      extensionMonodromyEvaluation A i p h hs t ξ q := by
  let S := (ShortComplex.mk i p h).map (Scheme.pointSmallEtale ξ).sheafFiber
  let z := quotientSectionStalk (ShortComplex.mk i p h) t ξ
  let e : (extensionMonodromy A i p h hs t ξ).obj.V ≃ abelianExtensionFiber S z :=
    ((finiteLocallyConstantSetMonodromyStalkIso ξ).app
    (lifts A i p h hs t)).toEquiv.trans
      (extensionFiberStalkEquiv (ShortComplex.mk i p h) t ξ)
  let T := extensionMonodromyTorsor A i p h hs t ξ
  change (e (a • q)).val = S.f ((constantAbelianStalkIso ξ A).inv a.toAdd) + (e q).val
  exact extensionFiberTransportTorsor_smul S (shortExact_geometricStalk ξ _ hs)
    z A (constantAbelianStalkIso ξ A).symm e a q
def

representedLiftMap

L90 ↗
EtaleFundamentalGroups.Cohomology.representedLiftMap
Source context 7 commands

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

noncomputable section
open AlgebraicGeometry CategoryTheory CategoryTheory.Limits Opposite EtaleCohomology
open scoped FintypeCatDiscrete
universe u
namespace EtaleFundamentalGroups.Cohomology
variable {X : Scheme.{u}} [ConnectedSpace X] (A : AddCommGrpCat.{u}) [Finite A]
  {E Q : Sheaf X.smallEtaleTopology AddCommGrpCat.{u}}
  (i : (constantSheaf X.smallEtaleTopology AddCommGrpCat.{u}).obj A ⟶ E)
  (p : E ⟶ Q) (h : i ≫ p = 0) (hs : (ShortComplex.mk i p h).ShortExact)
  (t : (Functor.const X.Etaleᵒᵖ).obj PUnit ⟶ Q.obj ⋙ forget AddCommGrpCat.{u})
  {Ω : 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]
  (f : E ⟶ finiteAbelianMonodromySheaf ξ M)
Lean source · statement
def representedLiftMap :
    lifts A i p h hs t ⟶
      (finiteEtaleEquivFiniteLocallyConstantSetSheaf X).functor.obj
        (finiteAbelianCover ξ M)
theorem

representedLiftMap_stalk

L98 ↗
EtaleFundamentalGroups.Cohomology.representedLiftMap_stalk
Source context 7 commands

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

noncomputable section
open AlgebraicGeometry CategoryTheory CategoryTheory.Limits Opposite EtaleCohomology
open scoped FintypeCatDiscrete
universe u
namespace EtaleFundamentalGroups.Cohomology
variable {X : Scheme.{u}} [ConnectedSpace X] (A : AddCommGrpCat.{u}) [Finite A]
  {E Q : Sheaf X.smallEtaleTopology AddCommGrpCat.{u}}
  (i : (constantSheaf X.smallEtaleTopology AddCommGrpCat.{u}).obj A ⟶ E)
  (p : E ⟶ Q) (h : i ≫ p = 0) (hs : (ShortComplex.mk i p h).ShortExact)
  (t : (Functor.const X.Etaleᵒᵖ).obj PUnit ⟶ Q.obj ⋙ forget AddCommGrpCat.{u})
  {Ω : 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]
  (f : E ⟶ finiteAbelianMonodromySheaf ξ M)
Lean source · statement
theorem representedLiftMap_stalk
    (q : (Scheme.pointSmallEtale ξ).sheafFiber.obj
      (extensionFiber (ShortComplex.mk i p h) t)) :
    ((Scheme.pointSmallEtale ξ).sheafFiberCompIso (forget AddCommGrpCat.{u})).hom.app
      (finiteAbelianMonodromySheaf ξ M)
      ((Scheme.pointSmallEtale ξ).sheafFiber.map
        (representedLiftMap A i p h hs t ξ M f).hom q) =
      (Scheme.pointSmallEtale ξ).sheafFiber.map f
        (extensionFiberStalkEquiv (ShortComplex.mk i p h) t ξ q).val
theorem

representedLiftMap_evaluation

L122 ↗
EtaleFundamentalGroups.Cohomology.representedLiftMap_evaluation
Source context 7 commands

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

noncomputable section
open AlgebraicGeometry CategoryTheory CategoryTheory.Limits Opposite EtaleCohomology
open scoped FintypeCatDiscrete
universe u
namespace EtaleFundamentalGroups.Cohomology
variable {X : Scheme.{u}} [ConnectedSpace X] (A : AddCommGrpCat.{u}) [Finite A]
  {E Q : Sheaf X.smallEtaleTopology AddCommGrpCat.{u}}
  (i : (constantSheaf X.smallEtaleTopology AddCommGrpCat.{u}).obj A ⟶ E)
  (p : E ⟶ Q) (h : i ≫ p = 0) (hs : (ShortComplex.mk i p h).ShortExact)
  (t : (Functor.const X.Etaleᵒᵖ).obj PUnit ⟶ Q.obj ⋙ forget AddCommGrpCat.{u})
  {Ω : 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]
  (f : E ⟶ finiteAbelianMonodromySheaf ξ M)
Lean source · statement
theorem representedLiftMap_evaluation
    (q : (extensionMonodromy A i p h hs t ξ).obj.V) :
    finiteAbelianMonodromyStalkAddEquiv ξ M
      ((Scheme.pointSmallEtale ξ).sheafFiber.map f
        (extensionMonodromyEvaluation A i p h hs t ξ q)) =
      finiteAbelianCoverFiberEquiv ξ M
        ((representedMonodromyIso ξ (finiteAbelianCover ξ M)).hom.hom.hom
          (((finiteLocallyConstantSetMonodromy ξ).functor.map
            (representedLiftMap A i p h hs t ξ M f)).hom.hom q))
theorem

extensionMonodromyEvaluation_smul

L156 ↗
EtaleFundamentalGroups.Cohomology.extensionMonodromyEvaluation_smul
Documentation

Evaluation of the actual lift monodromy in a finite descended abelian representation is equivariant for the original representation action.

Source context 7 commands

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

noncomputable section
open AlgebraicGeometry CategoryTheory CategoryTheory.Limits Opposite EtaleCohomology
open scoped FintypeCatDiscrete
universe u
namespace EtaleFundamentalGroups.Cohomology
variable {X : Scheme.{u}} [ConnectedSpace X] (A : AddCommGrpCat.{u}) [Finite A]
  {E Q : Sheaf X.smallEtaleTopology AddCommGrpCat.{u}}
  (i : (constantSheaf X.smallEtaleTopology AddCommGrpCat.{u}).obj A ⟶ E)
  (p : E ⟶ Q) (h : i ≫ p = 0) (hs : (ShortComplex.mk i p h).ShortExact)
  (t : (Functor.const X.Etaleᵒᵖ).obj PUnit ⟶ Q.obj ⋙ forget AddCommGrpCat.{u})
  {Ω : 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]
  (f : E ⟶ finiteAbelianMonodromySheaf ξ M)
Lean source · statement
theorem extensionMonodromyEvaluation_smul (g : Aut (FiniteEtale.fiber ξ))
    (q : (extensionMonodromy A i p h hs t ξ).obj.V) :
    finiteAbelianMonodromyStalkAddEquiv ξ M
      ((Scheme.pointSmallEtale ξ).sheafFiber.map f
        (extensionMonodromyEvaluation A i p h hs t ξ (g • q))) =
      g • finiteAbelianMonodromyStalkAddEquiv ξ M
        ((Scheme.pointSmallEtale ξ).sheafFiber.map f
          (extensionMonodromyEvaluation A i p h hs t ξ q))

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