Module

IdealSheafModule.lean

Nyll.AlgebraicCurves.Geometry.Sheaves.IdealSheafModule

6 declarations indexed from sourceView source ↗

Module documentation

Ideal sheaves and their associated modules

Constructs the module morphisms associated to an ideal sheaf and its closed subscheme.

Imports3

Mathlib.Algebra.Category.ModuleCat.Sheaf.PullbackFree
Nyll.SchemeTheory.Modules.Monoidal
Nyll.AlgebraicCurves.RelativeDivisors.RelEffCartierDiv

Imported by160

abbrev

unitToPushforwardUnit

L34 ↗

AlgebraicGeometry.Scheme.Hom.unitToPushforwardUnit

Documentation

The canonical map from the structure module to the pushforward structure module.

Source context 5 commands

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

universe u
open CategoryTheory CategoryTheory.Limits MonoidalCategory
noncomputable section
namespace AlgebraicGeometry
variable {X Y : Scheme.{u}}

Lean source · statement

abbrev Scheme.Hom.unitToPushforwardUnit (f : X ⟶ Y) :
    SheafOfModules.unit Y.ringCatSheaf ⟶
      (SheafOfModules.pushforward f.toRingCatSheafHom).obj (SheafOfModules.unit X.ringCatSheaf)

def

module

L42 ↗

AlgebraicGeometry.Scheme.IdealSheafData.module

Documentation

The ideal module, realized as the kernel of the quotient structure-sheaf map.

Source context 6 commands

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

universe u
open CategoryTheory CategoryTheory.Limits MonoidalCategory
noncomputable section
namespace AlgebraicGeometry
variable {X Y : Scheme.{u}}
namespace Scheme.IdealSheafData

Lean source · statement

def module (I : X.IdealSheafData) : X.Modules

def

moduleι

L46 ↗

AlgebraicGeometry.Scheme.IdealSheafData.moduleι

Documentation

The inclusion of the ideal module into the structure module.

Source context 6 commands

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

universe u
open CategoryTheory CategoryTheory.Limits MonoidalCategory
noncomputable section
namespace AlgebraicGeometry
variable {X Y : Scheme.{u}}
namespace Scheme.IdealSheafData

Lean source · statement

def moduleι (I : X.IdealSheafData) : I.module ⟶ 𝟙_ X.Modules

def

invModule

L50 ↗

AlgebraicGeometry.Scheme.IdealSheafData.invModule

Documentation

The dual of the ideal module.

Source context 6 commands

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

universe u
open CategoryTheory CategoryTheory.Limits MonoidalCategory
noncomputable section
namespace AlgebraicGeometry
variable {X Y : Scheme.{u}}
namespace Scheme.IdealSheafData

Lean source · statement

def invModule (I : X.IdealSheafData) : X.Modules

abbrev

idealModule

L56 ↗

AlgebraicGeometry.RelEffCartierDiv.idealModule

Documentation

The ideal module of the relative effective Cartier divisor.

Source context 5 commands

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

universe u
open CategoryTheory CategoryTheory.Limits MonoidalCategory
noncomputable section
namespace AlgebraicGeometry
variable {X Y : Scheme.{u}}

Lean source · statement

abbrev RelEffCartierDiv.idealModule {𝒞 S : Scheme.{u}} {f : 𝒞 ⟶ S} {r : ℕ} {T : Scheme.{u}}
    {g : T ⟶ S} (D : RelEffCartierDiv f r g) : (pullback f g).Modules

abbrev

lineBundle

L61 ↗

AlgebraicGeometry.RelEffCartierDiv.lineBundle

Documentation

The dual ideal module associated with the relative effective Cartier divisor.

Source context 5 commands

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

universe u
open CategoryTheory CategoryTheory.Limits MonoidalCategory
noncomputable section
namespace AlgebraicGeometry
variable {X Y : Scheme.{u}}

Lean source · statement

abbrev RelEffCartierDiv.lineBundle {𝒞 S : Scheme.{u}} {f : 𝒞 ⟶ S} {r : ℕ} {T : Scheme.{u}}
    {g : T ⟶ S} (D : RelEffCartierDiv f r g) : (pullback f g).Modules

Module documentation

Ideal sheaves and their associated modules

Declarations

unitToPushforwardUnit

module

moduleι

invModule

idealModule

lineBundle