NYLL
Module

ModulesDet.lean

Nyll.AlgebraicCurves.Geometry.Sheaves.ModulesDet
4 declarations indexed from sourceView source ↗

Module documentation

Exterior powers and determinants of module sheaves

Presheaf exterior powers descend through sheafification to exterior-power functors on module sheaves; their objects define the determinant notation.

Imports2
Imported by33

Declarations

abbrev

presheafExteriorPower

L33 ↗
AlgebraicGeometry.Scheme.Modules.presheafExteriorPower
Documentation

The exterior-power functor on the underlying module presheaves of the scheme.

Source context 4 commands

Surrounding namespaces, section variables, and local commands at this declaration.

universe u
open CategoryTheory
namespace AlgebraicGeometry.Scheme.Modules
variable (X : Scheme.{u})
Lean source · statement
abbrev presheafExteriorPower (n : ℕ) : X.PresheafOfModules ⥤ X.PresheafOfModules
def

exteriorPower

L37 ↗
AlgebraicGeometry.Scheme.Modules.exteriorPower
Documentation

The exterior-power functor on module sheaves, obtained by sheafifying presheaf powers.

Source context 4 commands

Surrounding namespaces, section variables, and local commands at this declaration.

universe u
open CategoryTheory
namespace AlgebraicGeometry.Scheme.Modules
variable (X : Scheme.{u})
Lean source · statement
def exteriorPower (n : ℕ) : X.Modules ⥤ X.Modules
abbrev

det

L43 ↗
AlgebraicGeometry.Scheme.Modules.det
Documentation

The module sheaf given by the specified exterior power of M.

Source context 5 commands

Surrounding namespaces, section variables, and local commands at this declaration.

universe u
open CategoryTheory
namespace AlgebraicGeometry.Scheme.Modules
variable (X : Scheme.{u})
variable {X} in
Lean source · statement
abbrev det (n : ℕ) (M : X.Modules) : X.Modules
lemma

exteriorPower_obj

L46 ↗
AlgebraicGeometry.Scheme.Modules.exteriorPower_obj
Source context 6 commands

Surrounding namespaces, section variables, and local commands at this declaration.

universe u
open CategoryTheory
namespace AlgebraicGeometry.Scheme.Modules
variable (X : Scheme.{u})
variable {X} in
variable {X} in
Lean source · statement
lemma exteriorPower_obj (n : ℕ) (M : X.Modules) :
    (exteriorPower X n).obj M =
      (_root_.PresheafOfModules.sheafification (𝟙 X.ringCatSheaf.obj)).obj
        ((presheafExteriorPower X n).obj M.val)

Statements and documentation are read from the Lean source at the revision shown. Source entries are not a measure of mathematical completeness.