The complex point of a simple algebra

The even part of the Γ-algebra of a simple countably presented algebra is the complex numbers and its odd part vanishes, so the Γ-algebra has a complex point on the nose: the inverse of the structure map, with nothing to check on the odd side.

This is the last input of the fibre functor: with a point in hand the base change of RS/Classical/Deligne/PointFibre.lean lands in finite-dimensional super vector spaces.

theorem RS.bijective_algebraMap_gammaEven {C : Type v} [CategoryTheory.SmallCategory C] [CategoryTheory.MonoidalCategory C] [CategoryTheory.SymmetricCategory C] [CategoryTheory.Abelian C] [CategoryTheory.RigidCategory C] [CategoryTheory.MonoidalPreadditive C] [CategoryTheory.Linear ℂ C] [CategoryTheory.Linear ℂ (CategoryTheory.Ind C)] [CategoryTheory.MonoidalLinear ℂ (CategoryTheory.Ind C)] (hu : HasScalarUnit C) (hsmul : IndOfLinear C) (hlen : ∀ (Z : C), ∃ (N : ℕ), LengthLE Z N) (L : OddLine (CategoryTheory.Ind C)) {𝔸 𝔹 : CategoryTheory.Ind C} [CategoryTheory.MonObj 𝔹] [CategoryTheory.IsCommMonObj 𝔹] (π : 𝔸 ⟶ 𝔹) [CategoryTheory.Epi π] (hcp : CountablyPresented 𝔸) (hne : CategoryTheory.MonObj.one ≠ 0) (hsimple : ∀ (I : CategoryTheory.Subobject 𝔹), IsIdeal 𝔹 I → I = ⊥ ∨ I = ⊤) : Function.Bijective ⇑(algebraMap ℂ (gammaAlgebra (CategoryTheory.Ind C) L 𝔹).even)

The structure map of the scalars is bijective for a simple countably presented algebra: injective because the scalars form a field, surjective because every scalar is a complex multiple of the unit.

noncomputable def RS.superPointOfSimple {C : Type v} [CategoryTheory.SmallCategory C] [CategoryTheory.MonoidalCategory C] [CategoryTheory.SymmetricCategory C] [CategoryTheory.Abelian C] [CategoryTheory.RigidCategory C] [CategoryTheory.MonoidalPreadditive C] [CategoryTheory.Linear ℂ C] [CategoryTheory.Linear ℂ (CategoryTheory.Ind C)] [CategoryTheory.MonoidalLinear ℂ (CategoryTheory.Ind C)] (hu : HasScalarUnit C) (hsmul : IndOfLinear C) (hlen : ∀ (Z : C), ∃ (N : ℕ), LengthLE Z N) (L : OddLine (CategoryTheory.Ind C)) {𝔸 𝔹 : CategoryTheory.Ind C} [CategoryTheory.MonObj 𝔹] [CategoryTheory.IsCommMonObj 𝔹] (π : 𝔸 ⟶ 𝔹) [CategoryTheory.Epi π] (hcp : CountablyPresented 𝔸) (hne : CategoryTheory.MonObj.one ≠ 0) (hsimple : ∀ (I : CategoryTheory.Subobject 𝔹), IsIdeal 𝔹 I → I = ⊥ ∨ I = ⊤) : SuperPoint (gammaAlgebra (CategoryTheory.Ind C) L 𝔹)

A simple countably presented algebra has a complex point. The even part is the complex numbers and the odd part vanishes, so the point is the inverse of the structure map and the vanishing condition is vacuous.

Equations

• RS.superPointOfSimple hu hsmul hlen L π hcp hne hsimple = { chi := ↑(AlgEquiv.ofBijective (Algebra.ofId ℂ (RS.gammaAlgebra (CategoryTheory.Ind C) L 𝔹).even) ⋯).symm, vanishing := ⋯ }