Module

ModulesRigidify.lean

Nyll.AlgebraicCurves.Geometry.Sheaves.ModulesRigidify

4 declarations indexed from sourceView source ↗

Module documentation

Rigidification of sheaves of modules

Tensor a module with the pullback of the dual of its restriction to a chosen section. Module isomorphisms induce isomorphisms of these rigidifications.

Imports1

Nyll.SchemeTheory.Modules.Monoidal

Imported by54

def

dualMapIso

L33 ↗

AlgebraicGeometry.Scheme.Modules.dualMapIso

Documentation

The isomorphism of dual modules induced contravariantly by an isomorphism of modules.

Source context 5 commands

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

universe u
open CategoryTheory MonoidalCategory
noncomputable section
namespace AlgebraicGeometry.Scheme.Modules
variable {T P : Scheme.{u}}

Lean source · statement

def dualMapIso {X : Scheme.{u}} {L L' : X.Modules} (e : L ≅ L') :
    Scheme.Modules.dual L ≅ Scheme.Modules.dual L'

def

rigidify

L38 ↗

AlgebraicGeometry.Scheme.Modules.rigidify

Documentation

The module tensored with the pullback of the dual of its restriction to the section.

Source context 5 commands

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

universe u
open CategoryTheory MonoidalCategory
noncomputable section
namespace AlgebraicGeometry.Scheme.Modules
variable {T P : Scheme.{u}}

Lean source · statement

def rigidify (σ : T ⟶ P) (q : P ⟶ T) (L : P.Modules) : P.Modules

lemma

rigidify_def

L42 ↗

AlgebraicGeometry.Scheme.Modules.rigidify_def

Source context 5 commands

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

universe u
open CategoryTheory MonoidalCategory
noncomputable section
namespace AlgebraicGeometry.Scheme.Modules
variable {T P : Scheme.{u}}

Lean source · statement

lemma rigidify_def (σ : T ⟶ P) (q : P ⟶ T) (L : P.Modules) :
    rigidify σ q L = L ⊗ (Scheme.Modules.pullback q).obj
      (Scheme.Modules.dual ((Scheme.Modules.pullback σ).obj L))

def

rigidifyMapIso

L47 ↗

AlgebraicGeometry.Scheme.Modules.rigidifyMapIso

Documentation

The isomorphism of rigidified modules induced by the given module isomorphism.

Source context 5 commands

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

universe u
open CategoryTheory MonoidalCategory
noncomputable section
namespace AlgebraicGeometry.Scheme.Modules
variable {T P : Scheme.{u}}

Lean source · statement

def rigidifyMapIso (σ : T ⟶ P) (q : P ⟶ T) {L L' : P.Modules} (e : L ≅ L') :
    rigidify σ q L ≅ rigidify σ q L'

Module documentation

Rigidification of sheaves of modules

Declarations

dualMapIso

rigidify

rigidify_def

rigidifyMapIso