NYLL
Module

CechSections.lean

Nyll.EtaleCohomology.Sites.CechSections
12 declarations indexed from sourceView source ↗

Module documentation

The actual degree-zero Čech section maps

The two projections from a scheme's self-fiber product give section maps into the same chosen iterated inverse image. Their comparison uses the existing composition isomorphisms and the actual pullback square equation.

Imports8
Imported by3

Declarations

def

pullback_eq_iso

L35 ↗
EtaleCohomology.pullback_eq_iso
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) (Λ : Type u) [CommRing Λ]
Lean source · statement
def pullback_eq_iso {Z : Scheme.{u}} {f g : Z ⟶ X} (h : f = g) :
    etalePullback f Λ ≅ etalePullback g Λ
def

etaleCechPullbackIso

L42 ↗
EtaleCohomology.etaleCechPullbackIso
Documentation

The canonical comparison between inverse images along the two projections of the self-fiber product.

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) (Λ : Type u) [CommRing Λ]
Lean source · statement
def etaleCechPullbackIso :
    etalePullback q Λ ⋙ etalePullback (pullback.fst q q) Λ ≅
      etalePullback q Λ ⋙ etalePullback (pullback.snd q q) Λ
lemma

sheaf_iso_chain_hom_app_app

L49 ↗
EtaleCohomology.sheaf_iso_chain_hom_app_app
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) (Λ : Type u) [CommRing Λ]
Lean source · statement
lemma sheaf_iso_chain_hom_app_app
    {A B C : Type*} [Category* A] [Category* B] [Category* C]
    {J : GrothendieckTopology B} {L₀ L₁ L₂ L₃ : A ⥤ Sheaf J C}
    (e₁ : L₀ ≅ L₁) (e : L₀ ≅ L₂) (e₂ : L₂ ≅ L₃) (a : A) (b : Bᵒᵖ) :
    (((e₁.symm ≪≫ e ≪≫ e₂).hom.app a).hom.app b) =
      (e₁.inv.app a).hom.app b ≫ (e.hom.app a).hom.app b ≫
        (e₂.hom.app a).hom.app b
theorem

etaleCechPullbackIso_hom_app_app

L60 ↗
EtaleCohomology.etaleCechPullbackIso_hom_app_app
Documentation

Evaluation of the actual Čech comparison uses the three individual comparison maps. The equality is supplied by functoriality of evaluation.

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) (Λ : Type u) [CommRing Λ]
Lean source · statement
theorem etaleCechPullbackIso_hom_app_app
    (F : Sheaf X.smallEtaleTopology (ModuleCat.{u} Λ)) :
    ((etaleCechPullbackIso q Λ).hom.app F).hom.app
        (op (Scheme.Etale.mk (𝟙 (pullback q q)))) =
      ((etalePullbackCompIso (pullback.fst q q) q Λ).inv.app F).hom.app
          (op (Scheme.Etale.mk (𝟙 (pullback q q)))) ≫
        ((pullback_eq_iso Λ (pullback.condition (f := q) (g := q))).hom.app F).hom.app
          (op (Scheme.Etale.mk (𝟙 (pullback q q)))) ≫
        ((etalePullbackCompIso (pullback.snd q q) q Λ).hom.app F).hom.app
          (op (Scheme.Etale.mk (𝟙 (pullback q q))))
def

etaleCechFirstSectionsMap

L77 ↗
EtaleCohomology.etaleCechFirstSectionsMap
Documentation

The first Čech section map, transported to the second iterated pullback.

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) (Λ : Type u) [CommRing Λ]
Lean source · statement
def etaleCechFirstSectionsMap (F : Sheaf X.smallEtaleTopology (ModuleCat.{u} Λ)) :
    ((etalePullback q Λ).obj F).obj.obj (op (Scheme.Etale.mk (𝟙 Y))) ⟶
      ((etalePullback (pullback.snd q q) Λ).obj ((etalePullback q Λ).obj F)).obj.obj
        (op (Scheme.Etale.mk (𝟙 (pullback q q))))
def

etaleCechSecondSectionsMap

