Exterior powers of presheaves of modules #

Let R be a presheaf of commutative rings on a category C. For a presheaf of R-modules M and n : ℕ, the n-th exterior power of M is the presheaf of modules whose sections over X are the exterior power ⋀[R.obj X]^n (M.obj X) (Mathlib's ModuleCat.exteriorPower), and whose restriction along f : X ⟶ Y sends m₁ ∧ ⋯ ∧ mₙ to M.map f m₁ ∧ ⋯ ∧ M.map f mₙ. This is the presheaf-level input to exterior powers of sheaves of modules, which are obtained by sheafification. As for Mathlib's monoidal structure on these presheaves of modules (PresheafOfModulesOfCommRing.monoidalCategoryStruct), modules are taken in the universe of the rings.

Main declarations #

PresheafOfModulesOfCommRing.exteriorPower n is the n-th exterior power, as an endofunctor of presheaves of R-modules; exteriorPower_obj_obj, exteriorPower_obj_map_mk and exteriorPower_map_app compute its sections, restriction maps and action on morphisms;
PresheafOfModulesOfCommRing.exteriorPowerZeroIso identifies the zeroth exterior power with the constant functor at the unit presheaf of modules R;
PresheafOfModulesOfCommRing.exteriorPowerOneIso identifies the first exterior power with the identity functor.

source

noncomputable def PresheafOfModulesOfCommRing.exteriorPowerObjMap {C : Type v} [CategoryTheory.Category.{w, v} C] {R : CategoryTheory.Functor Cᵒᵖ CommRingCat} (M : PresheafOfModulesOfCommRing R) (n : ℕ) {X Y : Cᵒᵖ} (f : X ⟶ Y) :

(M.obj X).exteriorPower n ⟶ (ModuleCat.restrictScalars (CommRingCat.Hom.hom (R.map f))).obj ((M.obj Y).exteriorPower n)

Auxiliary definition for exteriorPower: the restriction maps of the exterior power of a presheaf of modules, sending m₁ ∧ ⋯ ∧ mₙ to M.map f m₁ ∧ ⋯ ∧ M.map f mₙ.

Equations

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

Instances For

source

theorem PresheafOfModulesOfCommRing.exteriorPowerObjMap_mk {C : Type v} [CategoryTheory.Category.{w, v} C] {R : CategoryTheory.Functor Cᵒᵖ CommRingCat} (M : PresheafOfModulesOfCommRing R) (n : ℕ) {X Y : Cᵒᵖ} (f : X ⟶ Y) (x : Fin n → ↑(M.obj X)) :

(CategoryTheory.ConcreteCategory.hom (M.exteriorPowerObjMap n f)) (ModuleCat.exteriorPower.mk x) = ModuleCat.exteriorPower.mk fun (j : Fin n) => (CategoryTheory.ConcreteCategory.hom (M.map f)) (x j)

The restriction maps of the exterior power on decomposable elements.

source

noncomputable def PresheafOfModulesOfCommRing.exteriorPowerObj {C : Type v} [CategoryTheory.Category.{w, v} C] {R : CategoryTheory.Functor Cᵒᵖ CommRingCat} (M : PresheafOfModulesOfCommRing R) (n : ℕ) :

PresheafOfModulesOfCommRing R

Auxiliary definition for exteriorPower: the exterior power of a presheaf of modules.

Equations

M.exteriorPowerObj n = PresheafOfModulesOfCommRing.mk (fun (X : Cᵒᵖ) => (M.obj X).exteriorPower n) (fun {X Y : Cᵒᵖ} (f : X ⟶ Y) => M.exteriorPowerObjMap n f) ⋯ ⋯

Instances For

source

theorem PresheafOfModulesOfCommRing.exteriorPowerObjMap_naturality {C : Type v} [CategoryTheory.Category.{w, v} C] {R : CategoryTheory.Functor Cᵒᵖ CommRingCat} {M N : PresheafOfModulesOfCommRing R} (φ : M ⟶ N) (n : ℕ) {X Y : Cᵒᵖ} (f : X ⟶ Y) :

CategoryTheory.CategoryStruct.comp (M.exteriorPowerObjMap n f) ((ModuleCat.restrictScalars (CommRingCat.Hom.hom (R.map f))).map (ModuleCat.exteriorPower.map (PresheafOfModules.Hom.app' φ Y) n)) = CategoryTheory.CategoryStruct.comp (ModuleCat.exteriorPower.map (PresheafOfModules.Hom.app' φ X) n) (N.exteriorPowerObjMap n f)

The restriction maps of the exterior power are natural in the presheaf of modules.

source

noncomputable def PresheafOfModulesOfCommRing.exteriorPower {C : Type v} [CategoryTheory.Category.{w, v} C] {R : CategoryTheory.Functor Cᵒᵖ CommRingCat} (n : ℕ) :

CategoryTheory.Functor (PresheafOfModulesOfCommRing R) (PresheafOfModulesOfCommRing R)

The n-th exterior power of presheaves of modules over a presheaf of commutative rings, computed sectionwise: its sections over X are ⋀[R.obj X]^n (M.obj X), and its restriction maps send m₁ ∧ ⋯ ∧ mₙ to the wedge product of the restrictions of the mᵢ.

Equations

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

Instances For

source

theorem PresheafOfModulesOfCommRing.exteriorPower_obj_obj {C : Type v} [CategoryTheory.Category.{w, v} C] {R : CategoryTheory.Functor Cᵒᵖ CommRingCat} (n : ℕ) (M : PresheafOfModulesOfCommRing R) (X : Cᵒᵖ) :

((exteriorPower n).obj M).obj X = (M.obj X).exteriorPower n

The sections of the exterior power over X are the exterior power of the sections.

source

@[simp]

theorem PresheafOfModulesOfCommRing.exteriorPower_obj_map_mk {C : Type v} [CategoryTheory.Category.{w, v} C] {R : CategoryTheory.Functor Cᵒᵖ CommRingCat} (n : ℕ) (M : PresheafOfModulesOfCommRing R) {X Y : Cᵒᵖ} (f : X ⟶ Y) (x : Fin n → ↑(M.obj X)) :

(CategoryTheory.ConcreteCategory.hom (((exteriorPower n).obj M).map f)) (ModuleCat.exteriorPower.mk x) = ModuleCat.exteriorPower.mk fun (j : Fin n) => (CategoryTheory.ConcreteCategory.hom (M.map f)) (x j)

The restriction maps of the exterior power restrict each factor of a wedge product.

source

@[simp]

theorem PresheafOfModulesOfCommRing.exteriorPower_map_app {C : Type v} [CategoryTheory.Category.{w, v} C] {R : CategoryTheory.Functor Cᵒᵖ CommRingCat} (n : ℕ) {M N : PresheafOfModulesOfCommRing R} (φ : M ⟶ N) (X : Cᵒᵖ) :

((exteriorPower n).map φ).app X = ModuleCat.exteriorPower.map (PresheafOfModules.Hom.app' φ X) n

The exterior power of a morphism is computed sectionwise.

source

noncomputable def PresheafOfModulesOfCommRing.exteriorPowerZeroIso {C : Type v} [CategoryTheory.Category.{w, v} C] (R : CategoryTheory.Functor Cᵒᵖ CommRingCat) :

exteriorPower 0 ≅ (CategoryTheory.Functor.const (PresheafOfModulesOfCommRing R)).obj (unit R)

The zeroth exterior power of a presheaf of R-modules is the unit presheaf of modules R, naturally; on sections it is ModuleCat.exteriorPower.iso₀.

Equations