Documentation

TauCeti.AlgebraicGeometry.Modules.ExteriorPower.Pullback.Coherence

Coherence of exterior powers under pullback #

The canonical exterior-power comparison respects the identity and composition isomorphisms of module pullback. These equations concern the actual mate of the pushforward comparison, not a separately chosen isomorphism. They require no quasicoherence or finiteness hypotheses.

The pushforward equations are checked on sheafified wedges of local sections; the pullback equations follow from Mathlib's conjugacy of the canonical pullback and pushforward comparisons by CategoryTheory.Adjunction.app_comp_map_hom_app_of_mateEquiv and CategoryTheory.Adjunction.app_comp_map_inv_app_of_mateEquiv.

References #

source
theorem TauCeti.AlgebraicGeometry.pushforwardExteriorPowerComparison_id {X : AlgebraicGeometry.Scheme} (n : ℕ) (M : X.Modules) :
CategoryTheory.CategoryStruct.comp ((SheafOfModules.pushforwardExteriorPowerComparison (AlgebraicGeometry.Scheme.Hom.toRingCatSheafHom (CategoryTheory.CategoryStruct.id X)) n).app M) ((AlgebraicGeometry.Scheme.Modules.pushforwardId X).hom.app ((SheafOfModules.exteriorPower X.sheaf n).obj M)) = (SheafOfModules.exteriorPower X.sheaf n).map ((AlgebraicGeometry.Scheme.Modules.pushforwardId X).hom.app M)

The exterior-power comparison for identity pushforward agrees with the canonical identification of identity pushforward.

source
theorem TauCeti.AlgebraicGeometry.pushforwardExteriorPowerComparison_id_assoc {X : AlgebraicGeometry.Scheme} (n : ℕ) (M : X.Modules) {Z : SheafOfModules (SheafOfModules.ringCatSheaf X.sheaf)} (h : (CategoryTheory.Functor.id X.Modules).obj ((SheafOfModules.exteriorPower X.sheaf n).obj M) ⟶ Z) :
CategoryTheory.CategoryStruct.comp (CategoryTheory.CategoryStruct.comp ((SheafOfModules.pushforwardExteriorPowerComparison (AlgebraicGeometry.Scheme.Hom.toRingCatSheafHom (CategoryTheory.CategoryStruct.id X)) n).app M) ((AlgebraicGeometry.Scheme.Modules.pushforwardId X).hom.app ((SheafOfModules.exteriorPower X.sheaf n).obj M))) h = CategoryTheory.CategoryStruct.comp ((SheafOfModules.exteriorPower X.sheaf n).map ((AlgebraicGeometry.Scheme.Modules.pushforwardId X).hom.app M)) h

The exterior-power comparison for identity pushforward agrees with the canonical identification of identity pushforward.

source
theorem TauCeti.AlgebraicGeometry.pushforwardExteriorPowerComparison_comp {X Y Z : AlgebraicGeometry.Scheme} (f : X ⟶ Y) (g : Y ⟶ Z) (n : ℕ) (M : X.Modules) :
CategoryTheory.CategoryStruct.comp ((SheafOfModules.pushforwardExteriorPowerComparison (AlgebraicGeometry.Scheme.Hom.toRingCatSheafHom g) n).app ((AlgebraicGeometry.Scheme.Modules.pushforward f).obj M)) (CategoryTheory.CategoryStruct.comp ((AlgebraicGeometry.Scheme.Modules.pushforward g).map ((SheafOfModules.pushforwardExteriorPowerComparison (AlgebraicGeometry.Scheme.Hom.toRingCatSheafHom f) n).app M)) ((AlgebraicGeometry.Scheme.Modules.pushforwardComp f g).hom.app ((SheafOfModules.exteriorPower X.sheaf n).obj M))) = CategoryTheory.CategoryStruct.comp ((SheafOfModules.exteriorPower Z.sheaf n).map ((AlgebraicGeometry.Scheme.Modules.pushforwardComp f g).hom.app M)) ((SheafOfModules.pushforwardExteriorPowerComparison (AlgebraicGeometry.Scheme.Hom.toRingCatSheafHom (CategoryTheory.CategoryStruct.comp f g)) n).app M)

The exterior-power comparison for composite pushforward is the composite of the two successive comparisons, through the canonical pushforward composition isomorphism.

source
theorem TauCeti.AlgebraicGeometry.pushforwardExteriorPowerComparison_comp_assoc {X Y Z : AlgebraicGeometry.Scheme} (f : X ⟶ Y) (g : Y ⟶ Z) (n : ℕ) (M : X.Modules) {Z✝ : SheafOfModules (SheafOfModules.ringCatSheaf Z.sheaf)} (h : (AlgebraicGeometry.Scheme.Modules.pushforward (CategoryTheory.CategoryStruct.comp f g)).obj ((SheafOfModules.exteriorPower X.sheaf n).obj M) ⟶ Z✝) :
CategoryTheory.CategoryStruct.comp (CategoryTheory.CategoryStruct.comp ((SheafOfModules.pushforwardExteriorPowerComparison (AlgebraicGeometry.Scheme.Hom.toRingCatSheafHom g) n).app ((AlgebraicGeometry.Scheme.Modules.pushforward f).obj M)) (CategoryTheory.CategoryStruct.comp ((AlgebraicGeometry.Scheme.Modules.pushforward g).map ((SheafOfModules.pushforwardExteriorPowerComparison (AlgebraicGeometry.Scheme.Hom.toRingCatSheafHom f) n).app M)) ((AlgebraicGeometry.Scheme.Modules.pushforwardComp f g).hom.app ((SheafOfModules.exteriorPower X.sheaf n).obj M)))) h = CategoryTheory.CategoryStruct.comp (CategoryTheory.CategoryStruct.comp ((SheafOfModules.exteriorPower Z.sheaf n).map ((AlgebraicGeometry.Scheme.Modules.pushforwardComp f g).hom.app M)) ((SheafOfModules.pushforwardExteriorPowerComparison (AlgebraicGeometry.Scheme.Hom.toRingCatSheafHom (CategoryTheory.CategoryStruct.comp f g)) n).app M)) h

