class CategoryTheory.HasChevalleyProperty (C : Type u) [Category.{v, u} C] [MonoidalCategory C] [Limits.HasZeroMorphisms C] : Prop

A monoidal category C has the Chevalley property if the tensor product of two semisimple objects is again semisimple (so the full subcategory of semisimple objects is a monoidal subcategory).

• tensor_semisimple (X Y : C) : IsSemisimpleObject C X → IsSemisimpleObject C Y → IsSemisimpleObject C (MonoidalCategoryStruct.tensorObj X Y)

def CategoryTheory.Definition_1_31_1_ChevalleyProperty (C : Type u) [Category.{v, u} C] [MonoidalCategory C] [Limits.HasZeroMorphisms C] : Prop

Definition 1.31.1 (named restatement): the Chevalley property for a tensor category.

def CategoryTheory.Definition_1_31_1 (C : Type u) [Category.{v, u} C] [MonoidalCategory C] [Limits.HasZeroMorphisms C] : Prop

Definition 1.31.1: the Chevalley property for a tensor category, expressed as a proposition.

class CategoryTheory.IsPointedTensorCategory (C : Type u) [Category.{v, u} C] [MonoidalCategory C] [Limits.HasZeroMorphisms C] : Prop

A monoidal category is pointed in this Atlas formulation if every simple object has a tensor inverse, i.e. is invertible.

• simple_has_inverse (X : C) [Simple X] : ∃ (Y : C), Nonempty (MonoidalCategoryStruct.tensorObj X Y ≅ MonoidalCategoryStruct.tensorUnit C) ∧ Nonempty (MonoidalCategoryStruct.tensorObj Y X ≅ MonoidalCategoryStruct.tensorUnit C)

theorem CategoryTheory.chevalleyProperty_of_pointed (C : Type u) [Category.{v, u} C] [MonoidalCategory C] [Limits.HasZeroMorphisms C] [IsPointedTensorCategory C] : HasChevalleyProperty C

Helper for Proposition 1.31.2: a pointed tensor category has the Chevalley property.

theorem CategoryTheory.simple_of_tensor_inverse (C : Type u) [Category.{v, u} C] [MonoidalCategory C] [Limits.HasZeroMorphisms C] (X : C) (h : ∃ (Y : C), Nonempty (MonoidalCategoryStruct.tensorObj X Y ≅ MonoidalCategoryStruct.tensorUnit C) ∧ Nonempty (MonoidalCategoryStruct.tensorObj Y X ≅ MonoidalCategoryStruct.tensorUnit C)) : Simple X

Any object X with a tensor inverse Y (so X ⊗ Y ≅ 𝟙_ C and Y ⊗ X ≅ 𝟙_ C) is simple.

theorem CategoryTheory.Proposition_1_31_2 (C : Type u) [Category.{v, u} C] [MonoidalCategory C] [Preadditive C] [MonoidalPreadditive C] [Limits.HasFiniteBiproducts C] [IsPointedTensorCategory C] : HasChevalleyProperty C

Proposition 1.31.2: A pointed tensor category has the Chevalley property.

structure CategoryTheory.SemisimpleFiltration (C : Type u) [Category.{v, u} C] [Limits.HasZeroMorphisms C] (X : C) (n : ℕ) : Type u

A length-n semisimple filtration of an object X: a tuple of n semisimple objects intended as the associated graded pieces of a filtration of X.

• gradedPiece : Fin n → C
• gradedPiece_semisimple (i : Fin n) : IsSemisimpleObject C (self.gradedPiece i)

structure CategoryTheory.LoewyLengthData (C : Type u) [Category.{v, u} C] [MonoidalCategory C] [Limits.HasZeroMorphisms C] : Type u

Abstract data witnessing the existence of a Loewy length function on C: every object admits some semisimple filtration of positive length, filtrations are functorial in tensor products with multiplicative compatible length, and biproducts of semisimple objects are semisimple.

