The fibre functor into super vector spaces

Base change along a ℂ-point of the Γ-algebra turns each super module into a finite-dimensional super vector space (RS.toSuperVect of PointBaseChange.lean). This module upgrades that assignment to a functor, records its exactness, and assembles the fibre functor of Deligne's theorem out of the fibre functor over a splitting algebra and a ℂ-point of its Γ-algebra.

Three things are needed for the assembly and are established here.

• Super vector spaces are an abelian category. A super vector space is a Bool-indexed family of finite-dimensional complex vector spaces, and a morphism is a family of linear maps, so RS.SuperVect is equivalent to the category of functors from the discrete category on Bool to FGModuleCat ℂ. That functor category is abelian, and abelianness transports along an equivalence. This is what lets the exactness criterion RS.preservesFiniteLimits_of_shortExact be applied to a functor landing in RS.SuperVect.

• Base change is functorial. Tensoring with the residue module of the point is a functor, and RS.toSuperVect replaces the two components of the result by coordinate spaces of the same dimensions; conjugating by the coordinate equivalences turns the first into a functor to RS.SuperVect. The conjugation cancels in a composite, which is functoriality, and is additive componentwise, which is additivity.

• Exactness comes from freeness. Every module in the image of the fibre functor over a splitting algebra is free, so a short exact sequence of them splits, and base change carries the splitting across; a split short complex is short exact.

Faithfulness is then automatic: the functor is exact, so it carries the image factorisation of a morphism to an image factorisation, and an object whose fibre vanishes has both mixed ranks zero, hence zero fibre already over the algebra, hence — the unit of the algebra being a monomorphism — vanishes itself.

Contents

• RS.superVectComponents, RS.superVectAbelian: the equivalence with the diagram category, and the abelian structure it transports.
• RS.SuperCommAlgebra.Mod.instLinear, RS.SuperCommAlgebra.Mod.tensorHom_smul_left: the ℂ-linear structure of the super modules, and ℂ-linearity of the tensor product in the left variable.
• RS.superVectHom: base change of a morphism of super modules, with RS.superVectHom_id, superVectHom_comp, superVectHom_add and superVectHom_smul.
• RS.superVectFunctor: the base-change functor at a ℂ-point, with RS.superVectFunctor_additive and RS.superVectFunctor_linear.
• RS.finrank_superVectFunctor_even, finrank_superVectFunctor_odd: the two dimensions of the base change of a free value.
• RS.superVectSplitting, RS.superVectFunctor_shortExact, RS.superVectFunctor_preservesFiniteLimits, RS.superVectFunctor_preservesFiniteColimits, RS.superVectFunctor_preservesHomology: exactness.
• RS.deligneFibre: the fibre functor of a splitting algebra at a point, with its additivity, exactness (RS.deligneFibre_preservesFiniteLimits, deligneFibre_preservesFiniteColimits) and faithfulness (RS.deligneFibre_faithful).
• RS.exists_deligneFibre_of_point: the four properties packaged.

Super vector spaces form an abelian category

A super vector space is a Bool-indexed family of finite-dimensional complex vector spaces, and a morphism is a family of linear maps: the category is equivalent to the category of functors from the discrete category on Bool to the finite-dimensional complex vector spaces. That functor category is abelian, so RS.SuperVect is abelian too.

noncomputable def RS.superVectComponents : CategoryTheory.Functor SuperVect (CategoryTheory.Functor (CategoryTheory.Discrete Bool) (FGModuleCat ℂ))

The components of a super vector space, as a functor to the Bool-indexed diagrams of finite-dimensional complex vector spaces.

Equations

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

instance RS.superVectComponents_faithful : superVectComponents.Faithful

instance RS.superVectComponents_full : superVectComponents.Full

instance RS.superVectComponents_essSurj : superVectComponents.EssSurj

instance RS.superVectComponents_isEquivalence : superVectComponents.IsEquivalence

instance RS.instHasFiniteProductsSuperVect : CategoryTheory.Limits.HasFiniteProducts SuperVect

Super vector spaces have finite products, transported along the equivalence with the diagram category.

