Module

RepresenterPullback.lean

Nyll.EtaleFundamentalGroups.Cohomology.RepresenterPullback

5 declarations indexed from sourceView source ↗

Module documentation

Geometric pullback of finite locally constant representers

Inverse image of the actual sheaf of a finite étale cover is the sheaf of its scheme-theoretic base change. Consequently an arbitrary finite locally constant sheaf pulls back to the base change of its existing representer. These are comparisons of actual sheaves, not assumptions about monodromy.

Imports11

Nyll.EtaleCohomology.Constructible.FiniteEtaleSheaf
Nyll.EtaleCohomology.Constructible.FiniteLocallyConstantEquivalence
Nyll.EtaleCohomology.Constructible.FiniteLocallyConstantSet
Nyll.EtaleCohomology.Constructible.Monodromy
Nyll.EtaleCohomology.Sites.RepresentablePullback
Nyll.EtaleFundamentalGroups.GeometricFiber.Functoriality
Mathlib.CategoryTheory.ObjectProperty.FullSubcategory
Mathlib.CategoryTheory.NatIso
Mathlib.CategoryTheory.Functor.FullyFaithful
Mathlib.CategoryTheory.Action.Continuous
Mathlib.Topology.Category.FinTopCat

Imported by2

def

finiteEtaleSheafPullbackIso

L40 ↗

EtaleFundamentalGroups.Cohomology.finiteEtaleSheafPullbackIso

Documentation

Sheaf inverse image agrees naturally with base change of finite étale covers.

Source context 6 commands

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

noncomputable section
open AlgebraicGeometry CategoryTheory EtaleCohomology
open scoped FintypeCatDiscrete
universe u
namespace EtaleFundamentalGroups.Cohomology
variable {X Y : Scheme.{u}} (f : X ⟶ Y)

Lean source · statement

def finiteEtaleSheafPullbackIso :
    finiteEtaleSheaf Y ⋙ etaleSetPullback f ≅
      FiniteEtale.pullback f ⋙ finiteEtaleSheaf X

def

finiteLocallyConstantSetPullback

L49 ↗

EtaleFundamentalGroups.Cohomology.finiteLocallyConstantSetPullback

Documentation

Actual inverse image of a finite locally constant set sheaf.

Source context 6 commands

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

noncomputable section
open AlgebraicGeometry CategoryTheory EtaleCohomology
open scoped FintypeCatDiscrete
universe u
namespace EtaleFundamentalGroups.Cohomology
variable {X Y : Scheme.{u}} (f : X ⟶ Y)

Lean source · full declaration

def finiteLocallyConstantSetPullback :
    EtaleFiniteLocallyConstantSetSheaf Y ⥤ EtaleFiniteLocallyConstantSetSheaf X where
  obj G := ⟨(etaleSetPullback f).obj G.obj, G.property.pullback f⟩
  map k := ObjectProperty.homMk ((etaleSetPullback f).map k.hom)
  map_id G := by
    apply ObjectProperty.hom_ext
    exact (etaleSetPullback f).map_id G.obj
  map_comp k l := by
    apply ObjectProperty.hom_ext
    exact (etaleSetPullback f).map_comp k.hom l.hom

def

finiteLocallyConstantPullbackRepresenterIso

L62 ↗

EtaleFundamentalGroups.Cohomology.finiteLocallyConstantPullbackRepresenterIso

Documentation

The inverse image of the original sheaf is represented by the actual scheme base change of its chosen finite étale representer.

Source context 6 commands

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

noncomputable section
open AlgebraicGeometry CategoryTheory EtaleCohomology
open scoped FintypeCatDiscrete
universe u
namespace EtaleFundamentalGroups.Cohomology
variable {X Y : Scheme.{u}} (f : X ⟶ Y)

Lean source · statement

def finiteLocallyConstantPullbackRepresenterIso
    (G : EtaleFiniteLocallyConstantSetSheaf Y) :
    (etaleSetPullback f).obj G.obj ≅
      (finiteEtaleSheaf X).obj
        ((FiniteEtale.pullback f).obj
          ((finiteEtaleEquivFiniteLocallyConstantSetSheaf Y).inverse.obj G))

def

finiteLocallyConstantPullbackRepresenterNatIso

L78 ↗

EtaleFundamentalGroups.Cohomology.finiteLocallyConstantPullbackRepresenterNatIso

Documentation

The comparison of representers is natural in every morphism of finite locally constant sheaves. It follows by full faithfulness of the actual represented-sheaf functor, rather than a chosen compatibility hypothesis.

Source context 6 commands

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

noncomputable section
open AlgebraicGeometry CategoryTheory EtaleCohomology
open scoped FintypeCatDiscrete
universe u
namespace EtaleFundamentalGroups.Cohomology
variable {X Y : Scheme.{u}} (f : X ⟶ Y)

Lean source · statement

def finiteLocallyConstantPullbackRepresenterNatIso :
    finiteLocallyConstantSetPullback f ⋙
        (finiteEtaleEquivFiniteLocallyConstantSetSheaf X).inverse ≅
      (finiteEtaleEquivFiniteLocallyConstantSetSheaf Y).inverse ⋙
        FiniteEtale.pullback f

def

finiteLocallyConstantSetMonodromyPullbackIso

L110 ↗

EtaleFundamentalGroups.Cohomology.finiteLocallyConstantSetMonodromyPullbackIso

Documentation

Monodromy of actual sheaf inverse image is restriction along the actual scheme-induced homomorphism of étale fundamental groups. This is a natural isomorphism of finite continuous representations.

Source context 7 commands

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

noncomputable section
open AlgebraicGeometry CategoryTheory EtaleCohomology
open scoped FintypeCatDiscrete
universe u
namespace EtaleFundamentalGroups.Cohomology
variable {X Y : Scheme.{u}} (f : X ⟶ Y)
variable [ConnectedSpace X] [ConnectedSpace Y]
  {Ω : Type u} [Field Ω] [IsSepClosed Ω] (ξ : Spec (.of Ω) ⟶ X)

Lean source · statement

def finiteLocallyConstantSetMonodromyPullbackIso :
    finiteLocallyConstantSetPullback f ⋙
        (finiteLocallyConstantSetMonodromy ξ).functor ≅
      (finiteLocallyConstantSetMonodromy (ξ ≫ f)).functor ⋙
        ContAction.res FintypeCat (FiniteEtale.fundamentalGroupHom f ξ)

Module documentation

Geometric pullback of finite locally constant representers

Declarations

finiteEtaleSheafPullbackIso

finiteLocallyConstantSetPullback

finiteLocallyConstantPullbackRepresenterIso

finiteLocallyConstantPullbackRepresenterNatIso

finiteLocallyConstantSetMonodromyPullbackIso