• hasSemisimpleFiltration : C → ℕ → Prop
• hasSemisimpleFiltration_dec (X : C) : DecidablePred (self.hasSemisimpleFiltration X)
• hasSemisimpleFiltration_exists (X : C) : ∃ (n : ℕ), self.hasSemisimpleFiltration X n
• hasSemisimpleFiltration_pos (X : C) (n : ℕ) : self.hasSemisimpleFiltration X n → 1 ≤ n
• toFiltration (X : C) (n : ℕ) : self.hasSemisimpleFiltration X n → SemisimpleFiltration C X n
• filtration_tensor (X Y : C) (m n : ℕ) : m ≥ 1 → n ≥ 1 → ∀ (fX : SemisimpleFiltration C X m) (fY : SemisimpleFiltration C Y n), ∃ (candidateGradedPieces : Fin (m + n - 1) → C), (∀ (r : Fin (m + n - 1)), ∃ (k : ℕ) (pairs : Fin k → C) (hb : Limits.HasBiproduct pairs), (∀ (p : Fin k), ∃ (i : Fin m) (j : Fin n), pairs p = MonoidalCategoryStruct.tensorObj (fX.gradedPiece i) (fY.gradedPiece j)) ∧ Nonempty (candidateGradedPieces r ≅ ⨁ pairs)) ∧ ((∀ (r : Fin (m + n - 1)), IsSemisimpleObject C (candidateGradedPieces r)) → self.hasSemisimpleFiltration (MonoidalCategoryStruct.tensorObj X Y) (m + n - 1))
• semisimple_biproduct {k : ℕ} (f : Fin k → C) (hb : Limits.HasBiproduct f) : (∀ (i : Fin k), IsSemisimpleObject C (f i)) → IsSemisimpleObject C (⨁ f)

def CategoryTheory.LoewyLengthData.loewyLength {C : Type u} [Category.{v, u} C] [MonoidalCategory C] [Limits.HasZeroMorphisms C] (LD : LoewyLengthData C) (X : C) : ℕ

The Loewy length Lw(X) of an object X, defined as the smallest n for which a semisimple filtration of length n exists.

theorem CategoryTheory.LoewyLengthData.loewyLength_spec {C : Type u} [Category.{v, u} C] [MonoidalCategory C] [Limits.HasZeroMorphisms C] (LD : LoewyLengthData C) (X : C) : LD.hasSemisimpleFiltration X (LD.loewyLength X)

The Loewy length of X is attained: there is a semisimple filtration of length LD.loewyLength X.

theorem CategoryTheory.LoewyLengthData.loewyLength_le {C : Type u} [Category.{v, u} C] [MonoidalCategory C] [Limits.HasZeroMorphisms C] (LD : LoewyLengthData C) (X : C) (n : ℕ) (h : LD.hasSemisimpleFiltration X n) : LD.loewyLength X ≤ n

If X admits a semisimple filtration of length n, then loewyLength X ≤ n.

theorem CategoryTheory.LoewyLengthData.loewyLength_pos {C : Type u} [Category.{v, u} C] [MonoidalCategory C] [Limits.HasZeroMorphisms C] (LD : LoewyLengthData C) (X : C) : 1 ≤ LD.loewyLength X

The Loewy length is always at least 1.

theorem CategoryTheory.LoewyLengthData.loewyLength_tensor_le {C : Type u} [Category.{v, u} C] [MonoidalCategory C] [Limits.HasZeroMorphisms C] [hChev : HasChevalleyProperty C] (LD : LoewyLengthData C) (X Y : C) : LD.loewyLength (MonoidalCategoryStruct.tensorObj X Y) ≤ LD.loewyLength X + LD.loewyLength Y - 1

Proposition 1.31.3 (key inequality): under the Chevalley property, the Loewy length is subadditive on tensor products with a - 1 shift: Lw(X ⊗ Y) ≤ Lw(X) + Lw(Y) - 1.

theorem CategoryTheory.LoewyLengthData.loewyLength_tensor_le' {C : Type u} [Category.{v, u} C] [MonoidalCategory C] [Limits.HasZeroMorphisms C] [HasChevalleyProperty C] (LD : LoewyLengthData C) (X Y : C) : LD.loewyLength (MonoidalCategoryStruct.tensorObj X Y) + 1 ≤ LD.loewyLength X + LD.loewyLength Y