@[instance_reducible]

noncomputable instance RS.superVectAbelian : CategoryTheory.Abelian SuperVect

Super vector spaces form an abelian category.

Equations

• RS.superVectAbelian = CategoryTheory.abelianOfEquivalence RS.superVectComponents

ℂ-linearity of the super modules over a super algebra

Morphisms of super modules already carry a scaling by complex numbers; the module axioms and the bilinearity of composition hold componentwise, so the category is ℂ-linear. The tensor product is ℂ-linear in each variable for the same reason.

@[instance_reducible]

instance RS.SuperCommAlgebra.Mod.homModule {S : SuperCommAlgebra} (M N : S.Mod) : Module ℂ (M ⟶ N)

Morphisms of super modules form a ℂ-module.

Equations

• M.homModule N = { toSMul := M.homSMul N, mul_smul := ⋯, one_smul := ⋯, smul_zero := ⋯, smul_add := ⋯, add_smul := ⋯, zero_smul := ⋯ }

@[instance_reducible]

instance RS.SuperCommAlgebra.Mod.instLinear {S : SuperCommAlgebra} : CategoryTheory.Linear ℂ S.Mod

Super modules over a super algebra form a ℂ-linear category.

Equations

• RS.SuperCommAlgebra.Mod.instLinear = { homModule := inferInstance, smul_comp := ⋯, comp_smul := ⋯ }

theorem RS.SuperCommAlgebra.Mod.tensorHom_smul_left {S : SuperCommAlgebra} {M N P Q : S.Mod} (c : ℂ) (f : M ⟶ P) (g : N ⟶ Q) : tensorHom (c • f) g = c • tensorHom f g

The tensor product of super modules is ℂ-linear in the left variable.

instance RS.SuperCommAlgebra.Mod.tensorRightFunctor_linear {S : SuperCommAlgebra} (N : S.Mod) : CategoryTheory.Functor.Linear ℂ N.tensorRightFunctor

Tensoring on the right by a fixed module is ℂ-linear.

noncomputable def RS.superVectHom {S : SuperCommAlgebra} (P : SuperPoint S) {M N : S.Mod} [FiniteDimensional ℂ (M.tensor (SuperCommAlgebra.pointMod P)).even] [FiniteDimensional ℂ (M.tensor (SuperCommAlgebra.pointMod P)).odd] [FiniteDimensional ℂ (N.tensor (SuperCommAlgebra.pointMod P)).even] [FiniteDimensional ℂ (N.tensor (SuperCommAlgebra.pointMod P)).odd] (u : M ⟶ N) : toSuperVect P M ⟶ toSuperVect P N

Base change of a morphism of super modules along a ℂ-point. The morphism is tensored with the residue module and the result is read in the coordinates that RS.toSuperVect installs on the two components.

Equations

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

theorem RS.superVectHom_id {S : SuperCommAlgebra} (P : SuperPoint S) {M : S.Mod} [FiniteDimensional ℂ (M.tensor (SuperCommAlgebra.pointMod P)).even] [FiniteDimensional ℂ (M.tensor (SuperCommAlgebra.pointMod P)).odd] : superVectHom P (CategoryTheory.CategoryStruct.id M) = CategoryTheory.CategoryStruct.id (toSuperVect P M)

Base change fixes the identity.

theorem RS.superVectHom_comp {S : SuperCommAlgebra} (P : SuperPoint S) {M N Q : S.Mod} [FiniteDimensional ℂ (M.tensor (SuperCommAlgebra.pointMod P)).even] [FiniteDimensional ℂ (M.tensor (SuperCommAlgebra.pointMod P)).odd] [FiniteDimensional ℂ (N.tensor (SuperCommAlgebra.pointMod P)).even] [FiniteDimensional ℂ (N.tensor (SuperCommAlgebra.pointMod P)).odd] [FiniteDimensional ℂ (Q.tensor (SuperCommAlgebra.pointMod P)).even] [FiniteDimensional ℂ (Q.tensor (SuperCommAlgebra.pointMod P)).odd] (u : M ⟶ N) (v : N ⟶ Q) : superVectHom P (CategoryTheory.CategoryStruct.comp u v) = CategoryTheory.CategoryStruct.comp (superVectHom P u) (superVectHom P v)

