Module

PullbackComposition.lean

Nyll.EtaleCohomology.Sites.PullbackComposition

2 declarations indexed from sourceView source ↗

Module documentation

Composition of étale inverse and direct image

The pullback pasting isomorphism on the small étale sites gives the direct image composition isomorphism. The corresponding inverse image comparison follows from the constructed adjunctions and uniqueness of left adjoints.

Imports5

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

Imported by12

def

etalePushforwardCompIso

L32 ↗

EtaleCohomology.etalePushforwardCompIso

Documentation

Iterated direct image is direct image along the composite morphism.

Source context 5 commands

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

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

Lean source · statement

def etalePushforwardCompIso :
    etalePushforward f R ⋙ etalePushforward g R ≅ etalePushforward (f ≫ g) R

def

etalePullbackCompIso

L41 ↗

EtaleCohomology.etalePullbackCompIso