A common extension of a family of algebras

Any small family of nonzero commutative algebras of the ind-completion sits inside a single nonzero commutative algebra: their tensor product. This is the device of Deligne 2.11, which uses it to make every object mixed and every short exact sequence split simultaneously.

The index type is put in bijection with a well-ordered one so that the slot order required by the tensor product is available.

theorem RS.exists_common_algebra {C : Type v} [CategoryTheory.SmallCategory C] [CategoryTheory.MonoidalCategory C] [CategoryTheory.Abelian C] [CategoryTheory.Linear ℂ C] [CategoryTheory.MonoidalPreadditive C] [CategoryTheory.RigidCategory C] [CategoryTheory.SymmetricCategory (CategoryTheory.Ind C)] (hu : HasScalarUnit C) {ι : Type v} (B : ι → CategoryTheory.Ind C) [(i : ι) → CategoryTheory.MonObj (B i)] [∀ (i : ι), CategoryTheory.IsCommMonObj (B i)] (hB : ∀ (i : ι), CategoryTheory.MonObj.one ≠ 0) : ∃ (𝔸 : CategoryTheory.Ind C) (x : CategoryTheory.MonObj 𝔸) (_ : CategoryTheory.IsCommMonObj 𝔸), CategoryTheory.MonObj.one ≠ 0 ∧ ∀ (i : ι), ∃ (φ : B i ⟶ 𝔸), CategoryTheory.IsMonHom φ

A family of nonzero algebras has a common nonzero extension: their tensor product, into which each factor maps by a morphism of monoid objects.