The scalars of a simple algebra

For a commutative algebra object R whose only ideals are ⊥ and ⊤, multiplication by a nonzero even scalar is an isomorphism, so the even part of the Γ-algebra of R is a field; and the odd part of that Γ-algebra vanishes.

The mechanism is RS.mulBy: multiplication by an even scalar is a module endomorphism of R (RS.mul_comp_mulBy), so its kernel and its image are ideals (RS.isIdeal_kernelSubobject_mulBy, RS.isIdeal_imageSubobject_mulBy). Simplicity forces the kernel to be ⊥ and the image to be ⊤, whence the endomorphism is an isomorphism (RS.isIso_mulBy_of_simple) and the preimage of the unit inverts the scalar (RS.exists_inverse_of_simple).

The odd part goes the same way. An odd element f acts on R by RS.gmul f (𝟙 R), whose image is an ideal for the same reason; an odd element squares to zero, so that action kills its own image, and under either alternative of simplicity the action vanishes (RS.hom_oddLine_eq_zero_of_simple).

Convolution against the identity

theorem RS.whiskerLeft_comp_mul {D : Type u} [CategoryTheory.Category.{v, u} D] [CategoryTheory.MonoidalCategory D] (R : D) [CategoryTheory.MonObj R] {X : D} (k : X ⟶ R) : CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.whiskerLeft R k) CategoryTheory.MonObj.mul = gmul (CategoryTheory.CategoryStruct.id R) k

Whiskering a morphism into the algebra and multiplying is the convolution with the identity.

theorem RS.gmul_id_id {D : Type u} [CategoryTheory.Category.{v, u} D] [CategoryTheory.MonoidalCategory D] (R : D) [CategoryTheory.MonObj R] : gmul (CategoryTheory.CategoryStruct.id R) (CategoryTheory.CategoryStruct.id R) = CategoryTheory.MonObj.mul

The convolution of the identity with itself is the multiplication.

theorem RS.zero_gmul {D : Type u} [CategoryTheory.Category.{v, u} D] [CategoryTheory.MonoidalCategory D] [CategoryTheory.Preadditive D] [CategoryTheory.MonoidalPreadditive D] (R : D) [CategoryTheory.MonObj R] {X Y : D} (b : Y ⟶ R) : gmul 0 b = 0

Convolution with a zero morphism vanishes.

Multiplication by a scalar is a module endomorphism

theorem RS.leftUnitor_inv_gmul_comm {D : Type u} [CategoryTheory.Category.{v, u} D] [CategoryTheory.MonoidalCategory D] [CategoryTheory.BraidedCategory D] (R : D) [CategoryTheory.MonObj R] [CategoryTheory.IsCommMonObj R] {X : D} (a : X ⟶ R) (g : CategoryTheory.MonoidalCategoryStruct.tensorUnit D ⟶ R) : CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.leftUnitor X).inv (gmul g a) = CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.rightUnitor X).inv (gmul a g)

Convolution with an even scalar reads the same on either side, once the source is identified with its tensor with the unit.

theorem RS.mulBy_eq_gmul_id {D : Type u} [CategoryTheory.Category.{v, u} D] [CategoryTheory.MonoidalCategory D] [CategoryTheory.BraidedCategory D] (R : D) [CategoryTheory.MonObj R] [CategoryTheory.IsCommMonObj R] (g : CategoryTheory.MonoidalCategoryStruct.tensorUnit D ⟶ R) : mulBy R g = CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.rightUnitor R).inv (gmul (CategoryTheory.CategoryStruct.id R) g)

Multiplication by an even scalar, written on the other side.

theorem RS.mul_comp_mulBy {D : Type u} [CategoryTheory.Category.{v, u} D] [CategoryTheory.MonoidalCategory D] [CategoryTheory.BraidedCategory D] (R : D) [CategoryTheory.MonObj R] [CategoryTheory.IsCommMonObj R] (g : CategoryTheory.MonoidalCategoryStruct.tensorUnit D ⟶ R) : CategoryTheory.CategoryStruct.comp CategoryTheory.MonObj.mul (mulBy R g) = CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.whiskerLeft R (mulBy R g)) CategoryTheory.MonObj.mul