Reformulation of the Loewy length tensor inequality avoiding truncated subtraction: Lw(X ⊗ Y) + 1 ≤ Lw(X) + Lw(Y).

theorem CategoryTheory.Proposition_1_31_3 {C : Type u} [Category.{v, u} C] [MonoidalCategory C] [Limits.HasZeroMorphisms C] [HasChevalleyProperty C] (LD : LoewyLengthData C) (X Y : C) : LD.loewyLength (MonoidalCategoryStruct.tensorObj X Y) ≤ LD.loewyLength X + LD.loewyLength Y - 1

Proposition 1.31.3: In a tensor category with the Chevalley property, the Loewy length satisfies Lw(X ⊗ Y) ≤ Lw(X) + Lw(Y) - 1.

def CategoryTheory.loewyLengthDataOfSemisimple {C : Type u} [Category.{v, u} C] [MonoidalCategory C] [Limits.HasZeroMorphisms C] [IsSemisimpleCategory C] : LoewyLengthData C

In a semisimple category every object is already semisimple, so the Loewy length data is trivially given by length 1 filtrations.

structure CategoryTheory.IsHopfAlgebraFiltration (C : Type u) [Category.{v, u} C] [MonoidalCategory C] [Limits.HasZeroMorphisms C] [HasChevalleyProperty C] (LD : LoewyLengthData C) : Prop

Tensor-product compatibility for a coradical-style Loewy length: the filtration is a "Hopf algebra filtration" in the sense of Corollary 1.31.5 if loewyLength (X ⊗ Y) is controlled by the sum of the Loewy lengths of X and Y.

• filtration_tensor_compat (X Y : C) (i j : ℕ) : LD.loewyLength X ≤ i → LD.loewyLength Y ≤ j → LD.loewyLength (MonoidalCategoryStruct.tensorObj X Y) ≤ i + j

theorem CategoryTheory.pointed_coradicalFiltration_isHopfAlgebraFiltration {C : Type u} [Category.{v, u} C] [MonoidalCategory C] [Limits.HasZeroMorphisms C] [hChev : HasChevalleyProperty C] (LD : LoewyLengthData C) : IsHopfAlgebraFiltration C LD

Helper toward Corollary 1.31.5: in any tensor category with the Chevalley property, the Loewy length data automatically forms a Hopf algebra filtration on objects, since loewy length is multiplicatively well-behaved on tensor products.

structure CategoryTheory.IsFullHopfAlgebraFiltration (C : Type u) [Category.{v, u} C] [MonoidalCategory C] [Limits.HasZeroMorphisms C] [HasChevalleyProperty C] (LD : LoewyLengthData C) extends CategoryTheory.IsHopfAlgebraFiltration C LD : Prop

A Hopf algebra filtration is "full" if it is also preserved by taking right duals, matching S(H_i) = H_i in Corollary 1.31.5.

• filtration_tensor_compat (X Y : C) (i j : ℕ) : LD.loewyLength X ≤ i → LD.loewyLength Y ≤ j → LD.loewyLength (MonoidalCategoryStruct.tensorObj X Y) ≤ i + j
• dual_preserves_filtration (X : C) [HasRightDual X] (n : ℕ) : LD.loewyLength X ≤ n ↔ LD.loewyLength Xᘁ ≤ n

noncomputable def CategoryTheory.coradicalLoewyLengthData {C : Type u} [Category.{v, u} C] [MonoidalCategory C] [Limits.HasZeroMorphisms C] [IsPointedTensorCategory C] [HasChevalleyProperty C] : LoewyLengthData C

The Loewy length data for C coming from the coradical filtration in a pointed tensor category with the Chevalley property.

theorem CategoryTheory.coradicalLoewyLengthData_dual_preserves {C : Type u} [Category.{v, u} C] [MonoidalCategory C] [Limits.HasZeroMorphisms C] [IsPointedTensorCategory C] [HasChevalleyProperty C] (X : C) [HasRightDual X] (n : ℕ) : coradicalLoewyLengthData.loewyLength X ≤ n ↔ coradicalLoewyLengthData.loewyLength Xᘁ ≤ n

The coradical Loewy length data is invariant under taking right duals: an object X and Xᘁ have the same coradical Loewy length.