The open-square comparison on slice-site module sheaves

The restriction of an ordinary pushforward to a slice agrees with the pushforward on that slice. This comparison uses the independent open-square pushforward isomorphism, transported through the two slice-site equivalences. It is not a relative base-change isomorphism.

noncomputable def AlgebraicGeometry.Scheme.Modules.pushforwardOverIso {X Y : Scheme} (f : X ⟶ Y) (M : X.Modules) (U : Y.Opens) : SheafOfModules.over ((pushforward f).obj M) U ≅ (pushforwardOverFunctor f U).obj (SheafOfModules.over M ((TopologicalSpace.Opens.map f.base).obj U))

The independent open-square pushforward comparison, expressed on the slice site. Its middle factor is pushforwardRestrictNatIso; the remaining factors transport through overEquiv and overFunctorEquiv.

Equations

• One or more equations did not get rendered due to their size.

theorem AlgebraicGeometry.Scheme.Modules.overEquiv_map_pushforwardOverIso_hom {X Y : Scheme} (f : X ⟶ Y) (M : X.Modules) (U : Y.Opens) : (overEquiv U).functor.map (pushforwardOverIso f M U).hom = CategoryTheory.CategoryStruct.comp ((overFunctorEquiv U).hom.app ((pushforward f).obj M)) (CategoryTheory.CategoryStruct.comp ((pushforwardRestrictNatIso f U).hom.app M) (CategoryTheory.CategoryStruct.comp ((pushforward (f ∣_ U)).map ((overFunctorEquiv ((TopologicalSpace.Opens.map f.base).obj U)).inv.app M)) ((overEquiv U).counitIso.inv.app ((pushforward (f ∣_ U)).obj ((overEquiv ((TopologicalSpace.Opens.map f.base).obj U)).functor.obj (SheafOfModules.over M ((TopologicalSpace.Opens.map f.base).obj U)))))))

After applying the slice equivalence, pushforwardOverIso is the direct open-square comparison, between the two restriction-equivalence factors.

theorem AlgebraicGeometry.Scheme.Modules.overEquiv_map_pullbackOverIso_hom {X Y : Scheme} (f : X ⟶ Y) (N : Y.Modules) (U : Y.Opens) : (overEquiv ((TopologicalSpace.Opens.map f.base).obj U)).functor.map (pullbackOverIso f N U).hom = CategoryTheory.CategoryStruct.comp ((overFunctorEquiv ((TopologicalSpace.Opens.map f.base).obj U)).hom.app ((pullback f).obj N)) (CategoryTheory.CategoryStruct.comp ((pullbackRestrictNatIso f U).hom.app N) (CategoryTheory.CategoryStruct.comp ((pullback (f ∣_ U)).map ((overFunctorEquiv U).inv.app N)) ((overEquiv ((TopologicalSpace.Opens.map f.base).obj U)).counitIso.inv.app ((pullback (f ∣_ U)).obj ((overEquiv U).functor.obj (SheafOfModules.over N U))))))

The preexisting objectwise pullbackOverIso is the geometric pullback comparison after transport through the slice equivalence.

theorem AlgebraicGeometry.Scheme.Modules.overEquiv_map_pullbackOverAdjunction_unit {X Y : Scheme} (f : X ⟶ Y) (U : Y.Opens) (A : SheafOfModules (CategoryTheory.Sheaf.over Y.ringCatSheaf U)) : CategoryTheory.CategoryStruct.comp ((overEquiv U).functor.map ((pullbackOverAdjunction f U).unit.app A)) ((overEquiv U).counitIso.hom.app ((pushforward (f ∣_ U)).obj ((overEquiv ((TopologicalSpace.Opens.map f.base).obj U)).functor.obj ((overEquiv ((TopologicalSpace.Opens.map f.base).obj U)).inverse.obj ((pullback (f ∣_ U)).obj ((overEquiv U).functor.obj A)))))) = CategoryTheory.CategoryStruct.comp ((pullbackPushforwardAdjunction (f ∣_ U)).unit.app ((overEquiv U).functor.obj A)) ((pushforward (f ∣_ U)).map ((overEquiv ((TopologicalSpace.Opens.map f.base).obj U)).counitIso.inv.app ((pullback (f ∣_ U)).obj ((overEquiv U).functor.obj A))))

