Module

TensorPowers.lean

Nyll.SchemeTheory.Modules.TensorPowers

4 declarations indexed from sourceView source ↗

Module documentation

Tensor powers start at the unit, adjoin one tensor factor at a time, and carry the canonical degree-one comparison.

Imports1

Imported by15

def

AlgebraicGeometry.Scheme.Modules.tensorPow

Documentation

The iterated tensor power, with the tensor unit in degree zero.

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 tensorPow (L : X.Modules) : ℕ → X.Modules
  | 0 => 𝟙_ X.Modules
  | n + 1 => tensorPow L n ⊗ L

theorem

AlgebraicGeometry.Scheme.Modules.tensorPow_zero

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 · statement

theorem tensorPow_zero (L : X.Modules) : L.tensorPow 0 = 𝟙_ X.Modules

theorem

AlgebraicGeometry.Scheme.Modules.tensorPow_succ

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 · statement

theorem tensorPow_succ (L : X.Modules) (n : ℕ) : L.tensorPow (n + 1) = L.tensorPow n ⊗ L

def

AlgebraicGeometry.Scheme.Modules.tensorPowOneIso

Documentation

The degree-one tensor power identified with the original module by the left unitor.

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 · statement

def tensorPowOneIso (L : X.Modules) : L.tensorPow 1 ≅ L