Documentation

TauCeti.CategoryTheory.Monoidal.TensorPow.Basic

Tensor powers of an object of a monoidal category #

For an object X of a monoidal category C, TauCeti.tensorPow X n is the n-fold tensor power of X, nested to the right: tensorPow X 0 = 𝟙_ C and tensorPow X (n + 1) = X ⊗ tensorPow X n.

Splitting a tensor power into two blocks is the isomorphism TauCeti.tensorPowAddIso X m n : tensorPow X m ⊗ tensorPow X n ≅ tensorPow X (n + m), defined by recursion on m. The index n + m is the one for which this recursion is definitional; comparing with other ways of writing the same exponent goes through eqToHom. The comparison is associative (TauCeti.tensorPowAddIso_assoc) and unital. Appending a factor on the right is the isomorphism TauCeti.tensorPowSuccIso X n : tensorPow X n ⊗ X ≅ tensorPow X (n + 1), which is compatible with the block decompositions on either side.

These comparisons are what is needed to move factors of a tensor power from one end to the other, for example to state that rotating the factors of tensorPow X n one at a time n times is the identity.

Main declarations #

TauCeti.tensorPow: the tensor powers of an object;
TauCeti.tensorPowAddIso and TauCeti.tensorPowAddIso_assoc: the block decomposition isomorphisms and their associativity;
TauCeti.tensorPowSuccIso: appending a factor on the right, with its compatibilities TauCeti.tensorPowSuccIso_hom_whiskerRight_tensorPowAddIso_hom and TauCeti.tensorPowAddIso_hom_whiskerRight_tensorPowSuccIso_hom.

@[reducible]

def TauCeti.tensorPow {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.MonoidalCategory C] (X : C) :

ℕ → C

The n-th tensor power of X, nested to the right: tensorPow X 0 = 𝟙_ C and tensorPow X (n + 1) = X ⊗ tensorPow X n.

Instances For

theorem TauCeti.tensorPow_zero {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.MonoidalCategory C] (X : C) :

tensorPow X 0 = CategoryTheory.MonoidalCategoryStruct.tensorUnit C

The zeroth tensor power is the unit.

theorem TauCeti.tensorPow_succ {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.MonoidalCategory C] (X : C) (n : ℕ) :

tensorPow X (n + 1) = CategoryTheory.MonoidalCategoryStruct.tensorObj X (tensorPow X n)

The tensor power tensorPow X (n + 1) is X ⊗ tensorPow X n.

def TauCeti.tensorPowAddIso {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.MonoidalCategory C] (X : C) (m n : ℕ) :

CategoryTheory.MonoidalCategoryStruct.tensorObj (tensorPow X m) (tensorPow X n) ≅ tensorPow X (n + m)

The block decomposition tensorPow X m ⊗ tensorPow X n ≅ tensorPow X (n + m) of a tensor power, built from associators and the left unitor by recursion on m.

Instances For

@[simp]

theorem TauCeti.tensorPowAddIso_zero {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.MonoidalCategory C] (X : C) (n : ℕ) :

tensorPowAddIso X 0 n = CategoryTheory.MonoidalCategoryStruct.leftUnitor (tensorPow X n)

The block decomposition with an empty first block is the left unitor.

theorem TauCeti.tensorPowAddIso_succ {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.MonoidalCategory C] (X : C) (m n : ℕ) :

tensorPowAddIso X (m + 1) n = CategoryTheory.MonoidalCategoryStruct.associator X (tensorPow X m) (tensorPow X n) ≪≫ CategoryTheory.MonoidalCategory.whiskerLeftIso X (tensorPowAddIso X m n)

The recursive step of the block decomposition.

theorem TauCeti.tensorPowAddIso_succ_hom {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.MonoidalCategory C] (X : C) (m n : ℕ) :

(tensorPowAddIso X (m + 1) n).hom = CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.associator X (tensorPow X m) (tensorPow X n)).hom (CategoryTheory.MonoidalCategoryStruct.whiskerLeft X (tensorPowAddIso X m n).hom)

