Other results

Results named in the rest of Tau Ceti's TauCeti.CategoryTheory modules and in no roadmap's section, as Tau Ceti has them at commit ace60277.

DefinitionThe DG Yoneda lemma#

evaluation at the identity of X is an isomorphism from the Hom complex of right DG modules Hom(Hom(-, X), F) to the complex F(X).

TauCeti.dgRepresentableHomIso.{v} (R : Type v) [CommRing R] {C : Type v} [TauCeti.DGCategory R C]
  (X : C)
  (F :
    CategoryTheory.EnrichedFunctor (CochainComplex (ModuleCat R) ℤ) Cᵒᵖ
      (CochainComplex (ModuleCat R) ℤ)) :
  TauCeti.dgHomComplex R { toEnrichedFunctor := TauCeti.dgRepresentable R X }
      { toEnrichedFunctor := F } ≅
    F.obj (Opposite.op X)

Lean

Formalized in Tau Ceti as TauCeti.dgRepresentableHomIso.

Other forms

The DG Yoneda lemma, degreewise. Formalized in Tau Ceti as TauCeti.dgRepresentableHomEquiv.

TauCeti.dgRepresentableHomEquiv.{v} (R : Type v) [CommRing R] {C : Type v} [TauCeti.DGCategory R C]
  (X : C)
  (F :
    CategoryTheory.EnrichedFunctor (CochainComplex (ModuleCat R) ℤ) Cᵒᵖ
      (CochainComplex (ModuleCat R) ℤ))
  (n : ℤ) :
  TauCeti.DGHom R n { toEnrichedFunctor := TauCeti.dgRepresentable R X }
      { toEnrichedFunctor := F } ≃ₗ[R]
    ↑((F.obj (Opposite.op X)).X n)

Sources

• Tau Ceti documentation: TauCeti.dgRepresentableHomIso
• Source of TauCeti.dgRepresentableHomIso in TauCeti/CategoryTheory/DG/Yoneda.lean

LeanTauCeti.dgRepresentableHomIso · TauCeti.dgRepresentableHomEquiv

TheoremFrobenius reciprocity in multiplicity form#

N_{S T}^U is the multiplicity of T in Sᘁ ⊗ U, coming from (Sᘁ ⊗ U ⟶ T) ≃ (U ⟶ S ⊗ T).

