The two presentations of the fibre functor agree

Base change followed by realization was built twice: once directly, so that additivity could be proved without an additive structure on the module objects, and once as a composite, so that the monoidal comparison could be read off. The two are the same functor.

theorem RS.fibreFun_eq_fibreOver {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] : fibreFun L R = fibreOver L R

The direct and composite presentations of the fibre functor agree.

instance RS.fibreOver_additive {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] : (fibreOver L R).Additive

The composite presentation is additive.