Theorems · Definition · algebraic geometry

AlgebraicGeometry.Scheme.Modules.sheafComposePushforwardComp

{R S : CommRingCat} →
  (φ : R ⟶ S) →
    (CategoryTheory.sheafCompose (Opens.grothendieckTopology ↥(AlgebraicGeometry.Spec S))
            (ModuleCat.restrictScalars
              (CommRingCat.Hom.hom (AlgebraicGeometry.Scheme.Hom.appTop (AlgebraicGeometry.Spec.map φ))))).comp
        ((TopCat.Sheaf.pushforward (ModuleCat ↑((AlgebraicGeometry.Spec R).presheaf.obj (Opposite.op ⊤)))
              (AlgebraicGeometry.Spec.map φ).base).comp
          (CategoryTheory.sheafCompose (Opens.grothendieckTopology ↥(AlgebraicGeometry.Spec R))
            (ModuleCat.restrictScalars (CommRingCat.Hom.hom (AlgebraicGeometry.Scheme.ΓSpecIso R).inv)))) ≅
      (CategoryTheory.sheafCompose (Opens.grothendieckTopology ↥(AlgebraicGeometry.Spec S))
            (ModuleCat.restrictScalars (CommRingCat.Hom.hom (AlgebraicGeometry.Scheme.ΓSpecIso S).inv))).comp
        ((TopCat.Sheaf.pushforward (ModuleCat ↑S) (AlgebraicGeometry.Spec.map φ).base).comp
          (CategoryTheory.sheafCompose (Opens.grothendieckTopology ↥(AlgebraicGeometry.Spec R))
            (ModuleCat.restrictScalars (CommRingCat.Hom.hom φ))))

sheafCompose commutes with pushforward

Defined in

Mathlib.AlgebraicGeometry.Modules.Sheaf

Cited by

0 results in Mathlib

Foundations

Depth 139 from the axioms · uses propext, Classical.choice, Quot.sound