Base change respects composition: the conjugating equivalences cancel.

theorem RS.superVectHom_add {S : SuperCommAlgebra} (P : SuperPoint S) {M N : S.Mod} [FiniteDimensional ℂ (M.tensor (SuperCommAlgebra.pointMod P)).even] [FiniteDimensional ℂ (M.tensor (SuperCommAlgebra.pointMod P)).odd] [FiniteDimensional ℂ (N.tensor (SuperCommAlgebra.pointMod P)).even] [FiniteDimensional ℂ (N.tensor (SuperCommAlgebra.pointMod P)).odd] (u v : M ⟶ N) : superVectHom P (u + v) = superVectHom P u + superVectHom P v

Base change is additive.

theorem RS.superVectHom_smul {S : SuperCommAlgebra} (P : SuperPoint S) {M N : S.Mod} [FiniteDimensional ℂ (M.tensor (SuperCommAlgebra.pointMod P)).even] [FiniteDimensional ℂ (M.tensor (SuperCommAlgebra.pointMod P)).odd] [FiniteDimensional ℂ (N.tensor (SuperCommAlgebra.pointMod P)).even] [FiniteDimensional ℂ (N.tensor (SuperCommAlgebra.pointMod P)).odd] (c : ℂ) (u : M ⟶ N) : superVectHom P (c • u) = c • superVectHom P u

Base change is ℂ-linear.

noncomputable def RS.superVectFunctor {S : SuperCommAlgebra} (P : SuperPoint S) {E : Type u₂} [CategoryTheory.Category.{v₂, u₂} E] (G : CategoryTheory.Functor E S.Mod) (hE : ∀ (X : E), FiniteDimensional ℂ ((G.obj X).tensor (SuperCommAlgebra.pointMod P)).even) (hO : ∀ (X : E), FiniteDimensional ℂ ((G.obj X).tensor (SuperCommAlgebra.pointMod P)).odd) : CategoryTheory.Functor E SuperVect

The base-change functor at a ℂ-point. Each value of G is tensored with the residue module of the point and packaged as a super vector space; each morphism is conjugated through the coordinate equivalences.

Equations

• RS.superVectFunctor P G hE hO = { obj := fun (X : E) => RS.toSuperVect P (G.obj X), map := fun {X Y : E} (f : X ⟶ Y) => RS.superVectHom P (G.map f), map_id := ⋯, map_comp := ⋯ }

@[simp]

theorem RS.superVectFunctor_obj {S : SuperCommAlgebra} (P : SuperPoint S) {E : Type u₂} [CategoryTheory.Category.{v₂, u₂} E] (G : CategoryTheory.Functor E S.Mod) (hE : ∀ (X : E), FiniteDimensional ℂ ((G.obj X).tensor (SuperCommAlgebra.pointMod P)).even) (hO : ∀ (X : E), FiniteDimensional ℂ ((G.obj X).tensor (SuperCommAlgebra.pointMod P)).odd) (X : E) : (superVectFunctor P G hE hO).obj X = toSuperVect P (G.obj X)

@[simp]

theorem RS.superVectFunctor_map {S : SuperCommAlgebra} (P : SuperPoint S) {E : Type u₂} [CategoryTheory.Category.{v₂, u₂} E] (G : CategoryTheory.Functor E S.Mod) (hE : ∀ (X : E), FiniteDimensional ℂ ((G.obj X).tensor (SuperCommAlgebra.pointMod P)).even) (hO : ∀ (X : E), FiniteDimensional ℂ ((G.obj X).tensor (SuperCommAlgebra.pointMod P)).odd) {X Y : E} (f : X ⟶ Y) : (superVectFunctor P G hE hO).map f = superVectHom P (G.map f)

Additivity

