Deligne's theorem reduced to a genuinely small category

RS.DeligneTheoremStatement quantifies over a category A : Type u with Category.{v} A that is only essentially small, whereas the constructions of the development live over a SmallCategory. This module supplies the bridge: RS.deligneTheoremStatement_of_small derives the statement in its stated generality from the special case of a small category.

The route is Mathlib's CategoryTheory.SmallModel, carrying the monoidal structure transported along CategoryTheory.equivSmallModel (CategoryTheory.Monoidal.Transported). Along that equivalence:

• the abelian, preadditive, ℂ-linear, monoidal preadditive, monoidal ℂ-linear and rigid structures are transported to the small model (RS.SmallDeligne), the ℂ-linear one by RS.linearOfFullyFaithful and the rest by Mathlib's transfer lemmas;
• Deligne's three hypotheses are transported — RS.hasScalarUnit_of_fullyFaithful, RS.tensorGeneratedBy_map and RS.moderateLengthGrowth_map — using the comparison isomorphisms RS.tensorPowMapIso, RS.rightDualMapIso and RS.mixedPowMapIso of a monoidal equivalence, together with the behaviour of subquotients and of bounded length under a fully faithful functor (RS.isSubquotientOf_map, RS.lengthLE_of_map);
• the fibre functor comes back by precomposition, RS.DeligneFibreFunctor.precompose.

A linear structure pulled back along a fully faithful functor

@[implicit_reducible]

def RS.linearOfFullyFaithful (R : Type u_1) [Semiring R] {B : Type u₁} [CategoryTheory.Category.{v₁, u₁} B] [CategoryTheory.Preadditive B] {A : Type u₂} [CategoryTheory.Category.{v₂, u₂} A] [CategoryTheory.Preadditive A] [CategoryTheory.Linear R A] {G : CategoryTheory.Functor B A} (hG : G.FullyFaithful) [G.Additive] : CategoryTheory.Linear R B

The R-linear structure that a fully faithful additive functor into an R-linear category induces on its source: a morphism is rescaled by rescaling its image and taking the preimage.

Equations

• RS.linearOfFullyFaithful R hG = { homModule := fun (X Y : B) => Function.Injective.module R G.mapAddHom ⋯ ⋯, smul_comp := ⋯, comp_smul := ⋯ }

theorem RS.functorLinearOfFullyFaithful (R : Type u_1) [Semiring R] {B : Type u₁} [CategoryTheory.Category.{v₁, u₁} B] [CategoryTheory.Preadditive B] {A : Type u₂} [CategoryTheory.Category.{v₂, u₂} A] [CategoryTheory.Preadditive A] [CategoryTheory.Linear R A] {G : CategoryTheory.Functor B A} (hG : G.FullyFaithful) [G.Additive] : CategoryTheory.Functor.Linear R G

The inducing functor is linear for the induced structure: that structure is defined so that it is.

Comparison isomorphisms of a monoidal functor

noncomputable def RS.tensorPowMapIso {A : Type u₁} [CategoryTheory.Category.{v₁, u₁} A] [CategoryTheory.MonoidalCategory A] {B : Type u₂} [CategoryTheory.Category.{v₂, u₂} B] [CategoryTheory.MonoidalCategory B] (G : CategoryTheory.Functor A B) [G.Monoidal] (X : A) (n : ℕ) : G.obj (tensorPow A X n) ≅ tensorPow B (G.obj X) n

A monoidal functor carries a tensor power to the tensor power of the image: the comparison isomorphisms assembled by induction on the exponent.

Equations

• One or more equations did not get rendered due to their size.
• RS.tensorPowMapIso G X 0 = (CategoryTheory.Functor.Monoidal.εIso G).symm

noncomputable def RS.tensorPowCongrIso {B : Type u₂} [CategoryTheory.Category.{v₂, u₂} B] [CategoryTheory.MonoidalCategory B] {X Y : B} (i : X ≅ Y) (n : ℕ) : tensorPow B X n ≅ tensorPow B Y n

Tensor powers respect isomorphisms of the base object.

Equations

• RS.tensorPowCongrIso i 0 = CategoryTheory.Iso.refl (RS.tensorPow B X 0)
• RS.tensorPowCongrIso i n.succ = CategoryTheory.MonoidalCategory.tensorIso (RS.tensorPowCongrIso i n) i

noncomputable def RS.rightDualMapIso {A : Type u₁} [CategoryTheory.Category.{v₁, u₁} A] [CategoryTheory.MonoidalCategory A] [CategoryTheory.RigidCategory A] {B : Type u₂} [CategoryTheory.Category.{v₂, u₂} B] [CategoryTheory.MonoidalCategory B] [CategoryTheory.RigidCategory B] (e : A ≌ B) [e.inverse.Monoidal] (X : A) : e.functor.obj Xᘁ ≅ (e.functor.obj X)ᘁ

