Deligne's theorem assembled

RS.deligne_theorem proves RS.DeligneTheoremStatement (Catégories tensorielles, Théorème 0.6). It is RS.deligne_theorem_of_braided, which assembles the statement from RS.BraidedFibreHypothesis — that the fibre functor RS.deligneFibre of a splitting algebra at a complex point is symmetric monoidal — applied to RS.braidedFibreHypothesis, which discharges it from RS.nonempty_braided_deligneFibre.

The route is not Deligne's. His §4 obtains the passage from an arbitrary nonzero algebra of scalars to ℂ by descent along a faithfully flat Isom⊗ torsor. Here the tensor generator alone is split and one passes to a quotient by a maximal ideal: over a simple algebra the regular module and its twist by the odd line are simple objects of the module category, so a free mixed module is semisimple of finite length, the objects the algebra splits are closed under subquotients, and the scalars are a field of countable dimension over ℂ, hence ℂ. This is the pattern of Coulembier, Tannakian categories in positive characteristic, Duke Math. J. 169 (2020), Lemma 3.3.2(ii), with Lemmas 1.2.10 and 1.5.2.

• RS.deligneTheoremStatement_of_small (SmallReduction.lean) reduces the statement, which quantifies over essentially small categories, to the case of a genuinely small one.
• A tensor category need not contain an odd line, so the small category is replaced by its ℤ/2-graded doubling, whose ind-completion carries the odd line RS.doubledIndOddLine (Prop21General.lean).
• RS.exists_splitting_simple_algebra_doubled (DoubledSplit.lean) produces the simple commutative algebra of the ind-completion of the doubling that splits every embedded object into a mixed sum of copies of the unit and of the odd line, together with a complex point of its Γ-algebra.
• Simplicity supplies the sections that exactness of the fibre functor consumes. An embedded short exact sequence has an epimorphic right-hand map, so the free-module functor sends it to an epimorphism (RS.epi_freeModMap), and over a simple algebra every epimorphism out of a free mixed module splits (RS.exists_section_of_simple, SimpleSplit.lean).
• RS.deligneFibreFunctorOfPoint collects RS.deligneFibre and its properties into a RS.DeligneFibreFunctor; the ℂ-linear clause is RS.superVectFunctor_linear fed by RS.fibreFun_linear and RS.indOfFunctorLinear.
• RS.DeligneFibreFunctor.precompose restricts the fibre functor of the doubling along the even embedding, which is strong braided monoidal, exact, faithful and ℂ-linear.

One compatibility is needed for the last step. The even embedding is ℂ-linear for the structure the doubling inherits componentwise from its base, whereas the fibre construction runs at the structure induced by the scalar unit, RS.linearOfScalarUnit. The two agree: RS.scalarSmul_scalarUnitEquiv identifies the scalar action of a scalar unit with the ambient action in a monoidally ℂ-linear category, and RS.evenEmbedLinear_scalarUnit reads that off for the even embedding.

The scalar action of a scalar unit is the ambient action

theorem RS.scalarEnd_scalarUnitEquiv {D : Type u} [CategoryTheory.Category.{v, u} D] [CategoryTheory.MonoidalCategory D] [CategoryTheory.Preadditive D] [CategoryTheory.Linear ℂ D] [CategoryTheory.MonoidalPreadditive D] [CategoryTheory.MonoidalLinear ℂ D] (h : HasScalarUnit D) (c : ℂ) (X : D) : scalarEnd (scalarUnitEquiv h) c X = c • CategoryTheory.CategoryStruct.id X

The endomorphism attached to a scalar is the rescaled identity, when the scalar unit is the ambient action of ℂ on the endomorphisms of the tensor unit: whiskering c • 𝟙 onto X gives c • 𝟙 again because the tensor product is ℂ-bilinear, and the two unitors then cancel.

theorem RS.scalarSmul_scalarUnitEquiv {D : Type u} [CategoryTheory.Category.{v, u} D] [CategoryTheory.MonoidalCategory D] [CategoryTheory.Preadditive D] [CategoryTheory.Linear ℂ D] [CategoryTheory.MonoidalPreadditive D] [CategoryTheory.MonoidalLinear ℂ D] (h : HasScalarUnit D) {X Y : D} (c : ℂ) (f : X ⟶ Y) : scalarSmul (scalarUnitEquiv h) c f = c • f

The ℂ-linear structure induced by the ambient scalar unit is the ambient one. In a monoidally ℂ-linear category the action of RS.linearOfScalarUnit (scalarUnitEquiv h) on a hom-set is the given action, so the two structures may be used interchangeably.

The even embedding at the scalar-unit structure

theorem RS.scalarSmul_doubledScalarUnit {B : Type v} [CategoryTheory.SmallCategory B] [CategoryTheory.Abelian B] [CategoryTheory.Linear ℂ B] [CategoryTheory.MonoidalCategory B] [CategoryTheory.MonoidalPreadditive B] [CategoryTheory.MonoidalLinear ℂ B] (hu : HasScalarUnit B) {V W : Doubled B} (c : ℂ) (f : V ⟶ W) : scalarSmul (doubledScalarUnit hu) c f = c • f

The scalar action of RS.doubledScalarUnit on the doubling is the action the doubling inherits componentwise from its base.

theorem RS.evenEmbed_map_smul_doubled {B : Type v} [CategoryTheory.SmallCategory B] [CategoryTheory.Abelian B] [CategoryTheory.Linear ℂ B] [CategoryTheory.MonoidalCategory B] [CategoryTheory.MonoidalPreadditive B] [CategoryTheory.MonoidalLinear ℂ B] (hu : HasScalarUnit B) (c : ℂ) {V W : B} (f : V ⟶ W) : Doubled.evenEmbed.map (c • f) = scalarSmul (doubledScalarUnit hu) c (Doubled.evenEmbed.map f)

