Points tensor without vanishing in the ind-completion

RS.Classical.Deligne.PointTensor proves, in an abelian ℂ-linear rigid monoidal category with scalar unit, that the tensor of two nonzero points of the unit is nonzero. This file carries that statement across the embedding C ⥤ Ind C to the whole ind-completion — the fact Deligne asserts in 2.11 when he says the algebra 𝔸 is not zero, since the unit of a tensor product of algebras is (λ_ _).inv ≫ (η ⊗ₘ η).

The route is compactness, applied twice.

• RS.indOfTensorIso_hom_natural — the embedding-tensor comparison is natural in both variables at once, assembled from the two one-variable naturalities of RS.Classical.Deligne.IndTensorExact;
• RS.exists_indOf_point — a point of an embedded object is the embedding of a point downstairs, and vanishes only if that one does (RS.indOfUnitIso and RS.indOf_map_eq_zero_iff);
• RS.indTensorHom_point_ne_zero_indOf — the statement for two embedded objects, obtained by conjugating with the unit comparison RS.indOfUnitIso and the embedding-tensor comparison and appealing to RS.tensorHom_point_ne_zero downstairs;
• RS.tensor_unit_point_stage_left/_right — the finite-stage engine: if the tensor of a point with a point of a filtered colimit vanishes, it already vanishes at some stage of the diagram. Tensoring preserves filtered colimits (RS.tensorLeft_ind_preservesFilteredColimits) and the unit of Ind C is compact (RS.unit_colimit_eq_zero_iff);
• RS.indTensorHom_point_ne_zero_indOf_left — one embedded factor and one arbitrary, by presenting the second factor as a filtered colimit of embedded objects;
• RS.indTensorHom_point_ne_zero — both factors arbitrary, by the same descent in the first factor.

The filtered-colimit presentations are Mathlib's: Ind.presentation and Ind.colimitPresentationCompYoneda exhibit every ind-object as the colimit of X.presentation.F ⋙ Ind.yoneda over the filtered index category X.presentation.I.

Transport of a vanishing composite along a preserved colimit

theorem RS.comp_ι_comp_eq_zero {𝒜 : Type u} [CategoryTheory.Category.{v, u} 𝒜] [CategoryTheory.Limits.HasZeroMorphisms 𝒜] {I : Type v} [CategoryTheory.SmallCategory I] (D : CategoryTheory.Functor I 𝒜) [CategoryTheory.Limits.HasColimit D] (F : CategoryTheory.Functor 𝒜 𝒜) [CategoryTheory.Limits.PreservesColimit D F] {i : I} {W : 𝒜} (w : W ⟶ F.obj (D.obj i)) (h : CategoryTheory.CategoryStruct.comp w (F.map (CategoryTheory.Limits.colimit.ι D i)) = 0) : CategoryTheory.CategoryStruct.comp w (CategoryTheory.Limits.colimit.ι (D.comp F) i) = 0

If a morphism into the image of a stage dies against the image of a colimit injection, it dies against the colimit injection of the transported diagram. Stated with the domain written as F.obj (D.obj i) so that every composite below is type-correct without unfolding Functor.comp.

The embedding-tensor comparison in both variables

theorem RS.indOfTensorIso_hom_natural {C : Type v} [CategoryTheory.SmallCategory C] [CategoryTheory.MonoidalCategory C] {x x' y y' : C} (f : x ⟶ x') (g : y ⟶ y') : CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.tensorHom (indOf.map f) (indOf.map g)) (indOfTensorIso x' y').hom = CategoryTheory.CategoryStruct.comp (indOfTensorIso x y).hom (indOf.map (CategoryTheory.MonoidalCategoryStruct.tensorHom f g))

Naturality of the embedding-tensor comparison in both variables at once: RS.indOfTensorIso intertwines the tensor of two embedded morphisms with the embedding of their tensor. The two one-variable naturalities compose along MonoidalCategory.tensorHom_def.

Both factors embedded

theorem RS.exists_indOf_point {C : Type v} [CategoryTheory.SmallCategory C] [CategoryTheory.MonoidalCategory C] [CategoryTheory.Abelian C] {X : C} (u : CategoryTheory.MonoidalCategoryStruct.tensorUnit (CategoryTheory.Ind C) ⟶ indOf.obj X) : ∃ (u₀ : CategoryTheory.MonoidalCategoryStruct.tensorUnit C ⟶ X), indOf.map u₀ = CategoryTheory.CategoryStruct.comp indOfUnitIso.inv u ∧ (u ≠ 0 → u₀ ≠ 0)

A point of an embedded object comes from downstairs: read through the unit comparison RS.indOfUnitIso, it is the embedding of a point of the object in C, and that point is nonzero whenever the original is.

theorem RS.indTensorHom_point_ne_zero_indOf {C : Type v} [CategoryTheory.SmallCategory C] [CategoryTheory.MonoidalCategory C] [CategoryTheory.Abelian C] [CategoryTheory.Linear ℂ C] [CategoryTheory.MonoidalPreadditive C] [CategoryTheory.RigidCategory C] (hu : HasScalarUnit C) {X Y : C} {u : CategoryTheory.MonoidalCategoryStruct.tensorUnit (CategoryTheory.Ind C) ⟶ indOf.obj X} {v : CategoryTheory.MonoidalCategoryStruct.tensorUnit (CategoryTheory.Ind C) ⟶ indOf.obj Y} (hu0 : u ≠ 0) (hv0 : v ≠ 0) : CategoryTheory.MonoidalCategoryStruct.tensorHom u v ≠ 0