instance RS.superVectFunctor_additive {S : SuperCommAlgebra} (P : SuperPoint S) {E : Type u₂} [CategoryTheory.Category.{v₂, u₂} E] (G : CategoryTheory.Functor E S.Mod) (hE : ∀ (X : E), FiniteDimensional ℂ ((G.obj X).tensor (SuperCommAlgebra.pointMod P)).even) (hO : ∀ (X : E), FiniteDimensional ℂ ((G.obj X).tensor (SuperCommAlgebra.pointMod P)).odd) [CategoryTheory.Preadditive E] [G.Additive] : (superVectFunctor P G hE hO).Additive

The base-change functor is additive.

instance RS.superVectFunctor_linear {S : SuperCommAlgebra} (P : SuperPoint S) {E : Type u₂} [CategoryTheory.Category.{v₂, u₂} E] (G : CategoryTheory.Functor E S.Mod) (hE : ∀ (X : E), FiniteDimensional ℂ ((G.obj X).tensor (SuperCommAlgebra.pointMod P)).even) (hO : ∀ (X : E), FiniteDimensional ℂ ((G.obj X).tensor (SuperCommAlgebra.pointMod P)).odd) [CategoryTheory.Preadditive E] [CategoryTheory.Linear ℂ E] [CategoryTheory.Functor.Linear ℂ G] : CategoryTheory.Functor.Linear ℂ (superVectFunctor P G hE hO)

The base-change functor is ℂ-linear.

Dimensions

theorem RS.finrank_superVectFunctor_even {S : SuperCommAlgebra} (P : SuperPoint S) {E : Type u₂} [CategoryTheory.Category.{v₂, u₂} E] (G : CategoryTheory.Functor E S.Mod) (hE : ∀ (X : E), FiniteDimensional ℂ ((G.obj X).tensor (SuperCommAlgebra.pointMod P)).even) (hO : ∀ (X : E), FiniteDimensional ℂ ((G.obj X).tensor (SuperCommAlgebra.pointMod P)).odd) (X : E) (p q : ℕ) (e : G.obj X ≅ ⨁ fun (i : Fin p ⊕ Fin q) => Sum.elim (fun (x : Fin p) => S.unitMod) (fun (x : Fin q) => S.unitMod.shift) i) : Module.finrank ℂ ((superVectFunctor P G hE hO).obj X).even = p

The even dimension of the base change of a free value. If G takes X to a free super module of rank (p | q) then the even part of its base change has dimension p.

theorem RS.finrank_superVectFunctor_odd {S : SuperCommAlgebra} (P : SuperPoint S) {E : Type u₂} [CategoryTheory.Category.{v₂, u₂} E] (G : CategoryTheory.Functor E S.Mod) (hE : ∀ (X : E), FiniteDimensional ℂ ((G.obj X).tensor (SuperCommAlgebra.pointMod P)).even) (hO : ∀ (X : E), FiniteDimensional ℂ ((G.obj X).tensor (SuperCommAlgebra.pointMod P)).odd) (X : E) (p q : ℕ) (e : G.obj X ≅ ⨁ fun (i : Fin p ⊕ Fin q) => Sum.elim (fun (x : Fin p) => S.unitMod) (fun (x : Fin q) => S.unitMod.shift) i) : Module.finrank ℂ ((superVectFunctor P G hE hO).obj X).odd = q

The odd dimension of the base change of a free value.

Exactness

noncomputable def RS.superVectSplitting {S : SuperCommAlgebra} (P : SuperPoint S) {E : Type u₂} [CategoryTheory.Category.{v₂, u₂} E] (G : CategoryTheory.Functor E S.Mod) (hE : ∀ (X : E), FiniteDimensional ℂ ((G.obj X).tensor (SuperCommAlgebra.pointMod P)).even) (hO : ∀ (X : E), FiniteDimensional ℂ ((G.obj X).tensor (SuperCommAlgebra.pointMod P)).odd) [CategoryTheory.Abelian E] [G.Additive] (T : CategoryTheory.ShortComplex E) (σ : (T.map G).Splitting) : (T.map (superVectFunctor P G hE hO)).Splitting

A splitting of the image under G gives a splitting after base change. All three terms are free over the Γ-algebra, so the sequence splits before base change, and base change carries the splitting across.

