Pullbacks of free sheaves of modules #
Let S (resp.R) be a sheaf of rings on a category C (resp. D)
equipped with a Grothendieck topology J (resp. K).
Let F : C ⥤ D be a continuous functor.
Let φ be a morphism from S to the direct image of R.
We introduce unitToPushforwardObjUnit φ which is the morphism
in the category SheafOfModules S which corresponds to φ, and
show that the adjoint morphism
pullbackObjUnitToUnit φ : (pullback.{u} φ).obj (unit S) ⟶ unit R
is an isomorphism when F is a final functor.
More generally, the functor pullback φ sends the free sheaf
of modules free I to free I, see pullbackObjFreeIso and
freeFunctorCompPullbackIso.
def
SheafOfModules.pushforwardSections
{C : Type u₁}
[CategoryTheory.Category.{v₁, u₁} C]
{D : Type u₂}
[CategoryTheory.Category.{v₂, u₂} D]
{J : CategoryTheory.GrothendieckTopology C}
{K : CategoryTheory.GrothendieckTopology D}
{F : CategoryTheory.Functor C D}
{S : CategoryTheory.Sheaf J RingCat}
{R : CategoryTheory.Sheaf K RingCat}
[F.IsContinuous J K]
(φ : S ⟶ (F.sheafPushforwardContinuous RingCat J K).obj R)
[F.IsContinuous J K]
{M : SheafOfModules R}
(s : M.sections)
:
((pushforward φ).obj M).sections
The canonical map from the (global) sections of a sheaf of modules to the (global) sections of its pushforward.
Instances For
@[simp]
theorem
SheafOfModules.pushforwardSections_coe
{C : Type u₁}
[CategoryTheory.Category.{v₁, u₁} C]
{D : Type u₂}
[CategoryTheory.Category.{v₂, u₂} D]
{J : CategoryTheory.GrothendieckTopology C}
{K : CategoryTheory.GrothendieckTopology D}
{F : CategoryTheory.Functor C D}
{S : CategoryTheory.Sheaf J RingCat}
{R : CategoryTheory.Sheaf K RingCat}
[F.IsContinuous J K]
(φ : S ⟶ (F.sheafPushforwardContinuous RingCat J K).obj R)
[F.IsContinuous J K]
{M : SheafOfModules R}
(s : M.sections)
(x✝ : Cᵒᵖ)
:
theorem
SheafOfModules.bijective_pushforwardSections
{C : Type u₁}
[CategoryTheory.Category.{v₁, u₁} C]
{D : Type u₂}
[CategoryTheory.Category.{v₂, u₂} D]
{J : CategoryTheory.GrothendieckTopology C}
{K : CategoryTheory.GrothendieckTopology D}
{F : CategoryTheory.Functor C D}
{S : CategoryTheory.Sheaf J RingCat}
{R : CategoryTheory.Sheaf K RingCat}
[F.IsContinuous J K]
(φ : S ⟶ (F.sheafPushforwardContinuous RingCat J K).obj R)
(M : SheafOfModules R)
[F.IsContinuous J K]
[F.Final]
:
noncomputable def
SheafOfModules.unitToPushforwardObjUnit
{C : Type u₁}
[CategoryTheory.Category.{v₁, u₁} C]
{D : Type u₂}
[CategoryTheory.Category.{v₂, u₂} D]
{J : CategoryTheory.GrothendieckTopology C}
{K : CategoryTheory.GrothendieckTopology D}
{F : CategoryTheory.Functor C D}
{S : CategoryTheory.Sheaf J RingCat}
{R : CategoryTheory.Sheaf K RingCat}
[F.IsContinuous J K]
(φ : S ⟶ (F.sheafPushforwardContinuous RingCat J K).obj R)
[J.HasSheafCompose (CategoryTheory.forget₂ RingCat AddCommGrpCat)]
[K.HasSheafCompose (CategoryTheory.forget₂ RingCat AddCommGrpCat)]
:
The canonical morphism unit S ⟶ (pushforward.{u} φ).obj (unit R)
of sheaves of modules corresponding to a continuous map between ringed sites.
Equations
- One or more equations did not get rendered due to their size.
Instances For
theorem
SheafOfModules.unitToPushforwardObjUnit_val_app_apply
{C : Type u₁}
[CategoryTheory.Category.{v₁, u₁} C]
{D : Type u₂}
[CategoryTheory.Category.{v₂, u₂} D]
{J : CategoryTheory.GrothendieckTopology C}
{K : CategoryTheory.GrothendieckTopology D}
{F : CategoryTheory.Functor C D}
{S : CategoryTheory.Sheaf J RingCat}
{R : CategoryTheory.Sheaf K RingCat}
[F.IsContinuous J K]
(φ : S ⟶ (F.sheafPushforwardContinuous RingCat J K).obj R)
[J.HasSheafCompose (CategoryTheory.forget₂ RingCat AddCommGrpCat)]
[K.HasSheafCompose (CategoryTheory.forget₂ RingCat AddCommGrpCat)]
{X : Cᵒᵖ}
(a : ↑(S.val.obj X))
:
(CategoryTheory.ConcreteCategory.hom ((unitToPushforwardObjUnit φ).val.app X)) a = (CategoryTheory.ConcreteCategory.hom (φ.val.app X)) a
theorem
SheafOfModules.pushforwardSections_unitHomEquiv
{C : Type u₁}
[CategoryTheory.Category.{v₁, u₁} C]
{D : Type u₂}
[CategoryTheory.Category.{v₂, u₂} D]
{J : CategoryTheory.GrothendieckTopology C}
{K : CategoryTheory.GrothendieckTopology D}
{F : CategoryTheory.Functor C D}
{S : CategoryTheory.Sheaf J RingCat}
{R : CategoryTheory.Sheaf K RingCat}
[F.IsContinuous J K]
(φ : S ⟶ (F.sheafPushforwardContinuous RingCat J K).obj R)
[J.HasSheafCompose (CategoryTheory.forget₂ RingCat AddCommGrpCat)]
[K.HasSheafCompose (CategoryTheory.forget₂ RingCat AddCommGrpCat)]
{M : SheafOfModules R}
(f : unit R ⟶ M)
:
pushforwardSections φ (M.unitHomEquiv f) = ((pushforward φ).obj M).unitHomEquiv
(CategoryTheory.CategoryStruct.comp (unitToPushforwardObjUnit φ) ((pushforward φ).map f))
noncomputable def
SheafOfModules.pullbackObjUnitToUnit
{C : Type u₁}
[CategoryTheory.Category.{v₁, u₁} C]
{D : Type u₂}
[CategoryTheory.Category.{v₂, u₂} D]
{J : CategoryTheory.GrothendieckTopology C}
{K : CategoryTheory.GrothendieckTopology D}
{F : CategoryTheory.Functor C D}
{S : CategoryTheory.Sheaf J RingCat}
{R : CategoryTheory.Sheaf K RingCat}
[F.IsContinuous J K]
(φ : S ⟶ (F.sheafPushforwardContinuous RingCat J K).obj R)
[J.HasSheafCompose (CategoryTheory.forget₂ RingCat AddCommGrpCat)]
[K.HasSheafCompose (CategoryTheory.forget₂ RingCat AddCommGrpCat)]
[(pushforward φ).IsRightAdjoint]
:
The canonical morphism (pullback.{u} φ).obj (unit S) ⟶ unit R
of sheaves of modules corresponding to a continuous map between ringed sites.
Equations
- One or more equations did not get rendered due to their size.
Instances For
@[simp]
theorem
SheafOfModules.pullbackPushforwardAdjunction_homEquiv_symm_unitToPushforwardObjUnit
{C : Type u₁}
[CategoryTheory.Category.{v₁, u₁} C]
{D : Type u₂}
[CategoryTheory.Category.{v₂, u₂} D]
{J : CategoryTheory.GrothendieckTopology C}
{K : CategoryTheory.GrothendieckTopology D}
{F : CategoryTheory.Functor C D}
{S : CategoryTheory.Sheaf J RingCat}
{R : CategoryTheory.Sheaf K RingCat}
[F.IsContinuous J K]
(φ : S ⟶ (F.sheafPushforwardContinuous RingCat J K).obj R)
[J.HasSheafCompose (CategoryTheory.forget₂ RingCat AddCommGrpCat)]
[K.HasSheafCompose (CategoryTheory.forget₂ RingCat AddCommGrpCat)]
[(pushforward φ).IsRightAdjoint]
:
((pullbackPushforwardAdjunction φ).homEquiv (unit S) (unit R)).symm (unitToPushforwardObjUnit φ) = pullbackObjUnitToUnit φ
@[simp]
theorem
SheafOfModules.pullbackPushforwardAdjunction_homEquiv_pullbackObjUnitToUnit
{C : Type u₁}
[CategoryTheory.Category.{v₁, u₁} C]
{D : Type u₂}
[CategoryTheory.Category.{v₂, u₂} D]
{J : CategoryTheory.GrothendieckTopology C}
{K : CategoryTheory.GrothendieckTopology D}
{F : CategoryTheory.Functor C D}
{S : CategoryTheory.Sheaf J RingCat}
{R : CategoryTheory.Sheaf K RingCat}
[F.IsContinuous J K]
(φ : S ⟶ (F.sheafPushforwardContinuous RingCat J K).obj R)
[J.HasSheafCompose (CategoryTheory.forget₂ RingCat AddCommGrpCat)]
[K.HasSheafCompose (CategoryTheory.forget₂ RingCat AddCommGrpCat)]
[(pushforward φ).IsRightAdjoint]
:
((pullbackPushforwardAdjunction φ).homEquiv (unit S) (unit R)) (pullbackObjUnitToUnit φ) = unitToPushforwardObjUnit φ
instance
SheafOfModules.instIsIsoPullbackObjUnitToUnitOfFinal
{C : Type u₁}
[CategoryTheory.Category.{v₁, u₁} C]
{D : Type u₂}
[CategoryTheory.Category.{v₂, u₂} D]
{J : CategoryTheory.GrothendieckTopology C}
{K : CategoryTheory.GrothendieckTopology D}
{F : CategoryTheory.Functor C D}
{S : CategoryTheory.Sheaf J RingCat}
{R : CategoryTheory.Sheaf K RingCat}
[F.IsContinuous J K]
(φ : S ⟶ (F.sheafPushforwardContinuous RingCat J K).obj R)
[J.HasSheafCompose (CategoryTheory.forget₂ RingCat AddCommGrpCat)]
[K.HasSheafCompose (CategoryTheory.forget₂ RingCat AddCommGrpCat)]
[(pushforward φ).IsRightAdjoint]
[F.Final]
:
noncomputable def
SheafOfModules.pullbackObjFreeIso
{C : Type u₁}
[CategoryTheory.Category.{v₁, u₁} C]
{D : Type u₂}
[CategoryTheory.Category.{v₂, u₂} D]
{J : CategoryTheory.GrothendieckTopology C}
{K : CategoryTheory.GrothendieckTopology D}
{F : CategoryTheory.Functor C D}
{S : CategoryTheory.Sheaf J RingCat}
{R : CategoryTheory.Sheaf K RingCat}
[F.IsContinuous J K]
(φ : S ⟶ (F.sheafPushforwardContinuous RingCat J K).obj R)
[J.HasSheafCompose (CategoryTheory.forget₂ RingCat AddCommGrpCat)]
[K.HasSheafCompose (CategoryTheory.forget₂ RingCat AddCommGrpCat)]
[(pushforward φ).IsRightAdjoint]
[CategoryTheory.HasWeakSheafify J AddCommGrpCat]
[CategoryTheory.HasWeakSheafify K AddCommGrpCat]
[J.WEqualsLocallyBijective AddCommGrpCat]
[K.WEqualsLocallyBijective AddCommGrpCat]
[F.Final]
(I : Type u)
:
The pullback of a free sheaf of modules is a free sheaf of modules.
Equations
- One or more equations did not get rendered due to their size.
Instances For
@[simp]
theorem
SheafOfModules.pullback_map_ιFree_comp_pullbackObjFreeIso_hom
{C : Type u₁}
[CategoryTheory.Category.{v₁, u₁} C]
{D : Type u₂}
[CategoryTheory.Category.{v₂, u₂} D]
{J : CategoryTheory.GrothendieckTopology C}
{K : CategoryTheory.GrothendieckTopology D}
{F : CategoryTheory.Functor C D}
{S : CategoryTheory.Sheaf J RingCat}
{R : CategoryTheory.Sheaf K RingCat}
[F.IsContinuous J K]
(φ : S ⟶ (F.sheafPushforwardContinuous RingCat J K).obj R)
[J.HasSheafCompose (CategoryTheory.forget₂ RingCat AddCommGrpCat)]
[K.HasSheafCompose (CategoryTheory.forget₂ RingCat AddCommGrpCat)]
[(pushforward φ).IsRightAdjoint]
[CategoryTheory.HasWeakSheafify J AddCommGrpCat]
[CategoryTheory.HasWeakSheafify K AddCommGrpCat]
[J.WEqualsLocallyBijective AddCommGrpCat]
[K.WEqualsLocallyBijective AddCommGrpCat]
[F.Final]
{I : Type u}
(i : I)
:
CategoryTheory.CategoryStruct.comp ((pullback φ).map (ιFree i)) (pullbackObjFreeIso φ I).hom = CategoryTheory.CategoryStruct.comp (pullbackObjUnitToUnit φ) (ιFree i)
@[simp]
theorem
SheafOfModules.pullback_map_ιFree_comp_pullbackObjFreeIso_hom_assoc
{C : Type u₁}
[CategoryTheory.Category.{v₁, u₁} C]
{D : Type u₂}
[CategoryTheory.Category.{v₂, u₂} D]
{J : CategoryTheory.GrothendieckTopology C}
{K : CategoryTheory.GrothendieckTopology D}
{F : CategoryTheory.Functor C D}
{S : CategoryTheory.Sheaf J RingCat}
{R : CategoryTheory.Sheaf K RingCat}
[F.IsContinuous J K]
(φ : S ⟶ (F.sheafPushforwardContinuous RingCat J K).obj R)
[J.HasSheafCompose (CategoryTheory.forget₂ RingCat AddCommGrpCat)]
[K.HasSheafCompose (CategoryTheory.forget₂ RingCat AddCommGrpCat)]
[(pushforward φ).IsRightAdjoint]
[CategoryTheory.HasWeakSheafify J AddCommGrpCat]
[CategoryTheory.HasWeakSheafify K AddCommGrpCat]
[J.WEqualsLocallyBijective AddCommGrpCat]
[K.WEqualsLocallyBijective AddCommGrpCat]
[F.Final]
{I : Type u}
(i : I)
{Z : SheafOfModules R}
(h : free I ⟶ Z)
:
@[simp]
theorem
SheafOfModules.pullbackObjFreeIso_hom_naturality
{C : Type u₁}
[CategoryTheory.Category.{v₁, u₁} C]
{D : Type u₂}
[CategoryTheory.Category.{v₂, u₂} D]
{J : CategoryTheory.GrothendieckTopology C}
{K : CategoryTheory.GrothendieckTopology D}
{F : CategoryTheory.Functor C D}
{S : CategoryTheory.Sheaf J RingCat}
{R : CategoryTheory.Sheaf K RingCat}
[F.IsContinuous J K]
(φ : S ⟶ (F.sheafPushforwardContinuous RingCat J K).obj R)
[J.HasSheafCompose (CategoryTheory.forget₂ RingCat AddCommGrpCat)]
[K.HasSheafCompose (CategoryTheory.forget₂ RingCat AddCommGrpCat)]
[(pushforward φ).IsRightAdjoint]
[CategoryTheory.HasWeakSheafify J AddCommGrpCat]
[CategoryTheory.HasWeakSheafify K AddCommGrpCat]
[J.WEqualsLocallyBijective AddCommGrpCat]
[K.WEqualsLocallyBijective AddCommGrpCat]
[F.Final]
{I J✝ : Type u}
(f : I → J✝)
:
CategoryTheory.CategoryStruct.comp ((pullback φ).map (freeMap f)) (pullbackObjFreeIso φ J✝).hom = CategoryTheory.CategoryStruct.comp (pullbackObjFreeIso φ I).hom (freeMap f)
@[simp]
theorem
SheafOfModules.pullbackObjFreeIso_hom_naturality_assoc
{C : Type u₁}
[CategoryTheory.Category.{v₁, u₁} C]
{D : Type u₂}
[CategoryTheory.Category.{v₂, u₂} D]
{J : CategoryTheory.GrothendieckTopology C}
{K : CategoryTheory.GrothendieckTopology D}
{F : CategoryTheory.Functor C D}
{S : CategoryTheory.Sheaf J RingCat}
{R : CategoryTheory.Sheaf K RingCat}
[F.IsContinuous J K]
(φ : S ⟶ (F.sheafPushforwardContinuous RingCat J K).obj R)
[J.HasSheafCompose (CategoryTheory.forget₂ RingCat AddCommGrpCat)]
[K.HasSheafCompose (CategoryTheory.forget₂ RingCat AddCommGrpCat)]
[(pushforward φ).IsRightAdjoint]
[CategoryTheory.HasWeakSheafify J AddCommGrpCat]
[CategoryTheory.HasWeakSheafify K AddCommGrpCat]
[J.WEqualsLocallyBijective AddCommGrpCat]
[K.WEqualsLocallyBijective AddCommGrpCat]
[F.Final]
{I J✝ : Type u}
(f : I → J✝)
{Z : SheafOfModules R}
(h : free J✝ ⟶ Z)
:
noncomputable def
SheafOfModules.freeFunctorCompPullbackIso
{C : Type u₁}
[CategoryTheory.Category.{v₁, u₁} C]
{D : Type u₂}
[CategoryTheory.Category.{v₂, u₂} D]
{J : CategoryTheory.GrothendieckTopology C}
{K : CategoryTheory.GrothendieckTopology D}
{F : CategoryTheory.Functor C D}
{S : CategoryTheory.Sheaf J RingCat}
{R : CategoryTheory.Sheaf K RingCat}
[F.IsContinuous J K]
(φ : S ⟶ (F.sheafPushforwardContinuous RingCat J K).obj R)
[J.HasSheafCompose (CategoryTheory.forget₂ RingCat AddCommGrpCat)]
[K.HasSheafCompose (CategoryTheory.forget₂ RingCat AddCommGrpCat)]
[(pushforward φ).IsRightAdjoint]
[CategoryTheory.HasWeakSheafify J AddCommGrpCat]
[CategoryTheory.HasWeakSheafify K AddCommGrpCat]
[J.WEqualsLocallyBijective AddCommGrpCat]
[K.WEqualsLocallyBijective AddCommGrpCat]
[F.Final]
:
The canonical isomorphism freeFunctor ⋙ pullback φ ≅ freeFunctor for a
continuous map between ringed sites, when the underlying functor between the sites
is final.