NYLL
Module

PullbackSections.lean

Nyll.EtaleCohomology.Sites.PullbackSections
7 declarations indexed from sourceView source ↗

Module documentation

Actual sections pulled through a local factor

A commuting scheme square supplies an actual morphism into the small-site base change. Restricting the existing adjunction unit along this morphism pulls sections to the source. Naturality retains equations of local lifts against a global section, including along a finite refinement.

Imports5
Imported by9

Declarations

def

etaleBaseChangeLift

L34 ↗
EtaleCohomology.etaleBaseChangeLift
Documentation

The actual small-site arrow supplied by a commuting scheme square.

Source context 5 commands

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

noncomputable section
universe u
open AlgebraicGeometry CategoryTheory Limits Opposite
namespace EtaleCohomology
variable {X Y : Scheme.{u}} (q : Y ⟶ X)
Lean source · statement
def etaleBaseChangeLift {U : Y.Etale} {V : X.Etale}
    (l : U.left ⟶ V.left) (hl : l ≫ V.hom = U.hom ≫ q) :
    U ⟶ (etaleBaseChange q).obj V
def

etalePullbackSectionMap

L44 ↗
EtaleCohomology.etalePullbackSectionMap
Documentation

Pull a section through an actual local factor, using the chosen unit.

Source context 6 commands

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

noncomputable section
universe u
open AlgebraicGeometry CategoryTheory Limits Opposite
namespace EtaleCohomology
variable {X Y : Scheme.{u}} (q : Y ⟶ X)
variable (Λ : Type u) [CommRing Λ]
Lean source · statement
def etalePullbackSectionMap (F : Sheaf X.smallEtaleTopology (ModuleCat.{u} Λ))
    {U : Y.Etale} {V : X.Etale} (l : U.left ⟶ V.left)
    (hl : l ≫ V.hom = U.hom ≫ q) :
    F.obj.obj (op V) ⟶ ((etalePullback q Λ).obj F).obj.obj (op U)
def

etalePullbackGlobalSectionsMap

L52 ↗
EtaleCohomology.etalePullbackGlobalSectionsMap
Documentation

The actual map on global sections induced by inverse image.

Source context 6 commands

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

noncomputable section
universe u
open AlgebraicGeometry CategoryTheory Limits Opposite
namespace EtaleCohomology
variable {X Y : Scheme.{u}} (q : Y ⟶ X)
variable (Λ : Type u) [CommRing Λ]
Lean source · statement
def etalePullbackGlobalSectionsMap (F : Sheaf X.smallEtaleTopology (ModuleCat.{u} Λ)) :
    F.obj.obj (op (Scheme.Etale.mk (𝟙 X))) ⟶
      ((etalePullback q Λ).obj F).obj.obj (op (Scheme.Etale.mk (𝟙 Y)))
lemma

etalePullbackSectionMap_naturality

L58 ↗
EtaleCohomology.etalePullbackSectionMap_naturality
Documentation

Pulling a local section commutes with an actual sheaf morphism.

Source context 6 commands

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

noncomputable section
universe u
open AlgebraicGeometry CategoryTheory Limits Opposite
namespace EtaleCohomology
variable {X Y : Scheme.{u}} (q : Y ⟶ X)
variable (Λ : Type u) [CommRing Λ]
Lean source · statement
lemma etalePullbackSectionMap_naturality
    {F G : Sheaf X.smallEtaleTopology (ModuleCat.{u} Λ)} (η : F ⟶ G)
    {U : Y.Etale} {V : X.Etale} (l : U.left ⟶ V.left)
    (hl : l ≫ V.hom = U.hom ≫ q) :
    etalePullbackSectionMap q Λ F l hl ≫ ((etalePullback q Λ).map η).hom.app (op U) =
      η.hom.app (op V) ≫ etalePullbackSectionMap q Λ G l hl
lemma

etaleBaseChange_identity_hom_eq

L86 ↗
EtaleCohomology.etaleBaseChange_identity_hom_eq
Source context 6 commands

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

noncomputable section
universe u
open AlgebraicGeometry CategoryTheory Limits Opposite
namespace EtaleCohomology
variable {X Y : Scheme.{u}} (q : Y ⟶ X)
variable (Λ : Type u) [CommRing Λ]
Lean source · statement
lemma etaleBaseChange_identity_hom_eq {U : Y.Etale}
    (a b : U ⟶ (etaleBaseChange q).obj (Scheme.Etale.mk (𝟙 X))) : a = b
lemma

etalePullbackSectionMap_global_restriction

L94 ↗
EtaleCohomology.etalePullbackSectionMap_global_restriction
Documentation

A local pullback of the restriction of a global section is the restriction of its actual global pullback.

Source context 6 commands

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

