Module

SetPullbackComposition.lean

Nyll.EtaleCohomology.Sites.SetPullbackComposition

2 declarations indexed from sourceView source ↗

Module documentation

Composition of inverse and direct image for étale sheaves of sets

Scheme-theoretic pullback pasting gives the comparison of direct images. The inverse image comparison follows from the constructed adjunctions and uniqueness of left adjoints. No conditions on the scheme morphisms are needed.

Imports5

Nyll.EtaleCohomology.Sites.BaseChange
Nyll.EtaleCohomology.Sites.SetSheafFunctors
Mathlib.CategoryTheory.MorphismProperty.OverAdjunction
Mathlib.CategoryTheory.Sites.Continuous
Mathlib.CategoryTheory.Adjunction.Unique

Imported by4

def

etaleSetPushforwardCompIso

L32 ↗

EtaleCohomology.etaleSetPushforwardCompIso

Documentation

Iterated direct image of set-valued étale sheaves is direct image along the composite.

Source context 5 commands

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

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

Lean source · statement

def etaleSetPushforwardCompIso :
    etaleSetPushforward f ⋙ etaleSetPushforward g ≅ etaleSetPushforward (f ≫ g)

def

etaleSetPullbackCompIso

L41 ↗

EtaleCohomology.etaleSetPullbackCompIso