Module

Scheme_Modules_nonempty_tensorPow_mul_iso.lean

Nyll.AlgebraicCurves.Geometry.Sheaves.Scheme_Modules_nonempty_tensorPow_mul_iso

3 declarations indexed from sourceView source ↗

Module documentation

Scheme Modules nonempty tensor Pow mul iso

Imports2

Imported by3

def

tensorPowAdd

L37 ↗

AlgebraicCurves.Geometry.Sheaves.Proofs.Scheme_Modules_nonempty_tensorPow_mul_iso.TensorPowMulSol.tensorPowAdd

Documentation

The canonical isomorphism expressing a tensor power of a sum as the tensor product of the two powers.

Source context 7 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Sheaves.Proofs.Scheme_Modules_nonempty_tensorPow_mul_iso
universe u
open _root_.CategoryTheory
open _root_.AlgebraicGeometry
open _root_.CategoryTheory.MonoidalCategory
namespace TensorPowMulSol

Lean source · full declaration

def tensorPowAdd {X : Scheme.{u}} (L : X.Modules) (a : ℕ) :
    (b : ℕ) → (L.tensorPow (a + b) ≅ L.tensorPow a ⊗ L.tensorPow b)
  | 0 => (ρ_ _).symm
  | b + 1 => (tensorPowAdd L a b ⊗ᵢ Iso.refl L) ≪≫ α_ _ _ _

def

tensorPowMul

L46 ↗

AlgebraicCurves.Geometry.Sheaves.Proofs.Scheme_Modules_nonempty_tensorPow_mul_iso.TensorPowMulSol.tensorPowMul

Documentation

The canonical isomorphism expressing the tensor power with exponent a * b as the bth power of the ath power.

Source context 7 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Sheaves.Proofs.Scheme_Modules_nonempty_tensorPow_mul_iso
universe u
open _root_.CategoryTheory
open _root_.AlgebraicGeometry
open _root_.CategoryTheory.MonoidalCategory
namespace TensorPowMulSol

Lean source · full declaration

def tensorPowMul {X : Scheme.{u}} (L : X.Modules) (a : ℕ) :
    (b : ℕ) → (L.tensorPow (a * b) ≅ (L.tensorPow a).tensorPow b)
  | 0 => Iso.refl _
  | b + 1 => tensorPowAdd L (a * b) a ≪≫ (tensorPowMul L a b ⊗ᵢ Iso.refl _)

theorem

nonempty_tensorPow_mul_iso

L53 ↗

AlgebraicGeometry.Scheme.Modules.nonempty_tensorPow_mul_iso

Source context 6 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Sheaves.Proofs.Scheme_Modules_nonempty_tensorPow_mul_iso
universe u
open _root_.CategoryTheory
open _root_.AlgebraicGeometry
open _root_.CategoryTheory.MonoidalCategory

Lean source · statement

theorem _root_.AlgebraicGeometry.Scheme.Modules.nonempty_tensorPow_mul_iso {X : Scheme.{u}} (L :
  X.Modules) (a b : ℕ) :
    Nonempty (L.tensorPow (a * b) ≅ (L.tensorPow a).tensorPow b)

Module documentation

Scheme Modules nonempty tensor Pow mul iso

Declarations

tensorPowAdd

tensorPowMul

nonempty_tensorPow_mul_iso