Exterior powers of sheaves of modules

This geometric consumer sheafifies the categorical objectwise exterior power from Algebra/Category/ModuleCat/Presheaf/ExteriorPower.lean. It also proves that the top exterior power of a free rank-n module sheaf is the structure sheaf. The semilinear algebra and free-module calculations live under LinearAlgebra/ExteriorPower/.

@[implicit_reducible]

def AlgebraicGeometry.Scheme.Modules.exteriorPowerCategory {X : Scheme} : CategoryTheory.Category.{u, u + 1} X.Modules

Equations

• AlgebraicGeometry.Scheme.Modules.exteriorPowerCategory = { toCategoryStruct := AlgebraicGeometry.Scheme.Modules.instCategory.toCategoryStruct, id_comp := ⋯, comp_id := ⋯, assoc := ⋯ }

noncomputable def AlgebraicGeometry.Scheme.Modules.exteriorPower {X : Scheme} (E : X.Modules) (n : ℕ) : X.Modules

The exterior power of a sheaf of modules, obtained by sheafifying the objectwise exterior power presheaf.

Equations

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

noncomputable def AlgebraicGeometry.Scheme.Modules.exteriorPowerMapIso {X : Scheme} {E F : X.Modules} (e : E ≅ F) (n : ℕ) : E.exteriorPower n ≅ F.exteriorPower n

Exterior powers carry isomorphic module sheaves to isomorphic module sheaves.

Equations

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

noncomputable def AlgebraicGeometry.Scheme.Modules.exteriorPowerSheafification {X : Scheme} (E : X.Modules) (n : ℕ) : PresheafOfModules.exteriorPower X.presheaf ((SheafOfModules.forget X.ringCatSheaf).obj E) n ⟶ (SheafOfModules.forget X.ringCatSheaf).obj (E.exteriorPower n)

The sheafification unit defining the exterior power of a sheaf of modules.

Equations

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

noncomputable def AlgebraicGeometry.Scheme.Modules.topExteriorFreeIso {X : Scheme} (n : ℕ) : exteriorPower (SheafOfModules.free (ULift.{u, 0} (Fin n))) n ≅ SheafOfModules.unit X.ringCatSheaf

The top exterior power of the free rank-n module sheaf is the structure sheaf.

Equations

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