Multiplication by an even scalar is a module endomorphism: it commutes with the multiplication of the algebra in the second variable. Both sides say g·(a·b) = a·(g·b).

theorem RS.act_comp_gmul_id {D : Type u} [CategoryTheory.Category.{v, u} D] [CategoryTheory.MonoidalCategory D] [CategoryTheory.BraidedCategory D] (R : D) [CategoryTheory.MonObj R] [CategoryTheory.IsCommMonObj R] {X : D} (f : X ⟶ R) : CategoryTheory.CategoryStruct.comp (CategoryTheory.CategoryStruct.comp (β_ R (CategoryTheory.MonoidalCategoryStruct.tensorObj X R)).hom (CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.associator X R R).hom (CategoryTheory.MonoidalCategoryStruct.whiskerLeft X CategoryTheory.MonObj.mul))) (gmul f (CategoryTheory.CategoryStruct.id R)) = CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.whiskerLeft R (gmul f (CategoryTheory.CategoryStruct.id R))) CategoryTheory.MonObj.mul

The action of a fixed element is a module map. For any f : X ⟶ R the convolution gmul f (𝟙 R) absorbs multiplication by the algebra: a·(f·b) = f·(a·b).

Images as subobjects

noncomputable def RS.imageFactor {C : Type v} [CategoryTheory.SmallCategory C] [CategoryTheory.Abelian C] {X Y : CategoryTheory.Ind C} (k : X ⟶ Y) : X ⟶ CategoryTheory.Subobject.underlying.obj (CategoryTheory.Subobject.mk (CategoryTheory.Limits.image.ι k))

The factorisation of a morphism through its image, read as a morphism into the image subobject.

Equations

• RS.imageFactor k = CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.factorThruImage k) (CategoryTheory.Subobject.underlyingIso (CategoryTheory.Limits.image.ι k)).inv

theorem RS.imageFactor_arrow {C : Type v} [CategoryTheory.SmallCategory C] [CategoryTheory.Abelian C] {X Y : CategoryTheory.Ind C} (k : X ⟶ Y) : CategoryTheory.CategoryStruct.comp (imageFactor k) (CategoryTheory.Subobject.mk (CategoryTheory.Limits.image.ι k)).arrow = k

The factorisation through the image subobject recovers the morphism.

instance RS.epi_imageFactor {C : Type v} [CategoryTheory.SmallCategory C] [CategoryTheory.Abelian C] {X Y : CategoryTheory.Ind C} (k : X ⟶ Y) : CategoryTheory.Epi (imageFactor k)

The factorisation through the image subobject is an epimorphism.

Kernel and image are ideals

theorem RS.isIdeal_kernelSubobject_mulBy {C : Type v} [CategoryTheory.SmallCategory C] [CategoryTheory.MonoidalCategory C] [CategoryTheory.SymmetricCategory C] [CategoryTheory.Abelian C] [CategoryTheory.MonoidalPreadditive C] (R : CategoryTheory.Ind C) [CategoryTheory.MonObj R] [CategoryTheory.IsCommMonObj R] (g : CategoryTheory.MonoidalCategoryStruct.tensorUnit (CategoryTheory.Ind C) ⟶ R) : IsIdeal R (CategoryTheory.Limits.kernelSubobject (mulBy R g))

The kernel of multiplication by a scalar is an ideal: multiplication by a scalar is a module endomorphism, so anything it kills stays killed after multiplying by the algebra.

theorem RS.isIdeal_imageSubobject_of {C : Type v} [CategoryTheory.SmallCategory C] [CategoryTheory.MonoidalCategory C] [CategoryTheory.Abelian C] [CategoryTheory.RigidCategory C] [CategoryTheory.MonoidalPreadditive C] (R : CategoryTheory.Ind C) [CategoryTheory.MonObj R] {X : CategoryTheory.Ind C} (k : X ⟶ R) (θ : CategoryTheory.MonoidalCategoryStruct.tensorObj R X ⟶ X) (hθ : CategoryTheory.CategoryStruct.comp θ k = CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.whiskerLeft R k) CategoryTheory.MonObj.mul) : IsIdeal R (CategoryTheory.Subobject.mk (CategoryTheory.Limits.image.ι k))

