The symmetric-power pullback comparison for sheaves of modules #
Let F : C ⥤ D be a continuous functor between sites, S and R sheaves of commutative
rings, and φ : S ⟶ F_* R. This file constructs the canonical natural map
Symⁿ (φ_* M) ⟶ φ_* (Symⁿ M). It is the sheafification of the sectionwise comparison followed
by the unit of sheafification of Symⁿ M.
Its mate under an adjunction G ⊣ φ_* is the canonical natural map
G (Symⁿ M) ⟶ Symⁿ (G M). The adjunction is an explicit argument, so the same construction
applies both to pullback of sheaves of modules and to pullback of modules on schemes. In degree
one the comparison is an isomorphism for every such adjunction. The pushforward comparison
is invertible in every degree when the functor of sites is also cocontinuous and the
coefficient-ring map is an isomorphism.
As for exterior powers in TauCeti.Algebra.Category.ModuleCat.Sheaf.ExteriorPower.Pullback,
the pushforward comparison and its degree-one computation are instances of
TauCeti.SheafOfModules.sheafifyPushforwardComparison, applied to the symmetric-power comparison
of underlying presheaves.
Main declarations #
TauCeti.SheafOfModules.pushforwardSymmetricPowerComparison: the canonical mapSymⁿ (φ_* M) ⟶ φ_* (Symⁿ M);TauCeti.SheafOfModules.pullbackSymmetricPowerComparison: its mateG (Symⁿ M) ⟶ Symⁿ (G M);TauCeti.SheafOfModules.pullbackSymmetricPowerComparison_app_val_app_unit: its value on sheafified symmetric tensors in the image of the adjunction unit.
References #
- R. Hartshorne, Algebraic Geometry, Exercise II.5.16.
noncomputable def
TauCeti.SheafOfModules.pushforwardSymmetricPowerComparison
{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 Symⁿ (φ_* M) ⟶ φ_* (Symⁿ M): the sheafification
sheafifyPushforwardComparison of the sectionwise symmetric-power comparison.
Instances For
theorem
TauCeti.SheafOfModules.unit_comp_forget_map_pushforwardSymmetricPowerComparison_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.symmetricPower n).obj ((SheafOfModules.pushforward φ).obj M).val))
((SheafOfModules.forget (ringCatSheaf S)).map
(CategoryTheory.CategoryStruct.comp
(SheafOfModules.symmetricPowerIso n ((SheafOfModules.pushforward φ).obj M)).inv
((pushforwardSymmetricPowerComparison φ n).app M))) = CategoryTheory.CategoryStruct.comp
((PresheafOfModules.pushforwardSymmetricPowerComparison (commRingCatHom φ) n).app M.val)
((presheafPushforward φ).map
(CategoryTheory.CategoryStruct.comp
((PresheafOfModules.sheafificationAdjunction (CategoryTheory.CategoryStruct.id (ringCatSheaf R).obj)).unit.app
((PresheafOfModulesOfCommRing.symmetricPower n).obj M.val))
((SheafOfModules.forget (ringCatSheaf R)).map (SheafOfModules.symmetricPowerIso n M).inv)))
On underlying presheaves, the pushforward comparison restricted along the sheafification unit is the sectionwise comparison followed by the pushed-forward sheafification unit. This equation uniquely determines the comparison.
theorem
TauCeti.SheafOfModules.unit_comp_forget_map_pushforwardSymmetricPowerComparison_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.symmetricPower R n).obj M)) ⟶ Z)
:
CategoryTheory.CategoryStruct.comp
(CategoryTheory.CategoryStruct.comp
((PresheafOfModules.sheafificationAdjunction (CategoryTheory.CategoryStruct.id (ringCatSheaf S).obj)).unit.app
((PresheafOfModulesOfCommRing.symmetricPower n).obj ((SheafOfModules.pushforward φ).obj M).val))
((SheafOfModules.forget (ringCatSheaf S)).map
(CategoryTheory.CategoryStruct.comp
(SheafOfModules.symmetricPowerIso n ((SheafOfModules.pushforward φ).obj M)).inv
((pushforwardSymmetricPowerComparison φ n).app M))))
h = CategoryTheory.CategoryStruct.comp
(CategoryTheory.CategoryStruct.comp
((PresheafOfModules.pushforwardSymmetricPowerComparison (commRingCatHom φ) n).app M.val)
((presheafPushforward φ).map
(CategoryTheory.CategoryStruct.comp
((PresheafOfModules.sheafificationAdjunction (CategoryTheory.CategoryStruct.id (ringCatSheaf R).obj)).unit.app
((PresheafOfModulesOfCommRing.symmetricPower n).obj M.val))
((SheafOfModules.forget (ringCatSheaf R)).map (SheafOfModules.symmetricPowerIso n M).inv))))
h
On underlying presheaves, the pushforward comparison restricted along the sheafification unit is the sectionwise comparison followed by the pushed-forward sheafification unit. This equation uniquely determines the comparison.
@[simp]
theorem
TauCeti.SheafOfModules.pushforwardSymmetricPowerComparison_app_val_app_unit
{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ᵒᵖ)
(x : ↑((PresheafOfModulesOfCommRing.obj ((SheafOfModules.pushforward φ).obj M).val U).symmetricPower n))
:
(CategoryTheory.ConcreteCategory.hom (((pushforwardSymmetricPowerComparison φ n).app M).val.app U))
((CategoryTheory.ConcreteCategory.hom
((SheafOfModules.symmetricPowerIso n ((SheafOfModules.pushforward φ).obj M)).inv.val.app U))
((CategoryTheory.ConcreteCategory.hom
(((PresheafOfModules.sheafificationAdjunction
(CategoryTheory.CategoryStruct.id (ringCatSheaf S).obj)).unit.app
((PresheafOfModulesOfCommRing.symmetricPower n).obj ((SheafOfModules.pushforward φ).obj M).val)).app
U))
x)) = (CategoryTheory.ConcreteCategory.hom ((SheafOfModules.symmetricPowerIso n M).inv.val.app (F.op.obj U)))
((CategoryTheory.ConcreteCategory.hom
(((PresheafOfModules.sheafificationAdjunction (CategoryTheory.CategoryStruct.id (ringCatSheaf R).obj)).unit.app
((PresheafOfModulesOfCommRing.symmetricPower n).obj M.val)).app
(F.op.obj U)))
((SymmetricAlgebra.homogeneousSubmoduleMapₛₗ
((ModuleCat.semilinearMapAddEquiv (CommRingCat.Hom.hom ((commRingCatHom φ).app U))
((ModuleCat.restrictScalars (CommRingCat.Hom.hom ((commRingCatHom φ).app U))).obj
(PresheafOfModulesOfCommRing.obj M.val (F.op.obj U)))
(PresheafOfModulesOfCommRing.obj M.val (F.op.obj U))).symm
(CategoryTheory.CategoryStruct.id
((ModuleCat.restrictScalars (CommRingCat.Hom.hom ((commRingCatHom φ).app U))).obj
(PresheafOfModulesOfCommRing.obj M.val (F.op.obj U)))))
n)
x))
On sections over U, the pushforward comparison sends the sheafification of a sectionwise
symmetric tensor x of φ_* M to the sheafification of the same symmetric tensor of M over
F U, with its coefficients mapped along φ.
theorem
TauCeti.SheafOfModules.pushforwardSymmetricPowerComparison_app_comp_map_symmetricPowerOneIso
{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 symmetric-power comparison of pushforward is the identity of φ_* M,
read through the identifications Sym¹ M ≅ M.
theorem
TauCeti.SheafOfModules.pushforwardSymmetricPowerComparison_app_comp_map_symmetricPowerOneIso_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 ((pushforwardSymmetricPowerComparison φ 1).app M)
(CategoryTheory.CategoryStruct.comp
((SheafOfModules.pushforward φ).map ((SheafOfModules.symmetricPowerOneIso R).hom.app M)) h) = CategoryTheory.CategoryStruct.comp
((SheafOfModules.symmetricPowerOneIso S).hom.app ((SheafOfModules.pushforward φ).obj M)) h
In degree one, the symmetric-power comparison of pushforward is the identity of φ_* M,
read through the identifications Sym¹ M ≅ M.
instance
TauCeti.SheafOfModules.isIso_pushforwardSymmetricPowerComparison
{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 symmetric power.
noncomputable def
TauCeti.SheafOfModules.pullbackSymmetricPowerComparison
{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 map G (Symⁿ M) ⟶ Symⁿ (G M) for a left adjoint G of pushforward: the
mate of pushforwardSymmetricPowerComparison φ n under adj.
Instances For
theorem
TauCeti.SheafOfModules.mateEquiv_pullbackSymmetricPowerComparison
{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) (pullbackSymmetricPowerComparison adj n) = pushforwardSymmetricPowerComparison φ n
The mate of the symmetric-power pullback comparison is the pushforward comparison.
@[simp]
theorem
TauCeti.SheafOfModules.unit_comp_pushforward_pullbackSymmetricPowerComparison
{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.symmetricPower S n).obj M))
((SheafOfModules.pushforward φ).map ((pullbackSymmetricPowerComparison adj n).app M)) = CategoryTheory.CategoryStruct.comp ((SheafOfModules.symmetricPower S n).map (adj.unit.app M))
((pushforwardSymmetricPowerComparison φ n).app (G.obj M))
The adjunction equation characterizing the pullback comparison.
@[simp]
theorem
TauCeti.SheafOfModules.unit_comp_pushforward_pullbackSymmetricPowerComparison_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.symmetricPower R n).obj (G.obj M)) ⟶ Z)
:
CategoryTheory.CategoryStruct.comp (adj.unit.app ((SheafOfModules.symmetricPower S n).obj M))
(CategoryTheory.CategoryStruct.comp
((SheafOfModules.pushforward φ).map ((pullbackSymmetricPowerComparison adj n).app M)) h) = CategoryTheory.CategoryStruct.comp ((SheafOfModules.symmetricPower S n).map (adj.unit.app M))
(CategoryTheory.CategoryStruct.comp ((pushforwardSymmetricPowerComparison φ n).app (G.obj M)) h)
The adjunction equation characterizing the pullback comparison.
@[simp]
theorem
TauCeti.SheafOfModules.pullbackSymmetricPowerComparison_app_val_app_unit
{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ᵒᵖ)
(x : ↑((PresheafOfModulesOfCommRing.obj M.val U).symmetricPower n))
:
(CategoryTheory.ConcreteCategory.hom
(((pullbackSymmetricPowerComparison adj n).app M).val.app (Opposite.op (F.obj (Opposite.unop U)))))
((CategoryTheory.ConcreteCategory.hom ((adj.unit.app ((SheafOfModules.symmetricPower S n).obj M)).val.app U))
((CategoryTheory.ConcreteCategory.hom ((SheafOfModules.symmetricPowerIso n M).inv.val.app U))
((CategoryTheory.ConcreteCategory.hom
(((PresheafOfModules.sheafificationAdjunction
(CategoryTheory.CategoryStruct.id (ringCatSheaf S).obj)).unit.app
((PresheafOfModulesOfCommRing.symmetricPower n).obj M.val)).app
U))
x))) = (CategoryTheory.ConcreteCategory.hom
((SheafOfModules.symmetricPowerIso 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.symmetricPower n).obj (G.obj M).val)).app
(Opposite.op (F.obj (Opposite.unop U)))))
((SymmetricAlgebra.homogeneousSubmoduleMapₛₗ
((ModuleCat.semilinearMapAddEquiv (CommRingCat.Hom.hom ((commRingCatHom φ).app U))
(PresheafOfModulesOfCommRing.obj M.val U)
(PresheafOfModulesOfCommRing.obj (G.obj M).val (Opposite.op (F.obj (Opposite.unop U))))).symm
((adj.unit.app M).val.app U))
n)
x))
On the sheafification of a sectionwise symmetric tensor x in the image of the adjunction
unit, the pullback comparison takes the sheafification of the image of x under the map of
symmetric algebras induced by the unit.
theorem
TauCeti.SheafOfModules.pullbackSymmetricPowerComparison_app_comp_symmetricPowerOneIso
{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 ((pullbackSymmetricPowerComparison adj 1).app M)
((SheafOfModules.symmetricPowerOneIso R).hom.app (G.obj M)) = G.map ((SheafOfModules.symmetricPowerOneIso S).hom.app M)
In degree one, the pullback comparison is the identity of G M, read through the
identifications Sym¹ M ≅ M.
theorem
TauCeti.SheafOfModules.pullbackSymmetricPowerComparison_app_comp_symmetricPowerOneIso_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 G M, read through the
identifications Sym¹ M ≅ M.
instance
TauCeti.SheafOfModules.isIso_pullbackSymmetricPowerComparison_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.