The tensor of two nonzero points of embedded objects is nonzero: the unit comparison and the embedding-tensor comparison identify it with the embedding of the corresponding tensor downstairs, which is nonzero by RS.tensorHom_point_ne_zero.

The finite-stage engine

theorem RS.tensor_unit_point_stage_left {C : Type v} [CategoryTheory.SmallCategory C] [CategoryTheory.MonoidalCategory C] [CategoryTheory.Abelian C] {I : Type v} [CategoryTheory.SmallCategory I] [CategoryTheory.IsFiltered I] (D : CategoryTheory.Functor I (CategoryTheory.Ind C)) (M : CategoryTheory.Ind C) {i : I} (u : CategoryTheory.MonoidalCategoryStruct.tensorUnit (CategoryTheory.Ind C) ⟶ M) (g : CategoryTheory.MonoidalCategoryStruct.tensorUnit (CategoryTheory.Ind C) ⟶ D.obj i) (h : CategoryTheory.MonoidalCategoryStruct.tensorHom u (CategoryTheory.CategoryStruct.comp g (CategoryTheory.Limits.colimit.ι D i)) = 0) : ∃ (k : I) (α : i ⟶ k), CategoryTheory.MonoidalCategoryStruct.tensorHom u (CategoryTheory.CategoryStruct.comp g (D.map α)) = 0

Vanishing at a stage, second factor: if the tensor of a point of M with a point of a filtered colimit that factors through the stage i vanishes, then it already vanishes after some transition map out of i. Tensoring on the left preserves the filtered colimit, and the unit of Ind C is compact.

theorem RS.tensor_unit_point_stage_right {C : Type v} [CategoryTheory.SmallCategory C] [CategoryTheory.MonoidalCategory C] [CategoryTheory.Abelian C] {I : Type v} [CategoryTheory.SmallCategory I] [CategoryTheory.IsFiltered I] (D : CategoryTheory.Functor I (CategoryTheory.Ind C)) (N : CategoryTheory.Ind C) {i : I} (f : CategoryTheory.MonoidalCategoryStruct.tensorUnit (CategoryTheory.Ind C) ⟶ D.obj i) (v : CategoryTheory.MonoidalCategoryStruct.tensorUnit (CategoryTheory.Ind C) ⟶ N) (h : CategoryTheory.MonoidalCategoryStruct.tensorHom (CategoryTheory.CategoryStruct.comp f (CategoryTheory.Limits.colimit.ι D i)) v = 0) : ∃ (k : I) (α : i ⟶ k), CategoryTheory.MonoidalCategoryStruct.tensorHom (CategoryTheory.CategoryStruct.comp f (D.map α)) v = 0

Vanishing at a stage, first factor: the mirror image of RS.tensor_unit_point_stage_left, using that tensoring on the right preserves filtered colimits.

The general statement

theorem RS.indTensorHom_point_ne_zero_indOf_left {C : Type v} [CategoryTheory.SmallCategory C] [CategoryTheory.MonoidalCategory C] [CategoryTheory.Abelian C] [CategoryTheory.Linear ℂ C] [CategoryTheory.MonoidalPreadditive C] [CategoryTheory.RigidCategory C] (hu : HasScalarUnit C) {X : C} {N : CategoryTheory.Ind C} {u : CategoryTheory.MonoidalCategoryStruct.tensorUnit (CategoryTheory.Ind C) ⟶ indOf.obj X} {v : CategoryTheory.MonoidalCategoryStruct.tensorUnit (CategoryTheory.Ind C) ⟶ N} (hu0 : u ≠ 0) (hv0 : v ≠ 0) : CategoryTheory.MonoidalCategoryStruct.tensorHom u v ≠ 0

One embedded factor: the tensor of a nonzero point of an embedded object with a nonzero point of an arbitrary ind-object is nonzero. Present the second factor as a filtered colimit of embedded objects, factor the point through a stage, and use that a vanishing tensor vanishes at a stage.

theorem RS.indTensorHom_point_ne_zero {C : Type v} [CategoryTheory.SmallCategory C] [CategoryTheory.MonoidalCategory C] [CategoryTheory.Abelian C] [CategoryTheory.Linear ℂ C] [CategoryTheory.MonoidalPreadditive C] [CategoryTheory.RigidCategory C] (hu : HasScalarUnit C) {M N : CategoryTheory.Ind C} {u : CategoryTheory.MonoidalCategoryStruct.tensorUnit (CategoryTheory.Ind C) ⟶ M} {v : CategoryTheory.MonoidalCategoryStruct.tensorUnit (CategoryTheory.Ind C) ⟶ N} (hu0 : u ≠ 0) (hv0 : v ≠ 0) : CategoryTheory.MonoidalCategoryStruct.tensorHom u v ≠ 0

The tensor of two nonzero points of the ind-completion is nonzero (Deligne 2.11, the nonvanishing of the algebra 𝔸). Present the first factor as a filtered colimit of embedded objects, factor the point through a stage, and appeal to RS.indTensorHom_point_ne_zero_indOf_left.