TauCeti.fusionCoeff_eq_simpleMultiplicities_rightDual_tensor.{w', v, u} {C : Type u}
  [CategoryTheory.Category.{v, u} C] [CategoryTheory.Abelian C] [CategoryTheory.MonoidalCategory C]
  [CategoryTheory.MonoidalPreadditive C] [CategoryTheory.RigidCategory C] (k : Type w') [Field k]
  [IsAlgClosed k] [CategoryTheory.Linear k C] [CategoryTheory.MonoidalLinear k C]
  [TauCeti.IsFiniteSemisimpleCategory C] [∀ (X Y : C), FiniteDimensional k (X ⟶ Y)]
  (S T U : TauCeti.SimpleClasses C) :
  TauCeti.fusionCoeff k S T U =
    (TauCeti.simpleMultiplicities (CategoryTheory.MonoidalCategoryStruct.tensorObj S.reprᘁ U.repr))
      T

Lean

Formalized in Tau Ceti as TauCeti.fusionCoeff_eq_simpleMultiplicities_rightDual_tensor.

Other forms

Frobenius reciprocity for fusion coefficients. Formalized in Tau Ceti as TauCeti.fusionCoeff_dual_left.

TauCeti.fusionCoeff_dual_left.{w', v, u} {C : Type u} [CategoryTheory.Category.{v, u} C]
  [CategoryTheory.Abelian C] [CategoryTheory.MonoidalCategory C]
  [CategoryTheory.MonoidalPreadditive C] [CategoryTheory.RigidCategory C] (k : Type w') [Field k]
  [IsAlgClosed k] [CategoryTheory.Linear k C] [CategoryTheory.MonoidalLinear k C]
  [TauCeti.IsFiniteSemisimpleCategory C] [∀ (X Y : C), FiniteDimensional k (X ⟶ Y)]
  (S T U : TauCeti.SimpleClasses C) : TauCeti.fusionCoeff k S.dual T U = TauCeti.fusionCoeff k S U T

Frobenius reciprocity for fusion coefficients. Formalized in Tau Ceti as TauCeti.fusionCoeff_dual_right.

TauCeti.fusionCoeff_dual_right.{w', v, u} {C : Type u} [CategoryTheory.Category.{v, u} C]
  [CategoryTheory.Abelian C] [CategoryTheory.MonoidalCategory C]
  [CategoryTheory.MonoidalPreadditive C] [CategoryTheory.RigidCategory C] (k : Type w') [Field k]
  [IsAlgClosed k] [CategoryTheory.Linear k C] [CategoryTheory.MonoidalLinear k C]
  [TauCeti.IsFiniteSemisimpleCategory C] [∀ (X Y : C), FiniteDimensional k (X ⟶ Y)]
  (S T U : TauCeti.SimpleClasses C) : TauCeti.fusionCoeff k S T.dual U = TauCeti.fusionCoeff k U T S

Frobenius reciprocity in multiplicity form. Formalized in Tau Ceti as TauCeti.fusionCoeff_eq_simpleMultiplicities_tensor_rightDual.

TauCeti.fusionCoeff_eq_simpleMultiplicities_tensor_rightDual.{w', v, u} {C : Type u}
  [CategoryTheory.Category.{v, u} C] [CategoryTheory.Abelian C] [CategoryTheory.MonoidalCategory C]
  [CategoryTheory.MonoidalPreadditive C] [CategoryTheory.RigidCategory C] (k : Type w') [Field k]
  [IsAlgClosed k] [CategoryTheory.Linear k C] [CategoryTheory.MonoidalLinear k C]
  [TauCeti.IsFiniteSemisimpleCategory C] [∀ (X Y : C), FiniteDimensional k (X ⟶ Y)]
  (S T U : TauCeti.SimpleClasses C) :
  TauCeti.fusionCoeff k S T U =
    (TauCeti.simpleMultiplicities (CategoryTheory.MonoidalCategoryStruct.tensorObj U.repr T.reprᘁ))
      S

Sources

• Tau Ceti documentation: TauCeti.fusionCoeff_eq_simpleMultiplicities_rightDual_tensor
• Source of TauCeti.fusionCoeff_eq_simpleMultiplicities_rightDual_tensor in TauCeti/CategoryTheory/Semisimple/Rigid.lean

LeanTauCeti.fusionCoeff_eq_simpleMultiplicities_rightDual_tensor · TauCeti.fusionCoeff_dual_left · TauCeti.fusionCoeff_dual_right · TauCeti.fusionCoeff_eq_simpleMultiplicities_tensor_rightDual

Uses 1 · Used by 3

Statement usesTauCeti.fusionCoeff

Used byCharacters of the Grothendieck ring are ⋆-characters · TauCeti.frobeniusPerronDim · TauCeti.SplitK0.spectralRadius_fusionMatrix

TheoremNg–Schauenburg#

the (n + 1)-st iterate of E_V^{(n+1)} is the identity.

TauCeti.iterate_frobeniusSchurRotate_eq_id.{v, u} {C : Type u} [CategoryTheory.Category.{v, u} C]
  [CategoryTheory.MonoidalCategory C] [CategoryTheory.RigidCategory C] [TauCeti.PivotalCategory C]
  (V : C) (n : ℕ) : (TauCeti.frobeniusSchurRotate V n)^[n + 1] = id

Lean

Formalized in Tau Ceti as TauCeti.iterate_frobeniusSchurRotate_eq_id.

Sources

• Tau Ceti documentation: TauCeti.iterate_frobeniusSchurRotate_eq_id
• Source of TauCeti.iterate_frobeniusSchurRotate_eq_id in TauCeti/CategoryTheory/Monoidal/Pivotal/FrobeniusSchur/Basic.lean

LeanTauCeti.iterate_frobeniusSchurRotate_eq_id

Used by 1

Used byNg–Schauenburg trichotomy

TheoremNg–Schauenburg trichotomy#

for a simple object V (with Vᘁ simple and V ⟶ V finite-dimensional over an algebraically closed field k), the second Frobenius–Schur indicator takes values in {1, 0, -1}.

TauCeti.frobeniusSchurIndicator_two_eq_one_or_eq_zero_or_eq_neg_one.{w, v, u} {C : Type u}
  [CategoryTheory.Category.{v, u} C] [CategoryTheory.MonoidalCategory C]
  [CategoryTheory.Preadditive C] [CategoryTheory.MonoidalPreadditive C]
  [CategoryTheory.RigidCategory C] [TauCeti.PivotalCategory C] [CategoryTheory.Limits.HasKernels C]
  (k : Type w) [Field k] [IsAlgClosed k] [CategoryTheory.Linear k C]
  [CategoryTheory.MonoidalLinear k C] (V : C) [CategoryTheory.Simple V]
  [FiniteDimensional k (V ⟶ V)] [CategoryTheory.Simple Vᘁ] :
  TauCeti.frobeniusSchurIndicator k V 2 = 1 ∨
    TauCeti.frobeniusSchurIndicator k V 2 = 0 ∨ TauCeti.frobeniusSchurIndicator k V 2 = -1

Lean

Formalized in Tau Ceti as TauCeti.frobeniusSchurIndicator_two_eq_one_or_eq_zero_or_eq_neg_one.

Sources

• Tau Ceti documentation: TauCeti.frobeniusSchurIndicator_two_eq_one_or_eq_zero_or_eq_neg_one
• Source of TauCeti.frobeniusSchurIndicator_two_eq_one_or_eq_zero_or_eq_neg_one in TauCeti/CategoryTheory/Monoidal/Pivotal/FrobeniusSchur/Simple.lean

LeanTauCeti.frobeniusSchurIndicator_two_eq_one_or_eq_zero_or_eq_neg_one

Uses 1

Proof usesNg–Schauenburg

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.