The even embedding carries a rescaled morphism to the scalar-unit rescaling of its image.

theorem RS.evenEmbedLinear_scalarUnit {B : Type v} [CategoryTheory.SmallCategory B] [CategoryTheory.Abelian B] [CategoryTheory.Linear ℂ B] [CategoryTheory.MonoidalCategory B] [CategoryTheory.MonoidalPreadditive B] [CategoryTheory.MonoidalLinear ℂ B] (hu : HasScalarUnit B) : CategoryTheory.Functor.Linear ℂ Doubled.evenEmbed

The even embedding is ℂ-linear for the scalar-unit structure of the doubling, the structure at which the fibre construction runs.

The symmetry of the fibre functor

def RS.BraidedFibreHypothesis : Prop

The fibre functor of a splitting algebra at a complex point is symmetric monoidal. The assembly below takes this clause of Deligne's conclusion as a hypothesis, which RS.braidedFibreHypothesis discharges from RS.nonempty_braided_deligneFibre; the strong monoidal structure of the composite is RS.fibreRestrictMonoidal, and the Koszul sign of RS.SuperVect is the braiding it transports.

Equations

• One or more equations did not get rendered due to their size.

The fibre functor of a splitting algebra, packaged

noncomputable def RS.deligneFibreFunctorOfPoint {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)] [∀ (Z : CategoryTheory.Ind C), (CategoryTheory.MonoidalCategory.tensorRight Z).PreservesMonomorphisms] [indOf.Additive] [CategoryTheory.Functor.Linear ℂ indOf] (L : OddLine (CategoryTheory.Ind C)) (𝔸 : CategoryTheory.Ind C) [CategoryTheory.MonObj 𝔸] [CategoryTheory.IsCommMonObj 𝔸] (hmono : CategoryTheory.Mono CategoryTheory.MonObj.one) (hsp : SplitsOn L 𝔸 indOf) (hsec : ∀ (T : CategoryTheory.ShortComplex C), T.ShortExact → ∃ (s : freeMod 𝔸 (T.map indOf).X₃ ⟶ freeMod 𝔸 (T.map indOf).X₂), CategoryTheory.CategoryStruct.comp s (freeModMap 𝔸 (T.map indOf).g) = CategoryTheory.CategoryStruct.id (freeMod 𝔸 (T.map indOf).X₃)) (pt : SuperPoint (gammaAlgebra (CategoryTheory.Ind C) L 𝔸)) (hbraid : (deligneFibre L 𝔸 hsp pt).Braided) : DeligneFibreFunctor C

The conclusion of Deligne's theorem for a category split by an algebra with a complex point. Every clause of RS.DeligneFibreFunctor is available for RS.deligneFibre: it is additive and ℂ-linear because the embedding, the fibre functor over the algebra and base change all are; it is exact because the sections make each embedded short exact sequence split after base change; and it is faithful because the unit of the algebra is a monomorphism. Symmetry is the hypothesis hbraid.

Equations

• One or more equations did not get rendered due to their size.

Deligne's theorem

theorem RS.exists_deligneFibreFunctor_small {B : Type v} [CategoryTheory.SmallCategory B] [CategoryTheory.Abelian B] [CategoryTheory.Linear ℂ B] [CategoryTheory.MonoidalCategory B] [CategoryTheory.SymmetricCategory B] [CategoryTheory.MonoidalPreadditive B] [CategoryTheory.MonoidalLinear ℂ B] [CategoryTheory.Limits.HasFiniteBiproducts B] [CategoryTheory.RigidCategory B] (P : SchurPackage) (P₀ : SchurPackage) (hbr : BraidedFibreHypothesis) (hu : HasScalarUnit B) (X : B) (hgen : TensorGeneratedBy B X) (hgrow : ModerateLengthGrowth B) : Nonempty (DeligneFibreFunctor B)

Deligne's theorem for a small category. The doubling of B carries every hypothesis, and its ind-completion carries an odd line, so the simple algebra 𝔹 that splits the embedding is available together with a complex point of its Γ-algebra. Simplicity of 𝔹 supplies the sections, the nonvanishing of its unit makes that unit a monomorphism, and the resulting fibre functor of Doubled B restricts along the even embedding to one of B.

theorem RS.deligne_theorem_of_braided (P : SchurPackage) (P₀ : SchurPackage) (hbr : BraidedFibreHypothesis) : DeligneTheoremStatement

Deligne's theorem (Catégories tensorielles, Théorème 0.6), conditional on the symmetry of the fibre functor: every essentially small abelian ℂ-linear rigid symmetric monoidal category with ℂ-bilinear tensor product, scalar unit endomorphisms, a finite tensor generator and moderate growth of the lengths of its tensor powers admits an exact faithful ℂ-linear symmetric monoidal fibre functor to finite-dimensional super vector spaces.

theorem RS.braidedFibreHypothesis : BraidedFibreHypothesis

The braided hypothesis is discharged: the fibre functor of a splitting algebra at a complex point is symmetric monoidal, because the fibre functor over the algebra is and the base change at the point is.

theorem RS.deligne_theorem : DeligneTheoremStatement

Deligne's theorem (Catégories tensorielles, Théorème 0.6): every essentially small abelian ℂ-linear rigid symmetric monoidal category with ℂ-bilinear tensor product, scalar unit endomorphisms, a finite tensor generator and moderate growth of the lengths of its tensor powers admits an exact faithful ℂ-linear symmetric monoidal fibre functor to finite-dimensional super vector spaces.