Equations

• RS.superVectSplitting P G hE hO T σ = { r := RS.superVectHom P σ.r, s := RS.superVectHom P σ.s, f_r := ⋯, s_g := ⋯, id := ⋯ }

theorem RS.superVectFunctor_shortExact {S : SuperCommAlgebra} (P : SuperPoint S) {E : Type u₂} [CategoryTheory.Category.{v₂, u₂} E] (G : CategoryTheory.Functor E S.Mod) (hE : ∀ (X : E), FiniteDimensional ℂ ((G.obj X).tensor (SuperCommAlgebra.pointMod P)).even) (hO : ∀ (X : E), FiniteDimensional ℂ ((G.obj X).tensor (SuperCommAlgebra.pointMod P)).odd) [CategoryTheory.Abelian E] [G.Additive] (T : CategoryTheory.ShortComplex E) (σ : (T.map G).Splitting) : (T.map (superVectFunctor P G hE hO)).ShortExact

The base-change functor carries a split short exact sequence to a short exact sequence.

theorem RS.superVectFunctor_preservesFiniteLimits {S : SuperCommAlgebra} (P : SuperPoint S) {E : Type u₂} [CategoryTheory.Category.{v₂, u₂} E] (G : CategoryTheory.Functor E S.Mod) (hE : ∀ (X : E), FiniteDimensional ℂ ((G.obj X).tensor (SuperCommAlgebra.pointMod P)).even) (hO : ∀ (X : E), FiniteDimensional ℂ ((G.obj X).tensor (SuperCommAlgebra.pointMod P)).odd) [CategoryTheory.Abelian E] [G.Additive] (hsec : ∀ (T : CategoryTheory.ShortComplex E), T.ShortExact → Nonempty (T.map G).Splitting) : CategoryTheory.Limits.PreservesFiniteLimits (superVectFunctor P G hE hO)

The base-change functor preserves finite limits as soon as every short exact sequence splits after G.

theorem RS.superVectFunctor_preservesFiniteColimits {S : SuperCommAlgebra} (P : SuperPoint S) {E : Type u₂} [CategoryTheory.Category.{v₂, u₂} E] (G : CategoryTheory.Functor E S.Mod) (hE : ∀ (X : E), FiniteDimensional ℂ ((G.obj X).tensor (SuperCommAlgebra.pointMod P)).even) (hO : ∀ (X : E), FiniteDimensional ℂ ((G.obj X).tensor (SuperCommAlgebra.pointMod P)).odd) [CategoryTheory.Abelian E] [G.Additive] (hsec : ∀ (T : CategoryTheory.ShortComplex E), T.ShortExact → Nonempty (T.map G).Splitting) : CategoryTheory.Limits.PreservesFiniteColimits (superVectFunctor P G hE hO)

The base-change functor preserves finite colimits under the same hypothesis; with the previous statement it is exact.

theorem RS.superVectFunctor_preservesHomology {S : SuperCommAlgebra} (P : SuperPoint S) {E : Type u₂} [CategoryTheory.Category.{v₂, u₂} E] (G : CategoryTheory.Functor E S.Mod) (hE : ∀ (X : E), FiniteDimensional ℂ ((G.obj X).tensor (SuperCommAlgebra.pointMod P)).even) (hO : ∀ (X : E), FiniteDimensional ℂ ((G.obj X).tensor (SuperCommAlgebra.pointMod P)).odd) [CategoryTheory.Abelian E] [G.Additive] (hsec : ∀ (T : CategoryTheory.ShortComplex E), T.ShortExact → Nonempty (T.map G).Splitting) : (superVectFunctor P G hE hO).PreservesHomology

The base-change functor preserves homology, hence monomorphisms and epimorphisms.

The fibre functor of a splitting algebra at a point