The image of a module map is an ideal. If a morphism into the algebra absorbs multiplication by the algebra, its image does too: tensoring preserves the covering epimorphism onto the image.

theorem RS.isIdeal_imageSubobject_mulBy {C : Type v} [CategoryTheory.SmallCategory C] [CategoryTheory.MonoidalCategory C] [CategoryTheory.SymmetricCategory C] [CategoryTheory.Abelian C] [CategoryTheory.RigidCategory C] [CategoryTheory.MonoidalPreadditive C] (R : CategoryTheory.Ind C) [CategoryTheory.MonObj R] [CategoryTheory.IsCommMonObj R] (g : CategoryTheory.MonoidalCategoryStruct.tensorUnit (CategoryTheory.Ind C) ⟶ R) : IsIdeal R (CategoryTheory.Subobject.mk (CategoryTheory.Limits.image.ι (mulBy R g)))

The image of multiplication by a scalar is an ideal.

Simplicity makes multiplication invertible

theorem RS.eq_zero_of_imageSubobject_eq_bot {C : Type v} [CategoryTheory.SmallCategory C] [CategoryTheory.Abelian C] {X Y : CategoryTheory.Ind C} {k : X ⟶ Y} (h : CategoryTheory.Subobject.mk (CategoryTheory.Limits.image.ι k) = ⊥) : k = 0

A subobject equal to ⊥ has a zero arrow, so a morphism whose image it is vanishes.

theorem RS.epi_of_imageSubobject_eq_top {C : Type v} [CategoryTheory.SmallCategory C] [CategoryTheory.Abelian C] {X Y : CategoryTheory.Ind C} {k : X ⟶ Y} (h : CategoryTheory.Subobject.mk (CategoryTheory.Limits.image.ι k) = ⊤) : CategoryTheory.Epi k

A morphism whose image subobject is ⊤ is an epimorphism.

theorem RS.isIso_mulBy_of_simple {C : Type v} [CategoryTheory.SmallCategory C] [CategoryTheory.MonoidalCategory C] [CategoryTheory.SymmetricCategory C] [CategoryTheory.Abelian C] [CategoryTheory.RigidCategory C] [CategoryTheory.MonoidalPreadditive C] (R : CategoryTheory.Ind C) [CategoryTheory.MonObj R] [CategoryTheory.IsCommMonObj R] (hsimple : ∀ (I : CategoryTheory.Subobject R), IsIdeal R I → I = ⊥ ∨ I = ⊤) {g : CategoryTheory.MonoidalCategoryStruct.tensorUnit (CategoryTheory.Ind C) ⟶ R} (hg : g ≠ 0) : CategoryTheory.IsIso (mulBy R g)

Simplicity makes multiplication by a nonzero scalar invertible. The kernel is an ideal different from ⊤, because a scalar whose multiplication vanishes is itself zero; the image is an ideal different from ⊥, for the same reason. So the kernel is ⊥ and the image is ⊤, and a monomorphism which is an epimorphism of an abelian category is an isomorphism. No hypothesis on the unit is needed: a nonzero scalar already rules out both bad alternatives.

The even part is a field

