Documentation

Atlas.TensorCategories.code.UnitSemisimplicity.UnitSimple

theorem TensorCategories.simple_of_endoIsIso {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] [CategoryTheory.Abelian C] {X : C} (hne : ¬CategoryTheory.Limits.IsZero X) (hendo : ∀ (g : X X), g 0CategoryTheory.IsIso g) (hlift : ∀ {Y : C} (f : Y X) [CategoryTheory.Mono f], f 0∃ (k : X Y), k 0) :

A nonzero object whose nonzero endomorphisms are all isomorphisms and whose every nonzero monomorphism from another object admits a nonzero "lift" X ⟶ Y is simple.

theorem TensorCategories.pi_single_corner {n : } {M : Fin nType u_1} [(i : Fin n) → Ring (M i)] (i : Fin n) (x : (j : Fin n) → M j) :
Pi.single i 1 * x * Pi.single i 1 = Pi.single i (x i)

Sandwiching x : ∀ j, M j between two single-coordinate vectors Pi.single i 1 projects to the i-th coordinate Pi.single i (x i).

theorem TensorCategories.pi_single_mul_pi_single {n : } {M : Fin nType u_1} [(i : Fin n) → Ring (M i)] (i : Fin n) (a b : M i) :
Pi.single i a * Pi.single i b = Pi.single i (a * b)

The product of two single-coordinate vectors at the same index multiplies the factors and remains supported at that index.

theorem TensorCategories.commSemisimpleRing_primitiveIdempotents (R : Type u_1) [Ring R] [IsSemisimpleRing R] (hcomm : ∀ (a b : R), a * b = b * a) :
∃ (n : ) (e : Fin nR), CompleteOrthogonalIdempotents e (∀ (i : Fin n), e i 0) ∀ (i : Fin n) (h : R), h 0e i * h * e i = h∃ (sinv : R), h * sinv = e i sinv * h = e i

A semisimple ring whose multiplication is commutative admits a complete orthogonal family of primitive idempotents e i, and each corner ring e i · R · e i containing a nonzero element is a field (so the element has an inverse).

Helper: if ι, π split an idempotent e : X ⟶ X whose corner π · g · ι has a two-sided inverse sinv (in the corner sense), then g : fi ⟶ fi is an isomorphism.

If End(𝟙_ C) is semisimple, then there is a complete orthogonal family of primitive idempotents e i such that for any objects f i that split each e i, every nonzero endomorphism of f i is an isomorphism.

theorem TensorCategories.idempotent_summands_simple {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.MonoidalCategory C] [CategoryTheory.Preadditive C] [CategoryTheory.Abelian C] (_hss : IsSemisimpleRing (CategoryTheory.End (CategoryTheory.MonoidalCategoryStruct.tensorUnit C))) {n : } (e : Fin nCategoryTheory.End (CategoryTheory.MonoidalCategoryStruct.tensorUnit C)) (_hcoi : CompleteOrthogonalIdempotents e) (f : Fin nC) (ι_hom : (i : Fin n) → f i CategoryTheory.MonoidalCategoryStruct.tensorUnit C) (π_hom : (i : Fin n) → CategoryTheory.MonoidalCategoryStruct.tensorUnit C f i) (_hretract : ∀ (i : Fin n), CategoryTheory.CategoryStruct.comp (ι_hom i) (π_hom i) = CategoryTheory.CategoryStruct.id (f i)) (hsplit : ∀ (i : Fin n), CategoryTheory.CategoryStruct.comp (π_hom i) (ι_hom i) = e i) (hne : ∀ (i : Fin n), e i 0) (hendo : ∀ (i : Fin n) (g : f i f i), g 0CategoryTheory.IsIso g) (hlift : ∀ (i : Fin n) {Y : C} (m : Y f i) [CategoryTheory.Mono m], m 0∃ (k : f i Y), k 0) (i : Fin n) :

Each summand f i arising from splitting a primitive idempotent of End(𝟙) is a simple object, given the endomorphism-isomorphism and lifting hypotheses.

Any morphism between summands f i ⟶ f j corresponding to distinct primitive orthogonal idempotents of End(𝟙) is zero, using commutativity of End(𝟙).

theorem TensorCategories.idempotent_summands_simple_and_noniso {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.MonoidalCategory C] [CategoryTheory.Preadditive C] [CategoryTheory.Abelian C] (hss : IsSemisimpleRing (CategoryTheory.End (CategoryTheory.MonoidalCategoryStruct.tensorUnit C))) {n : } (e : Fin nCategoryTheory.End (CategoryTheory.MonoidalCategoryStruct.tensorUnit C)) (hcoi : CompleteOrthogonalIdempotents e) (f : Fin nC) (ι_hom : (i : Fin n) → f i CategoryTheory.MonoidalCategoryStruct.tensorUnit C) (π_hom : (i : Fin n) → CategoryTheory.MonoidalCategoryStruct.tensorUnit C f i) (hretract : ∀ (i : Fin n), CategoryTheory.CategoryStruct.comp (ι_hom i) (π_hom i) = CategoryTheory.CategoryStruct.id (f i)) (hsplit : ∀ (i : Fin n), CategoryTheory.CategoryStruct.comp (π_hom i) (ι_hom i) = e i) (hne : ∀ (i : Fin n), e i 0) (hendo : ∀ (i : Fin n) (g : f i f i), g 0CategoryTheory.IsIso g) (hlift : ∀ (i : Fin n) {Y : C} (m : Y f i) [CategoryTheory.Mono m], m 0∃ (k : f i Y), k 0) :
(∀ (i : Fin n), CategoryTheory.Simple (f i)) ∀ (i j : Fin n), i j¬Nonempty (f i f j)

Strengthening of idempotent_summands_simple: the summands f i are not only simple but also pairwise non-isomorphic.

A complete orthogonal family of idempotents in End(𝟙_ C) gives rise to a biproduct decomposition 𝟙_ C ≅ ⨁ f i whose summands split each idempotent.

Instances For

    Under semisimplicity of End(𝟙_ C) and a lifting axiom, the unit object decomposes as a biproduct of pairwise non-isomorphic simple objects. This is the categorical form of Corollary 1.15.2 and Theorem 1.15.8 (ii).

    A nonzero object in a preadditive category with binary biproducts is indecomposable whenever every nonzero endomorphism is an isomorphism.

    Corollary 1.15.2: the unit object decomposes as a biproduct of pairwise non-isomorphic indecomposable objects, assuming End(𝟙_ C) is semisimple.

    Predicate asserting that the unit object 𝟙_ C decomposes as a finite biproduct of pairwise non-isomorphic simple objects — the content of Theorem 1.15.8 (ii).

    Instances For

      If X is a retract of the unit object via (ι, π), then every nonzero monomorphism m : Y ⟶ X admits a nonzero "lift" X ⟶ Y. This supplies the hlift hypothesis needed to establish simplicity for unit summands.

      Theorem 1.15.8 (ii): in an abelian rigid monoidally biexact category with Artinian unit object and Artinian endomorphism ring of 𝟙, the unit decomposes as a finite biproduct of pairwise non-isomorphic simple objects.