instance RS.indFibre_additive {C : Type v} [CategoryTheory.SmallCategory C] [CategoryTheory.MonoidalCategory C] [CategoryTheory.SymmetricCategory C] [CategoryTheory.Abelian C] [CategoryTheory.MonoidalPreadditive C] [CategoryTheory.Linear ℂ (CategoryTheory.Ind C)] [CategoryTheory.MonoidalLinear ℂ (CategoryTheory.Ind C)] (L : OddLine (CategoryTheory.Ind C)) (𝔸 : CategoryTheory.Ind C) [CategoryTheory.MonObj 𝔸] [CategoryTheory.IsCommMonObj 𝔸] : (indOf.comp (fibreFun L 𝔸)).Additive

The restricted fibre functor is additive.

theorem RS.finiteDimensional_indFibre_even {C : Type v} [CategoryTheory.SmallCategory C] [CategoryTheory.MonoidalCategory C] [CategoryTheory.SymmetricCategory C] [CategoryTheory.Abelian C] [CategoryTheory.MonoidalPreadditive C] [CategoryTheory.Linear ℂ (CategoryTheory.Ind C)] [CategoryTheory.MonoidalLinear ℂ (CategoryTheory.Ind C)] (L : OddLine (CategoryTheory.Ind C)) (𝔸 : CategoryTheory.Ind C) [CategoryTheory.MonObj 𝔸] [CategoryTheory.IsCommMonObj 𝔸] (hsp : SplitsOn L 𝔸 indOf) (P : SuperPoint (gammaAlgebra (CategoryTheory.Ind C) L 𝔸)) (X : C) : FiniteDimensional ℂ (((indOf.comp (fibreFun L 𝔸)).obj X).tensor (SuperCommAlgebra.pointMod P)).even

The even part of the fibre of an embedded object at a point is finite dimensional, for an algebra splitting the embedding.

theorem RS.finiteDimensional_indFibre_odd {C : Type v} [CategoryTheory.SmallCategory C] [CategoryTheory.MonoidalCategory C] [CategoryTheory.SymmetricCategory C] [CategoryTheory.Abelian C] [CategoryTheory.MonoidalPreadditive C] [CategoryTheory.Linear ℂ (CategoryTheory.Ind C)] [CategoryTheory.MonoidalLinear ℂ (CategoryTheory.Ind C)] (L : OddLine (CategoryTheory.Ind C)) (𝔸 : CategoryTheory.Ind C) [CategoryTheory.MonObj 𝔸] [CategoryTheory.IsCommMonObj 𝔸] (hsp : SplitsOn L 𝔸 indOf) (P : SuperPoint (gammaAlgebra (CategoryTheory.Ind C) L 𝔸)) (X : C) : FiniteDimensional ℂ (((indOf.comp (fibreFun L 𝔸)).obj X).tensor (SuperCommAlgebra.pointMod P)).odd

The odd part of the fibre of an embedded object at a point is finite dimensional.

noncomputable def RS.deligneFibre {C : Type v} [CategoryTheory.SmallCategory C] [CategoryTheory.MonoidalCategory C] [CategoryTheory.SymmetricCategory C] [CategoryTheory.Abelian C] [CategoryTheory.MonoidalPreadditive C] [CategoryTheory.Linear ℂ (CategoryTheory.Ind C)] [CategoryTheory.MonoidalLinear ℂ (CategoryTheory.Ind C)] (L : OddLine (CategoryTheory.Ind C)) (𝔸 : CategoryTheory.Ind C) [CategoryTheory.MonObj 𝔸] [CategoryTheory.IsCommMonObj 𝔸] (hsp : SplitsOn L 𝔸 indOf) (P : SuperPoint (gammaAlgebra (CategoryTheory.Ind C) L 𝔸)) : CategoryTheory.Functor C SuperVect

The fibre functor into super vector spaces: embed, take the fibre over the splitting algebra, and base change to the ℂ-point.

Equations

• RS.deligneFibre L 𝔸 hsp P = RS.superVectFunctor P (RS.indOf.comp (RS.fibreFun L 𝔸)) ⋯ ⋯

