The exterior-power pullback comparison for module presheaves

Pushforward, including restriction of scalars, has a canonical comparison from the exterior power of a pushforward to the pushforward of the exterior power. On sections it sends a wedge over the source coefficient ring to the same wedge over the target coefficient ring. Taking its mate under the pullback--pushforward adjunction constructs a natural map α* (⋀ⁿ M) ⟶ ⋀ⁿ (α* M) for pullback of module presheaves. Only the adjunction is needed for this construction. This supplies the sectionwise input to exterior-power pullback comparisons for sheaves. Unlike precomposition alone, restriction of scalars does not generally give an isomorphism of exterior powers. When the coefficient map is an isomorphism, the pushforward comparison is invertible.

In degree one the pushforward comparison is the identity, read through the identifications ⋀¹ M ≅ M.

The construction uses the module-level restriction-of-scalars comparison and Mathlib's CategoryTheory.mateEquiv for the pullback--pushforward adjunction. The wedge formula specifies the pushforward comparison, and the unit equation specifies the pullback comparison.

References

• R. Hartshorne, Algebraic Geometry, Exercise II.5.16.

noncomputable def TauCeti.PresheafOfModules.pushforwardExteriorPowerComparison {C : Type v} [CategoryTheory.Category.{w, v} C] {D : Type v'} [CategoryTheory.Category.{w', v'} D] {F : CategoryTheory.Functor C D} {S : CategoryTheory.Functor Cᵒᵖ CommRingCat} {R : CategoryTheory.Functor Dᵒᵖ CommRingCat} (α : S ⟶ F.op.comp R) (n : ℕ) : (PresheafOfModulesOfCommRing.pushforward α).comp (PresheafOfModulesOfCommRing.exteriorPower n) ⟶ (PresheafOfModulesOfCommRing.exteriorPower n).comp (PresheafOfModulesOfCommRing.pushforward α)

Pushforward of module presheaves carries the canonical exterior-power comparison. It changes the coefficient ring of a wedge, without changing its factors.

@[simp]

theorem TauCeti.PresheafOfModules.pushforwardExteriorPowerComparison_app_app_mk {C : Type v} [CategoryTheory.Category.{w, v} C] {D : Type v'} [CategoryTheory.Category.{w', v'} D] {F : CategoryTheory.Functor C D} {S : CategoryTheory.Functor Cᵒᵖ CommRingCat} {R : CategoryTheory.Functor Dᵒᵖ CommRingCat} (α : S ⟶ F.op.comp R) (n : ℕ) (M : PresheafOfModulesOfCommRing R) (U : Cᵒᵖ) (m : Fin n → ↑(((PresheafOfModulesOfCommRing.pushforward α).obj M).obj U)) : (CategoryTheory.ConcreteCategory.hom (PresheafOfModules.Hom.app' ((pushforwardExteriorPowerComparison α n).app M) U)) (ModuleCat.exteriorPower.mk m) = ModuleCat.exteriorPower.mk m

The presheaf comparison sends a decomposable wedge to the wedge with the same factors, now balanced over the target ring.

@[simp]

