NYLL
Module

PullbackGlobalSectionsComposition.lean

Nyll.EtaleCohomology.Sites.PullbackGlobalSectionsComposition
2 declarations indexed from sourceView source ↗

Module documentation

Composition of actual inverse-image maps on global sections

The chosen inverse images compose through the existing adjoint-uniqueness isomorphism. Evaluating its unit equation and the actual base-change maps at identity objects proves the corresponding equation on global sections.

Imports10
Imported by3

Declarations

lemma

etalePullbackComp_unit

L39 ↗
EtaleCohomology.etalePullbackComp_unit
Documentation

The actual inverse-image composition comparison intertwines the two adjunction units.

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 Z : Scheme.{u}} (p : Z ⟶ Y) (q : Y ⟶ X)
variable (Λ : Type u) [CommRing Λ]
Lean source · statement
lemma etalePullbackComp_unit
    (F : Sheaf X.smallEtaleTopology (ModuleCat.{u} Λ)) :
    (etalePullbackPushforwardAdjunction (p ≫ q) Λ).unit.app F ≫
        (etalePushforward (p ≫ q) Λ).map ((etalePullbackCompIso p q Λ).hom.app F) =
      ((etalePullbackPushforwardAdjunction q Λ).unit.app F ≫
        (etalePushforward q Λ).map ((etalePullbackPushforwardAdjunction p Λ).unit.app
          ((etalePullback q Λ).obj F))) ≫
        (etalePushforwardCompIso p q Λ).hom.app
          ((etalePullback p Λ).obj ((etalePullback q Λ).obj F))
theorem

etalePullbackGlobalSectionsMap_comp

L61 ↗
EtaleCohomology.etalePullbackGlobalSectionsMap_comp
Documentation

Pulling a global section twice equals pulling it along the composite, under the existing canonical composition isomorphism of inverse images.

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 Z : Scheme.{u}} (p : Z ⟶ Y) (q : Y ⟶ X)
variable (Λ : Type u) [CommRing Λ]
Lean source · statement
theorem etalePullbackGlobalSectionsMap_comp
    (F : Sheaf X.smallEtaleTopology (ModuleCat.{u} Λ)) :
    etalePullbackGlobalSectionsMap (p ≫ q) Λ F ≫
        ((etalePullbackCompIso p q Λ).hom.app F).hom.app
          (op (Scheme.Etale.mk (𝟙 Z))) =
      etalePullbackGlobalSectionsMap q Λ F ≫
        etalePullbackGlobalSectionsMap p Λ ((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.