instance RS.deligneFibre_additive {C : Type v} [CategoryTheory.SmallCategory C] [CategoryTheory.MonoidalCategory C] [CategoryTheory.SymmetricCategory C] [CategoryTheory.Abelian C] [CategoryTheory.MonoidalPreadditive C] [CategoryTheory.Linear ℂ (CategoryTheory.Ind C)] [CategoryTheory.MonoidalLinear ℂ (CategoryTheory.Ind C)] (L : OddLine (CategoryTheory.Ind C)) (𝔸 : CategoryTheory.Ind C) [CategoryTheory.MonObj 𝔸] [CategoryTheory.IsCommMonObj 𝔸] (hsp : SplitsOn L 𝔸 indOf) (P : SuperPoint (gammaAlgebra (CategoryTheory.Ind C) L 𝔸)) : (deligneFibre L 𝔸 hsp P).Additive

The fibre functor is additive.

Exactness

theorem RS.indFibre_nonempty_splitting {C : Type v} [CategoryTheory.SmallCategory C] [CategoryTheory.MonoidalCategory C] [CategoryTheory.SymmetricCategory C] [CategoryTheory.Abelian C] [CategoryTheory.RigidCategory C] [CategoryTheory.MonoidalPreadditive C] [CategoryTheory.Linear ℂ (CategoryTheory.Ind C)] [CategoryTheory.MonoidalLinear ℂ (CategoryTheory.Ind C)] (L : OddLine (CategoryTheory.Ind C)) (𝔸 : CategoryTheory.Ind C) [CategoryTheory.MonObj 𝔸] [CategoryTheory.IsCommMonObj 𝔸] (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₃)) (T : CategoryTheory.ShortComplex C) (hT : T.ShortExact) : Nonempty (T.map (indOf.comp (fibreFun L 𝔸))).Splitting

The base-change hypothesis of RS.exists_fibre_algebra, as a splitting of each embedded short exact sequence after the fibre functor.

theorem RS.deligneFibre_preservesFiniteLimits {C : Type v} [CategoryTheory.SmallCategory C] [CategoryTheory.MonoidalCategory C] [CategoryTheory.SymmetricCategory C] [CategoryTheory.Abelian C] [CategoryTheory.RigidCategory C] [CategoryTheory.MonoidalPreadditive C] [CategoryTheory.Linear ℂ (CategoryTheory.Ind C)] [CategoryTheory.MonoidalLinear ℂ (CategoryTheory.Ind C)] (L : OddLine (CategoryTheory.Ind C)) (𝔸 : CategoryTheory.Ind C) [CategoryTheory.MonObj 𝔸] [CategoryTheory.IsCommMonObj 𝔸] (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₃)) (P : SuperPoint (gammaAlgebra (CategoryTheory.Ind C) L 𝔸)) : CategoryTheory.Limits.PreservesFiniteLimits (deligneFibre L 𝔸 hsp P)

The fibre functor preserves finite limits.

theorem RS.deligneFibre_preservesFiniteColimits {C : Type v} [CategoryTheory.SmallCategory C] [CategoryTheory.MonoidalCategory C] [CategoryTheory.SymmetricCategory C] [CategoryTheory.Abelian C] [CategoryTheory.RigidCategory C] [CategoryTheory.MonoidalPreadditive C] [CategoryTheory.Linear ℂ (CategoryTheory.Ind C)] [CategoryTheory.MonoidalLinear ℂ (CategoryTheory.Ind C)] (L : OddLine (CategoryTheory.Ind C)) (𝔸 : CategoryTheory.Ind C) [CategoryTheory.MonObj 𝔸] [CategoryTheory.IsCommMonObj 𝔸] (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₃)) (P : SuperPoint (gammaAlgebra (CategoryTheory.Ind C) L 𝔸)) : CategoryTheory.Limits.PreservesFiniteColimits (deligneFibre L 𝔸 hsp P)

The fibre functor preserves finite colimits; with the previous statement it is exact.

Dimensions and faithfulness

