NYLL
Module

MonodromyPullback.lean

Nyll.EtaleFundamentalGroups.Cohomology.MonodromyPullback
7 declarations indexed from sourceView source ↗

Module documentation

Geometric monodromy under an actual scheme morphism

A morphism from a finite locally constant sheaf into the direct image of another one gives a morphism between their representing finite étale covers after base change. On geometric fibers this is equivariant for the actual homomorphism of fundamental groups induced by the scheme morphism.

Imports4
Imported by2

Declarations

def

finiteEtaleMapOfSheafPushforward

L35 ↗
EtaleFundamentalGroups.Cohomology.finiteEtaleMapOfSheafPushforward
Documentation

The actual Yoneda section of a sheaf morphism into a direct image gives a morphism from the base change of its representing cover.

Source context 6 commands

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

noncomputable section
universe u
open AlgebraicGeometry CategoryTheory CategoryTheory.PreGaloisCategory EtaleCohomology
open scoped FintypeCatDiscrete
namespace EtaleFundamentalGroups.Cohomology
variable {X Y : Scheme.{u}} (f : X ⟶ Y)
Lean source · statement
def finiteEtaleMapOfSheafPushforward (V : FiniteEtale Y) (W : FiniteEtale X)
    (α : (finiteEtaleSheaf Y).obj V ⟶
      (etaleSetPushforward f).obj ((finiteEtaleSheaf X).obj W)) :
    (FiniteEtale.pullback f).obj V ⟶ W
theorem

finiteEtaleMapOfSheafPushforward_naturality

L43 ↗
EtaleFundamentalGroups.Cohomology.finiteEtaleMapOfSheafPushforward_naturality
Source context 6 commands

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

noncomputable section
universe u
open AlgebraicGeometry CategoryTheory CategoryTheory.PreGaloisCategory EtaleCohomology
open scoped FintypeCatDiscrete
namespace EtaleFundamentalGroups.Cohomology
variable {X Y : Scheme.{u}} (f : X ⟶ Y)
Lean source · statement
theorem finiteEtaleMapOfSheafPushforward_naturality
    (V : FiniteEtale Y) (W : FiniteEtale X)
    (α : (finiteEtaleSheaf Y).obj V ⟶
      (etaleSetPushforward f).obj ((finiteEtaleSheaf X).obj W))
    (v : V ⟶ V) (w : W ⟶ W)
    (h : (finiteEtaleSheaf Y).map v ≫ α =
      α ≫ (etaleSetPushforward f).map ((finiteEtaleSheaf X).map w)) :
    (FiniteEtale.pullback f).map v ≫ finiteEtaleMapOfSheafPushforward f V W α =
      finiteEtaleMapOfSheafPushforward f V W α ≫ w
def

finiteLocallyConstantRepresenterPullbackMap

L63 ↗
EtaleFundamentalGroups.Cohomology.finiteLocallyConstantRepresenterPullbackMap
Documentation

The representing-cover morphism associated to a map of actual sheaves.

Source context 6 commands

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

noncomputable section
universe u
open AlgebraicGeometry CategoryTheory CategoryTheory.PreGaloisCategory EtaleCohomology
open scoped FintypeCatDiscrete
namespace EtaleFundamentalGroups.Cohomology
variable {X Y : Scheme.{u}} (f : X ⟶ Y)
Lean source · statement
def finiteLocallyConstantRepresenterPullbackMap
    (F : EtaleFiniteLocallyConstantSetSheaf Y)
    (G : EtaleFiniteLocallyConstantSetSheaf X)
    (α : F.obj ⟶ (etaleSetPushforward f).obj G.obj) :
    (FiniteEtale.pullback f).obj
        ((finiteEtaleEquivFiniteLocallyConstantSetSheaf Y).inverse.obj F) ⟶
      (finiteEtaleEquivFiniteLocallyConstantSetSheaf X).inverse.obj G
theorem

finiteLocallyConstantRepresenterPullbackMap_naturality

L75 ↗
EtaleFundamentalGroups.Cohomology.finiteLocallyConstantRepresenterPullbackMap_naturality
Source context 6 commands

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

noncomputable section
universe u
open AlgebraicGeometry CategoryTheory CategoryTheory.PreGaloisCategory EtaleCohomology
open scoped FintypeCatDiscrete
namespace EtaleFundamentalGroups.Cohomology
variable {X Y : Scheme.{u}} (f : X ⟶ Y)
Lean source · statement
theorem finiteLocallyConstantRepresenterPullbackMap_naturality
    (F : EtaleFiniteLocallyConstantSetSheaf Y)
    (G : EtaleFiniteLocallyConstantSetSheaf X)
    (α : F.obj ⟶ (etaleSetPushforward f).obj G.obj)
    (a : F ⟶ F) (b : G ⟶ G)
    (h : a.hom ≫ α = α ≫ (etaleSetPushforward f).map b.hom) :
    (FiniteEtale.pullback f).map
        ((finiteEtaleEquivFiniteLocallyConstantSetSheaf Y).inverse.map a) ≫
      finiteLocallyConstantRepresenterPullbackMap f F G α =
    finiteLocallyConstantRepresenterPullbackMap f F G α ≫
      (finiteEtaleEquivFiniteLocallyConstantSetSheaf X).inverse.map b