The exterior-power comparison for composite pushforward is the composite of the two successive comparisons, through the canonical pushforward composition isomorphism.

source
@[simp]
theorem TauCeti.AlgebraicGeometry.pullbackExteriorPowerComparison_id {X : AlgebraicGeometry.Scheme} (n : ℕ) (M : X.Modules) :
CategoryTheory.CategoryStruct.comp ((AlgebraicGeometry.Scheme.Modules.pullbackExteriorPowerComparison (CategoryTheory.CategoryStruct.id X) n).app M) ((SheafOfModules.exteriorPower X.sheaf n).map ((AlgebraicGeometry.Scheme.Modules.pullbackId X).hom.app M)) = (AlgebraicGeometry.Scheme.Modules.pullbackId X).hom.app ((SheafOfModules.exteriorPower X.sheaf n).obj M)

The exterior-power comparison along the identity is induced by the canonical identity isomorphism of module pullback.

source
theorem TauCeti.AlgebraicGeometry.pullbackExteriorPowerComparison_id_assoc {X : AlgebraicGeometry.Scheme} (n : ℕ) (M : X.Modules) {Z : X.Modules} (h : (SheafOfModules.exteriorPower X.sheaf n).obj M ⟶ Z) :
CategoryTheory.CategoryStruct.comp (CategoryTheory.CategoryStruct.comp ((AlgebraicGeometry.Scheme.Modules.pullbackExteriorPowerComparison (CategoryTheory.CategoryStruct.id X) n).app M) ((SheafOfModules.exteriorPower X.sheaf n).map ((AlgebraicGeometry.Scheme.Modules.pullbackId X).hom.app M))) h = CategoryTheory.CategoryStruct.comp ((AlgebraicGeometry.Scheme.Modules.pullbackId X).hom.app ((SheafOfModules.exteriorPower X.sheaf n).obj M)) h

The exterior-power comparison along the identity is induced by the canonical identity isomorphism of module pullback.

source
theorem TauCeti.AlgebraicGeometry.pullbackExteriorPowerComparison_comp {X Y Z : AlgebraicGeometry.Scheme} (f : X ⟶ Y) (g : Y ⟶ Z) (n : ℕ) (M : Z.Modules) :
CategoryTheory.CategoryStruct.comp ((AlgebraicGeometry.Scheme.Modules.pullbackExteriorPowerComparison (CategoryTheory.CategoryStruct.comp f g) n).app M) ((SheafOfModules.exteriorPower X.sheaf n).map ((AlgebraicGeometry.Scheme.Modules.pullbackComp f g).inv.app M)) = CategoryTheory.CategoryStruct.comp ((AlgebraicGeometry.Scheme.Modules.pullbackComp f g).inv.app ((SheafOfModules.exteriorPower Z.sheaf n).obj M)) (CategoryTheory.CategoryStruct.comp ((AlgebraicGeometry.Scheme.Modules.pullback f).map ((AlgebraicGeometry.Scheme.Modules.pullbackExteriorPowerComparison g n).app M)) ((AlgebraicGeometry.Scheme.Modules.pullbackExteriorPowerComparison f n).app ((AlgebraicGeometry.Scheme.Modules.pullback g).obj M)))

The exterior-power comparison for a composite agrees with the two successive comparisons, using the canonical composition isomorphism of module pullback.

source
theorem TauCeti.AlgebraicGeometry.pullbackExteriorPowerComparison_comp_assoc {X Y Z : AlgebraicGeometry.Scheme} (f : X ⟶ Y) (g : Y ⟶ Z) (n : ℕ) (M : Z.Modules) {Z✝ : X.Modules} (h : (SheafOfModules.exteriorPower X.sheaf n).obj ((AlgebraicGeometry.Scheme.Modules.pullback f).obj ((AlgebraicGeometry.Scheme.Modules.pullback g).obj M)) ⟶ Z✝) :
CategoryTheory.CategoryStruct.comp (CategoryTheory.CategoryStruct.comp ((AlgebraicGeometry.Scheme.Modules.pullbackExteriorPowerComparison (CategoryTheory.CategoryStruct.comp f g) n).app M) ((SheafOfModules.exteriorPower X.sheaf n).map ((AlgebraicGeometry.Scheme.Modules.pullbackComp f g).inv.app M))) h = CategoryTheory.CategoryStruct.comp (CategoryTheory.CategoryStruct.comp ((AlgebraicGeometry.Scheme.Modules.pullbackComp f g).inv.app ((SheafOfModules.exteriorPower Z.sheaf n).obj M)) (CategoryTheory.CategoryStruct.comp ((AlgebraicGeometry.Scheme.Modules.pullback f).map ((AlgebraicGeometry.Scheme.Modules.pullbackExteriorPowerComparison g n).app M)) ((AlgebraicGeometry.Scheme.Modules.pullbackExteriorPowerComparison f n).app ((AlgebraicGeometry.Scheme.Modules.pullback g).obj M)))) h

The exterior-power comparison for a composite agrees with the two successive comparisons, using the canonical composition isomorphism of module pullback.