theorem RS.id_eq_zero_of_deligneFibre_id_eq_zero {C : Type v} [CategoryTheory.SmallCategory C] [CategoryTheory.MonoidalCategory C] [CategoryTheory.SymmetricCategory C] [CategoryTheory.Abelian C] [CategoryTheory.MonoidalPreadditive C] [CategoryTheory.Linear ℂ (CategoryTheory.Ind C)] [CategoryTheory.MonoidalLinear ℂ (CategoryTheory.Ind C)] (L : OddLine (CategoryTheory.Ind C)) (𝔸 : CategoryTheory.Ind C) [CategoryTheory.MonObj 𝔸] [CategoryTheory.IsCommMonObj 𝔸] [∀ (Z : CategoryTheory.Ind C), (CategoryTheory.MonoidalCategory.tensorRight Z).PreservesMonomorphisms] (hmono : CategoryTheory.Mono CategoryTheory.MonObj.one) (hsp : SplitsOn L 𝔸 indOf) (P : SuperPoint (gammaAlgebra (CategoryTheory.Ind C) L 𝔸)) (Z : C) (hz : CategoryTheory.CategoryStruct.id ((deligneFibre L 𝔸 hsp P).obj Z) = 0) : CategoryTheory.CategoryStruct.id Z = 0

The fibre functor detects the zero object. If the fibre of an object is a zero super vector space then both ranks of its mixed sum vanish, so its fibre over the algebra is already zero, and the unit of the algebra being a monomorphism forces the object to vanish.

theorem RS.deligneFibre_faithful {C : Type v} [CategoryTheory.SmallCategory C] [CategoryTheory.MonoidalCategory C] [CategoryTheory.SymmetricCategory C] [CategoryTheory.Abelian C] [CategoryTheory.RigidCategory C] [CategoryTheory.MonoidalPreadditive C] [CategoryTheory.Linear ℂ (CategoryTheory.Ind C)] [CategoryTheory.MonoidalLinear ℂ (CategoryTheory.Ind C)] (L : OddLine (CategoryTheory.Ind C)) (𝔸 : CategoryTheory.Ind C) [CategoryTheory.MonObj 𝔸] [CategoryTheory.IsCommMonObj 𝔸] [∀ (Z : CategoryTheory.Ind C), (CategoryTheory.MonoidalCategory.tensorRight Z).PreservesMonomorphisms] (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₃)) (P : SuperPoint (gammaAlgebra (CategoryTheory.Ind C) L 𝔸)) : (deligneFibre L 𝔸 hsp P).Faithful

The fibre functor is faithful. It is exact, so it carries the image factorisation of a morphism to an image factorisation; a morphism killed by the functor therefore has zero image, and an object with zero fibre is zero.

The packaged statement

theorem RS.exists_deligneFibre_of_point {C : Type v} [CategoryTheory.SmallCategory C] [CategoryTheory.MonoidalCategory C] [CategoryTheory.SymmetricCategory C] [CategoryTheory.Abelian C] [CategoryTheory.RigidCategory C] [CategoryTheory.MonoidalPreadditive C] [CategoryTheory.Linear ℂ (CategoryTheory.Ind C)] [CategoryTheory.MonoidalLinear ℂ (CategoryTheory.Ind C)] (L : OddLine (CategoryTheory.Ind C)) (𝔸 : CategoryTheory.Ind C) [CategoryTheory.MonObj 𝔸] [CategoryTheory.IsCommMonObj 𝔸] [∀ (Z : CategoryTheory.Ind C), (CategoryTheory.MonoidalCategory.tensorRight Z).PreservesMonomorphisms] (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₃)) (P : SuperPoint (gammaAlgebra (CategoryTheory.Ind C) L 𝔸)) : ∃ (ω : CategoryTheory.Functor C SuperVect), ω.Additive ∧ Nonempty (CategoryTheory.Limits.PreservesFiniteLimits ω) ∧ Nonempty (CategoryTheory.Limits.PreservesFiniteColimits ω) ∧ ω.Faithful

A fibre functor into super vector spaces from a splitting algebra with a ℂ-point. Over an algebra whose unit is a nonzero monomorphism, which splits every embedded object into a mixed sum and every embedded short exact sequence after base change, the composite of the embedding, the fibre functor over the algebra and base change along the point is an additive, exact and faithful functor to finite-dimensional super vector spaces.