Exterior powers of presheaves of modules

The exterior power of a presheaf of modules is defined objectwise, using the semilinear exterior powers of its restriction maps. This construction is valid over an arbitrary category and ring presheaf; geometric sheafifications belong in their corresponding consumer layer.

noncomputable def PresheafOfModules.exteriorPower {C : Type w} [CategoryTheory.Category.{w', w} C] (A : CategoryTheory.Functor Cᵒᵖ CommRingCat) (Q : PresheafOfModules (A.comp (CategoryTheory.forget₂ CommRingCat RingCat))) (n : ℕ) : PresheafOfModules (A.comp (CategoryTheory.forget₂ CommRingCat RingCat))

The objectwise exterior power of a presheaf of modules. Its restriction maps are the semilinear exterior powers of the original restriction maps.

Equations

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

@[simp]

theorem PresheafOfModules.exteriorPower_obj {C : Type w} [CategoryTheory.Category.{w', w} C] (A : CategoryTheory.Functor Cᵒᵖ CommRingCat) (Q : PresheafOfModules (A.comp (CategoryTheory.forget₂ CommRingCat RingCat))) (n : ℕ) (U : Cᵒᵖ) : (exteriorPower A Q n).obj U = (Q.obj U).exteriorPower n

noncomputable def PresheafOfModules.exteriorPower.map {C : Type w} [CategoryTheory.Category.{w', w} C] {A : CategoryTheory.Functor Cᵒᵖ CommRingCat} {Q Q' : PresheafOfModules (A.comp (CategoryTheory.forget₂ CommRingCat RingCat))} (f : Q ⟶ Q') (n : ℕ) : exteriorPower A Q n ⟶ exteriorPower A Q' n

Exterior power is functorial in morphisms of presheaves of modules.

Equations

• PresheafOfModules.exteriorPower.map f n = { app := fun (U : Cᵒᵖ) => ModuleCat.exteriorPower.map (f.app U) n, naturality := ⋯ }

@[simp]

theorem PresheafOfModules.exteriorPower.map_app_ιMulti {C : Type w} [CategoryTheory.Category.{w', w} C] {A : CategoryTheory.Functor Cᵒᵖ CommRingCat} {Q Q' : PresheafOfModules (A.comp (CategoryTheory.forget₂ CommRingCat RingCat))} (f : Q ⟶ Q') (n : ℕ) (U : Cᵒᵖ) (x : Fin n → ↑(Q.obj U)) : (CategoryTheory.ConcreteCategory.hom ((map f n).app U)) (ModuleCat.exteriorPower.mk x) = ModuleCat.exteriorPower.mk (⇑(CategoryTheory.ConcreteCategory.hom (f.app U)) ∘ x)

@[simp]

theorem PresheafOfModules.exteriorPower.map_id {C : Type w} [CategoryTheory.Category.{w', w} C] {A : CategoryTheory.Functor Cᵒᵖ CommRingCat} (Q : PresheafOfModules (A.comp (CategoryTheory.forget₂ CommRingCat RingCat))) (n : ℕ) : map (CategoryTheory.CategoryStruct.id Q) n = CategoryTheory.CategoryStruct.id (exteriorPower A Q n)

@[simp]

theorem PresheafOfModules.exteriorPower.map_comp {C : Type w} [CategoryTheory.Category.{w', w} C] {A : CategoryTheory.Functor Cᵒᵖ CommRingCat} {Q Q' Q'' : PresheafOfModules (A.comp (CategoryTheory.forget₂ CommRingCat RingCat))} (f : Q ⟶ Q') (g : Q' ⟶ Q'') (n : ℕ) : map (CategoryTheory.CategoryStruct.comp f g) n = CategoryTheory.CategoryStruct.comp (map f n) (map g n)

noncomputable def PresheafOfModules.exteriorPower.mapIso {C : Type w} [CategoryTheory.Category.{w', w} C] {A : CategoryTheory.Functor Cᵒᵖ CommRingCat} {Q Q' : PresheafOfModules (A.comp (CategoryTheory.forget₂ CommRingCat RingCat))} (e : Q ≅ Q') (n : ℕ) : exteriorPower A Q n ≅ exteriorPower A Q' n

Exterior power sends an isomorphism of presheaves to an isomorphism.

Equations

• PresheafOfModules.exteriorPower.mapIso e n = { hom := PresheafOfModules.exteriorPower.map e.hom n, inv := PresheafOfModules.exteriorPower.map e.inv n, hom_inv_id := ⋯, inv_hom_id := ⋯ }

noncomputable def PresheafOfModules.exteriorPowerFunctor {C : Type w} [CategoryTheory.Category.{w', w} C] (A : CategoryTheory.Functor Cᵒᵖ CommRingCat) (n : ℕ) : CategoryTheory.Functor (PresheafOfModules (A.comp (CategoryTheory.forget₂ CommRingCat RingCat))) (PresheafOfModules (A.comp (CategoryTheory.forget₂ CommRingCat RingCat)))

Exterior power as an endofunctor on presheaves of modules.

Equations

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