A monoidal equivalence of rigid categories carries right duals to right duals: the image of a dualising pair is a dualising pair because the inverse functor reflects one, and right duals are unique up to isomorphism.

Equations

• RS.rightDualMapIso e X = CategoryTheory.rightDualIso (CategoryTheory.ExactPairing.ofFullyFaithful e.inverse (e.functor.obj X) (e.functor.obj Xᘁ)) CategoryTheory.HasRightDual.exact

noncomputable def RS.mixedPowMapIso {A : Type u₁} [CategoryTheory.Category.{v₁, u₁} A] [CategoryTheory.MonoidalCategory A] [CategoryTheory.RigidCategory A] {B : Type u₂} [CategoryTheory.Category.{v₂, u₂} B] [CategoryTheory.MonoidalCategory B] [CategoryTheory.RigidCategory B] (e : A ≌ B) [e.functor.Monoidal] [e.inverse.Monoidal] (X : A) (a b : ℕ) : e.functor.obj (mixedPow A X a b) ≅ mixedPow B (e.functor.obj X) a b

A monoidal equivalence of rigid categories carries mixed tensor powers to mixed tensor powers.

Equations

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

Subquotients and bounded length along a functor

theorem RS.isSubquotientOf_map {A : Type u₁} [CategoryTheory.Category.{v₁, u₁} A] {B : Type u₂} [CategoryTheory.Category.{v₂, u₂} B] (G : CategoryTheory.Functor A B) [G.PreservesMonomorphisms] [G.PreservesEpimorphisms] {Y Z : A} (h : IsSubquotientOf Y Z) : IsSubquotientOf (G.obj Y) (G.obj Z)

A functor preserving monomorphisms and epimorphisms carries subquotients to subquotients.

theorem RS.IsSubquotientOf.congr {A : Type u₁} [CategoryTheory.Category.{v₁, u₁} A] {Y Y' Z Z' : A} (h : IsSubquotientOf Y Z) (iY : Y ≅ Y') (iZ : Z ≅ Z') : IsSubquotientOf Y' Z'

The subquotient relation transfers along isomorphisms of both arguments.

theorem RS.lengthLE_of_map {A : Type u₁} [CategoryTheory.Category.{v₁, u₁} A] {B : Type u₂} [CategoryTheory.Category.{v₂, u₂} B] (G : CategoryTheory.Functor B A) (hG : G.FullyFaithful) [G.PreservesMonomorphisms] {Z : B} {k : ℕ} (h : LengthLE (G.obj Z) k) : LengthLE Z k

A fully faithful functor preserving monomorphisms reflects the length bound: it embeds the subobject order of Z in that of G.obj Z, so a strictly increasing chain over Z gives one over G.obj Z.

Deligne's hypotheses along an equivalence

theorem RS.hasScalarUnit_of_fullyFaithful {A : Type u₁} [CategoryTheory.Category.{v₁, u₁} A] [CategoryTheory.Preadditive A] [CategoryTheory.Linear ℂ A] [CategoryTheory.MonoidalCategory A] {B : Type u₂} [CategoryTheory.Category.{v₂, u₂} B] [CategoryTheory.Preadditive B] [CategoryTheory.Linear ℂ B] [CategoryTheory.MonoidalCategory B] (G : CategoryTheory.Functor B A) (hG : G.FullyFaithful) [CategoryTheory.Functor.Linear ℂ G] [G.Monoidal] (h : HasScalarUnit A) : HasScalarUnit B

Scalar unit endomorphisms transfer along a fully faithful ℂ-linear monoidal functor: the map c ↦ c • 𝟙 on the source is carried onto the one on the target by the functor followed by conjugation with the unit comparison, and both of those are bijective.

theorem RS.tensorGeneratedBy_map {A : Type u₁} [CategoryTheory.Category.{v₁, u₁} A] [CategoryTheory.Preadditive A] [CategoryTheory.Limits.HasFiniteBiproducts A] [CategoryTheory.MonoidalCategory A] [CategoryTheory.RigidCategory A] {B : Type u₂} [CategoryTheory.Category.{v₂, u₂} B] [CategoryTheory.Preadditive B] [CategoryTheory.Limits.HasFiniteBiproducts B] [CategoryTheory.MonoidalCategory B] [CategoryTheory.RigidCategory B] (e : A ≌ B) [e.functor.Monoidal] [e.inverse.Monoidal] [e.functor.Additive] {X : A} (h : TensorGeneratedBy A X) : TensorGeneratedBy B (e.functor.obj X)

