Module

ModulesNormModule.lean

Nyll.AlgebraicCurves.Geometry.Sheaves.ModulesNormModule

11 declarations indexed from sourceView source ↗

Module documentation

Modules Norm Module

Imports2

Imported by37

def

normModule

L31 ↗

AlgebraicGeometry.Scheme.Modules.normModule

Documentation

The module sheaf det d (π_* L) tensored with the dual of det d (π_* 𝟙).

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.Scheme.Modules
variable {X Y : Scheme.{u}}

Lean source · statement

def normModule (π : X ⟶ Y) (d : ℕ) (L : X.Modules) : Y.Modules

theorem

normModule_def

L34 ↗

AlgebraicGeometry.Scheme.Modules.normModule_def

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.Scheme.Modules
variable {X Y : Scheme.{u}}

Lean source · statement

theorem normModule_def (π : X ⟶ Y) (d : ℕ) (L : X.Modules) :
    normModule π d L = det d ((pushforward π).obj L) ⊗ dual (det d ((pushforward π).obj (𝟙_
      X.Modules)))

def

normModuleFunctor

L40 ↗

AlgebraicGeometry.Scheme.Modules.normModuleFunctor

Documentation

The functor taking L to normModule π d L, using exterior powers of pushforward and a fixed dual determinant factor.

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.Scheme.Modules
variable {X Y : Scheme.{u}}

Lean source · statement

def normModuleFunctor (π : X ⟶ Y) (d : ℕ) : X.Modules ⥤ Y.Modules

theorem

normModuleFunctor_obj

L44 ↗

AlgebraicGeometry.Scheme.Modules.normModuleFunctor_obj

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.Scheme.Modules
variable {X Y : Scheme.{u}}

Lean source · statement

theorem normModuleFunctor_obj (π : X ⟶ Y) (d : ℕ) (L : X.Modules) :
    (normModuleFunctor π d).obj L = normModule π d L

theorem

normModuleFunctor_map

L47 ↗

AlgebraicGeometry.Scheme.Modules.normModuleFunctor_map

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.Scheme.Modules
variable {X Y : Scheme.{u}}

Lean source · statement

theorem normModuleFunctor_map (π : X ⟶ Y) (d : ℕ) {L L' : X.Modules} (f : L ⟶ L') :
    (normModuleFunctor π d).map f =
      (exteriorPower Y d).map ((pushforward π).map f) ▷ dual (det d ((pushforward π).obj (𝟙_
        X.Modules)))

def

normModuleMapIso

L53 ↗

AlgebraicGeometry.Scheme.Modules.normModuleMapIso

Documentation

The isomorphism of norm modules induced by an isomorphism of the input module sheaves.

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.Scheme.Modules
variable {X Y : Scheme.{u}}

Lean source · statement

def normModuleMapIso (π : X ⟶ Y) (d : ℕ) {L L' : X.Modules} (e : L ≅ L') :
    normModule π d L ≅ normModule π d L'

def

dualCongr

L58 ↗

AlgebraicGeometry.Scheme.Modules.dualCongr

Documentation

The isomorphism of dual module sheaves induced contravariantly by e.

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.Scheme.Modules
variable {X Y : Scheme.{u}}

Lean source · full declaration

def dualCongr {A B : Y.Modules} (e : A ≅ B) : dual A ≅ dual B where
  hom := (MonoidalClosed.pre e.inv).app (𝟙_ Y.Modules)
  inv := (MonoidalClosed.pre e.hom).app (𝟙_ Y.Modules)
  hom_inv_id := by
    rw [← NatTrans.comp_app, ← MonoidalClosed.pre_map, e.hom_inv_id, MonoidalClosed.pre_id,
      NatTrans.id_app]
  inv_hom_id := by
    rw [← NatTrans.comp_app, ← MonoidalClosed.pre_map, e.inv_hom_id, MonoidalClosed.pre_id,
      NatTrans.id_app]

def

normModuleIdIso

L70 ↗

AlgebraicGeometry.Scheme.Modules.normModuleIdIso

Documentation

Identify the norm along the identity with det d L tensored with the dual of the determinant of the unit 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.Scheme.Modules
variable {X Y : Scheme.{u}}

Lean source · statement

def normModuleIdIso (d : ℕ) (L : X.Modules) :
    normModule (𝟙 X) d L ≅ det d L ⊗ dual (det d (𝟙_ X.Modules))

def

normModuleCongr

L76 ↗

AlgebraicGeometry.Scheme.Modules.normModuleCongr

Documentation

The comparison of norm modules associated to equal scheme morphisms π and π'.

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.Scheme.Modules
variable {X Y : Scheme.{u}}

Lean source · statement

def normModuleCongr {π π' : X ⟶ Y} (h : π = π') (d : ℕ) (L : X.Modules) :
    normModule π d L ≅ normModule π' d L

theorem

normModule_tensorUnit

L81 ↗

AlgebraicGeometry.Scheme.Modules.normModule_tensorUnit

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.Scheme.Modules
variable {X Y : Scheme.{u}}

Lean source · statement

theorem normModule_tensorUnit (π : X ⟶ Y) (d : ℕ) :
    normModule π d (𝟙_ X.Modules) =
      det d ((pushforward π).obj (𝟙_ X.Modules)) ⊗ dual (det d ((pushforward π).obj (𝟙_
        X.Modules)))

def

normModuleUnitEval

L88 ↗

AlgebraicGeometry.Scheme.Modules.normModuleUnitEval

Documentation

Evaluate the determinant factor against its dual to map the norm of the unit module to the unit 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.Scheme.Modules
variable {X Y : Scheme.{u}}

Lean source · statement

def normModuleUnitEval (π : X ⟶ Y) (d : ℕ) : normModule π d (𝟙_ X.Modules) ⟶ 𝟙_ Y.Modules

Module documentation

Modules Norm Module

Declarations