The fibre functor over the splitting algebra

Assembling the three properties over the algebra of RS.exists_splitting_algebra: the restriction of the fibre functor along the Ind-embedding is strong monoidal, it is exact, and it is faithful once the unit of the algebra is a monomorphism.

The braiding of Ind C is hypothesised here, through SymmetricCategory (Ind C), and is deliberately not also available by transport from a braiding of C. Assuming BraidedCategory C as well would put two unrelated BraidedCategory (Ind C) instances in scope — the transported one of RS.Classical.Deligne.IndMonoidal and the one underlying the hypothesised symmetry — and IsCommMonObj 𝔸, whose commutativity law is stated against a braiding, would then be a different class in the variable block from the one the fibre-functor lemmas below consume. The variable block therefore names the symmetry of Ind C only, matching RS.Classical.Deligne.UniversalAlgebra.

@[implicit_reducible]

noncomputable def RS.indFibreMonoidal {C : Type v} [CategoryTheory.SmallCategory C] [CategoryTheory.MonoidalCategory C] [CategoryTheory.Abelian C] [CategoryTheory.Linear ℂ (CategoryTheory.Ind C)] [CategoryTheory.MonoidalPreadditive (CategoryTheory.Ind C)] [CategoryTheory.MonoidalLinear ℂ (CategoryTheory.Ind C)] [CategoryTheory.SymmetricCategory (CategoryTheory.Ind C)] [CategoryTheory.Limits.HasCoequalizers (CategoryTheory.Ind C)] [∀ (Z : CategoryTheory.Ind C), CategoryTheory.Limits.PreservesColimitsOfShape CategoryTheory.Limits.WalkingParallelPair (CategoryTheory.MonoidalCategory.tensorLeft Z)] [CategoryTheory.Limits.HasFiniteBiproducts (CategoryTheory.Ind C)] (L : OddLine (CategoryTheory.Ind C)) (𝔸 : CategoryTheory.Ind C) [CategoryTheory.MonObj 𝔸] [CategoryTheory.IsCommMonObj 𝔸] (hsp : SplitsOn L 𝔸 indOf) : (indOf.comp (fibreOver L 𝔸)).Monoidal

The restricted fibre functor is strong monoidal over an algebra that splits the embedded objects.

Equations

• RS.indFibreMonoidal L 𝔸 hsp = RS.fibreRestrictMonoidal L 𝔸 RS.indOf hsp

theorem RS.indFibre_faithful {C : Type v} [CategoryTheory.SmallCategory C] [CategoryTheory.MonoidalCategory C] [CategoryTheory.Abelian C] [CategoryTheory.Linear ℂ (CategoryTheory.Ind C)] [CategoryTheory.MonoidalPreadditive (CategoryTheory.Ind C)] [CategoryTheory.MonoidalLinear ℂ (CategoryTheory.Ind C)] [CategoryTheory.SymmetricCategory (CategoryTheory.Ind C)] [CategoryTheory.Limits.HasFiniteBiproducts (CategoryTheory.Ind C)] (L : OddLine (CategoryTheory.Ind C)) (𝔸 : CategoryTheory.Ind C) [CategoryTheory.MonObj 𝔸] [CategoryTheory.IsCommMonObj 𝔸] (hmono : CategoryTheory.Mono CategoryTheory.MonObj.one) (hsp : SplitsOn L 𝔸 indOf) [∀ (Z : CategoryTheory.Ind C), (CategoryTheory.MonoidalCategory.tensorRight Z).PreservesMonomorphisms] : (indOf.comp (fibreFun L 𝔸)).Faithful

The restricted fibre functor is faithful over an algebra that splits the embedded objects, provided its unit is a monomorphism.

Exactness of the restricted fibre functor

theorem RS.indOf_shortExact {C : Type v} [CategoryTheory.SmallCategory C] [CategoryTheory.Abelian C] {S : CategoryTheory.ShortComplex C} (hS : S.ShortExact) : (S.map indOf).ShortExact

The embedding carries a short exact sequence of C to a short exact sequence of Ind C: it is additive, it preserves limits, and it preserves finite colimits.