Finite tensor generation transfers along a monoidal equivalence: the image of a generator generates, because the equivalence carries the subquotient witness of the preimage of an object to one for the object, biproducts to biproducts and mixed powers to mixed powers.

theorem RS.moderateLengthGrowth_map {A : Type u₁} [CategoryTheory.Category.{v₁, u₁} A] [CategoryTheory.MonoidalCategory A] {B : Type u₂} [CategoryTheory.Category.{v₂, u₂} B] [CategoryTheory.MonoidalCategory B] (e : A ≌ B) [e.inverse.Monoidal] (h : ModerateLengthGrowth A) : ModerateLengthGrowth B

Moderate length growth transfers along a monoidal equivalence: the inverse functor carries a tensor power to the tensor power of the preimage, and reflects the length bound.

The fibre functor along a functor

noncomputable def RS.DeligneFibreFunctor.precompose {A : Type u₁} [CategoryTheory.Category.{v₁, u₁} A] [CategoryTheory.MonoidalCategory A] [CategoryTheory.SymmetricCategory A] [CategoryTheory.Preadditive A] [CategoryTheory.Linear ℂ A] {B : Type u₂} [CategoryTheory.Category.{v₂, u₂} B] [CategoryTheory.MonoidalCategory B] [CategoryTheory.SymmetricCategory B] [CategoryTheory.Preadditive B] [CategoryTheory.Linear ℂ B] (F : DeligneFibreFunctor B) (G : CategoryTheory.Functor A B) [G.Braided] [G.Additive] [CategoryTheory.Functor.Linear ℂ G] [G.Faithful] [CategoryTheory.Limits.PreservesFiniteLimits G] [CategoryTheory.Limits.PreservesFiniteColimits G] : DeligneFibreFunctor A

Precomposing a Deligne fibre functor with an exact, faithful, ℂ-linear symmetric monoidal functor gives a Deligne fibre functor: every clause of the conclusion is stable under composition.

Equations

• F.precompose G = { ω := G.comp F.ω, braided := inferInstance, additive := ⋯, linear := ⋯, faithful := ⋯, preservesFiniteLimits := ⋯, preservesFiniteColimits := ⋯ }

The small model of a candidate tensor category

@[reducible]

noncomputable def RS.SmallDeligne (A : Type u) [CategoryTheory.Category.{v, u} A] [CategoryTheory.EssentiallySmall.{v, v, u} A] : Type v

The small model of an essentially small monoidal category, carrying the monoidal structure transported along CategoryTheory.equivSmallModel.

Equations

• RS.SmallDeligne A = CategoryTheory.Monoidal.Transported (CategoryTheory.equivSmallModel A)

@[reducible]

noncomputable def RS.smallDeligneEquiv (A : Type u) [CategoryTheory.Category.{v, u} A] [CategoryTheory.EssentiallySmall.{v, v, u} A] : A ≌ SmallDeligne A

The transporting equivalence onto the small model, monoidal by construction.

Equations

• RS.smallDeligneEquiv A = CategoryTheory.Monoidal.equivalenceTransported (CategoryTheory.equivSmallModel A)

@[implicit_reducible]

noncomputable def RS.smallDelignePreadditive (A : Type u) [CategoryTheory.Category.{v, u} A] [CategoryTheory.Abelian A] [CategoryTheory.EssentiallySmall.{v, v, u} A] : CategoryTheory.Preadditive (SmallDeligne A)

The preadditive structure of the small model.

Equations

• RS.smallDelignePreadditive A = CategoryTheory.Preadditive.ofFullyFaithful (RS.smallDeligneEquiv A).fullyFaithfulInverse

theorem RS.smallDeligneInverseAdditive (A : Type u) [CategoryTheory.Category.{v, u} A] [CategoryTheory.Abelian A] [CategoryTheory.EssentiallySmall.{v, v, u} A] : (smallDeligneEquiv A).inverse.Additive

The inverse of the transporting equivalence is additive.

theorem RS.smallDeligneFunctorAdditive (A : Type u) [CategoryTheory.Category.{v, u} A] [CategoryTheory.Abelian A] [CategoryTheory.EssentiallySmall.{v, v, u} A] : (smallDeligneEquiv A).functor.Additive

The transporting equivalence is additive.

@[implicit_reducible]

noncomputable def RS.smallDeligneLinear (A : Type u) [CategoryTheory.Category.{v, u} A] [CategoryTheory.Abelian A] [CategoryTheory.Linear ℂ A] [CategoryTheory.EssentiallySmall.{v, v, u} A] : CategoryTheory.Linear ℂ (SmallDeligne A)

The ℂ-linear structure of the small model.

Equations

