Documentation

LeanPool.RegtsSevenster.RS.Classical.Deligne.Prop21General

Deligne's Proposition 2.1 without an odd line #

RS.exists_fibre_functor produces the fibre algebra and its fibre functor for a category whose ind-completion already carries an odd line. A tensor category need not contain such an object; Deligne's device is to pass to the ℤ/2-graded doubling, which always does, and to restrict along the even embedding.

This module runs that device. The doubling of a small abelian rigid symmetric monoidal ℂ-linear category with scalar unit endomorphisms and moderate length growth inherits every one of those hypotheses, and its ind-completion carries the image of the odd line RS.doubledOddLine under the embedding. Proposition 2.1 upstairs therefore applies, and the resulting fibre functor restricts along the even embedding A ⥤ Doubled A, which is strong braided monoidal, exact and faithful; each of the four conclusions composes.

The hypothesis of 2.1 — that every object is killed by some Schur functor — is supplied by the growth dichotomy RS.forall_exists_schurKilled, applied to the doubling.

source
noncomputable def RS.doubledScalarUnit {A : Type v} [CategoryTheory.SmallCategory A] [CategoryTheory.MonoidalCategory A] [CategoryTheory.Abelian A] [CategoryTheory.MonoidalPreadditive A] [CategoryTheory.Linear ℂ A] (hu : HasScalarUnit A) :
ℂ ≃+* CategoryTheory.End (CategoryTheory.MonoidalCategoryStruct.tensorUnit (Doubled A))

The scalar unit of the doubling, as the ring isomorphism that Proposition 2.1 consumes: the unit of the doubling is the unit of A in even degree, so its endomorphisms are the scalars.

Equations
Instances For
    source
    noncomputable def RS.doubledIndOddLine {A : Type v} [CategoryTheory.SmallCategory A] [CategoryTheory.MonoidalCategory A] [CategoryTheory.SymmetricCategory A] [CategoryTheory.Abelian A] [CategoryTheory.MonoidalPreadditive A] :
    OddLine (CategoryTheory.Ind (Doubled A))

    The odd line of the ind-completion of the doubling: the image of the odd line of the doubling under the embedding, which is strong braided monoidal and additive.

    Equations
    Instances For
      source
      theorem RS.exists_fibre_functor_general {A : Type v} [CategoryTheory.SmallCategory A] [CategoryTheory.MonoidalCategory A] [CategoryTheory.SymmetricCategory A] [CategoryTheory.Abelian A] [CategoryTheory.RigidCategory A] [CategoryTheory.MonoidalPreadditive A] [CategoryTheory.Linear ℂ A] (P : SchurPackage) (P₀ : SchurPackage) (hu : HasScalarUnit A) (hgrow : ModerateLengthGrowth A) :
      ∃ (𝔸 : CategoryTheory.Ind (Doubled A)) (x : CategoryTheory.MonObj 𝔸) (x_1 : CategoryTheory.IsCommMonObj 𝔸), CategoryTheory.MonObj.one ≠ 0 ∧ Nonempty (Doubled.evenEmbed.comp (indOf.comp (fibreOver doubledIndOddLine 𝔸))).Monoidal ∧ Nonempty (CategoryTheory.Limits.PreservesFiniteLimits (Doubled.evenEmbed.comp (indOf.comp (fibreFun doubledIndOddLine 𝔸)))) ∧ Nonempty (CategoryTheory.Limits.PreservesFiniteColimits (Doubled.evenEmbed.comp (indOf.comp (fibreFun doubledIndOddLine 𝔸)))) ∧ (Doubled.evenEmbed.comp (indOf.comp (fibreFun doubledIndOddLine 𝔸))).Faithful

      Deligne's Proposition 2.1 in general: no odd line is assumed. The category is doubled, Proposition 2.1 runs on the doubling — whose ind-completion carries an odd line — and the fibre functor obtained there is restricted along the even embedding. The composite is strong monoidal, preserves finite limits and finite colimits, and is faithful.