theorem TauCeti.PresheafOfModules.pushforwardExteriorPowerComparison_app_comp_map_exteriorPowerOneIso {C : Type v} [CategoryTheory.Category.{w, v} C] {D : Type v'} [CategoryTheory.Category.{w', v'} D] {F : CategoryTheory.Functor C D} {S : CategoryTheory.Functor Cᵒᵖ CommRingCat} {R : CategoryTheory.Functor Dᵒᵖ CommRingCat} (α : S ⟶ F.op.comp R) (M : PresheafOfModulesOfCommRing R) : CategoryTheory.CategoryStruct.comp ((pushforwardExteriorPowerComparison α 1).app M) ((PresheafOfModulesOfCommRing.pushforward α).map ((PresheafOfModulesOfCommRing.exteriorPowerOneIso R).hom.app M)) = (PresheafOfModulesOfCommRing.exteriorPowerOneIso S).hom.app ((PresheafOfModulesOfCommRing.pushforward α).obj M)

In degree one, the pushforward comparison is the identity of α_* M, read through the identifications of first exterior powers with the presheaves themselves.

@[simp]

theorem TauCeti.PresheafOfModules.pushforwardExteriorPowerComparison_app_comp_map_exteriorPowerOneIso_assoc {C : Type v} [CategoryTheory.Category.{w, v} C] {D : Type v'} [CategoryTheory.Category.{w', v'} D] {F : CategoryTheory.Functor C D} {S : CategoryTheory.Functor Cᵒᵖ CommRingCat} {R : CategoryTheory.Functor Dᵒᵖ CommRingCat} (α : S ⟶ F.op.comp R) (M : PresheafOfModulesOfCommRing R) {Z : PresheafOfModulesOfCommRing S} (h : (PresheafOfModulesOfCommRing.pushforward α).obj M ⟶ Z) : CategoryTheory.CategoryStruct.comp ((pushforwardExteriorPowerComparison α 1).app M) (CategoryTheory.CategoryStruct.comp ((PresheafOfModulesOfCommRing.pushforward α).map ((PresheafOfModulesOfCommRing.exteriorPowerOneIso R).hom.app M)) h) = CategoryTheory.CategoryStruct.comp ((PresheafOfModulesOfCommRing.exteriorPowerOneIso S).hom.app ((PresheafOfModulesOfCommRing.pushforward α).obj M)) h

In degree one, the pushforward comparison is the identity of α_* M, read through the identifications of first exterior powers with the presheaves themselves.

instance TauCeti.PresheafOfModules.isIso_pushforwardExteriorPowerComparison {C : Type v} [CategoryTheory.Category.{w, v} C] {D : Type v'} [CategoryTheory.Category.{w', v'} D] {F : CategoryTheory.Functor C D} {S : CategoryTheory.Functor Cᵒᵖ CommRingCat} {R : CategoryTheory.Functor Dᵒᵖ CommRingCat} (α : S ⟶ F.op.comp R) [CategoryTheory.IsIso α] (n : ℕ) : CategoryTheory.IsIso (pushforwardExteriorPowerComparison α n)

Pushforward along an isomorphism of coefficient presheaves preserves exterior powers sectionwise.

noncomputable def TauCeti.PresheafOfModules.pullbackExteriorPowerComparison {C : Type v} [CategoryTheory.Category.{w, v} C] {D : Type v'} [CategoryTheory.Category.{w', v'} D] {F : CategoryTheory.Functor C D} {S : CategoryTheory.Functor Cᵒᵖ CommRingCat} {R : CategoryTheory.Functor Dᵒᵖ CommRingCat} (α : S ⟶ F.op.comp R) [(PresheafOfModulesOfCommRing.pushforward α).IsRightAdjoint] (n : ℕ) : (PresheafOfModulesOfCommRing.exteriorPower n).comp (PresheafOfModulesOfCommRing.pullback α) ⟶ (PresheafOfModulesOfCommRing.pullback α).comp (PresheafOfModulesOfCommRing.exteriorPower n)

The canonical map from the pullback of an exterior power to the exterior power of a pullback, characterized by compatibility with the pullback unit and wedges.

@[simp]

theorem TauCeti.PresheafOfModules.unit_comp_pushforward_pullbackExteriorPowerComparison {C : Type v} [CategoryTheory.Category.{w, v} C] {D : Type v'} [CategoryTheory.Category.{w', v'} D] {F : CategoryTheory.Functor C D} {S : CategoryTheory.Functor Cᵒᵖ CommRingCat} {R : CategoryTheory.Functor Dᵒᵖ CommRingCat} (α : S ⟶ F.op.comp R) [(PresheafOfModulesOfCommRing.pushforward α).IsRightAdjoint] (n : ℕ) (M : PresheafOfModulesOfCommRing S) : CategoryTheory.CategoryStruct.comp ((PresheafOfModulesOfCommRing.pullbackPushforwardAdjunction α).unit.app ((PresheafOfModulesOfCommRing.exteriorPower n).obj M)) ((PresheafOfModulesOfCommRing.pushforward α).map ((pullbackExteriorPowerComparison α n).app M)) = CategoryTheory.CategoryStruct.comp ((PresheafOfModulesOfCommRing.exteriorPower n).map ((PresheafOfModulesOfCommRing.pullbackPushforwardAdjunction α).unit.app M)) ((pushforwardExteriorPowerComparison α n).app ((PresheafOfModulesOfCommRing.pullback α).obj M))

The adjunction equation characterizes the canonical pullback comparison.

@[simp]

theorem TauCeti.PresheafOfModules.unit_comp_pushforward_pullbackExteriorPowerComparison_assoc {C : Type v} [CategoryTheory.Category.{w, v} C] {D : Type v'} [CategoryTheory.Category.{w', v'} D] {F : CategoryTheory.Functor C D} {S : CategoryTheory.Functor Cᵒᵖ CommRingCat} {R : CategoryTheory.Functor Dᵒᵖ CommRingCat} (α : S ⟶ F.op.comp R) [(PresheafOfModulesOfCommRing.pushforward α).IsRightAdjoint] (n : ℕ) (M : PresheafOfModulesOfCommRing S) {Z : PresheafOfModulesOfCommRing S} (h : (PresheafOfModulesOfCommRing.pushforward α).obj ((PresheafOfModulesOfCommRing.exteriorPower n).obj ((PresheafOfModulesOfCommRing.pullback α).obj M)) ⟶ Z) : CategoryTheory.CategoryStruct.comp ((PresheafOfModulesOfCommRing.pullbackPushforwardAdjunction α).unit.app ((PresheafOfModulesOfCommRing.exteriorPower n).obj M)) (CategoryTheory.CategoryStruct.comp ((PresheafOfModulesOfCommRing.pushforward α).map ((pullbackExteriorPowerComparison α n).app M)) h) = CategoryTheory.CategoryStruct.comp ((PresheafOfModulesOfCommRing.exteriorPower n).map ((PresheafOfModulesOfCommRing.pullbackPushforwardAdjunction α).unit.app M)) (CategoryTheory.CategoryStruct.comp ((pushforwardExteriorPowerComparison α n).app ((PresheafOfModulesOfCommRing.pullback α).obj M)) h)

The adjunction equation characterizes the canonical pullback comparison.

@[simp]

theorem TauCeti.PresheafOfModules.pullbackExteriorPowerComparison_app_app_unit_mk {C : Type v} [CategoryTheory.Category.{w, v} C] {D : Type v'} [CategoryTheory.Category.{w', v'} D] {F : CategoryTheory.Functor C D} {S : CategoryTheory.Functor Cᵒᵖ CommRingCat} {R : CategoryTheory.Functor Dᵒᵖ CommRingCat} (α : S ⟶ F.op.comp R) [(PresheafOfModulesOfCommRing.pushforward α).IsRightAdjoint] (n : ℕ) (M : PresheafOfModulesOfCommRing S) (U : Cᵒᵖ) (m : Fin n → ↑(M.obj U)) : (CategoryTheory.ConcreteCategory.hom (PresheafOfModules.Hom.app' ((PresheafOfModulesOfCommRing.pushforward α).map ((pullbackExteriorPowerComparison α n).app M)) U)) ((CategoryTheory.ConcreteCategory.hom (PresheafOfModules.Hom.app' ((PresheafOfModulesOfCommRing.pullbackPushforwardAdjunction α).unit.app ((PresheafOfModulesOfCommRing.exteriorPower n).obj M)) U)) (ModuleCat.exteriorPower.mk m)) = ModuleCat.exteriorPower.mk fun (i : Fin n) => (CategoryTheory.ConcreteCategory.hom (PresheafOfModules.Hom.app' ((PresheafOfModulesOfCommRing.pullbackPushforwardAdjunction α).unit.app M) U)) (m i)

On a wedge in the image of the pullback unit, the pullback comparison takes the wedge of the images of its factors under the unit.