theorem RS.indFibre_shortExact {C : Type v} [CategoryTheory.SmallCategory C] [CategoryTheory.MonoidalCategory C] [CategoryTheory.Abelian C] [CategoryTheory.MonoidalPreadditive C] [CategoryTheory.RigidCategory C] [CategoryTheory.Linear ℂ (CategoryTheory.Ind C)] [CategoryTheory.MonoidalPreadditive (CategoryTheory.Ind C)] [CategoryTheory.MonoidalLinear ℂ (CategoryTheory.Ind C)] [CategoryTheory.SymmetricCategory (CategoryTheory.Ind C)] (L : OddLine (CategoryTheory.Ind C)) (𝔸 : CategoryTheory.Ind C) [CategoryTheory.MonObj 𝔸] [CategoryTheory.IsCommMonObj 𝔸] (hsec : ∀ (S : CategoryTheory.ShortComplex C), S.ShortExact → ∃ (s : freeMod 𝔸 (S.map indOf).X₃ ⟶ freeMod 𝔸 (S.map indOf).X₂), CategoryTheory.CategoryStruct.comp s (freeModMap 𝔸 (S.map indOf).g) = CategoryTheory.CategoryStruct.id (freeMod 𝔸 (S.map indOf).X₃)) (S : CategoryTheory.ShortComplex C) (hS : S.ShortExact) : (S.map (indOf.comp (fibreFun L 𝔸))).ShortExact

The restricted fibre functor carries short exact sequences to short exact sequences, given a base-change section over 𝔸 for each embedded sequence.

theorem RS.indFibre_preservesFiniteLimits {C : Type v} [CategoryTheory.SmallCategory C] [CategoryTheory.MonoidalCategory C] [CategoryTheory.Abelian C] [CategoryTheory.MonoidalPreadditive C] [CategoryTheory.RigidCategory C] [CategoryTheory.Linear ℂ (CategoryTheory.Ind C)] [CategoryTheory.MonoidalPreadditive (CategoryTheory.Ind C)] [CategoryTheory.MonoidalLinear ℂ (CategoryTheory.Ind C)] [CategoryTheory.SymmetricCategory (CategoryTheory.Ind C)] (L : OddLine (CategoryTheory.Ind C)) (𝔸 : CategoryTheory.Ind C) [CategoryTheory.MonObj 𝔸] [CategoryTheory.IsCommMonObj 𝔸] (hsec : ∀ (S : CategoryTheory.ShortComplex C), S.ShortExact → ∃ (s : freeMod 𝔸 (S.map indOf).X₃ ⟶ freeMod 𝔸 (S.map indOf).X₂), CategoryTheory.CategoryStruct.comp s (freeModMap 𝔸 (S.map indOf).g) = CategoryTheory.CategoryStruct.id (freeMod 𝔸 (S.map indOf).X₃)) : CategoryTheory.Limits.PreservesFiniteLimits (indOf.comp (fibreFun L 𝔸))

The restricted fibre functor preserves finite limits over an algebra that supplies a base-change section for every embedded short exact sequence.

theorem RS.indFibre_preservesFiniteColimits {C : Type v} [CategoryTheory.SmallCategory C] [CategoryTheory.MonoidalCategory C] [CategoryTheory.Abelian C] [CategoryTheory.MonoidalPreadditive C] [CategoryTheory.RigidCategory C] [CategoryTheory.Linear ℂ (CategoryTheory.Ind C)] [CategoryTheory.MonoidalPreadditive (CategoryTheory.Ind C)] [CategoryTheory.MonoidalLinear ℂ (CategoryTheory.Ind C)] [CategoryTheory.SymmetricCategory (CategoryTheory.Ind C)] (L : OddLine (CategoryTheory.Ind C)) (𝔸 : CategoryTheory.Ind C) [CategoryTheory.MonObj 𝔸] [CategoryTheory.IsCommMonObj 𝔸] (hsec : ∀ (S : CategoryTheory.ShortComplex C), S.ShortExact → ∃ (s : freeMod 𝔸 (S.map indOf).X₃ ⟶ freeMod 𝔸 (S.map indOf).X₂), CategoryTheory.CategoryStruct.comp s (freeModMap 𝔸 (S.map indOf).g) = CategoryTheory.CategoryStruct.id (freeMod 𝔸 (S.map indOf).X₃)) : CategoryTheory.Limits.PreservesFiniteColimits (indOf.comp (fibreFun L 𝔸))

The restricted fibre functor preserves finite colimits under the same hypothesis; with the previous statement it is exact.