Module

AbelianPullbackConstants.lean

Nyll.EtaleCohomology.Classical.AbelianPullbackConstants

3 declarations indexed from sourceView source ↗

Module documentation

Constant sections under actual abelian inverse image

The constant-sheaf inverse-image comparison is defined by uniqueness of left adjoints. Its adjoint sends each original constant section to the same section on the base-changed etale scheme. In particular it preserves the integer section one used to represent degree-one cohomology classes by extension fibers.

Imports5

Nyll.EtaleCohomology.Classical.AbelianSheafFunctors
Nyll.EtaleCohomology.Sites.ConstantPullback
Mathlib.CategoryTheory.Adjunction.Unique
Mathlib.CategoryTheory.Sites.ConstantSheaf
Mathlib.CategoryTheory.Sites.Sheafification

Imported by2

theorem

constantSheafAdj_homEquiv_section

L31 ↗

EtaleCohomology.constantSheafAdj_homEquiv_section

Source context 4 commands

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

noncomputable section
universe u
open AlgebraicGeometry CategoryTheory CategoryTheory.Limits Opposite
namespace EtaleCohomology

Lean source · statement

theorem constantSheafAdj_homEquiv_section (X : Scheme.{u})
    (T : X.Etale) (hT : IsTerminal T) (A : AddCommGrpCat.{u})
    (E : Sheaf X.smallEtaleTopology AddCommGrpCat.{u})
    (g : (constantSheaf X.smallEtaleTopology AddCommGrpCat.{u}).obj A ⟶ E) :
    (constantSheafAdj X.smallEtaleTopology AddCommGrpCat.{u} hT).homEquiv A E g =
      (toSheafify X.smallEtaleTopology ((Functor.const X.Etaleᵒᵖ).obj A)).app (op T) ≫
        g.hom.app (op T)

theorem

constantPullbackSection

L39 ↗

EtaleCohomology.constantPullbackSection

Source context 4 commands

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

noncomputable section
universe u
open AlgebraicGeometry CategoryTheory CategoryTheory.Limits Opposite
namespace EtaleCohomology

Lean source · statement

theorem constantPullbackSection
    {X Y : Scheme.{u}} (f : X ⟶ Y)
    (L : Sheaf Y.smallEtaleTopology AddCommGrpCat.{u} ⥤
      Sheaf X.smallEtaleTopology AddCommGrpCat.{u})
    (adj : L ⊣ etaleAbelianPushforward f) (A : AddCommGrpCat.{u}) (U : Y.Etale) :
    (toSheafify Y.smallEtaleTopology ((Functor.const Y.Etaleᵒᵖ).obj A)).app (op U) ≫
        (adj.homEquiv _ _
          ((Sites.constantSheafCompLeftAdjointIso (etaleBaseChange f) AddCommGrpCat.{u}
            terminalIsTerminal
              (terminalIsTerminal.isTerminalObj (etaleBaseChange f) (⊤_ Y.Etale))
                L adj).hom.app A)).hom.app (op U) =
      (toSheafify X.smallEtaleTopology ((Functor.const X.Etaleᵒᵖ).obj A)).app
        (op ((etaleBaseChange f).obj U))

theorem

etaleAbelianPullbackConstantIso_hom_section

L99 ↗

EtaleCohomology.etaleAbelianPullbackConstantIso_hom_section

Documentation

The adjoint of the actual constant inverse-image comparison sends a constant coefficient to the same coefficient on each base-changed etale scheme.

Source context 4 commands

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

noncomputable section
universe u
open AlgebraicGeometry CategoryTheory CategoryTheory.Limits Opposite
namespace EtaleCohomology

Lean source · statement

theorem etaleAbelianPullbackConstantIso_hom_section
    {X Y : Scheme.{u}} (f : X ⟶ Y) (A : AddCommGrpCat.{u}) (U : Y.Etale) :
    (toSheafify Y.smallEtaleTopology ((Functor.const Y.Etaleᵒᵖ).obj A)).app (op U) ≫
        ((etaleAbelianPullbackPushforwardAdjunction f).homEquiv _ _
          ((etaleAbelianPullbackConstantIso f).hom.app A)).hom.app (op U) =
      (toSheafify X.smallEtaleTopology ((Functor.const X.Etaleᵒᵖ).obj A)).app
        (op ((etaleBaseChange f).obj U))

Module documentation

Constant sections under actual abelian inverse image

Declarations

constantSheafAdj_homEquiv_section

constantPullbackSection

etaleAbelianPullbackConstantIso_hom_section