theorem RS.exists_inverse_of_simple {C : Type v} [CategoryTheory.SmallCategory C] [CategoryTheory.MonoidalCategory C] [CategoryTheory.SymmetricCategory C] [CategoryTheory.Abelian C] [CategoryTheory.RigidCategory C] [CategoryTheory.MonoidalPreadditive C] (R : CategoryTheory.Ind C) [CategoryTheory.MonObj R] [CategoryTheory.IsCommMonObj R] (hsimple : ∀ (I : CategoryTheory.Subobject R), IsIdeal R I → I = ⊥ ∨ I = ⊤) {g : CategoryTheory.MonoidalCategoryStruct.tensorUnit (CategoryTheory.Ind C) ⟶ R} (hg : g ≠ 0) : ∃ (g' : CategoryTheory.MonoidalCategoryStruct.tensorUnit (CategoryTheory.Ind C) ⟶ R), CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.leftUnitor (CategoryTheory.MonoidalCategoryStruct.tensorUnit (CategoryTheory.Ind C))).inv (gmul g g') = CategoryTheory.MonObj.one

Every nonzero even scalar of a simple algebra is invertible: the preimage of the unit under multiplication by the scalar is its inverse.

theorem RS.isField_gammaEven {C : Type v} [CategoryTheory.SmallCategory C] [CategoryTheory.MonoidalCategory C] [CategoryTheory.SymmetricCategory C] [CategoryTheory.Abelian C] [CategoryTheory.RigidCategory C] [CategoryTheory.MonoidalPreadditive C] (R : CategoryTheory.Ind C) [CategoryTheory.MonObj R] [CategoryTheory.IsCommMonObj R] [CategoryTheory.Linear ℂ (CategoryTheory.Ind C)] [CategoryTheory.MonoidalLinear ℂ (CategoryTheory.Ind C)] (L : OddLine (CategoryTheory.Ind C)) (hsimple : ∀ (I : CategoryTheory.Subobject R), IsIdeal R I → I = ⊥ ∨ I = ⊤) (hne : CategoryTheory.MonObj.one ≠ 0) : IsField (gammaAlgebra (CategoryTheory.Ind C) L R).even

The even part of the Γ-algebra of a simple algebra is a field.

@[reducible]

noncomputable def RS.gammaEvenField {C : Type v} [CategoryTheory.SmallCategory C] [CategoryTheory.MonoidalCategory C] [CategoryTheory.SymmetricCategory C] [CategoryTheory.Abelian C] [CategoryTheory.RigidCategory C] [CategoryTheory.MonoidalPreadditive C] (R : CategoryTheory.Ind C) [CategoryTheory.MonObj R] [CategoryTheory.IsCommMonObj R] [CategoryTheory.Linear ℂ (CategoryTheory.Ind C)] [CategoryTheory.MonoidalLinear ℂ (CategoryTheory.Ind C)] (L : OddLine (CategoryTheory.Ind C)) (hsimple : ∀ (I : CategoryTheory.Subobject R), IsIdeal R I → I = ⊥ ∨ I = ⊤) (hne : CategoryTheory.MonObj.one ≠ 0) : Field (gammaAlgebra (CategoryTheory.Ind C) L R).even

The even part of the Γ-algebra of a simple algebra, as a field.

Equations

• RS.gammaEvenField R L hsimple hne = ⋯.toField

The odd part vanishes

theorem RS.hom_oddLine_eq_zero_of_simple {C : Type v} [CategoryTheory.SmallCategory C] [CategoryTheory.MonoidalCategory C] [CategoryTheory.SymmetricCategory C] [CategoryTheory.Abelian C] [CategoryTheory.RigidCategory C] [CategoryTheory.MonoidalPreadditive C] (R : CategoryTheory.Ind C) [CategoryTheory.MonObj R] [CategoryTheory.IsCommMonObj R] [CategoryTheory.Linear ℂ (CategoryTheory.Ind C)] (L : OddLine (CategoryTheory.Ind C)) (hsimple : ∀ (I : CategoryTheory.Subobject R), IsIdeal R I → I = ⊥ ∨ I = ⊤) (f : L.obj ⟶ R) : f = 0

The odd part of the Γ-algebra of a simple algebra vanishes. An odd element f acts on the algebra by gmul f (𝟙 R), whose image is an ideal, so simplicity leaves two alternatives and the action vanishes under both: if the image is ⊥ the action is zero outright, and if the image is ⊤ the action is an epimorphism, which the square-zero law of an odd element makes annihilate itself. Evaluating the zero action at the unit returns f.