Module

TensorPowerComparison.lean

Nyll.SchemeTheory.Modules.TensorPowerComparison

3 declarations indexed from sourceView source ↗

Module documentation

Canonical comparisons for tensor powers of module sheaves

Tensor powers add under tensor product, transport along an isomorphism, and commute with pullback. Each comparison is constructed recursively from the monoidal structure.

Imports2

Imported by3

def

tensorPowAdd

L37 ↗

AlgebraicGeometry.Scheme.Modules.tensorPowAdd

Documentation

Tensoring powers of degrees m and n gives the power of degree m + n.

Source context 5 commands

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

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

Lean source · full declaration

def tensorPowAdd (L : X.Modules) (m : ℕ) :
    (n : ℕ) → (L.tensorPow m ⊗ L.tensorPow n ≅ L.tensorPow (m + n))
  | 0 => ρ_ (L.tensorPow m)
  | n + 1 =>
    (α_ (L.tensorPow m) (L.tensorPow n) L).symm ≪≫ whiskerRightIso (tensorPowAdd L m n) L

def

tensorPowMapIso

L44 ↗

AlgebraicGeometry.Scheme.Modules.tensorPowMapIso

Documentation

Transport a tensor power along an isomorphism of its module sheaf.

Source context 5 commands

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

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

Lean source · full declaration

def tensorPowMapIso {L₁ L₂ : X.Modules} (e : L₁ ≅ L₂) :
    (n : ℕ) → (L₁.tensorPow n ≅ L₂.tensorPow n)
  | 0 => Iso.refl _
  | n + 1 => tensorIso (tensorPowMapIso e n) e

def

pullbackTensorPowIso

L50 ↗

AlgebraicGeometry.Scheme.Modules.pullbackTensorPowIso

Documentation

Pullback commutes with tensor powers through its canonical monoidal comparison.

Source context 5 commands

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

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

Lean source · full declaration

def pullbackTensorPowIso {Y : Scheme.{u}} (c : X ⟶ Y) (L : Y.Modules) :
    (n : ℕ) → ((Modules.pullback c).obj (L.tensorPow n) ≅
      ((Modules.pullback c).obj L).tensorPow n)
  | 0 => pullbackTensorUnitObjIso c
  | n + 1 => pullbackTensorObjIso c (L.tensorPow n) L ≪≫
      whiskerRightIso (pullbackTensorPowIso c L n) ((Modules.pullback c).obj L)

Module documentation

Canonical comparisons for tensor powers of module sheaves

Declarations

tensorPowAdd

tensorPowMapIso

pullbackTensorPowIso