Module

RepresentablePullback.lean

Nyll.EtaleCohomology.Sites.RepresentablePullback

9 declarations indexed from sourceView source ↗

Module documentation

Natural inverse-image comparison for represented étale sheaves

The existing objectwise isomorphism between the inverse image of a represented sheaf and the sheaf represented by scheme base change is natural in the represented object. Its adjoint is the identity section, which also proves compatibility with composition of base changes. The composition law uses the already constructed sheaf pullback comparison and the canonical scheme pullback-pasting isomorphism, without changing either construction.

Imports9

Nyll.EtaleCohomology.Sites.BaseChange
Nyll.EtaleCohomology.Sites.SetSheafFunctors
Nyll.EtaleCohomology.Sites.SetPullbackComposition
Nyll.EtaleCohomology.Sites.Subcanonical
Mathlib.CategoryTheory.Adjunction.Basic
Mathlib.CategoryTheory.Adjunction.Unique
Mathlib.CategoryTheory.Sites.Subcanonical
Mathlib.CategoryTheory.MorphismProperty.OverAdjunction
Mathlib.CategoryTheory.NatIso

Imported by2

lemma

etaleSetPullbackYonedaObjIso_hom_homEquiv

L37 ↗

EtaleCohomology.etaleSetPullbackYonedaObjIso_hom_homEquiv

Documentation

Under the inverse-image adjunction, the representable comparison corresponds to the identity section of the base-changed étale scheme.

Source context 5 commands

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

noncomputable section
open AlgebraicGeometry CategoryTheory Limits Opposite
universe u
namespace EtaleCohomology
variable {X Y Z : Scheme.{u}} (f : X ⟶ Y)

Lean source · statement

lemma etaleSetPullbackYonedaObjIso_hom_homEquiv (U : Y.Etale) :
    (etaleSetPullbackPushforwardAdjunction f).homEquiv _ _
        (etaleSetPullbackYonedaObjIso f U).hom =
      Y.smallEtaleTopology.yonedaEquiv.symm (𝟙 ((etaleBaseChange f).obj U))

lemma

etaleSetPullbackYonedaObjIso_hom_comp_homEquiv

L49 ↗

EtaleCohomology.etaleSetPullbackYonedaObjIso_hom_comp_homEquiv

Documentation

The adjoint of a morphism after the representable comparison is its Yoneda section.

Source context 5 commands

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

noncomputable section
open AlgebraicGeometry CategoryTheory Limits Opposite
universe u
namespace EtaleCohomology
variable {X Y Z : Scheme.{u}} (f : X ⟶ Y)

Lean source · statement

lemma etaleSetPullbackYonedaObjIso_hom_comp_homEquiv (U : Y.Etale)
    (G : Sheaf X.smallEtaleTopology (Type u))
    (k : X.smallEtaleTopology.yoneda.obj ((etaleBaseChange f).obj U) ⟶ G) :
    (etaleSetPullbackPushforwardAdjunction f).homEquiv _ _
        ((etaleSetPullbackYonedaObjIso f U).hom ≫ k) =
      Y.smallEtaleTopology.yonedaEquiv.symm (X.smallEtaleTopology.yonedaEquiv k)

lemma

etaleSetPullbackYonedaObjIso_hom_naturality

L60 ↗

EtaleCohomology.etaleSetPullbackYonedaObjIso_hom_naturality

Documentation

The existing objectwise comparison is natural in the represented étale scheme.

Source context 5 commands

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

noncomputable section
open AlgebraicGeometry CategoryTheory Limits Opposite
universe u
namespace EtaleCohomology
variable {X Y Z : Scheme.{u}} (f : X ⟶ Y)

Lean source · statement

lemma etaleSetPullbackYonedaObjIso_hom_naturality {U V : Y.Etale} (k : U ⟶ V) :
    (etaleSetPullback f).map (Y.smallEtaleTopology.yoneda.map k) ≫
        (etaleSetPullbackYonedaObjIso f V).hom =
      (etaleSetPullbackYonedaObjIso f U).hom ≫
        X.smallEtaleTopology.yoneda.map ((etaleBaseChange f).map k)