Transporting the unit of the composite slice-site adjunction through the outer equivalence gives the actual unit for the restricted scheme morphism, followed by the inverse counit of the inner equivalence.

theorem AlgebraicGeometry.Scheme.Modules.pushforwardOverFunctor_map_transport {X Y : Scheme} (f : X ⟶ Y) (U : Y.Opens) {A B : SheafOfModules (CategoryTheory.Sheaf.over X.ringCatSheaf ((TopologicalSpace.Opens.map f.base).obj U))} (g : A ⟶ B) : CategoryTheory.CategoryStruct.comp ((overEquiv U).counitIso.inv.app ((pushforward (f ∣_ U)).obj ((overEquiv ((TopologicalSpace.Opens.map f.base).obj U)).functor.obj A))) (CategoryTheory.CategoryStruct.comp ((overEquiv U).functor.map ((pushforwardOverFunctor f U).map g)) ((overEquiv U).counitIso.hom.app ((pushforward (f ∣_ U)).obj ((overEquiv ((TopologicalSpace.Opens.map f.base).obj U)).functor.obj B)))) = (pushforward (f ∣_ U)).map ((overEquiv ((TopologicalSpace.Opens.map f.base).obj U)).functor.map g)

Mapping a slice-site morphism by pushforward agrees, under the outer equivalence's counit, with mapping its transported morphism by the restricted scheme pushforward.

theorem AlgebraicGeometry.Scheme.Modules.pushforwardOverIso_map_normal_form {X Y : Scheme} (f : X ⟶ Y) (M : X.Modules) (U : Y.Opens) {B : SheafOfModules (CategoryTheory.Sheaf.over X.ringCatSheaf ((TopologicalSpace.Opens.map f.base).obj U))} (g : SheafOfModules.over M ((TopologicalSpace.Opens.map f.base).obj U) ⟶ B) : CategoryTheory.CategoryStruct.comp ((overEquiv U).functor.map (pushforwardOverIso f M U).hom) (CategoryTheory.CategoryStruct.comp ((overEquiv U).functor.map ((pushforwardOverFunctor f U).map g)) ((overEquiv U).counitIso.hom.app ((pushforward (f ∣_ U)).obj ((overEquiv ((TopologicalSpace.Opens.map f.base).obj U)).functor.obj B)))) = CategoryTheory.CategoryStruct.comp ((overFunctorEquiv U).hom.app ((pushforward f).obj M)) (CategoryTheory.CategoryStruct.comp ((pushforwardRestrictNatIso f U).hom.app M) ((pushforward (f ∣_ U)).map (CategoryTheory.CategoryStruct.comp ((overFunctorEquiv ((TopologicalSpace.Opens.map f.base).obj U)).inv.app M) ((overEquiv ((TopologicalSpace.Opens.map f.base).obj U)).functor.map g))))

The slice-site pushforward comparison followed by a slice morphism has this direct open-square normal form after applying the outer equivalence and its counit. This is not the slice-site unit square or a relative IsIso.

theorem AlgebraicGeometry.Scheme.Modules.pullbackOverIso_unit_app {X Y : Scheme} (f : X ⟶ Y) (N : Y.Modules) (U : Y.Opens) : CategoryTheory.CategoryStruct.comp ((SheafOfModules.overFunctor Y.ringCatSheaf U).map ((pullbackPushforwardAdjunction f).unit.app N)) (CategoryTheory.CategoryStruct.comp (pushforwardOverIso f ((pullback f).obj N) U).hom ((pushforwardOverFunctor f U).map (pullbackOverIso f N U).hom)) = (pullbackOverAdjunction f U).unit.app (SheafOfModules.over N U)

The actual global pullback unit and the composite slice-site unit agree after restriction and the independent open-square comparisons.