The recursive step of the block decomposition, on morphisms.

theorem TauCeti.tensorPowAddIso_succ_inv {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.MonoidalCategory C] (X : C) (m n : ℕ) :

(tensorPowAddIso X (m + 1) n).inv = CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.whiskerLeft X (tensorPowAddIso X m n).inv) (CategoryTheory.MonoidalCategoryStruct.associator X (tensorPow X m) (tensorPow X n)).inv

The recursive step of the inverse block decomposition.

theorem TauCeti.tensorPowAddIso_one_hom {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.MonoidalCategory C] (X : C) (n : ℕ) :

(tensorPowAddIso X 1 n).hom = CategoryTheory.MonoidalCategoryStruct.whiskerRight (CategoryTheory.MonoidalCategoryStruct.rightUnitor X).hom (tensorPow X n)

The block decomposition with a first block of length one removes its trailing tensor unit.

theorem TauCeti.tensorPowAddIso_one_inv {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.MonoidalCategory C] (X : C) (n : ℕ) :

(tensorPowAddIso X 1 n).inv = CategoryTheory.MonoidalCategoryStruct.whiskerRight (CategoryTheory.MonoidalCategoryStruct.rightUnitor X).inv (tensorPow X n)

The inverse block decomposition with a first block of length one inserts its tensor unit.

theorem TauCeti.tensorPowAddIso_zero_right_hom {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.MonoidalCategory C] (X : C) (m : ℕ) :

(tensorPowAddIso X m 0).hom = CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.rightUnitor (tensorPow X m)).hom (CategoryTheory.eqToHom ⋯)

The block decomposition with an empty second block is the right unitor.

theorem TauCeti.tensorPowAddIso_zero_right_inv {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.MonoidalCategory C] (X : C) (m : ℕ) :

(tensorPowAddIso X m 0).inv = CategoryTheory.CategoryStruct.comp (CategoryTheory.eqToHom ⋯) (CategoryTheory.MonoidalCategoryStruct.rightUnitor (tensorPow X m)).inv

The inverse of the block decomposition with an empty second block is the inverse of the right unitor.

theorem TauCeti.tensorPowAddIso_assoc {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.MonoidalCategory C] (X : C) (a b c : ℕ) :

CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.whiskerRight (tensorPowAddIso X a b).hom (tensorPow X c)) (tensorPowAddIso X (b + a) c).hom = CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.associator (tensorPow X a) (tensorPow X b) (tensorPow X c)).hom (CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.whiskerLeft (tensorPow X a) (tensorPowAddIso X b c).hom) (CategoryTheory.CategoryStruct.comp (tensorPowAddIso X a (c + b)).hom (CategoryTheory.eqToHom ⋯)))

Associativity of the block decompositions: splitting tensorPow X (c + (b + a)) into three blocks of lengths a, b, c does not depend on the order of the two splittings.

theorem TauCeti.eqToHom_whiskerRight_tensorPowAddIso_hom {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.MonoidalCategory C] (X : C) {m m' : ℕ} (h : m = m') (n : ℕ) :

CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.whiskerRight (CategoryTheory.eqToHom ⋯) (tensorPow X n)) (tensorPowAddIso X m' n).hom = CategoryTheory.CategoryStruct.comp (tensorPowAddIso X m n).hom (CategoryTheory.eqToHom ⋯)

The block decomposition is natural in the length of the first block.

theorem TauCeti.eqToHom_whiskerRight_tensorPowAddIso_hom_assoc {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.MonoidalCategory C] (X : C) {m m' : ℕ} (h : m = m') (n : ℕ) {Z : C} (h✝ : tensorPow X (n + m') ⟶ Z) :

CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.whiskerRight (CategoryTheory.eqToHom ⋯) (tensorPow X n)) (CategoryTheory.CategoryStruct.comp (tensorPowAddIso X m' n).hom h✝) = CategoryTheory.CategoryStruct.comp (tensorPowAddIso X m n).hom (CategoryTheory.CategoryStruct.comp (CategoryTheory.eqToHom ⋯) h✝)

The block decomposition is natural in the length of the first block.

theorem TauCeti.whiskerLeft_eqToHom_tensorPowAddIso_hom {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.MonoidalCategory C] (X : C) (m : ℕ) {n n' : ℕ} (h : n = n') :

CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.whiskerLeft (tensorPow X m) (CategoryTheory.eqToHom ⋯)) (tensorPowAddIso X m n').hom = CategoryTheory.CategoryStruct.comp (tensorPowAddIso X m n).hom (CategoryTheory.eqToHom ⋯)

The block decomposition is natural in the length of the second block.

theorem TauCeti.whiskerLeft_eqToHom_tensorPowAddIso_hom_assoc {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.MonoidalCategory C] (X : C) (m : ℕ) {n n' : ℕ} (h : n = n') {Z : C} (h✝ : tensorPow X (n' + m) ⟶ Z) :

CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.whiskerLeft (tensorPow X m) (CategoryTheory.eqToHom ⋯)) (CategoryTheory.CategoryStruct.comp (tensorPowAddIso X m n').hom h✝) = CategoryTheory.CategoryStruct.comp (tensorPowAddIso X m n).hom (CategoryTheory.CategoryStruct.comp (CategoryTheory.eqToHom ⋯) h✝)

The block decomposition is natural in the length of the second block.

def TauCeti.tensorPowSuccIso {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.MonoidalCategory C] (X : C) (n : ℕ) :

CategoryTheory.MonoidalCategoryStruct.tensorObj (tensorPow X n) X ≅ tensorPow X (n + 1)

Appending a factor on the right: tensorPow X n ⊗ X ≅ tensorPow X (n + 1), the block decomposition with a second block of length one.

Instances For

theorem TauCeti.tensorPowSuccIso_hom {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.MonoidalCategory C] (X : C) (n : ℕ) :

(tensorPowSuccIso X n).hom = CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.whiskerLeft (tensorPow X n) (CategoryTheory.MonoidalCategoryStruct.rightUnitor X).inv) (CategoryTheory.CategoryStruct.comp (tensorPowAddIso X n 1).hom (CategoryTheory.eqToHom ⋯))

The formula for appending a factor on the right.

@[simp]

theorem TauCeti.tensorPowSuccIso_zero_hom {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.MonoidalCategory C] (X : C) :

(tensorPowSuccIso X 0).hom = CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.leftUnitor X).hom (CategoryTheory.MonoidalCategoryStruct.rightUnitor X).inv

Appending a factor on the right of the zeroth tensor power swaps the left and right unitors.

@[simp]

theorem TauCeti.tensorPowSuccIso_zero_inv {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.MonoidalCategory C] (X : C) :

(tensorPowSuccIso X 0).inv = CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.rightUnitor X).hom (CategoryTheory.MonoidalCategoryStruct.leftUnitor X).inv

The inverse of tensorPowSuccIso at 0.

theorem TauCeti.tensorPowSuccIso_succ_hom {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.MonoidalCategory C] (X : C) (n : ℕ) :

(tensorPowSuccIso X (n + 1)).hom = CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.associator X (tensorPow X n) X).hom (CategoryTheory.MonoidalCategoryStruct.whiskerLeft X (tensorPowSuccIso X n).hom)

Recursive step for appending a factor on the right of a tensor power.

theorem TauCeti.tensorPowSuccIso_hom_whiskerRight_tensorPowAddIso_hom {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.MonoidalCategory C] (X : C) (m n : ℕ) :

CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.whiskerRight (tensorPowSuccIso X m).hom (tensorPow X n)) (tensorPowAddIso X (m + 1) n).hom = CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.associator (tensorPow X m) X (tensorPow X n)).hom (CategoryTheory.CategoryStruct.comp (tensorPowAddIso X m (n + 1)).hom (CategoryTheory.eqToHom ⋯))

Appending a factor to the first of two blocks and then joining them is joining the factor to the second block.

theorem TauCeti.tensorPowSuccIso_hom_whiskerRight_tensorPowAddIso_hom_assoc {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.MonoidalCategory C] (X : C) (m n : ℕ) {Z : C} (h : tensorPow X (n + (m + 1)) ⟶ Z) :

Appending a factor to the first of two blocks and then joining them is joining the factor to the second block.

theorem TauCeti.tensorPowAddIso_hom_whiskerRight_tensorPowSuccIso_hom {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.MonoidalCategory C] (X : C) (m n : ℕ) :

Joining two blocks and then appending a factor is appending the factor to the second block and then joining.

theorem TauCeti.tensorPowAddIso_hom_whiskerRight_tensorPowSuccIso_hom_assoc {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.MonoidalCategory C] (X : C) (m n : ℕ) {Z : C} (h : tensorPow X (n + m + 1) ⟶ Z) :

Joining two blocks and then appending a factor is appending the factor to the second block and then joining.

def TauCeti.tensorPowMap {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.MonoidalCategory C] {X Y : C} (f : X ⟶ Y) (n : ℕ) :

tensorPow X n ⟶ tensorPow Y n

The n-th tensor power f ⊗ₘ ⋯ ⊗ₘ f of a morphism f : X ⟶ Y.

Instances For

@[simp]

theorem TauCeti.tensorPowMap_zero {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.MonoidalCategory C] {X Y : C} (f : X ⟶ Y) :

tensorPowMap f 0 = CategoryTheory.CategoryStruct.id (CategoryTheory.MonoidalCategoryStruct.tensorUnit C)

The zeroth tensor power of a morphism is the identity of the unit.

theorem TauCeti.tensorPowMap_succ {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.MonoidalCategory C] {X Y : C} (f : X ⟶ Y) (n : ℕ) :

tensorPowMap f (n + 1) = CategoryTheory.MonoidalCategoryStruct.tensorHom f (tensorPowMap f n)

The tensor power tensorPowMap f (n + 1) is f ⊗ₘ tensorPowMap f n.

@[simp]

theorem TauCeti.tensorPowMap_id {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.MonoidalCategory C] (X : C) (n : ℕ) :

tensorPowMap (CategoryTheory.CategoryStruct.id X) n = CategoryTheory.CategoryStruct.id (tensorPow X n)

The tensor powers of an identity are identities.

@[simp]

theorem TauCeti.tensorPowMap_comp {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.MonoidalCategory C] {X Y Z : C} (f : X ⟶ Y) (g : Y ⟶ Z) (n : ℕ) :

tensorPowMap (CategoryTheory.CategoryStruct.comp f g) n = CategoryTheory.CategoryStruct.comp (tensorPowMap f n) (tensorPowMap g n)

The tensor powers of a composite are the composites of the tensor powers.

theorem TauCeti.tensorPowMap_comp_assoc {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.MonoidalCategory C] {X Y Z : C} (f : X ⟶ Y) (g : Y ⟶ Z) (n : ℕ) {Z✝ : C} (h : tensorPow Z n ⟶ Z✝) :

CategoryTheory.CategoryStruct.comp (tensorPowMap (CategoryTheory.CategoryStruct.comp f g) n) h = CategoryTheory.CategoryStruct.comp (tensorPowMap f n) (CategoryTheory.CategoryStruct.comp (tensorPowMap g n) h)

The tensor powers of a composite are the composites of the tensor powers.

def TauCeti.tensorPowMapIso {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.MonoidalCategory C] {X Y : C} (e : X ≅ Y) (n : ℕ) :

tensorPow X n ≅ tensorPow Y n

The tensor powers of an isomorphism, as an isomorphism.

Instances For

@[simp]

theorem TauCeti.tensorPowMapIso_hom {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.MonoidalCategory C] {X Y : C} (e : X ≅ Y) (n : ℕ) :

(tensorPowMapIso e n).hom = tensorPowMap e.hom n

The tensor powers of an isomorphism, on morphisms.

@[simp]

theorem TauCeti.tensorPowMapIso_inv {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.MonoidalCategory C] {X Y : C} (e : X ≅ Y) (n : ℕ) :

(tensorPowMapIso e n).inv = tensorPowMap e.inv n

The tensor powers of an isomorphism, on inverses.

theorem TauCeti.tensorPowAddIso_hom_naturality {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.MonoidalCategory C] {X Y : C} (f : X ⟶ Y) (m n : ℕ) :

CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.tensorHom (tensorPowMap f m) (tensorPowMap f n)) (tensorPowAddIso Y m n).hom = CategoryTheory.CategoryStruct.comp (tensorPowAddIso X m n).hom (tensorPowMap f (n + m))

