Documentation

Atlas.TensorCategories.code.TraceNonzero

source
class TensorCategories.SemisimpleCategory (C : Type u_1) [CategoryTheory.Category.{u_2, u_1} C] :
Prop

Working semisimplicity assumption on a category: every mono is a split mono and every epi is a split epi.

Instances
    source
    def TensorCategories.leftQuantumTraceLocal {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.MonoidalCategory C] [CategoryTheory.RigidCategory C] {V : C} (a : V ⟶ Vᘁᘁ) :
    CategoryTheory.MonoidalCategoryStruct.tensorUnit C ⟶ CategoryTheory.MonoidalCategoryStruct.tensorUnit C

    Local helper definition of the left quantum trace of a : V ⟶ V** in this file.

    Instances For
      source
      theorem TensorCategories.finrank_hom_unit_tensor_dual_eq_finrank_end {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.MonoidalCategory C] [CategoryTheory.RigidCategory C] (k : Type w) [Field k] [IsAlgClosed k] [CategoryTheory.Preadditive C] [CategoryTheory.Linear k C] [CategoryTheory.Abelian C] [CategoryTheory.MonoidalPreadditive C] [CategoryTheory.MonoidalLinear k C] (V : C) [CategoryTheory.Simple V] [FiniteDimensional k (V ⟶ V)] [FiniteDimensional k (CategoryTheory.MonoidalCategoryStruct.tensorUnit C ⟶ CategoryTheory.MonoidalCategoryStruct.tensorObj V Vᘁ)] :
      Module.finrank k (CategoryTheory.MonoidalCategoryStruct.tensorUnit C ⟶ CategoryTheory.MonoidalCategoryStruct.tensorObj V Vᘁ) = Module.finrank k (V ⟶ V)

      For a simple object V in a rigid category, the Hom-space Hom(𝟙, V ⊗ V*) has the same k-dimension as the endomorphism algebra of V.

      source
      theorem TensorCategories.isSplitEpi_cokernel_π_of_isSplitMono {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] [CategoryTheory.Abelian C] {X Y : C} (f : X ⟶ Y) [hf : CategoryTheory.IsSplitMono f] :
      CategoryTheory.IsSplitEpi (CategoryTheory.Limits.cokernel.π f)

      If f is a split mono in an abelian preadditive category, then the cokernel projection cokernel.π f is a split epi.

      source
      theorem TensorCategories.finrank_ge_two_of_mono_and_nonzero_cokernel_desc {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.MonoidalCategory C] (k : Type w) [Field k] [CategoryTheory.Preadditive C] [CategoryTheory.Linear k C] [CategoryTheory.Abelian C] [SemisimpleCategory C] [CategoryTheory.Simple (CategoryTheory.MonoidalCategoryStruct.tensorUnit C)] {X : C} (f : CategoryTheory.MonoidalCategoryStruct.tensorUnit C ⟶ X) (_hf_mono : CategoryTheory.Mono f) (g' : CategoryTheory.Limits.cokernel f ⟶ CategoryTheory.MonoidalCategoryStruct.tensorUnit C) (_hg' : g' ≠ 0) [FiniteDimensional k (CategoryTheory.MonoidalCategoryStruct.tensorUnit C ⟶ X)] :
      Module.finrank k (CategoryTheory.MonoidalCategoryStruct.tensorUnit C ⟶ X) ≥ 2

      In a semisimple category with simple unit, if f : 𝟙 → X is a mono and the cokernel admits a nonzero map back to 𝟙, then dim Hom(𝟙, X) ≥ 2.

      source
      theorem TensorCategories.composition_nonzero_of_finrank_one {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.MonoidalCategory C] (k : Type w) [Field k] [CategoryTheory.Preadditive C] [CategoryTheory.Linear k C] [CategoryTheory.Abelian C] [SemisimpleCategory C] [CategoryTheory.Simple (CategoryTheory.MonoidalCategoryStruct.tensorUnit C)] {X : C} (f : CategoryTheory.MonoidalCategoryStruct.tensorUnit C ⟶ X) (g : X ⟶ CategoryTheory.MonoidalCategoryStruct.tensorUnit C) [FiniteDimensional k (CategoryTheory.MonoidalCategoryStruct.tensorUnit C ⟶ X)] (hfin : Module.finrank k (CategoryTheory.MonoidalCategoryStruct.tensorUnit C ⟶ X) = 1) (hf : f ≠ 0) (hg : g ≠ 0) :
      CategoryTheory.CategoryStruct.comp f g ≠ 0

      In a semisimple category with simple unit, if dim Hom(𝟙, X) = 1 then the composition of any two nonzero morphisms 𝟙 → X and X → 𝟙 is nonzero.

      source
      theorem TensorCategories.coevaluation_ne_zero_of_simple {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.MonoidalCategory C] [CategoryTheory.RigidCategory C] [CategoryTheory.Preadditive C] [CategoryTheory.MonoidalPreadditive C] {V : C} [CategoryTheory.Simple V] :
      η_ V Vᘁ ≠ 0

      The coevaluation morphism η_ V (Vᘁ) : 𝟙 → V ⊗ V* of a simple object is nonzero.

      source
      theorem TensorCategories.evaluation_ne_zero_of_simple {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.MonoidalCategory C] [CategoryTheory.RigidCategory C] [CategoryTheory.Preadditive C] [CategoryTheory.MonoidalPreadditive C] {V : C} [CategoryTheory.Simple V] :
      ε_ Vᘁ Vᘁᘁ ≠ 0

      The evaluation morphism ε_ (Vᘁ) ((Vᘁ)ᘁ) : V* ⊗ V** → 𝟙 associated to a simple object is nonzero.