def

etaleSetPullbackYonedaIso

L73 ↗

EtaleCohomology.etaleSetPullbackYonedaIso

Documentation

Inverse image of represented étale sheaves agrees naturally with scheme base change.

Source context 5 commands

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

noncomputable section
open AlgebraicGeometry CategoryTheory Limits Opposite
universe u
namespace EtaleCohomology
variable {X Y Z : Scheme.{u}} (f : X ⟶ Y)

Lean source · statement

def etaleSetPullbackYonedaIso :
    Y.smallEtaleTopology.yoneda ⋙ etaleSetPullback f ≅
      etaleBaseChange f ⋙ X.smallEtaleTopology.yoneda

lemma

etaleSetPullbackYonedaIso_app

L80 ↗

EtaleCohomology.etaleSetPullbackYonedaIso_app

Documentation

The natural comparison retains exactly the previously constructed objectwise isomorphisms.

Source context 5 commands

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

noncomputable section
open AlgebraicGeometry CategoryTheory Limits Opposite
universe u
namespace EtaleCohomology
variable {X Y Z : Scheme.{u}} (f : X ⟶ Y)

Lean source · statement

lemma etaleSetPullbackYonedaIso_app (U : Y.Etale) :
    (etaleSetPullbackYonedaIso f).app U = etaleSetPullbackYonedaObjIso f U

lemma

pullbackCompIso_hom_homEquiv

L85 ↗

EtaleCohomology.pullbackCompIso_hom_homEquiv

Source context 6 commands

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

noncomputable section
open AlgebraicGeometry CategoryTheory Limits Opposite
universe u
namespace EtaleCohomology
variable {X Y Z : Scheme.{u}} (f : X ⟶ Y)
variable (g : Y ⟶ Z)

Lean source · statement

lemma pullbackCompIso_hom_homEquiv
    (G : Sheaf Z.smallEtaleTopology (Type u)) (H : Sheaf X.smallEtaleTopology (Type u))
    (k : (etaleSetPullback f).obj ((etaleSetPullback g).obj G) ⟶ H) :
    (etaleSetPullbackPushforwardAdjunction (f ≫ g)).homEquiv _ _
        ((etaleSetPullbackCompIso f g).hom.app G ≫ k) =
      (etaleSetPullbackPushforwardAdjunction g).homEquiv _ _
        ((etaleSetPullbackPushforwardAdjunction f).homEquiv _ _ k) ≫
          (etaleSetPushforwardCompIso f g).hom.app H

lemma

iteratedYoneda_homEquiv

L99 ↗

EtaleCohomology.iteratedYoneda_homEquiv

Source context 6 commands

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

noncomputable section
open AlgebraicGeometry CategoryTheory Limits Opposite
universe u
namespace EtaleCohomology
variable {X Y Z : Scheme.{u}} (f : X ⟶ Y)
variable (g : Y ⟶ Z)

Lean source · statement

lemma iteratedYoneda_homEquiv (U : Z.Etale) :
    (etaleSetPullbackPushforwardAdjunction g).homEquiv _ _
      ((etaleSetPullbackPushforwardAdjunction f).homEquiv _ _
        ((etaleSetPullback f).map (etaleSetPullbackYonedaObjIso g U).hom ≫
          (etaleSetPullbackYonedaObjIso f ((etaleBaseChange g).obj U)).hom)) =
      Z.smallEtaleTopology.yonedaEquiv.symm
        (𝟙 ((etaleBaseChange f).obj ((etaleBaseChange g).obj U)))

lemma

iteratedYoneda_pushforwardComp

L111 ↗

EtaleCohomology.iteratedYoneda_pushforwardComp

Source context 6 commands

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

noncomputable section
open AlgebraicGeometry CategoryTheory Limits Opposite
universe u
namespace EtaleCohomology
variable {X Y Z : Scheme.{u}} (f : X ⟶ Y)
variable (g : Y ⟶ Z)