• RS.smallDeligneLinear A = RS.linearOfFullyFaithful ℂ (RS.smallDeligneEquiv A).fullyFaithfulInverse

theorem RS.smallDeligneInverseLinear (A : Type u) [CategoryTheory.Category.{v, u} A] [CategoryTheory.Abelian A] [CategoryTheory.Linear ℂ A] [CategoryTheory.EssentiallySmall.{v, v, u} A] : CategoryTheory.Functor.Linear ℂ (smallDeligneEquiv A).inverse

The inverse of the transporting equivalence is ℂ-linear.

theorem RS.smallDeligneFunctorLinear (A : Type u) [CategoryTheory.Category.{v, u} A] [CategoryTheory.Abelian A] [CategoryTheory.Linear ℂ A] [CategoryTheory.EssentiallySmall.{v, v, u} A] : CategoryTheory.Functor.Linear ℂ (smallDeligneEquiv A).functor

The transporting equivalence is ℂ-linear.

theorem RS.smallDeligneFiniteLimits (A : Type u) [CategoryTheory.Category.{v, u} A] [CategoryTheory.Abelian A] [CategoryTheory.EssentiallySmall.{v, v, u} A] : CategoryTheory.Limits.HasFiniteLimits (SmallDeligne A)

The small model has finite limits.

@[implicit_reducible]

noncomputable def RS.smallDeligneAbelian (A : Type u) [CategoryTheory.Category.{v, u} A] [CategoryTheory.Abelian A] [CategoryTheory.EssentiallySmall.{v, v, u} A] : CategoryTheory.Abelian (SmallDeligne A)

The small model is abelian.

Equations

• RS.smallDeligneAbelian A = CategoryTheory.abelianOfEquivalence (RS.smallDeligneEquiv A).inverse

theorem RS.smallDeligneBiproducts (A : Type u) [CategoryTheory.Category.{v, u} A] [CategoryTheory.Abelian A] [CategoryTheory.EssentiallySmall.{v, v, u} A] : CategoryTheory.Limits.HasFiniteBiproducts (SmallDeligne A)

The small model has finite biproducts.

theorem RS.smallDeligneMonoidalPreadditive (A : Type u) [CategoryTheory.Category.{v, u} A] [CategoryTheory.Abelian A] [CategoryTheory.MonoidalCategory A] [CategoryTheory.MonoidalPreadditive A] [CategoryTheory.EssentiallySmall.{v, v, u} A] : CategoryTheory.MonoidalPreadditive (SmallDeligne A)

The tensor product of the small model is biadditive.

theorem RS.smallDeligneMonoidalLinear (A : Type u) [CategoryTheory.Category.{v, u} A] [CategoryTheory.Abelian A] [CategoryTheory.Linear ℂ A] [CategoryTheory.MonoidalCategory A] [CategoryTheory.MonoidalPreadditive A] [CategoryTheory.MonoidalLinear ℂ A] [CategoryTheory.EssentiallySmall.{v, v, u} A] : CategoryTheory.MonoidalLinear ℂ (SmallDeligne A)

The tensor product of the small model is ℂ-bilinear.

@[implicit_reducible]

noncomputable def RS.smallDeligneRigid (A : Type u) [CategoryTheory.Category.{v, u} A] [CategoryTheory.MonoidalCategory A] [CategoryTheory.RigidCategory A] [CategoryTheory.EssentiallySmall.{v, v, u} A] : CategoryTheory.RigidCategory (SmallDeligne A)

The small model is rigid.

Equations

• RS.smallDeligneRigid A = CategoryTheory.rigidCategoryOfEquivalence (RS.smallDeligneEquiv A).symm.toAdjunction

theorem RS.deligneTheoremStatement_of_small (h : ∀ (B : Type v) [inst : CategoryTheory.SmallCategory B] [inst_1 : CategoryTheory.Abelian B] [inst_2 : CategoryTheory.Linear ℂ B] [inst_3 : CategoryTheory.MonoidalCategory B] [inst_4 : CategoryTheory.SymmetricCategory B] [inst_5 : CategoryTheory.MonoidalPreadditive B] [CategoryTheory.MonoidalLinear ℂ B] [inst_7 : CategoryTheory.Limits.HasFiniteBiproducts B] [inst_8 : CategoryTheory.RigidCategory B], HasScalarUnit B → (∃ (X : B), TensorGeneratedBy B X) → ModerateLengthGrowth B → Nonempty (DeligneFibreFunctor B)) : DeligneTheoremStatement

Deligne's theorem reduces to the small case. Given the conclusion of Théorème 0.6 for every small category carrying the hypotheses, it holds for every essentially small one: transport the structure and the hypotheses to the small model, apply the small case, and precompose the resulting fibre functor with the transporting equivalence.