The unit of a big tensor product survives #
If the tensor of two nonzero points is nonzero, then a finite tensor product of algebras with nonvanishing units again has a nonvanishing unit, by induction on the slots. The unit of the whole family is the unit of any finite stage followed by the stage inclusion, so it survives as soon as the unit of the ambient category can be tested against the filtered colimit one stage at a time.
theorem
RS.listTensor_one_ne_zero
{D : Type u}
[CategoryTheory.Category.{v, u} D]
[CategoryTheory.MonoidalCategory D]
[CategoryTheory.BraidedCategory D]
[CategoryTheory.Preadditive D]
{ι : Type v}
(B : ι → D)
[(i : ι) → CategoryTheory.MonObj (B i)]
(h1 : CategoryTheory.CategoryStruct.id (CategoryTheory.MonoidalCategoryStruct.tensorUnit D) ≠ 0)
(hbin :
∀ {M N : D} (u : CategoryTheory.MonoidalCategoryStruct.tensorUnit D ⟶ M)
(v : CategoryTheory.MonoidalCategoryStruct.tensorUnit D ⟶ N),
u ≠ 0 → v ≠ 0 → CategoryTheory.MonoidalCategoryStruct.tensorHom u v ≠ 0)
(hB : ∀ (i : ι), CategoryTheory.MonObj.one ≠ 0)
(l : List ι)
:
The unit of a finite fold survives: the unit of a tensor product of monoid objects is the tensor of their units, so it is nonzero as soon as the binary statement holds.
theorem
RS.finTensor_one_ne_zero
{D : Type u}
[CategoryTheory.Category.{v, u} D]
[CategoryTheory.MonoidalCategory D]
[CategoryTheory.BraidedCategory D]
[CategoryTheory.Preadditive D]
{ι : Type v}
(B : ι → D)
[(i : ι) → CategoryTheory.MonObj (B i)]
[LinearOrder ι]
(h1 : CategoryTheory.CategoryStruct.id (CategoryTheory.MonoidalCategoryStruct.tensorUnit D) ≠ 0)
(hbin :
∀ {M N : D} (u : CategoryTheory.MonoidalCategoryStruct.tensorUnit D ⟶ M)
(v : CategoryTheory.MonoidalCategoryStruct.tensorUnit D ⟶ N),
u ≠ 0 → v ≠ 0 → CategoryTheory.MonoidalCategoryStruct.tensorHom u v ≠ 0)
(hB : ∀ (i : ι), CategoryTheory.MonObj.one ≠ 0)
(s : Finset ι)
:
The unit of a finite sub-tensor-product survives.
theorem
RS.bigTensorUnit_ne_zero
{D : Type u}
[CategoryTheory.Category.{v, u} D]
[CategoryTheory.MonoidalCategory D]
[CategoryTheory.BraidedCategory D]
[CategoryTheory.Preadditive D]
{ι : Type v}
(B : ι → D)
[(i : ι) → CategoryTheory.MonObj (B i)]
[LinearOrder ι]
[CategoryTheory.Limits.HasColimitsOfShape (Finset ι) D]
(h1 : CategoryTheory.CategoryStruct.id (CategoryTheory.MonoidalCategoryStruct.tensorUnit D) ≠ 0)
(hbin :
∀ {M N : D} (u : CategoryTheory.MonoidalCategoryStruct.tensorUnit D ⟶ M)
(v : CategoryTheory.MonoidalCategoryStruct.tensorUnit D ⟶ N),
u ≠ 0 → v ≠ 0 → CategoryTheory.MonoidalCategoryStruct.tensorHom u v ≠ 0)
(hB : ∀ (i : ι), CategoryTheory.MonObj.one ≠ 0)
(hstage :
∀ (s : Finset ι) (f : CategoryTheory.MonoidalCategoryStruct.tensorUnit D ⟶ finTensor B s),
CategoryTheory.CategoryStruct.comp f (bigTensorStage B s) = 0 →
∃ (t : Finset ι) (h : s ⊆ t), CategoryTheory.CategoryStruct.comp f (finTensorIncl B h) = 0)
:
The unit of the big tensor product survives, given that a point of the colimit vanishes only if it already vanishes at a later stage.