The unit comparison of the fibre functor

The free module of the tensor unit is the regular module, whose realization is the Γ-algebra viewed over itself, that is, the unit of the tensor product of super modules. The unit comparison of the fibre functor is therefore an isomorphism outright, and on the two components it is composition with the inverse right unitor of the algebra.

noncomputable def RS.fibreEpsIso {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] : (gammaAlgebra D L R).unitMod ≅ gammaModule D L R (freeMod R (CategoryTheory.MonoidalCategoryStruct.tensorUnit D)).X

The unit comparison of the fibre functor.

Equations

• RS.fibreEpsIso L R = ((RS.gammaModuleFunctor L R).mapIso (RS.freeModUnitIso R)).symm

@[reducible, inline]

noncomputable abbrev RS.fibreEps {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] : (gammaAlgebra D L R).unitMod ⟶ gammaModule D L R (freeMod R (CategoryTheory.MonoidalCategoryStruct.tensorUnit D)).X

The unit comparison, as a morphism.

Equations

• RS.fibreEps L R = (RS.fibreEpsIso L R).hom

@[simp]

theorem RS.fibreEps_evenMap {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] (x : CategoryTheory.MonoidalCategoryStruct.tensorUnit D ⟶ R) : (fibreEps L R).evenMap x = CategoryTheory.CategoryStruct.comp x (CategoryTheory.MonoidalCategoryStruct.rightUnitor R).inv

The unit comparison on the even component: composition with the inverse right unitor of the algebra.

@[simp]

theorem RS.fibreEps_oddMap {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] (u : L.obj ⟶ R) : (fibreEps L R).oddMap u = CategoryTheory.CategoryStruct.comp u (CategoryTheory.MonoidalCategoryStruct.rightUnitor R).inv

The unit comparison on the odd component: composition with the inverse right unitor of the algebra.

instance RS.instIsIsoModGammaAlgebraFibreEps {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.IsIso (fibreEps L R)