Lean source · full declaration

lemma iteratedYoneda_pushforwardComp (U : Z.Etale) :
    Z.smallEtaleTopology.yonedaEquiv.symm
        (𝟙 ((etaleBaseChange f).obj ((etaleBaseChange g).obj U))) ≫
      (etaleSetPushforwardCompIso f g).hom.app
        (X.smallEtaleTopology.yoneda.obj ((etaleBaseChange f).obj ((etaleBaseChange g).obj U))) =
    Z.smallEtaleTopology.yonedaEquiv.symm
      ((MorphismProperty.Over.pullbackComp
        (P := show MorphismProperty Scheme.{u} from @Etale) (Q := ⊤) f g).hom.app U) := by
  erw [Z.smallEtaleTopology.yonedaEquiv_symm_naturality_right]
  congr 1

lemma

etaleSetPullbackYonedaObjIso_comp_hom

L125 ↗

EtaleCohomology.etaleSetPullbackYonedaObjIso_comp_hom

Documentation

The representable comparison respects composition: the scheme pullback-pasting isomorphism agrees with the comparison for sheaf inverse images and the two successive representable comparisons.

Source context 6 commands

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

noncomputable section
open AlgebraicGeometry CategoryTheory Limits Opposite
universe u
namespace EtaleCohomology
variable {X Y Z : Scheme.{u}} (f : X ⟶ Y)
variable (g : Y ⟶ Z)

Lean source · full declaration

lemma etaleSetPullbackYonedaObjIso_comp_hom (U : Z.Etale) :
    (etaleSetPullbackYonedaObjIso (f ≫ g) U).hom ≫
        X.smallEtaleTopology.yoneda.map
          ((MorphismProperty.Over.pullbackComp
            (P := show MorphismProperty Scheme.{u} from @Etale) (Q := ⊤) f g).hom.app U) =
      (etaleSetPullbackCompIso f g).hom.app (Z.smallEtaleTopology.yoneda.obj U) ≫
        (etaleSetPullback f).map (etaleSetPullbackYonedaObjIso g U).hom ≫
          (etaleSetPullbackYonedaObjIso f ((etaleBaseChange g).obj U)).hom := by
  let e : etaleBaseChange (f ≫ g) ≅ etaleBaseChange g ⋙ etaleBaseChange f :=
    MorphismProperty.Over.pullbackComp
      (P := show MorphismProperty Scheme.{u} from @Etale) (Q := ⊤) f g
  let H := X.smallEtaleTopology.yoneda.obj ((etaleBaseChange f).obj ((etaleBaseChange g).obj U))
  let k : (etaleSetPullback f).obj
      ((etaleSetPullback g).obj (Z.smallEtaleTopology.yoneda.obj U)) ⟶ H :=
    (etaleSetPullback f).map (etaleSetPullbackYonedaObjIso g U).hom ≫
      (etaleSetPullbackYonedaObjIso f ((etaleBaseChange g).obj U)).hom
  apply ((etaleSetPullbackPushforwardAdjunction (f ≫ g)).homEquiv _ H).injective
  have hl := (etaleSetPullbackYonedaObjIso_hom_comp_homEquiv
    (f ≫ g) U H (X.smallEtaleTopology.yoneda.map (e.hom.app U))).trans
      (congrArg Z.smallEtaleTopology.yonedaEquiv.symm
        (X.smallEtaleTopology.yonedaEquiv_yoneda_map (e.hom.app U)))
  have hr := (pullbackCompIso_hom_homEquiv f g
    (Z.smallEtaleTopology.yoneda.obj U) H k).trans
      ((congrArg (fun a => a ≫ (etaleSetPushforwardCompIso f g).hom.app H)
        (iteratedYoneda_homEquiv f g U)).trans (iteratedYoneda_pushforwardComp f g U))
  exact hl.trans hr.symm

Module documentation

Natural inverse-image comparison for represented étale sheaves

Declarations