Basic exterior powers of sheaves of modules #
Given a site (C, J) carrying a sheaf of commutative rings R and n : ℕ, the n-th exterior
power of a sheaf of R-modules M is obtained by taking sectionwise exterior powers
⋀[R(U)]^n M(U) (PresheafOfModulesOfCommRing.exteriorPower) and sheafifying, exactly as
the tensor product TauCeti.SheafOfModules.tensorProduct sheafifies sectionwise tensor products.
On a scheme X this gives SheafOfModules.exteriorPower X.sheaf n : X.Modules ⥤ X.Modules, the
exterior powers of 𝒪ₓ-modules from which determinants of vector bundles are built.
Main declarations #
SheafOfModules.exteriorPower R nis then-th exterior power, as an endofunctor of sheaves ofR-modules;SheafOfModules.exteriorPowerIsoandSheafOfModules.exteriorPower_mapare its defining identification with the sheafification of the sectionwise exterior power;SheafOfModules.exteriorPowerZeroIsoidentifies⋀⁰ Mwith the structure sheaf;SheafOfModules.exteriorPowerOneIsoidentifies⋀¹ MwithM;SheafOfModules.presheafPushforwardExteriorPowerIsoidentifies the exterior power of the pushforward of a presheaf of modules with the pushforward of its exterior power;SheafOfModules.pushforwardExteriorPowerIsoidentifies the pushforward of⋀ⁿ Malong a continuous and cocontinuous functor with the exterior power of the pushforward ofM, andSheafOfModules.overExteriorPowerIsospecializes it to the restriction(⋀ⁿ M)|_X ≅ ⋀ⁿ (M|_X)to a slice site; both are natural inM(pushforwardExteriorPowerIso_hom_naturality,overExteriorPowerIso_hom_naturality).
The restriction comparison lets local computations of exterior powers, such as those on the charts of a locally free sheaf, be carried out on the restriction to a covering object.
noncomputable def
SheafOfModules.exteriorPower
{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]
(R : CategoryTheory.Sheaf J CommRingCat)
(n : ℕ)
:
The n-th exterior power of sheaves of R-modules: the sectionwise exterior power of the
underlying presheaf of modules, sheafified.
Equations
- One or more equations did not get rendered due to their size.
Instances For
noncomputable def
SheafOfModules.exteriorPowerIso
{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]
{R : CategoryTheory.Sheaf J CommRingCat}
(n : ℕ)
(M : SheafOfModules (TauCeti.SheafOfModules.ringCatSheaf R))
:
The defining identification of the exterior power of a sheaf of modules with the sheafification of the sectionwise exterior power of its underlying presheaf of modules.
Equations
Instances For
theorem
SheafOfModules.exteriorPower_map
{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]
{R : CategoryTheory.Sheaf J CommRingCat}
(n : ℕ)
{M N : SheafOfModules (TauCeti.SheafOfModules.ringCatSheaf R)}
(φ : M ⟶ N)
:
(exteriorPower R n).map φ = CategoryTheory.CategoryStruct.comp (exteriorPowerIso n M).hom
(CategoryTheory.CategoryStruct.comp
((PresheafOfModules.sheafification
(CategoryTheory.CategoryStruct.id (TauCeti.SheafOfModules.ringCatSheaf R).obj)).map
((PresheafOfModulesOfCommRing.exteriorPower n).map φ.val))
(exteriorPowerIso n N).inv)
The exterior power of a morphism of sheaves of modules is the sheafification of the sectionwise exterior power of the underlying morphism of presheaves of modules.
noncomputable def
SheafOfModules.exteriorPowerZeroIso
{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]
(R : CategoryTheory.Sheaf J CommRingCat)
:
The zeroth exterior power of a sheaf of modules is the structure sheaf, naturally.
Equations
- One or more equations did not get rendered due to their size.
Instances For
noncomputable def
SheafOfModules.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]
(R : CategoryTheory.Sheaf J CommRingCat)
:
The first exterior power of a sheaf of modules is the sheaf itself, naturally.
Equations
- One or more equations did not get rendered due to their size.
Instances For
@[simp]
theorem
SheafOfModules.exteriorPowerZeroIso_hom_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]
{R : CategoryTheory.Sheaf J CommRingCat}
(M : SheafOfModules (TauCeti.SheafOfModules.ringCatSheaf R))
:
(exteriorPowerZeroIso R).hom.app M = CategoryTheory.CategoryStruct.comp (exteriorPowerIso 0 M).hom
(CategoryTheory.CategoryStruct.comp
((PresheafOfModules.sheafification
(CategoryTheory.CategoryStruct.id (TauCeti.SheafOfModules.ringCatSheaf R).obj)).map
((PresheafOfModulesOfCommRing.exteriorPowerZeroIso R.obj).hom.app M.val))
(TauCeti.SheafOfModules.sheafificationIso (TauCeti.SheafOfModules.ringCatSheaf R)
(unit (TauCeti.SheafOfModules.ringCatSheaf R))).hom)
On components, exteriorPowerZeroIso is the sheafification of the presheaf-level
identification PresheafOfModulesOfCommRing.exteriorPowerZeroIso, followed by the identification of
the sheafified unit with the structure sheaf.
theorem
SheafOfModules.exteriorPowerZeroIso_hom_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]
{R : CategoryTheory.Sheaf J CommRingCat}
(M : SheafOfModules (TauCeti.SheafOfModules.ringCatSheaf R))
{Z : SheafOfModules (TauCeti.SheafOfModules.ringCatSheaf R)}
(h :
((CategoryTheory.Functor.const (SheafOfModules (TauCeti.SheafOfModules.ringCatSheaf R))).obj
(unit (TauCeti.SheafOfModules.ringCatSheaf R))).obj
M ⟶ Z)
:
CategoryTheory.CategoryStruct.comp ((exteriorPowerZeroIso R).hom.app M) h = CategoryTheory.CategoryStruct.comp (exteriorPowerIso 0 M).hom
(CategoryTheory.CategoryStruct.comp
(CategoryTheory.CategoryStruct.comp
((PresheafOfModules.sheafification
(CategoryTheory.CategoryStruct.id (TauCeti.SheafOfModules.ringCatSheaf R).obj)).map
((PresheafOfModulesOfCommRing.exteriorPowerZeroIso R.obj).hom.app M.val))
(TauCeti.SheafOfModules.sheafificationIso (TauCeti.SheafOfModules.ringCatSheaf R)
(unit (TauCeti.SheafOfModules.ringCatSheaf R))).hom)
h)
On components, exteriorPowerZeroIso is the sheafification of the presheaf-level
identification PresheafOfModulesOfCommRing.exteriorPowerZeroIso, followed by the identification of
the sheafified unit with the structure sheaf.
@[simp]
theorem
SheafOfModules.exteriorPowerOneIso_hom_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]
{R : CategoryTheory.Sheaf J CommRingCat}
(M : SheafOfModules (TauCeti.SheafOfModules.ringCatSheaf R))
:
(exteriorPowerOneIso R).hom.app M = CategoryTheory.CategoryStruct.comp (exteriorPowerIso 1 M).hom
(CategoryTheory.CategoryStruct.comp
((PresheafOfModules.sheafification
(CategoryTheory.CategoryStruct.id (TauCeti.SheafOfModules.ringCatSheaf R).obj)).map
((PresheafOfModulesOfCommRing.exteriorPowerOneIso R.obj).hom.app M.val))
(TauCeti.SheafOfModules.sheafificationIso (TauCeti.SheafOfModules.ringCatSheaf R) M).hom)
On components, exteriorPowerOneIso is the sheafification of the presheaf-level
identification PresheafOfModulesOfCommRing.exteriorPowerOneIso, followed by the counit
TauCeti.SheafOfModules.sheafificationIso.
theorem
SheafOfModules.exteriorPowerOneIso_hom_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]
{R : CategoryTheory.Sheaf J CommRingCat}
(M : SheafOfModules (TauCeti.SheafOfModules.ringCatSheaf R))
{Z : SheafOfModules (TauCeti.SheafOfModules.ringCatSheaf R)}
(h : M ⟶ Z)
:
CategoryTheory.CategoryStruct.comp ((exteriorPowerOneIso R).hom.app M) h = CategoryTheory.CategoryStruct.comp (exteriorPowerIso 1 M).hom
(CategoryTheory.CategoryStruct.comp
((PresheafOfModules.sheafification
(CategoryTheory.CategoryStruct.id (TauCeti.SheafOfModules.ringCatSheaf R).obj)).map
((PresheafOfModulesOfCommRing.exteriorPowerOneIso R.obj).hom.app M.val))
(CategoryTheory.CategoryStruct.comp
(TauCeti.SheafOfModules.sheafificationIso (TauCeti.SheafOfModules.ringCatSheaf R) M).hom h))
On components, exteriorPowerOneIso is the sheafification of the presheaf-level
identification PresheafOfModulesOfCommRing.exteriorPowerOneIso, followed by the counit
TauCeti.SheafOfModules.sheafificationIso.
noncomputable def
SheafOfModules.presheafPushforwardExteriorPowerIso
{C : Type u₁}
[CategoryTheory.Category.{v₁, u₁} C]
{J : CategoryTheory.GrothendieckTopology C}
[J.HasSheafCompose (CategoryTheory.forget₂ CommRingCat RingCat)]
{R : CategoryTheory.Sheaf J CommRingCat}
{D : Type u₂}
[CategoryTheory.Category.{v₂, u₂} D]
{K : CategoryTheory.GrothendieckTopology D}
[K.HasSheafCompose (CategoryTheory.forget₂ CommRingCat RingCat)]
(F : CategoryTheory.Functor D C)
[F.IsContinuous K J]
(n : ℕ)
:
(PresheafOfModulesOfCommRing.exteriorPower n).comp
(PresheafOfModules.pushforward
(TauCeti.SheafOfModules.pushforwardRingIso F (TauCeti.SheafOfModules.ringCatSheaf R)).inv) ≅ (PresheafOfModules.pushforward
(TauCeti.SheafOfModules.pushforwardRingIso F (TauCeti.SheafOfModules.ringCatSheaf R)).inv).comp
(PresheafOfModulesOfCommRing.exteriorPower n)
Exterior powers of presheaves of modules commute with the pushforward of presheaves of modules
underlying pushforwardModule F R: over X, both sides have sections ⋀[R(F X)]^n M(F X) and
the same restriction maps.
Equations
- One or more equations did not get rendered due to their size.
Instances For
@[simp]
theorem
SheafOfModules.presheafPushforwardExteriorPowerIso_hom_app_app
{C : Type u₁}
[CategoryTheory.Category.{v₁, u₁} C]
{J : CategoryTheory.GrothendieckTopology C}
[J.HasSheafCompose (CategoryTheory.forget₂ CommRingCat RingCat)]
{R : CategoryTheory.Sheaf J CommRingCat}
{D : Type u₂}
[CategoryTheory.Category.{v₂, u₂} D]
{K : CategoryTheory.GrothendieckTopology D}
[K.HasSheafCompose (CategoryTheory.forget₂ CommRingCat RingCat)]
(F : CategoryTheory.Functor D C)
[F.IsContinuous K J]
(n : ℕ)
(M : PresheafOfModules (TauCeti.SheafOfModules.ringCatSheaf R).obj)
(X : Dᵒᵖ)
:
On sections, presheafPushforwardExteriorPowerIso is the identity of ⋀[R(F X)]^n M(F X).
@[simp]
theorem
SheafOfModules.presheafPushforwardExteriorPowerIso_inv_app_app
{C : Type u₁}
[CategoryTheory.Category.{v₁, u₁} C]
{J : CategoryTheory.GrothendieckTopology C}
[J.HasSheafCompose (CategoryTheory.forget₂ CommRingCat RingCat)]
{R : CategoryTheory.Sheaf J CommRingCat}
{D : Type u₂}
[CategoryTheory.Category.{v₂, u₂} D]
{K : CategoryTheory.GrothendieckTopology D}
[K.HasSheafCompose (CategoryTheory.forget₂ CommRingCat RingCat)]
(F : CategoryTheory.Functor D C)
[F.IsContinuous K J]
(n : ℕ)
(M : PresheafOfModules (TauCeti.SheafOfModules.ringCatSheaf R).obj)
(X : Dᵒᵖ)
:
On sections, the inverse of presheafPushforwardExteriorPowerIso is the identity of
⋀[R(F X)]^n M(F X).
noncomputable def
SheafOfModules.pushforwardExteriorPowerIso
{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]
{R : CategoryTheory.Sheaf J CommRingCat}
{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 D C)
[F.IsContinuous K J]
[F.IsCocontinuous K J]
(n : ℕ)
(M : SheafOfModules (TauCeti.SheafOfModules.ringCatSheaf R))
:
(TauCeti.SheafOfModules.pushforwardModule F R).obj ((exteriorPower R n).obj M) ≅ (exteriorPower (TauCeti.SheafOfModules.pushforwardCommRing F R) n).obj
((TauCeti.SheafOfModules.pushforwardModule F R).obj M)
For each sheaf of modules M, pushforward along a continuous and cocontinuous functor
commutes with the n-th exterior power: F_*(⋀ⁿ M) ≅ ⋀ⁿ (F_* M).
Equations
- One or more equations did not get rendered due to their size.
Instances For
@[simp]
theorem
SheafOfModules.pushforwardExteriorPowerIso_hom
{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]
{R : CategoryTheory.Sheaf J CommRingCat}
{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 D C)
[F.IsContinuous K J]
[F.IsCocontinuous K J]
(n : ℕ)
(M : SheafOfModules (TauCeti.SheafOfModules.ringCatSheaf R))
:
(pushforwardExteriorPowerIso F n M).hom = CategoryTheory.CategoryStruct.comp ((TauCeti.SheafOfModules.pushforwardModule F R).map (exteriorPowerIso n M).hom)
(CategoryTheory.CategoryStruct.comp
(TauCeti.SheafOfModules.pushforwardSheafificationIso F (TauCeti.SheafOfModules.ringCatSheaf R)
((PresheafOfModulesOfCommRing.exteriorPower n).obj M.val)).hom
(CategoryTheory.CategoryStruct.comp
((PresheafOfModules.sheafification
(CategoryTheory.CategoryStruct.id
(TauCeti.SheafOfModules.ringCatSheaf (TauCeti.SheafOfModules.pushforwardCommRing F R)).obj)).map
((presheafPushforwardExteriorPowerIso F n).hom.app M.val))
(exteriorPowerIso n ((TauCeti.SheafOfModules.pushforwardModule F R).obj M)).inv))
The forward map of pushforwardExteriorPowerIso is the sheafification--pushforward comparison
followed by the sheafified presheaf-level comparison presheafPushforwardExteriorPowerIso, read
through the defining identifications of the two exterior powers.
theorem
SheafOfModules.pushforwardExteriorPowerIso_hom_naturality
{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]
{R : CategoryTheory.Sheaf J CommRingCat}
{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 D C)
[F.IsContinuous K J]
[F.IsCocontinuous K J]
(n : ℕ)
{M N : SheafOfModules (TauCeti.SheafOfModules.ringCatSheaf R)}
(φ : M ⟶ N)
:
CategoryTheory.CategoryStruct.comp ((TauCeti.SheafOfModules.pushforwardModule F R).map ((exteriorPower R n).map φ))
(pushforwardExteriorPowerIso F n N).hom = CategoryTheory.CategoryStruct.comp (pushforwardExteriorPowerIso F n M).hom
((exteriorPower (TauCeti.SheafOfModules.pushforwardCommRing F R) n).map
((TauCeti.SheafOfModules.pushforwardModule F R).map φ))
pushforwardExteriorPowerIso is natural in the sheaf of modules.
theorem
SheafOfModules.pushforwardExteriorPowerIso_hom_naturality_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]
{R : CategoryTheory.Sheaf J CommRingCat}
{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 D C)
[F.IsContinuous K J]
[F.IsCocontinuous K J]
(n : ℕ)
{M N : SheafOfModules (TauCeti.SheafOfModules.ringCatSheaf R)}
(φ : M ⟶ N)
{Z : SheafOfModules (TauCeti.SheafOfModules.ringCatSheaf (TauCeti.SheafOfModules.pushforwardCommRing F R))}
(h :
(exteriorPower (TauCeti.SheafOfModules.pushforwardCommRing F R) n).obj
((TauCeti.SheafOfModules.pushforwardModule F R).obj N) ⟶ Z)
:
CategoryTheory.CategoryStruct.comp ((TauCeti.SheafOfModules.pushforwardModule F R).map ((exteriorPower R n).map φ))
(CategoryTheory.CategoryStruct.comp (pushforwardExteriorPowerIso F n N).hom h) = CategoryTheory.CategoryStruct.comp (pushforwardExteriorPowerIso F n M).hom
(CategoryTheory.CategoryStruct.comp
((exteriorPower (TauCeti.SheafOfModules.pushforwardCommRing F R) n).map
((TauCeti.SheafOfModules.pushforwardModule F R).map φ))
h)
pushforwardExteriorPowerIso is natural in the sheaf of modules.
noncomputable def
SheafOfModules.overExteriorPowerIso
{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]
{R : CategoryTheory.Sheaf J CommRingCat}
(n : ℕ)
(M : SheafOfModules (TauCeti.SheafOfModules.ringCatSheaf R))
(X : C)
[(J.over X).HasSheafCompose (CategoryTheory.forget₂ CommRingCat RingCat)]
[CategoryTheory.HasWeakSheafify (J.over X) AddCommGrpCat]
[(J.over X).WEqualsLocallyBijective AddCommGrpCat]
:
For each object X of the site, the restriction of ⋀ⁿ M to the slice site over X is the
n-th exterior power of the restriction of M.
Equations
Instances For
@[simp]
theorem
SheafOfModules.overExteriorPowerIso_hom
{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]
{R : CategoryTheory.Sheaf J CommRingCat}
(n : ℕ)
(M : SheafOfModules (TauCeti.SheafOfModules.ringCatSheaf R))
(X : C)
[(J.over X).HasSheafCompose (CategoryTheory.forget₂ CommRingCat RingCat)]
[CategoryTheory.HasWeakSheafify (J.over X) AddCommGrpCat]
[(J.over X).WEqualsLocallyBijective AddCommGrpCat]
:
(overExteriorPowerIso n M X).hom = (pushforwardExteriorPowerIso (CategoryTheory.Over.forget X) n M).hom
The forward map of overExteriorPowerIso is the slice-site instance of
pushforwardExteriorPowerIso_hom.
theorem
SheafOfModules.overExteriorPowerIso_hom_naturality
{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]
{R : CategoryTheory.Sheaf J CommRingCat}
(n : ℕ)
{M N : SheafOfModules (TauCeti.SheafOfModules.ringCatSheaf R)}
(φ : M ⟶ N)
(X : C)
[(J.over X).HasSheafCompose (CategoryTheory.forget₂ CommRingCat RingCat)]
[CategoryTheory.HasWeakSheafify (J.over X) AddCommGrpCat]
[(J.over X).WEqualsLocallyBijective AddCommGrpCat]
:
CategoryTheory.CategoryStruct.comp (Hom.over ((exteriorPower R n).map φ) X) (overExteriorPowerIso n N X).hom = CategoryTheory.CategoryStruct.comp (overExteriorPowerIso n M X).hom ((exteriorPower (R.over X) n).map (Hom.over φ X))
overExteriorPowerIso is natural in the sheaf of modules.
theorem
SheafOfModules.overExteriorPowerIso_hom_naturality_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]
{R : CategoryTheory.Sheaf J CommRingCat}
(n : ℕ)
{M N : SheafOfModules (TauCeti.SheafOfModules.ringCatSheaf R)}
(φ : M ⟶ N)
(X : C)
[(J.over X).HasSheafCompose (CategoryTheory.forget₂ CommRingCat RingCat)]
[CategoryTheory.HasWeakSheafify (J.over X) AddCommGrpCat]
[(J.over X).WEqualsLocallyBijective AddCommGrpCat]
{Z : SheafOfModules ((TauCeti.SheafOfModules.ringCatSheaf R).over X)}
(h : (exteriorPower (R.over X) n).obj (N.over X) ⟶ Z)
:
CategoryTheory.CategoryStruct.comp
(CategoryTheory.CategoryStruct.comp (Hom.over ((exteriorPower R n).map φ) X) (overExteriorPowerIso n N X).hom) h = CategoryTheory.CategoryStruct.comp
(CategoryTheory.CategoryStruct.comp (overExteriorPowerIso n M X).hom
((exteriorPower (R.over X) n).map (Hom.over φ X)))
h
overExteriorPowerIso is natural in the sheaf of modules.