The block decompositions are natural.

theorem TauCeti.tensorPowAddIso_hom_naturality_assoc {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.MonoidalCategory C] {X Y : C} (f : X ⟶ Y) (m n : ℕ) {Z : C} (h : tensorPow Y (n + m) ⟶ Z) :

CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.tensorHom (tensorPowMap f m) (tensorPowMap f n)) (CategoryTheory.CategoryStruct.comp (tensorPowAddIso Y m n).hom h) = CategoryTheory.CategoryStruct.comp (tensorPowAddIso X m n).hom (CategoryTheory.CategoryStruct.comp (tensorPowMap f (n + m)) h)

The block decompositions are natural.

theorem TauCeti.tensorPowMap_eqToHom {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.MonoidalCategory C] {X Y : C} (f : X ⟶ Y) {m n : ℕ} (h : m = n) :

CategoryTheory.CategoryStruct.comp (tensorPowMap f m) (CategoryTheory.eqToHom ⋯) = CategoryTheory.CategoryStruct.comp (CategoryTheory.eqToHom ⋯) (tensorPowMap f n)

Transporting along an equality of exponents commutes with the tensor powers of a morphism.

theorem TauCeti.tensorPowMap_eqToHom_assoc {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.MonoidalCategory C] {X Y : C} (f : X ⟶ Y) {m n : ℕ} (h : m = n) {Z : C} (h✝ : tensorPow Y n ⟶ Z) :