L86 ↗
EtaleCohomology.etaleCechSecondSectionsMap
Documentation

The second Čech section map.

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) (Λ : Type u) [CommRing Λ]
Lean source · statement
def etaleCechSecondSectionsMap (F : Sheaf X.smallEtaleTopology (ModuleCat.{u} Λ)) :
    ((etalePullback q Λ).obj F).obj.obj (op (Scheme.Etale.mk (𝟙 Y))) ⟶
      ((etalePullback (pullback.snd q q) Λ).obj ((etalePullback q Λ).obj F)).obj.obj
        (op (Scheme.Etale.mk (𝟙 (pullback q q))))
lemma

globalSectionsMap_eqToIso

L92 ↗
EtaleCohomology.globalSectionsMap_eqToIso
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) (Λ : Type u) [CommRing Λ]
Lean source · statement
lemma globalSectionsMap_eqToIso
    {Z : Scheme.{u}} {f g : Z ⟶ X} (h : f = g)
    (F : Sheaf X.smallEtaleTopology (ModuleCat.{u} Λ)) :
    etalePullbackGlobalSectionsMap f Λ F ≫
        ((pullback_eq_iso Λ h).hom.app F).hom.app
          (op (Scheme.Etale.mk (𝟙 Z))) =
      etalePullbackGlobalSectionsMap g Λ F
lemma

cech_diagram_condition

L103 ↗
EtaleCohomology.cech_diagram_condition
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) (Λ : Type u) [CommRing Λ]
Lean source · statement
lemma cech_diagram_condition
    {C : Type*} [Category* C] {A B C₁ C₂ D₁ D₂ : C}
    (a : A ⟶ B) (b₁ : B ⟶ D₁) (b₂ : B ⟶ D₂)
    (c₁ : A ⟶ C₁) (c₂ : A ⟶ C₂)
    (e₁ : C₁ ⟶ D₁) (d₁ : D₁ ⟶ C₁) (e : C₁ ⟶ C₂) (e₂ : C₂ ⟶ D₂)
    (hinv : e₁ ≫ d₁ = 𝟙 C₁)
    (hc₁ : c₁ ≫ e₁ = a ≫ b₁) (hc₂ : c₂ ≫ e₂ = a ≫ b₂)
    (he : c₁ ≫ e = c₂) :
    a ≫ (b₁ ≫ (d₁ ≫ e ≫ e₂)) = a ≫ b₂
theorem

etaleCechSections_condition

L120 ↗
EtaleCohomology.etaleCechSections_condition
Documentation

The actual global pullback map equalizes the two Čech section maps.

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) (Λ : Type u) [CommRing Λ]
Lean source · statement
theorem etaleCechSections_condition
    (F : Sheaf X.smallEtaleTopology (ModuleCat.{u} Λ)) :
    etalePullbackGlobalSectionsMap q Λ F ≫ etaleCechFirstSectionsMap q Λ F =
      etalePullbackGlobalSectionsMap q Λ F ≫ etaleCechSecondSectionsMap q Λ F
lemma

stalkUnit_eqToIso

