Exterior powers of free sheaves of modules

Let R be a sheaf of commutative rings on a small site. If I is a finite linearly ordered type, the n-th exterior power of the free sheaf of R-modules on I is free on the set Set.powersetCard I n of n-element subsets of I: over each object W, the sections of free I form a free R(W)-module with basis the sections eᵢ = freeSection i (TauCeti.SheafOfModules.freeBasis), so their n-th exterior power is free with basis the wedge products e_{i₁} ∧ ⋯ ∧ e_{iₙ} for i₁ < ⋯ < iₙ (Mathlib's Module.Basis.exteriorPower). These bases are preserved by the restriction maps, so they identify the sectionwise exterior power of free I with the underlying presheaf of free (Set.powersetCard I n), and sheafifying gives ⋀ⁿ (free I) ≅ free (Set.powersetCard I n).

Main declarations

• SheafOfModules.presheafExteriorPowerFreeIso: the sectionwise exterior power of free I is the underlying presheaf of free (Set.powersetCard I n), sending the wedge product of the basis sections indexed by s to the basis section indexed by s (presheafExteriorPowerFreeIso_hom_app_ιMulti_family);
• SheafOfModules.exteriorPowerFreeIso: ⋀ⁿ (free I) ≅ free (Set.powersetCard I n).

References

• [R. Hartshorne, Algebraic Geometry][hartshorne1977], Chapter II, Exercise 5.16

noncomputable def SheafOfModules.presheafExteriorPowerFreeIso {C : Type u} [CategoryTheory.SmallCategory C] {J : CategoryTheory.GrothendieckTopology C} [J.HasSheafCompose (CategoryTheory.forget₂ CommRingCat RingCat)] [CategoryTheory.HasWeakSheafify J AddCommGrpCat] [J.WEqualsLocallyBijective AddCommGrpCat] {R : CategoryTheory.Sheaf J CommRingCat} (I : Type u) [Finite I] [LinearOrder I] (n : ℕ) : (PresheafOfModulesOfCommRing.exteriorPower n).obj (free I).val ≅ (free ↑(Set.powersetCard I n)).val

The sectionwise n-th exterior power of the free sheaf of modules on a finite linearly ordered type I is the underlying presheaf of the free sheaf on the n-element subsets of I: over each object W it maps the basis of ⋀[R(W)]^n induced by freeBasis I W to freeBasis (Set.powersetCard I n) W.

Equations

• One or more equations did not get rendered due to their size.

theorem SheafOfModules.presheafExteriorPowerFreeIso_hom_app_ιMulti_family {C : Type u} [CategoryTheory.SmallCategory C] {J : CategoryTheory.GrothendieckTopology C} [J.HasSheafCompose (CategoryTheory.forget₂ CommRingCat RingCat)] [CategoryTheory.HasWeakSheafify J AddCommGrpCat] [J.WEqualsLocallyBijective AddCommGrpCat] {R : CategoryTheory.Sheaf J CommRingCat} (I : Type u) [Finite I] [LinearOrder I] (n : ℕ) (W : Cᵒᵖ) (s : ↑(Set.powersetCard I n)) : (CategoryTheory.ConcreteCategory.hom ((presheafExteriorPowerFreeIso I n).hom.app W)) (exteriorPower.ιMulti_family (↑(R.obj.obj W)) n (fun (i : I) => PresheafOfModules.sections.eval (freeSection i) W) s) = PresheafOfModules.sections.eval (freeSection s) W

presheafExteriorPowerFreeIso sends the wedge product, in increasing order, of the basis sections of free I indexed by an n-element subset s to the basis section indexed by s.

theorem SheafOfModules.presheafExteriorPowerFreeIso_inv_app_freeSection {C : Type u} [CategoryTheory.SmallCategory C] {J : CategoryTheory.GrothendieckTopology C} [J.HasSheafCompose (CategoryTheory.forget₂ CommRingCat RingCat)] [CategoryTheory.HasWeakSheafify J AddCommGrpCat] [J.WEqualsLocallyBijective AddCommGrpCat] {R : CategoryTheory.Sheaf J CommRingCat} (I : Type u) [Finite I] [LinearOrder I] (n : ℕ) (W : Cᵒᵖ) (s : ↑(Set.powersetCard I n)) : (CategoryTheory.ConcreteCategory.hom ((presheafExteriorPowerFreeIso I n).inv.app W)) (PresheafOfModules.sections.eval (freeSection s) W) = exteriorPower.ιMulti_family (↑(R.obj.obj W)) n (fun (i : I) => PresheafOfModules.sections.eval (freeSection i) W) s

The inverse of presheafExteriorPowerFreeIso sends the basis section indexed by an n-element subset s to the wedge product, in increasing order, of the basis sections of free I indexed by s.

noncomputable def SheafOfModules.exteriorPowerFreeIso {C : Type u} [CategoryTheory.SmallCategory C] {J : CategoryTheory.GrothendieckTopology C} [J.HasSheafCompose (CategoryTheory.forget₂ CommRingCat RingCat)] [CategoryTheory.HasWeakSheafify J AddCommGrpCat] [J.WEqualsLocallyBijective AddCommGrpCat] {R : CategoryTheory.Sheaf J CommRingCat} (I : Type u) [Finite I] [LinearOrder I] (n : ℕ) : (exteriorPower R n).obj (free I) ≅ free ↑(Set.powersetCard I n)

The n-th exterior power of the free sheaf of modules on a finite linearly ordered type I is the free sheaf on the n-element subsets of I.

Equations

• One or more equations did not get rendered due to their size.

@[simp]

theorem SheafOfModules.exteriorPowerFreeIso_hom {C : Type u} [CategoryTheory.SmallCategory C] {J : CategoryTheory.GrothendieckTopology C} [J.HasSheafCompose (CategoryTheory.forget₂ CommRingCat RingCat)] [CategoryTheory.HasWeakSheafify J AddCommGrpCat] [J.WEqualsLocallyBijective AddCommGrpCat] {R : CategoryTheory.Sheaf J CommRingCat} (I : Type u) [Finite I] [LinearOrder I] (n : ℕ) : (exteriorPowerFreeIso I n).hom = CategoryTheory.CategoryStruct.comp (exteriorPowerIso n (free I)).hom (CategoryTheory.CategoryStruct.comp ((PresheafOfModules.sheafification (CategoryTheory.CategoryStruct.id (TauCeti.SheafOfModules.ringCatSheaf R).obj)).map (presheafExteriorPowerFreeIso I n).hom) (TauCeti.SheafOfModules.sheafificationIso (TauCeti.SheafOfModules.ringCatSheaf R) (free ↑(Set.powersetCard I n))).hom)

The forward map of exteriorPowerFreeIso is the sheafification of presheafExteriorPowerFreeIso, followed by the identification of the sheafified underlying presheaf of a free sheaf with that sheaf.