The exterior-power pullback comparison for sheaves of modules #
Let F : C ⥤ D be a continuous functor between sites, S and R sheaves of commutative
rings on C and D, and φ : S ⟶ F_* R a morphism of the underlying sheaves of rings. This file
constructs the canonical natural map ⋀ⁿ (φ_* M) ⟶ φ_* (⋀ⁿ M) for sheaves of R-modules M.
It is the sheafification of the sectionwise comparison
TauCeti.PresheafOfModules.pushforwardExteriorPowerComparison, which changes the coefficient ring
of a wedge without changing its factors, followed by the unit of sheafification of ⋀ⁿ M.
Its mate under an adjunction G ⊣ φ_* is the canonical natural map G (⋀ⁿ M) ⟶ ⋀ⁿ (G M). The
adjunction is an explicit argument, so that the comparison f^* (⋀ⁿ M) ⟶ ⋀ⁿ (f^* M) is available
for each model of pullback: SheafOfModules.pullbackPushforwardAdjunction φ gives it for
SheafOfModules.pullback φ, and, for a morphism of schemes f,
AlgebraicGeometry.Scheme.Modules.pullbackPushforwardAdjunction f gives it for
AlgebraicGeometry.Scheme.Modules.pullback f. Both maps are characterized on sheafified wedges
of sections. In degree one the comparison is an isomorphism, for every such adjunction.
Main declarations #
TauCeti.SheafOfModules.pushforwardExteriorPowerComparison φ n: the natural map⋀ⁿ (φ_* M) ⟶ φ_* (⋀ⁿ M), determined on underlying presheaves byunit_comp_forget_map_pushforwardExteriorPowerComparison_appand computed on sheafified wedges bypushforwardExteriorPowerComparison_app_val_app_mk;TauCeti.SheafOfModules.pullbackExteriorPowerComparison adj n: the natural mapG (⋀ⁿ M) ⟶ ⋀ⁿ (G M)for a left adjointGofφ_*, characterized by the adjunction equationunit_comp_pushforward_pullbackExteriorPowerComparisonand computed on the unit images of sheafified wedges bypullbackExteriorPowerComparison_app_val_app_unit_mk.
The construction transfers the presheaf-level comparisons of
TauCeti.Algebra.Category.ModuleCat.Presheaf.ExteriorPower.Pullback to sheaves by the general
sheafification TauCeti.SheafOfModules.sheafifyPushforwardComparison of sectionwise pushforward
comparisons, which uses the pushforward of underlying presheaves
TauCeti.SheafOfModules.presheafPushforward as in the lax monoidal structure of
TauCeti.Algebra.Category.ModuleCat.Sheaf.TensorProduct.Pushforward.
When the coefficient map is an isomorphism and the site functor is also cocontinuous, the pushforward comparison is invertible.
References #
- R. Hartshorne, Algebraic Geometry, Exercise II.5.16.
noncomputable def
TauCeti.SheafOfModules.pushforwardExteriorPowerComparison
{C : Type u₁}
[CategoryTheory.Category.{v₁, u₁} C]
{J : CategoryTheory.GrothendieckTopology C}
[J.HasSheafCompose (CategoryTheory.forget₂ CommRingCat RingCat)]
[CategoryTheory.HasWeakSheafify J AddCommGrpCat]
[J.WEqualsLocallyBijective AddCommGrpCat]
{D : Type u₂}
[CategoryTheory.Category.{v₂, u₂} D]
{K : CategoryTheory.GrothendieckTopology D}
[K.HasSheafCompose (CategoryTheory.forget₂ CommRingCat RingCat)]
[CategoryTheory.HasWeakSheafify K AddCommGrpCat]
[K.WEqualsLocallyBijective AddCommGrpCat]
{F : CategoryTheory.Functor C D}
[F.IsContinuous J K]
{S : CategoryTheory.Sheaf J CommRingCat}
{R : CategoryTheory.Sheaf K CommRingCat}
(φ : ringCatSheaf S ⟶ (F.sheafPushforwardContinuous RingCat J K).obj (ringCatSheaf R))
(n : ℕ)
:
The canonical natural map ⋀ⁿ (φ_* M) ⟶ φ_* (⋀ⁿ M): the sheafification
sheafifyPushforwardComparison of the sectionwise exterior-power comparison. On sections it sends
the sheafified wedge of sections of M to their sheafified wedge over the target coefficient ring
(pushforwardExteriorPowerComparison_app_val_app_mk).
Instances For
theorem
TauCeti.SheafOfModules.unit_comp_forget_map_pushforwardExteriorPowerComparison_app
{C : Type u₁}
[CategoryTheory.Category.{v₁, u₁} C]
{J : CategoryTheory.GrothendieckTopology C}
[J.HasSheafCompose (CategoryTheory.forget₂ CommRingCat RingCat)]
[CategoryTheory.HasWeakSheafify J AddCommGrpCat]
[J.WEqualsLocallyBijective AddCommGrpCat]
{D : Type u₂}
[CategoryTheory.Category.{v₂, u₂} D]
{K : CategoryTheory.GrothendieckTopology D}
[K.HasSheafCompose (CategoryTheory.forget₂ CommRingCat RingCat)]
[CategoryTheory.HasWeakSheafify K AddCommGrpCat]
[K.WEqualsLocallyBijective AddCommGrpCat]
{F : CategoryTheory.Functor C D}
[F.IsContinuous J K]
{S : CategoryTheory.Sheaf J CommRingCat}
{R : CategoryTheory.Sheaf K CommRingCat}
(φ : ringCatSheaf S ⟶ (F.sheafPushforwardContinuous RingCat J K).obj (ringCatSheaf R))
(n : ℕ)
(M : SheafOfModules (ringCatSheaf R))
:
CategoryTheory.CategoryStruct.comp
((PresheafOfModules.sheafificationAdjunction (CategoryTheory.CategoryStruct.id (ringCatSheaf S).obj)).unit.app
((PresheafOfModulesOfCommRing.exteriorPower n).obj ((SheafOfModules.pushforward φ).obj M).val))
((SheafOfModules.forget (ringCatSheaf S)).map
(CategoryTheory.CategoryStruct.comp (SheafOfModules.exteriorPowerIso n ((SheafOfModules.pushforward φ).obj M)).inv
((pushforwardExteriorPowerComparison φ n).app M))) = CategoryTheory.CategoryStruct.comp
((PresheafOfModules.pushforwardExteriorPowerComparison (commRingCatHom φ) n).app M.val)
((presheafPushforward φ).map
(CategoryTheory.CategoryStruct.comp
((PresheafOfModules.sheafificationAdjunction (CategoryTheory.CategoryStruct.id (ringCatSheaf R).obj)).unit.app
((PresheafOfModulesOfCommRing.exteriorPower n).obj M.val))
((SheafOfModules.forget (ringCatSheaf R)).map (SheafOfModules.exteriorPowerIso n M).inv)))
On underlying presheaves, the pushforward comparison restricted along the sheafification unit
is the sectionwise comparison followed by the pushforward of the sheafification unit of ⋀ⁿ M.
This determines the comparison, by the universal property of sheafification.
theorem
TauCeti.SheafOfModules.unit_comp_forget_map_pushforwardExteriorPowerComparison_app_assoc
{C : Type u₁}
[CategoryTheory.Category.{v₁, u₁} C]
{J : CategoryTheory.GrothendieckTopology C}
[J.HasSheafCompose (CategoryTheory.forget₂ CommRingCat RingCat)]
[CategoryTheory.HasWeakSheafify J AddCommGrpCat]
[J.WEqualsLocallyBijective AddCommGrpCat]
{D : Type u₂}
[CategoryTheory.Category.{v₂, u₂} D]
{K : CategoryTheory.GrothendieckTopology D}
[K.HasSheafCompose (CategoryTheory.forget₂ CommRingCat RingCat)]
[CategoryTheory.HasWeakSheafify K AddCommGrpCat]
[K.WEqualsLocallyBijective AddCommGrpCat]
{F : CategoryTheory.Functor C D}
[F.IsContinuous J K]
{S : CategoryTheory.Sheaf J CommRingCat}
{R : CategoryTheory.Sheaf K CommRingCat}
(φ : ringCatSheaf S ⟶ (F.sheafPushforwardContinuous RingCat J K).obj (ringCatSheaf R))
(n : ℕ)
(M : SheafOfModules (ringCatSheaf R))
{Z : PresheafOfModules (ringCatSheaf S).obj}
(h :
(SheafOfModules.forget (ringCatSheaf S)).obj
((SheafOfModules.pushforward φ).obj ((SheafOfModules.exteriorPower R n).obj M)) ⟶ Z)
:
CategoryTheory.CategoryStruct.comp
(CategoryTheory.CategoryStruct.comp
((PresheafOfModules.sheafificationAdjunction (CategoryTheory.CategoryStruct.id (ringCatSheaf S).obj)).unit.app
((PresheafOfModulesOfCommRing.exteriorPower n).obj ((SheafOfModules.pushforward φ).obj M).val))
((SheafOfModules.forget (ringCatSheaf S)).map
(CategoryTheory.CategoryStruct.comp
(SheafOfModules.exteriorPowerIso n ((SheafOfModules.pushforward φ).obj M)).inv
((pushforwardExteriorPowerComparison φ n).app M))))
h = CategoryTheory.CategoryStruct.comp
(CategoryTheory.CategoryStruct.comp
((PresheafOfModules.pushforwardExteriorPowerComparison (commRingCatHom φ) n).app M.val)
((presheafPushforward φ).map
(CategoryTheory.CategoryStruct.comp
((PresheafOfModules.sheafificationAdjunction (CategoryTheory.CategoryStruct.id (ringCatSheaf R).obj)).unit.app
((PresheafOfModulesOfCommRing.exteriorPower n).obj M.val))
((SheafOfModules.forget (ringCatSheaf R)).map (SheafOfModules.exteriorPowerIso n M).inv))))
h
On underlying presheaves, the pushforward comparison restricted along the sheafification unit
is the sectionwise comparison followed by the pushforward of the sheafification unit of ⋀ⁿ M.
This determines the comparison, by the universal property of sheafification.
@[simp]
theorem
TauCeti.SheafOfModules.pushforwardExteriorPowerComparison_app_val_app_mk
{C : Type u₁}
[CategoryTheory.Category.{v₁, u₁} C]
{J : CategoryTheory.GrothendieckTopology C}
[J.HasSheafCompose (CategoryTheory.forget₂ CommRingCat RingCat)]
[CategoryTheory.HasWeakSheafify J AddCommGrpCat]
[J.WEqualsLocallyBijective AddCommGrpCat]
{D : Type u₂}
[CategoryTheory.Category.{v₂, u₂} D]
{K : CategoryTheory.GrothendieckTopology D}
[K.HasSheafCompose (CategoryTheory.forget₂ CommRingCat RingCat)]
[CategoryTheory.HasWeakSheafify K AddCommGrpCat]
[K.WEqualsLocallyBijective AddCommGrpCat]
{F : CategoryTheory.Functor C D}
[F.IsContinuous J K]
{S : CategoryTheory.Sheaf J CommRingCat}
{R : CategoryTheory.Sheaf K CommRingCat}
(φ : ringCatSheaf S ⟶ (F.sheafPushforwardContinuous RingCat J K).obj (ringCatSheaf R))
(n : ℕ)
(M : SheafOfModules (ringCatSheaf R))
(U : Cᵒᵖ)
(m : Fin n → ↑(PresheafOfModulesOfCommRing.obj ((SheafOfModules.pushforward φ).obj M).val U))
:
(CategoryTheory.ConcreteCategory.hom (((pushforwardExteriorPowerComparison φ n).app M).val.app U))
((CategoryTheory.ConcreteCategory.hom
((SheafOfModules.exteriorPowerIso n ((SheafOfModules.pushforward φ).obj M)).inv.val.app U))
((CategoryTheory.ConcreteCategory.hom
(((PresheafOfModules.sheafificationAdjunction
(CategoryTheory.CategoryStruct.id (ringCatSheaf S).obj)).unit.app
((PresheafOfModulesOfCommRing.exteriorPower n).obj ((SheafOfModules.pushforward φ).obj M).val)).app
U))
(ModuleCat.exteriorPower.mk m))) = (CategoryTheory.ConcreteCategory.hom ((SheafOfModules.exteriorPowerIso n M).inv.val.app (F.op.obj U)))
((CategoryTheory.ConcreteCategory.hom
(((PresheafOfModules.sheafificationAdjunction (CategoryTheory.CategoryStruct.id (ringCatSheaf R).obj)).unit.app
((PresheafOfModulesOfCommRing.exteriorPower n).obj M.val)).app
(F.op.obj U)))
(ModuleCat.exteriorPower.mk m))
On sections over U, the pushforward comparison sends the sheafified wedge m₁ ∧ ⋯ ∧ mₙ of
sections of φ_* M to the sheafified wedge of the same sections of M over F U, balanced over
the target coefficient ring.
theorem
TauCeti.SheafOfModules.pushforwardExteriorPowerComparison_app_comp_map_exteriorPowerOneIso
{C : Type u₁}
[CategoryTheory.Category.{v₁, u₁} C]
{J : CategoryTheory.GrothendieckTopology C}
[J.HasSheafCompose (CategoryTheory.forget₂ CommRingCat RingCat)]
[CategoryTheory.HasWeakSheafify J AddCommGrpCat]
[J.WEqualsLocallyBijective AddCommGrpCat]
{D : Type u₂}
[CategoryTheory.Category.{v₂, u₂} D]
{K : CategoryTheory.GrothendieckTopology D}
[K.HasSheafCompose (CategoryTheory.forget₂ CommRingCat RingCat)]
[CategoryTheory.HasWeakSheafify K AddCommGrpCat]
[K.WEqualsLocallyBijective AddCommGrpCat]
{F : CategoryTheory.Functor C D}
[F.IsContinuous J K]
{S : CategoryTheory.Sheaf J CommRingCat}
{R : CategoryTheory.Sheaf K CommRingCat}
(φ : ringCatSheaf S ⟶ (F.sheafPushforwardContinuous RingCat J K).obj (ringCatSheaf R))
(M : SheafOfModules (ringCatSheaf R))
:
In degree one, the exterior-power comparison of pushforward is the identity of φ_* M, read
through the identifications ⋀¹ M ≅ M.
theorem
TauCeti.SheafOfModules.pushforwardExteriorPowerComparison_app_comp_map_exteriorPowerOneIso_assoc
{C : Type u₁}
[CategoryTheory.Category.{v₁, u₁} C]
{J : CategoryTheory.GrothendieckTopology C}
[J.HasSheafCompose (CategoryTheory.forget₂ CommRingCat RingCat)]
[CategoryTheory.HasWeakSheafify J AddCommGrpCat]
[J.WEqualsLocallyBijective AddCommGrpCat]
{D : Type u₂}
[CategoryTheory.Category.{v₂, u₂} D]
{K : CategoryTheory.GrothendieckTopology D}
[K.HasSheafCompose (CategoryTheory.forget₂ CommRingCat RingCat)]
[CategoryTheory.HasWeakSheafify K AddCommGrpCat]
[K.WEqualsLocallyBijective AddCommGrpCat]
{F : CategoryTheory.Functor C D}
[F.IsContinuous J K]
{S : CategoryTheory.Sheaf J CommRingCat}
{R : CategoryTheory.Sheaf K CommRingCat}
(φ : ringCatSheaf S ⟶ (F.sheafPushforwardContinuous RingCat J K).obj (ringCatSheaf R))
(M : SheafOfModules (ringCatSheaf R))
{Z : SheafOfModules (ringCatSheaf S)}
(h : (SheafOfModules.pushforward φ).obj M ⟶ Z)
:
CategoryTheory.CategoryStruct.comp ((pushforwardExteriorPowerComparison φ 1).app M)
(CategoryTheory.CategoryStruct.comp
((SheafOfModules.pushforward φ).map ((SheafOfModules.exteriorPowerOneIso R).hom.app M)) h) = CategoryTheory.CategoryStruct.comp
((SheafOfModules.exteriorPowerOneIso S).hom.app ((SheafOfModules.pushforward φ).obj M)) h
In degree one, the exterior-power comparison of pushforward is the identity of φ_* M, read
through the identifications ⋀¹ M ≅ M.
instance
TauCeti.SheafOfModules.isIso_pushforwardExteriorPowerComparison
{C : Type u₁}
[CategoryTheory.Category.{v₁, u₁} C]
{J : CategoryTheory.GrothendieckTopology C}
[J.HasSheafCompose (CategoryTheory.forget₂ CommRingCat RingCat)]
[CategoryTheory.HasWeakSheafify J AddCommGrpCat]
[J.WEqualsLocallyBijective AddCommGrpCat]
{D : Type u₂}
[CategoryTheory.Category.{v₂, u₂} D]
{K : CategoryTheory.GrothendieckTopology D}
[K.HasSheafCompose (CategoryTheory.forget₂ CommRingCat RingCat)]
[CategoryTheory.HasWeakSheafify K AddCommGrpCat]
[K.WEqualsLocallyBijective AddCommGrpCat]
{F : CategoryTheory.Functor C D}
[F.IsContinuous J K]
{S : CategoryTheory.Sheaf J CommRingCat}
{R : CategoryTheory.Sheaf K CommRingCat}
(φ : ringCatSheaf S ⟶ (F.sheafPushforwardContinuous RingCat J K).obj (ringCatSheaf R))
[F.IsCocontinuous J K]
[CategoryTheory.IsIso φ]
(n : ℕ)
:
Restriction along a continuous and cocontinuous functor with an isomorphism of coefficient sheaves preserves every exterior power.
noncomputable def
TauCeti.SheafOfModules.pullbackExteriorPowerComparison
{C : Type u₁}
[CategoryTheory.Category.{v₁, u₁} C]
{J : CategoryTheory.GrothendieckTopology C}
[J.HasSheafCompose (CategoryTheory.forget₂ CommRingCat RingCat)]
[CategoryTheory.HasWeakSheafify J AddCommGrpCat]
[J.WEqualsLocallyBijective AddCommGrpCat]
{D : Type u₂}
[CategoryTheory.Category.{v₂, u₂} D]
{K : CategoryTheory.GrothendieckTopology D}
[K.HasSheafCompose (CategoryTheory.forget₂ CommRingCat RingCat)]
[CategoryTheory.HasWeakSheafify K AddCommGrpCat]
[K.WEqualsLocallyBijective AddCommGrpCat]
{F : CategoryTheory.Functor C D}
[F.IsContinuous J K]
{S : CategoryTheory.Sheaf J CommRingCat}
{R : CategoryTheory.Sheaf K CommRingCat}
{φ : ringCatSheaf S ⟶ (F.sheafPushforwardContinuous RingCat J K).obj (ringCatSheaf R)}
{G : CategoryTheory.Functor (SheafOfModules (ringCatSheaf S)) (SheafOfModules (ringCatSheaf R))}
(adj : G ⊣ SheafOfModules.pushforward φ)
(n : ℕ)
:
The canonical natural map G (⋀ⁿ M) ⟶ ⋀ⁿ (G M) for a left adjoint G of the pushforward
φ_*, such as the pullback of sheaves of modules: the mate of
pushforwardExteriorPowerComparison φ n under adj.
Instances For
theorem
TauCeti.SheafOfModules.mateEquiv_pullbackExteriorPowerComparison
{C : Type u₁}
[CategoryTheory.Category.{v₁, u₁} C]
{J : CategoryTheory.GrothendieckTopology C}
[J.HasSheafCompose (CategoryTheory.forget₂ CommRingCat RingCat)]
[CategoryTheory.HasWeakSheafify J AddCommGrpCat]
[J.WEqualsLocallyBijective AddCommGrpCat]
{D : Type u₂}
[CategoryTheory.Category.{v₂, u₂} D]
{K : CategoryTheory.GrothendieckTopology D}
[K.HasSheafCompose (CategoryTheory.forget₂ CommRingCat RingCat)]
[CategoryTheory.HasWeakSheafify K AddCommGrpCat]
[K.WEqualsLocallyBijective AddCommGrpCat]
{F : CategoryTheory.Functor C D}
[F.IsContinuous J K]
{S : CategoryTheory.Sheaf J CommRingCat}
{R : CategoryTheory.Sheaf K CommRingCat}
{φ : ringCatSheaf S ⟶ (F.sheafPushforwardContinuous RingCat J K).obj (ringCatSheaf R)}
{G : CategoryTheory.Functor (SheafOfModules (ringCatSheaf S)) (SheafOfModules (ringCatSheaf R))}
(adj : G ⊣ SheafOfModules.pushforward φ)
(n : ℕ)
:
(CategoryTheory.mateEquiv adj adj) (pullbackExteriorPowerComparison adj n) = pushforwardExteriorPowerComparison φ n
The mate of the exterior-power pullback comparison is the sectionwise pushforward comparison.
@[simp]
theorem
TauCeti.SheafOfModules.unit_comp_pushforward_pullbackExteriorPowerComparison
{C : Type u₁}
[CategoryTheory.Category.{v₁, u₁} C]
{J : CategoryTheory.GrothendieckTopology C}
[J.HasSheafCompose (CategoryTheory.forget₂ CommRingCat RingCat)]
[CategoryTheory.HasWeakSheafify J AddCommGrpCat]
[J.WEqualsLocallyBijective AddCommGrpCat]
{D : Type u₂}
[CategoryTheory.Category.{v₂, u₂} D]
{K : CategoryTheory.GrothendieckTopology D}
[K.HasSheafCompose (CategoryTheory.forget₂ CommRingCat RingCat)]
[CategoryTheory.HasWeakSheafify K AddCommGrpCat]
[K.WEqualsLocallyBijective AddCommGrpCat]
{F : CategoryTheory.Functor C D}
[F.IsContinuous J K]
{S : CategoryTheory.Sheaf J CommRingCat}
{R : CategoryTheory.Sheaf K CommRingCat}
{φ : ringCatSheaf S ⟶ (F.sheafPushforwardContinuous RingCat J K).obj (ringCatSheaf R)}
{G : CategoryTheory.Functor (SheafOfModules (ringCatSheaf S)) (SheafOfModules (ringCatSheaf R))}
(adj : G ⊣ SheafOfModules.pushforward φ)
(n : ℕ)
(M : SheafOfModules (ringCatSheaf S))
:
CategoryTheory.CategoryStruct.comp (adj.unit.app ((SheafOfModules.exteriorPower S n).obj M))
((SheafOfModules.pushforward φ).map ((pullbackExteriorPowerComparison adj n).app M)) = CategoryTheory.CategoryStruct.comp ((SheafOfModules.exteriorPower S n).map (adj.unit.app M))
((pushforwardExteriorPowerComparison φ n).app (G.obj M))
The adjunction equation characterizing the pullback comparison.
@[simp]
theorem
TauCeti.SheafOfModules.unit_comp_pushforward_pullbackExteriorPowerComparison_assoc
{C : Type u₁}
[CategoryTheory.Category.{v₁, u₁} C]
{J : CategoryTheory.GrothendieckTopology C}
[J.HasSheafCompose (CategoryTheory.forget₂ CommRingCat RingCat)]
[CategoryTheory.HasWeakSheafify J AddCommGrpCat]
[J.WEqualsLocallyBijective AddCommGrpCat]
{D : Type u₂}
[CategoryTheory.Category.{v₂, u₂} D]
{K : CategoryTheory.GrothendieckTopology D}
[K.HasSheafCompose (CategoryTheory.forget₂ CommRingCat RingCat)]
[CategoryTheory.HasWeakSheafify K AddCommGrpCat]
[K.WEqualsLocallyBijective AddCommGrpCat]
{F : CategoryTheory.Functor C D}
[F.IsContinuous J K]
{S : CategoryTheory.Sheaf J CommRingCat}
{R : CategoryTheory.Sheaf K CommRingCat}
{φ : ringCatSheaf S ⟶ (F.sheafPushforwardContinuous RingCat J K).obj (ringCatSheaf R)}
{G : CategoryTheory.Functor (SheafOfModules (ringCatSheaf S)) (SheafOfModules (ringCatSheaf R))}
(adj : G ⊣ SheafOfModules.pushforward φ)
(n : ℕ)
(M : SheafOfModules (ringCatSheaf S))
{Z : SheafOfModules (ringCatSheaf S)}
(h : (SheafOfModules.pushforward φ).obj ((SheafOfModules.exteriorPower R n).obj (G.obj M)) ⟶ Z)
:
CategoryTheory.CategoryStruct.comp (adj.unit.app ((SheafOfModules.exteriorPower S n).obj M))
(CategoryTheory.CategoryStruct.comp
((SheafOfModules.pushforward φ).map ((pullbackExteriorPowerComparison adj n).app M)) h) = CategoryTheory.CategoryStruct.comp ((SheafOfModules.exteriorPower S n).map (adj.unit.app M))
(CategoryTheory.CategoryStruct.comp ((pushforwardExteriorPowerComparison φ n).app (G.obj M)) h)
The adjunction equation characterizing the pullback comparison.
@[simp]
theorem
TauCeti.SheafOfModules.pullbackExteriorPowerComparison_app_val_app_unit_mk
{C : Type u₁}
[CategoryTheory.Category.{v₁, u₁} C]
{J : CategoryTheory.GrothendieckTopology C}
[J.HasSheafCompose (CategoryTheory.forget₂ CommRingCat RingCat)]
[CategoryTheory.HasWeakSheafify J AddCommGrpCat]
[J.WEqualsLocallyBijective AddCommGrpCat]
{D : Type u₂}
[CategoryTheory.Category.{v₂, u₂} D]
{K : CategoryTheory.GrothendieckTopology D}
[K.HasSheafCompose (CategoryTheory.forget₂ CommRingCat RingCat)]
[CategoryTheory.HasWeakSheafify K AddCommGrpCat]
[K.WEqualsLocallyBijective AddCommGrpCat]
{F : CategoryTheory.Functor C D}
[F.IsContinuous J K]
{S : CategoryTheory.Sheaf J CommRingCat}
{R : CategoryTheory.Sheaf K CommRingCat}
{φ : ringCatSheaf S ⟶ (F.sheafPushforwardContinuous RingCat J K).obj (ringCatSheaf R)}
{G : CategoryTheory.Functor (SheafOfModules (ringCatSheaf S)) (SheafOfModules (ringCatSheaf R))}
(adj : G ⊣ SheafOfModules.pushforward φ)
(n : ℕ)
(M : SheafOfModules (ringCatSheaf S))
(U : Cᵒᵖ)
(m : Fin n → ↑(PresheafOfModulesOfCommRing.obj M.val U))
:
(CategoryTheory.ConcreteCategory.hom
(((pullbackExteriorPowerComparison adj n).app M).val.app (Opposite.op (F.obj (Opposite.unop U)))))
((CategoryTheory.ConcreteCategory.hom ((adj.unit.app ((SheafOfModules.exteriorPower S n).obj M)).val.app U))
((CategoryTheory.ConcreteCategory.hom ((SheafOfModules.exteriorPowerIso n M).inv.val.app U))
((CategoryTheory.ConcreteCategory.hom
(((PresheafOfModules.sheafificationAdjunction
(CategoryTheory.CategoryStruct.id (ringCatSheaf S).obj)).unit.app
((PresheafOfModulesOfCommRing.exteriorPower n).obj M.val)).app
U))
(ModuleCat.exteriorPower.mk m)))) = (CategoryTheory.ConcreteCategory.hom
((SheafOfModules.exteriorPowerIso n (G.obj M)).inv.val.app (Opposite.op (F.obj (Opposite.unop U)))))
((CategoryTheory.ConcreteCategory.hom
(((PresheafOfModules.sheafificationAdjunction (CategoryTheory.CategoryStruct.id (ringCatSheaf R).obj)).unit.app
((PresheafOfModulesOfCommRing.exteriorPower n).obj (G.obj M).val)).app
(Opposite.op (F.obj (Opposite.unop U)))))
(ModuleCat.exteriorPower.mk fun (i : Fin n) =>
(CategoryTheory.ConcreteCategory.hom ((adj.unit.app M).val.app U)) (m i)))
On a sheafified wedge in the image of the adjunction unit, the pullback comparison takes the sheafified wedge of the images of its factors under the unit.
theorem
TauCeti.SheafOfModules.pullbackExteriorPowerComparison_app_comp_exteriorPowerOneIso
{C : Type u₁}
[CategoryTheory.Category.{v₁, u₁} C]
{J : CategoryTheory.GrothendieckTopology C}
[J.HasSheafCompose (CategoryTheory.forget₂ CommRingCat RingCat)]
[CategoryTheory.HasWeakSheafify J AddCommGrpCat]
[J.WEqualsLocallyBijective AddCommGrpCat]
{D : Type u₂}
[CategoryTheory.Category.{v₂, u₂} D]
{K : CategoryTheory.GrothendieckTopology D}
[K.HasSheafCompose (CategoryTheory.forget₂ CommRingCat RingCat)]
[CategoryTheory.HasWeakSheafify K AddCommGrpCat]
[K.WEqualsLocallyBijective AddCommGrpCat]
{F : CategoryTheory.Functor C D}
[F.IsContinuous J K]
{S : CategoryTheory.Sheaf J CommRingCat}
{R : CategoryTheory.Sheaf K CommRingCat}
{φ : ringCatSheaf S ⟶ (F.sheafPushforwardContinuous RingCat J K).obj (ringCatSheaf R)}
{G : CategoryTheory.Functor (SheafOfModules (ringCatSheaf S)) (SheafOfModules (ringCatSheaf R))}
(adj : G ⊣ SheafOfModules.pushforward φ)
(M : SheafOfModules (ringCatSheaf S))
:
CategoryTheory.CategoryStruct.comp ((pullbackExteriorPowerComparison adj 1).app M)
((SheafOfModules.exteriorPowerOneIso R).hom.app (G.obj M)) = G.map ((SheafOfModules.exteriorPowerOneIso S).hom.app M)
In degree one, the pullback comparison is the identity of φ^* M, read through the
identifications ⋀¹ M ≅ M. In particular it is an isomorphism in degree one.
theorem
TauCeti.SheafOfModules.pullbackExteriorPowerComparison_app_comp_exteriorPowerOneIso_assoc
{C : Type u₁}
[CategoryTheory.Category.{v₁, u₁} C]
{J : CategoryTheory.GrothendieckTopology C}
[J.HasSheafCompose (CategoryTheory.forget₂ CommRingCat RingCat)]
[CategoryTheory.HasWeakSheafify J AddCommGrpCat]
[J.WEqualsLocallyBijective AddCommGrpCat]
{D : Type u₂}
[CategoryTheory.Category.{v₂, u₂} D]
{K : CategoryTheory.GrothendieckTopology D}
[K.HasSheafCompose (CategoryTheory.forget₂ CommRingCat RingCat)]
[CategoryTheory.HasWeakSheafify K AddCommGrpCat]
[K.WEqualsLocallyBijective AddCommGrpCat]
{F : CategoryTheory.Functor C D}
[F.IsContinuous J K]
{S : CategoryTheory.Sheaf J CommRingCat}
{R : CategoryTheory.Sheaf K CommRingCat}
{φ : ringCatSheaf S ⟶ (F.sheafPushforwardContinuous RingCat J K).obj (ringCatSheaf R)}
{G : CategoryTheory.Functor (SheafOfModules (ringCatSheaf S)) (SheafOfModules (ringCatSheaf R))}
(adj : G ⊣ SheafOfModules.pushforward φ)
(M : SheafOfModules (ringCatSheaf S))
{Z : SheafOfModules (ringCatSheaf R)}
(h : G.obj M ⟶ Z)
:
In degree one, the pullback comparison is the identity of φ^* M, read through the
identifications ⋀¹ M ≅ M. In particular it is an isomorphism in degree one.
instance
TauCeti.SheafOfModules.isIso_pullbackExteriorPowerComparison_one
{C : Type u₁}
[CategoryTheory.Category.{v₁, u₁} C]
{J : CategoryTheory.GrothendieckTopology C}
[J.HasSheafCompose (CategoryTheory.forget₂ CommRingCat RingCat)]
[CategoryTheory.HasWeakSheafify J AddCommGrpCat]
[J.WEqualsLocallyBijective AddCommGrpCat]
{D : Type u₂}
[CategoryTheory.Category.{v₂, u₂} D]
{K : CategoryTheory.GrothendieckTopology D}
[K.HasSheafCompose (CategoryTheory.forget₂ CommRingCat RingCat)]
[CategoryTheory.HasWeakSheafify K AddCommGrpCat]
[K.WEqualsLocallyBijective AddCommGrpCat]
{F : CategoryTheory.Functor C D}
[F.IsContinuous J K]
{S : CategoryTheory.Sheaf J CommRingCat}
{R : CategoryTheory.Sheaf K CommRingCat}
{φ : ringCatSheaf S ⟶ (F.sheafPushforwardContinuous RingCat J K).obj (ringCatSheaf R)}
{G : CategoryTheory.Functor (SheafOfModules (ringCatSheaf S)) (SheafOfModules (ringCatSheaf R))}
(adj : G ⊣ SheafOfModules.pushforward φ)
:
The pullback comparison is an isomorphism in degree one.