L149 ↗
EtaleCohomology.stalkUnit_eqToIso
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) (Λ : Type u) [CommRing Λ]
Lean source · full declaration
lemma stalkUnit_eqToIso
    {Z : Scheme.{u}} {f g : Z ⟶ X} (h : f = g)
    {Ω : Type u} [Field Ω] [IsSepClosed Ω]
    (t : Spec (CommRingCat.of Ω) ⟶ X)
    (s : {s : Spec (CommRingCat.of Ω) ⟶ Z // s ≫ f = t})
    (F : Sheaf X.smallEtaleTopology (ModuleCat.{u} Λ)) :
    ((Scheme.pointSmallEtale t).sheafFiber.map
        ((etalePullbackPushforwardAdjunction f Λ).unit.app F) ≫
      etalePushforwardStalkComponent f t s ((etalePullback f Λ).obj F)) ≫
      (Scheme.pointSmallEtale s.val).sheafFiber.map ((pullback_eq_iso Λ h).hom.app F) =
    (Scheme.pointSmallEtale t).sheafFiber.map
        ((etalePullbackPushforwardAdjunction g Λ).unit.app F) ≫
      etalePushforwardStalkComponent g t
        ⟨s.val, by rw [← h]; exact s.property⟩ ((etalePullback g Λ).obj F) := by
  cases h
  let k : (Scheme.pointSmallEtale t).sheafFiber.obj F ⟶
      (Scheme.pointSmallEtale s.val).sheafFiber.obj ((etalePullback f Λ).obj F) :=
    (Scheme.pointSmallEtale t).sheafFiber.map
        ((etalePullbackPushforwardAdjunction f Λ).unit.app F) ≫
      etalePushforwardStalkComponent f t s ((etalePullback f Λ).obj F)
  change k ≫ (Scheme.pointSmallEtale s.val).sheafFiber.map (𝟙 _) = k
  rw [(Scheme.pointSmallEtale s.val).sheafFiber.map_id, Category.comp_id]
lemma

iso_chain_hom_app

L172 ↗
EtaleCohomology.iso_chain_hom_app
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) (Λ : Type u) [CommRing Λ]
Lean source · statement
lemma iso_chain_hom_app
    {C D : Type*} [Category* C] [Category* D] {F₀ F₁ F₂ F₃ : C ⥤ D}
    (e₁ : F₀ ≅ F₁) (e : F₀ ≅ F₂) (e₂ : F₂ ≅ F₃) (a : C) :
    (e₁.symm ≪≫ e ≪≫ e₂).hom.app a =
      e₁.inv.app a ≫ e.hom.app a ≫ e₂.hom.app a
theorem

etaleCechPullbackIso_stalk_unit_comp

L180 ↗
EtaleCohomology.etaleCechPullbackIso_stalk_unit_comp
Documentation

The Čech comparison identifies the two composite unit maps on stalks at any common geometric lift to the self-fiber product.

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) (Λ : Type u) [CommRing Λ]
Lean source · statement
theorem etaleCechPullbackIso_stalk_unit_comp
    {Ω : Type u} [Field Ω] [IsSepClosed Ω]
    (t : Spec (CommRingCat.of Ω) ⟶ X)
    (s₁ s₂ : {s : Spec (CommRingCat.of Ω) ⟶ Y // s ≫ q = t})
    (w : Spec (CommRingCat.of Ω) ⟶ pullback q q)
    (hw₁ : w ≫ pullback.fst q q = s₁.val)
    (hw₂ : w ≫ pullback.snd q q = s₂.val)
    (F : Sheaf X.smallEtaleTopology (ModuleCat.{u} Λ)) :
    ((Scheme.pointSmallEtale t).sheafFiber.map
        ((etalePullbackPushforwardAdjunction q Λ).unit.app F) ≫
      etalePushforwardStalkComponent q t s₁ ((etalePullback q Λ).obj F)) ≫
      ((Scheme.pointSmallEtale s₁.val).sheafFiber.map
          ((etalePullbackPushforwardAdjunction (pullback.fst q q) Λ).unit.app
            ((etalePullback q Λ).obj F)) ≫
        etalePushforwardStalkComponent (pullback.fst q q) s₁.val ⟨w, hw₁⟩
          ((etalePullback (pullback.fst q q) Λ).obj ((etalePullback q Λ).obj F))) ≫
      (Scheme.pointSmallEtale w).sheafFiber.map ((etaleCechPullbackIso q Λ).hom.app F) =
    ((Scheme.pointSmallEtale t).sheafFiber.map
        ((etalePullbackPushforwardAdjunction q Λ).unit.app F) ≫
      etalePushforwardStalkComponent q t s₂ ((etalePullback q Λ).obj F)) ≫
      ((Scheme.pointSmallEtale s₂.val).sheafFiber.map
          ((etalePullbackPushforwardAdjunction (pullback.snd q q) Λ).unit.app
            ((etalePullback q Λ).obj F)) ≫
        etalePushforwardStalkComponent (pullback.snd q q) s₂.val ⟨w, hw₂⟩
          ((etalePullback (pullback.snd q q) Λ).obj ((etalePullback q Λ).obj F)))

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