CategoryTheory.CategoryStruct.comp (tensorPowMap f m) (CategoryTheory.CategoryStruct.comp (CategoryTheory.eqToHom ⋯) h✝) = CategoryTheory.CategoryStruct.comp (CategoryTheory.eqToHom ⋯) (CategoryTheory.CategoryStruct.comp (tensorPowMap f n) h✝)

Transporting along an equality of exponents commutes with the tensor powers of a morphism.

theorem TauCeti.tensorPowSuccIso_hom_naturality {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.MonoidalCategory C] {X Y : C} (f : X ⟶ Y) (n : ℕ) :

CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.tensorHom (tensorPowMap f n) f) (tensorPowSuccIso Y n).hom = CategoryTheory.CategoryStruct.comp (tensorPowSuccIso X n).hom (tensorPowMap f (n + 1))

Appending a factor on the right is natural.

theorem TauCeti.tensorPowSuccIso_hom_naturality_assoc {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.MonoidalCategory C] {X Y : C} (f : X ⟶ Y) (n : ℕ) {Z : C} (h : tensorPow Y (n + 1) ⟶ Z) :

CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.tensorHom (tensorPowMap f n) f) (CategoryTheory.CategoryStruct.comp (tensorPowSuccIso Y n).hom h) = CategoryTheory.CategoryStruct.comp (tensorPowSuccIso X n).hom (CategoryTheory.CategoryStruct.comp (tensorPowMap f (n + 1)) h)

Appending a factor on the right is natural.