Documentation

LeanPool.RegtsSevenster.RS.Classical.Deligne.MulBy

Multiplication by a scalar #

For an algebra R in a monoidal category, an element g : 𝟙 ⟶ R of the even part of its Γ-algebra acts on R by multiplication. The resulting endomorphism RS.mulBy g sends the unit to g, and composing any element of the Γ-algebra into it is the convolution product with g.

This is the calculus behind the scalar computation for a simple algebra: multiplication by a nonzero even element has an ideal for its kernel and an ideal for its image, so simplicity makes it invertible, and the preimage of the unit is then an inverse for g.

source
noncomputable def RS.mulBy {D : Type u} [CategoryTheory.Category.{v, u} D] [CategoryTheory.MonoidalCategory D] (R : D) [CategoryTheory.MonObj R] (g : CategoryTheory.MonoidalCategoryStruct.tensorUnit D ⟶ R) :
R ⟶ R

Multiplication by an even scalar.

Equations
Instances For
    source
    theorem RS.comp_mulBy {D : Type u} [CategoryTheory.Category.{v, u} D] [CategoryTheory.MonoidalCategory D] (R : D) [CategoryTheory.MonObj R] {X : D} (g : CategoryTheory.MonoidalCategoryStruct.tensorUnit D ⟶ R) (h : X ⟶ R) :
    CategoryTheory.CategoryStruct.comp h (mulBy R g) = CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.leftUnitor X).inv (gmul g h)

    Multiplication by a scalar, applied to any element of the Γ-algebra, is the convolution product.

    source
    @[simp]
    theorem RS.unit_comp_mulBy {D : Type u} [CategoryTheory.Category.{v, u} D] [CategoryTheory.MonoidalCategory D] (R : D) [CategoryTheory.MonObj R] (g : CategoryTheory.MonoidalCategoryStruct.tensorUnit D ⟶ R) :
    CategoryTheory.CategoryStruct.comp CategoryTheory.MonObj.one (mulBy R g) = g

    Multiplication by a scalar sends the unit to that scalar.

    source
    @[simp]
    theorem RS.mulBy_one {D : Type u} [CategoryTheory.Category.{v, u} D] [CategoryTheory.MonoidalCategory D] (R : D) [CategoryTheory.MonObj R] :
    mulBy R CategoryTheory.MonObj.one = CategoryTheory.CategoryStruct.id R

    Multiplication by the unit is the identity.

    source
    theorem RS.mulBy_add {D : Type u} [CategoryTheory.Category.{v, u} D] [CategoryTheory.MonoidalCategory D] [CategoryTheory.Preadditive D] [CategoryTheory.MonoidalPreadditive D] (R : D) [CategoryTheory.MonObj R] (g g' : CategoryTheory.MonoidalCategoryStruct.tensorUnit D ⟶ R) :
    mulBy R (g + g') = mulBy R g + mulBy R g'

    Multiplication by a scalar is additive in the scalar.

    source
    @[simp]
    theorem RS.mulBy_zero {D : Type u} [CategoryTheory.Category.{v, u} D] [CategoryTheory.MonoidalCategory D] [CategoryTheory.Preadditive D] [CategoryTheory.MonoidalPreadditive D] (R : D) [CategoryTheory.MonObj R] :
    mulBy R 0 = 0

    Multiplication by the zero scalar is zero.

    source
    theorem RS.eq_zero_of_mulBy_eq_zero {D : Type u} [CategoryTheory.Category.{v, u} D] [CategoryTheory.MonoidalCategory D] [CategoryTheory.Preadditive D] (R : D) [CategoryTheory.MonObj R] {g : CategoryTheory.MonoidalCategoryStruct.tensorUnit D ⟶ R} (h : mulBy R g = 0) :
    g = 0

    A scalar whose multiplication vanishes is itself zero.

    source
    theorem RS.gmul_self_eq_zero_of_oddLine {D : Type u} [CategoryTheory.Category.{v, u} D] [CategoryTheory.MonoidalCategory D] [CategoryTheory.SymmetricCategory D] [CategoryTheory.Preadditive D] [CategoryTheory.Linear ℂ D] (R : D) [CategoryTheory.MonObj R] [CategoryTheory.IsCommMonObj R] (L : OddLine D) (f : L.obj ⟶ R) :
    gmul f f = 0

    An odd scalar squares to zero. The self-braiding of the odd line is −1, and convolution against a commutative algebra is commutative up to that braiding, so the square of an odd element is its own negative.