Module

EtaleSlice.lean

Nyll.EtaleCohomology.Sites.EtaleSlice

5 declarations indexed from sourceView source ↗

Module documentation

Slices of the small étale category

An object of the slice of X.Etale over U is an étale scheme over U.left. The structural map is étale by the existing cancellation theorem for maps between schemes étale over the same base. The inverse functor uses composition with U.hom.

The construction adapts Over.iteratedSliceEquiv to the small étale category: https://github.com/leanprover-community/mathlib4/blob/065356127b1dc0016f66b7283ce0ce2c4055aa55/Mathlib/CategoryTheory/Comma/Over/Basic.lean The small-site functors, explicit proofs and representing-equivalence transport are the new adaptation. The transported presheaf may take values in any universe.

Imports8

Nyll.EtaleCohomology.Sites.EtaleRestriction
Mathlib.AlgebraicGeometry.Morphisms.Etale
Mathlib.CategoryTheory.Adjunction.Basic
Mathlib.CategoryTheory.Comma.Over.Basic
Mathlib.CategoryTheory.Equivalence
Mathlib.CategoryTheory.MorphismProperty.Comma
Mathlib.CategoryTheory.Opposites
Mathlib.CategoryTheory.Yoneda

Imported by3

def

etaleSliceForward

L43 ↗

EtaleCohomology.etaleSliceForward

Documentation

Regard a map to U in the small étale category as an étale scheme over U.left.

Source context 5 commands

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

noncomputable section
open AlgebraicGeometry CategoryTheory
universe u v
namespace EtaleCohomology
variable {X : Scheme.{u}} (U : X.Etale)

Lean source · full declaration

def etaleSliceForward : Over U ⥤ U.left.Etale where
  obj T := MorphismProperty.Over.mk ⊤ T.hom.left inferInstance
  map f := MorphismProperty.Over.homMk f.left.left
    (congrArg (fun k => k.left) f.w)
  map_id T := by apply MorphismProperty.Over.Hom.ext; rfl
  map_comp f g := by apply MorphismProperty.Over.Hom.ext; rfl

def

etaleSliceBackward

L51 ↗

EtaleCohomology.etaleSliceBackward

Documentation

Compose an étale scheme over U.left with U.hom, retaining its map to U.

Source context 5 commands

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

noncomputable section
open AlgebraicGeometry CategoryTheory
universe u v
namespace EtaleCohomology
variable {X : Scheme.{u}} (U : X.Etale)

Lean source · full declaration

def etaleSliceBackward : U.left.Etale ⥤ Over U where
  obj W := Over.mk (MorphismProperty.Over.homMk W.hom (by rfl) :
    (etalePostcompose U.hom).obj W ⟶ U)
  map f := Over.homMk ((etalePostcompose U.hom).map f)
    (MorphismProperty.Over.Hom.ext f.w)
  map_id W := by
    apply Over.OverMorphism.ext
    apply MorphismProperty.Over.Hom.ext
    rfl
  map_comp f g := by
    apply Over.OverMorphism.ext
    apply MorphismProperty.Over.Hom.ext
    rfl

lemma

etaleSliceBackward_forget

L66 ↗

EtaleCohomology.etaleSliceBackward_forget

Documentation

Forgetting the map to U from the inverse slice functor is ordinary postcomposition.

Source context 5 commands

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

noncomputable section
open AlgebraicGeometry CategoryTheory
universe u v
namespace EtaleCohomology
variable {X : Scheme.{u}} (U : X.Etale)

Lean source · statement

lemma etaleSliceBackward_forget :
    etaleSliceBackward U ⋙ Over.forget U = etalePostcompose U.hom

def

etaleSliceEquiv

L70 ↗

EtaleCohomology.etaleSliceEquiv

Documentation

The slice of the small étale category over U is the small étale category of U.left.

Source context 5 commands

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

noncomputable section
open AlgebraicGeometry CategoryTheory
universe u v
namespace EtaleCohomology
variable {X : Scheme.{u}} (U : X.Etale)

Lean source · full declaration

def etaleSliceEquiv : Over U ≌ U.left.Etale where
  functor := etaleSliceForward U
  inverse := etaleSliceBackward U
  unitIso := NatIso.ofComponents (fun T =>
    Over.isoMk (MorphismProperty.Over.isoMk (Iso.refl _) (by
      change (𝟙 T.left.left) ≫ (T.hom.left ≫ U.hom) = T.left.hom
      exact (Category.id_comp _).trans T.hom.w)) (by
        apply MorphismProperty.Over.Hom.ext
        exact Category.id_comp T.hom.left)) (by
      intro T S f
      apply Over.OverMorphism.ext
      apply MorphismProperty.Over.Hom.ext
      change f.left.left ≫ 𝟙 _ = 𝟙 _ ≫ f.left.left
      rw [Category.comp_id, Category.id_comp])
  counitIso := NatIso.ofComponents (fun W =>
    MorphismProperty.Over.isoMk (Iso.refl _) (Category.id_comp W.hom)) (by
      intro W V f
      apply MorphismProperty.Over.Hom.ext
      change f.left ≫ 𝟙 _ = 𝟙 _ ≫ f.left
      rw [Category.comp_id, Category.id_comp])
  functor_unitIso_comp T := by
    apply MorphismProperty.Over.Hom.ext
    exact Category.id_comp (𝟙 T.left.left)

def

representableByEtaleSlice

L96 ↗

EtaleCohomology.representableByEtaleSlice

Documentation

An actual ordinary local representation induces a representation on the slice of the original small étale category.

Source context 5 commands

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

noncomputable section
open AlgebraicGeometry CategoryTheory
universe u v
namespace EtaleCohomology
variable {X : Scheme.{u}} (U : X.Etale)

Lean source · statement

def representableByEtaleSlice (F : X.Etaleᵒᵖ ⥤ Type v) (W : U.left.Etale)
    (h : ((etalePostcompose U.hom).op ⋙ F).RepresentableBy W) :
    ((Over.forget U).op ⋙ F).RepresentableBy ((etaleSliceEquiv U).inverse.obj W)

Module documentation

Slices of the small étale category

Declarations

etaleSliceForward

etaleSliceBackward

etaleSliceBackward_forget

etaleSliceEquiv

representableByEtaleSlice