def

finiteLocallyConstantMonodromyPullbackMap

L112 ↗
EtaleFundamentalGroups.Cohomology.finiteLocallyConstantMonodromyPullbackMap
Documentation

The geometric-fiber map uses the canonical base-change fiber comparison and the actual morphism of finite étale representers.

Source context 8 commands

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

noncomputable section
universe u
open AlgebraicGeometry CategoryTheory CategoryTheory.PreGaloisCategory EtaleCohomology
open scoped FintypeCatDiscrete
namespace EtaleFundamentalGroups.Cohomology
variable {X Y : Scheme.{u}} (f : X ⟶ Y)
variable [ConnectedSpace X] [ConnectedSpace Y]
variable {Ω : Type u} [Field Ω] [IsSepClosed Ω] (ξ : Spec (.of Ω) ⟶ X)
Lean source · statement
def finiteLocallyConstantMonodromyPullbackMap
    (F : EtaleFiniteLocallyConstantSetSheaf Y)
    (G : EtaleFiniteLocallyConstantSetSheaf X)
    (α : F.obj ⟶ (etaleSetPushforward f).obj G.obj) :
    ((finiteLocallyConstantSetMonodromy (ξ ≫ f)).functor.obj F).obj.V →
      ((finiteLocallyConstantSetMonodromy ξ).functor.obj G).obj.V
theorem

finiteLocallyConstantMonodromyPullbackMap_smul

L125 ↗
EtaleFundamentalGroups.Cohomology.finiteLocallyConstantMonodromyPullbackMap_smul
Documentation

The geometric map commutes with the fundamental group action through the actual induced homomorphism of geometric fiber functors.

Source context 8 commands

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

noncomputable section
universe u
open AlgebraicGeometry CategoryTheory CategoryTheory.PreGaloisCategory EtaleCohomology
open scoped FintypeCatDiscrete
namespace EtaleFundamentalGroups.Cohomology
variable {X Y : Scheme.{u}} (f : X ⟶ Y)
variable [ConnectedSpace X] [ConnectedSpace Y]
variable {Ω : Type u} [Field Ω] [IsSepClosed Ω] (ξ : Spec (.of Ω) ⟶ X)
Lean source · statement
theorem finiteLocallyConstantMonodromyPullbackMap_smul
    (F : EtaleFiniteLocallyConstantSetSheaf Y)
    (G : EtaleFiniteLocallyConstantSetSheaf X)
    (α : F.obj ⟶ (etaleSetPushforward f).obj G.obj)
    (g : Aut (FiniteEtale.fiber ξ))
    (x : ((finiteLocallyConstantSetMonodromy (ξ ≫ f)).functor.obj F).obj.V) :
    finiteLocallyConstantMonodromyPullbackMap f ξ F G α
        ((FiniteEtale.fundamentalGroupHom f ξ g) • x) =
      g • finiteLocallyConstantMonodromyPullbackMap f ξ F G α x
theorem

finiteLocallyConstantMonodromyPullbackMap_naturality

L150 ↗
EtaleFundamentalGroups.Cohomology.finiteLocallyConstantMonodromyPullbackMap_naturality
Documentation

A commuting diagram of actual sheaves remains a commuting diagram on geometric monodromy after the scheme pullback.

Source context 8 commands

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

noncomputable section
universe u
open AlgebraicGeometry CategoryTheory CategoryTheory.PreGaloisCategory EtaleCohomology
open scoped FintypeCatDiscrete
namespace EtaleFundamentalGroups.Cohomology
variable {X Y : Scheme.{u}} (f : X ⟶ Y)
variable [ConnectedSpace X] [ConnectedSpace Y]
variable {Ω : Type u} [Field Ω] [IsSepClosed Ω] (ξ : Spec (.of Ω) ⟶ X)
Lean source · statement
theorem finiteLocallyConstantMonodromyPullbackMap_naturality
    (F : EtaleFiniteLocallyConstantSetSheaf Y)
    (G : EtaleFiniteLocallyConstantSetSheaf X)
    (α : F.obj ⟶ (etaleSetPushforward f).obj G.obj)
    (a : F ⟶ F) (b : G ⟶ G)
    (h : a.hom ≫ α = α ≫ (etaleSetPushforward f).map b.hom)
    (x : ((finiteLocallyConstantSetMonodromy (ξ ≫ f)).functor.obj F).obj.V) :
    finiteLocallyConstantMonodromyPullbackMap f ξ F G α
        (((finiteLocallyConstantSetMonodromy (ξ ≫ f)).functor.map a).hom.hom x) =
      ((finiteLocallyConstantSetMonodromy ξ).functor.map b).hom.hom
        (finiteLocallyConstantMonodromyPullbackMap f ξ F G α x)

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