The fibre functor is complex-linear

The fibre functor is built by whiskering with the algebra and composing, and both operations are complex-linear, so the functor is. This is the last field of RS.DeligneFibreFunctor that the fibre construction does not supply on its own.

instance RS.fibreFun_linear {D : Type u} [CategoryTheory.Category.{v, u} D] [CategoryTheory.MonoidalCategory D] [CategoryTheory.SymmetricCategory D] [CategoryTheory.Preadditive D] [CategoryTheory.MonoidalPreadditive D] [CategoryTheory.Linear ℂ D] [CategoryTheory.MonoidalLinear ℂ D] (L : OddLine D) (R : D) [CategoryTheory.MonObj R] [CategoryTheory.IsCommMonObj R] : CategoryTheory.Functor.Linear ℂ (fibreFun L R)

The fibre functor is complex-linear.