noncomputable section
universe u
open AlgebraicGeometry CategoryTheory Limits Opposite
namespace EtaleCohomology
variable {X Y : Scheme.{u}} (q : Y ⟶ X)
variable (Λ : Type u) [CommRing Λ]
Lean source · full declaration
lemma etalePullbackSectionMap_global_restriction
    (G : Sheaf X.smallEtaleTopology (ModuleCat.{u} Λ))
    {U : Y.Etale} {V : X.Etale} (g : V ⟶ Scheme.Etale.mk (𝟙 X))
    (l : U.left ⟶ V.left) (hl : l ≫ V.hom = U.hom ≫ q) :
    G.obj.map g.op ≫ etalePullbackSectionMap q Λ G l hl =
      etalePullbackGlobalSectionsMap q Λ G ≫ ((etalePullback q Λ).obj G).obj.map
        (MorphismProperty.Over.homMk
          (P := show MorphismProperty Scheme.{u} from @Etale) (Q := ⊤)
          (A := U) (B := Scheme.Etale.mk (𝟙 Y)) U.hom (Category.comp_id U.hom)).op := by
  let H : Y.Etaleᵒᵖ ⥤ ModuleCat.{u} Λ := ((etalePullback q Λ).obj G).obj
  let V₀ : X.Etale := Scheme.Etale.mk (𝟙 X)
  let U₀ : Y.Etale := Scheme.Etale.mk (𝟙 Y)
  let W : Y.Etale := (etaleBaseChange q).obj V
  let W₀ : Y.Etale := (etaleBaseChange q).obj V₀
  let a : U ⟶ W := etaleBaseChangeLift q l hl
  let b : U₀ ⟶ W₀ :=
    etaleBaseChangeLift q q ((Category.comp_id q).trans (Category.id_comp q).symm)
  let j : U ⟶ U₀ := MorphismProperty.Over.homMk
    (P := show MorphismProperty Scheme.{u} from @Etale) (Q := ⊤)
    U.hom (Category.comp_id U.hom)
  let gq : W ⟶ W₀ := (etaleBaseChange q).map g
  have hab : a ≫ gq = j ≫ b := etaleBaseChange_identity_hom_eq q _ _
  let uV : G.obj.obj (op V) ⟶ H.obj (op W) :=
    ((etalePullbackPushforwardAdjunction q Λ).unit.app G).hom.app (op V)
  let u₀ : G.obj.obj (op V₀) ⟶ H.obj (op W₀) :=
    ((etalePullbackPushforwardAdjunction q Λ).unit.app G).hom.app (op V₀)
  let r : G.obj.obj (op V₀) ⟶ G.obj.obj (op V) := G.obj.map g.op
  let ha : H.obj (op W) ⟶ H.obj (op U) := H.map a.op
  let hb : H.obj (op W₀) ⟶ H.obj (op U₀) := H.map b.op
  let hj : H.obj (op U₀) ⟶ H.obj (op U) := H.map j.op
  let hg : H.obj (op W₀) ⟶ H.obj (op W) := H.map gq.op
  have hunit : r ≫ uV = u₀ ≫ hg :=
    ((etalePullbackPushforwardAdjunction q Λ).unit.app G).hom.naturality g.op
  have hmap : hg ≫ ha = hb ≫ hj := by
    calc
      hg ≫ ha = H.map (a ≫ gq).op := (H.map_comp gq.op a.op).symm
      _ = H.map (j ≫ b).op := congrArg (fun k : U ⟶ W₀ => H.map k.op) hab
      _ = hb ≫ hj := H.map_comp b.op j.op
  change r ≫ (uV ≫ ha) = (u₀ ≫ hb) ≫ hj
  rw [← Category.assoc, hunit, Category.assoc, hmap, ← Category.assoc]
theorem

etalePullbackSectionMap_local_lift

L137 ↗
EtaleCohomology.etalePullbackSectionMap_local_lift
Documentation

An actual local lift remains a lift after pullback through its local factor, with the original global section transported by the actual unit.

Source context 6 commands

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

noncomputable section
universe u
open AlgebraicGeometry CategoryTheory Limits Opposite
namespace EtaleCohomology
variable {X Y : Scheme.{u}} (q : Y ⟶ X)
variable (Λ : Type u) [CommRing Λ]
Lean source · full declaration
theorem etalePullbackSectionMap_local_lift
    {F G : Sheaf X.smallEtaleTopology (ModuleCat.{u} Λ)} (η : F ⟶ G)
    {U : Y.Etale} {V : X.Etale} (g : V ⟶ Scheme.Etale.mk (𝟙 X))
    (l : U.left ⟶ V.left) (hl : l ≫ V.hom = U.hom ≫ q)
    (a : F.obj.obj (op V)) (t : G.obj.obj (op (Scheme.Etale.mk (𝟙 X))))
    (ha : η.hom.app (op V) a = G.obj.map g.op t) :
    ((etalePullback q Λ).map η).hom.app (op U) (etalePullbackSectionMap q Λ F l hl a) =
      ((etalePullback q Λ).obj G).obj.map
        (MorphismProperty.Over.homMk
          (P := show MorphismProperty Scheme.{u} from @Etale) (Q := ⊤)
          (A := U) (B := Scheme.Etale.mk (𝟙 Y)) U.hom (Category.comp_id U.hom)).op
        (etalePullbackGlobalSectionsMap q Λ G t) := by
  have hn := congrArg (fun k : F.obj.obj (op V) ⟶
      ((etalePullback q Λ).obj G).obj.obj (op U) => k a)
    (etalePullbackSectionMap_naturality q Λ η l hl)
  have hg := congrArg (fun k : G.obj.obj (op (Scheme.Etale.mk (𝟙 X))) ⟶
      ((etalePullback q Λ).obj G).obj.obj (op U) => k t)
    (etalePullbackSectionMap_global_restriction q Λ G g l hl)
  change ((etalePullback q Λ).map η).hom.app (op U)
      (etalePullbackSectionMap q Λ F l hl a) =
    etalePullbackSectionMap q Λ G l hl (η.hom.app (op V) a) at hn
  rw [ha] at hn
  exact hn.trans hg

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