The fibre functor is faithful #
A free module on an object that becomes a mixed sum is generated, as a module, by finitely many morphisms out of the unit and out of the odd line. So a morphism killed by the fibre functor is killed after base change; and if the unit of the algebra is a monomorphism that is enough to kill the morphism itself.
theorem
RS.whiskerLeft_eq_zero_of_fibre
{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]
[CategoryTheory.Limits.HasFiniteBiproducts D]
(L : OddLine D)
(R : D)
[CategoryTheory.MonObj R]
[CategoryTheory.IsCommMonObj R]
{V W : D}
(fm : V ⟶ W)
{p q : ℕ}
(e : freeMod R V ≅ freeMod R (L.mix p q))
(h : (fibreFun L R).map fm = 0)
:
A morphism killed by the fibre functor is killed by base change.
theorem
RS.eq_zero_of_whiskerLeft
{D : Type u}
[CategoryTheory.Category.{v, u} D]
[CategoryTheory.MonoidalCategory D]
[CategoryTheory.Preadditive D]
(R : D)
[CategoryTheory.MonObj R]
[∀ (Z : D), (CategoryTheory.MonoidalCategory.tensorRight Z).PreservesMonomorphisms]
(hη : CategoryTheory.Mono CategoryTheory.MonObj.one)
{V W : D}
(fm : V ⟶ W)
(h : CategoryTheory.MonoidalCategoryStruct.whiskerLeft R fm = 0)
:
Base change is faithful when the unit is a monomorphism.
theorem
RS.fibreFun_map_eq_zero
{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]
[CategoryTheory.Limits.HasFiniteBiproducts D]
(L : OddLine D)
(R : D)
[CategoryTheory.MonObj R]
[CategoryTheory.IsCommMonObj R]
[∀ (Z : D), (CategoryTheory.MonoidalCategory.tensorRight Z).PreservesMonomorphisms]
(hη : CategoryTheory.Mono CategoryTheory.MonObj.one)
{V W : D}
(fm : V ⟶ W)
{p q : ℕ}
(e : freeMod R V ≅ freeMod R (L.mix p q))
(h : (fibreFun L R).map fm = 0)
:
The fibre functor is faithful on the objects that become mixed sums.