Direct sums of curved duplexes

The componentwise biproduct of two curved duplexes has the same curvature. Its differentials are the direct sums of the original differentials. The componentwise projections exhibit this object as the categorical binary product; preadditivity makes it a biproduct. In particular, finite-projective matrix factorizations inherit these sums.

noncomputable def TauCeti.CurvedDuplex.biprod {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] {R : Type w} [Semiring R] [CategoryTheory.Linear R C] [CategoryTheory.Limits.HasBinaryBiproducts C] {w₀ : R} (X Y : CurvedDuplex C w₀) : CurvedDuplex C w₀

The componentwise direct sum of two curved duplexes with the same curvature.

Equations

• X.biprod Y = { X₀ := X.X₀ ⊞ Y.X₀, X₁ := X.X₁ ⊞ Y.X₁, d₀ := CategoryTheory.Limits.biprod.map X.d₀ Y.d₀, d₁ := CategoryTheory.Limits.biprod.map X.d₁ Y.d₁, d₀_comp_d₁ := ⋯, d₁_comp_d₀ := ⋯ }

@[simp]

theorem TauCeti.CurvedDuplex.biprod_X₀ {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] {R : Type w} [Semiring R] [CategoryTheory.Linear R C] [CategoryTheory.Limits.HasBinaryBiproducts C] {w₀ : R} (X Y : CurvedDuplex C w₀) : (X.biprod Y).X₀ = (X.X₀ ⊞ Y.X₀)

@[simp]

theorem TauCeti.CurvedDuplex.biprod_X₁ {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] {R : Type w} [Semiring R] [CategoryTheory.Linear R C] [CategoryTheory.Limits.HasBinaryBiproducts C] {w₀ : R} (X Y : CurvedDuplex C w₀) : (X.biprod Y).X₁ = (X.X₁ ⊞ Y.X₁)

@[simp]

theorem TauCeti.CurvedDuplex.biprod_d₀ {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] {R : Type w} [Semiring R] [CategoryTheory.Linear R C] [CategoryTheory.Limits.HasBinaryBiproducts C] {w₀ : R} (X Y : CurvedDuplex C w₀) : (X.biprod Y).d₀ = CategoryTheory.Limits.biprod.map X.d₀ Y.d₀

@[simp]

theorem TauCeti.CurvedDuplex.biprod_d₁ {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] {R : Type w} [Semiring R] [CategoryTheory.Linear R C] [CategoryTheory.Limits.HasBinaryBiproducts C] {w₀ : R} (X Y : CurvedDuplex C w₀) : (X.biprod Y).d₁ = CategoryTheory.Limits.biprod.map X.d₁ Y.d₁

noncomputable def TauCeti.CurvedDuplex.biprodFst {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] {R : Type w} [Semiring R] [CategoryTheory.Linear R C] [CategoryTheory.Limits.HasBinaryBiproducts C] {w₀ : R} (X Y : CurvedDuplex C w₀) : X.biprod Y ⟶ X

Projection to the first curved duplex.

Equations

• X.biprodFst Y = { f₀ := CategoryTheory.Limits.biprod.fst, f₁ := CategoryTheory.Limits.biprod.fst, comm₀ := ⋯, comm₁ := ⋯ }

noncomputable def TauCeti.CurvedDuplex.biprodSnd {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] {R : Type w} [Semiring R] [CategoryTheory.Linear R C] [CategoryTheory.Limits.HasBinaryBiproducts C] {w₀ : R} (X Y : CurvedDuplex C w₀) : X.biprod Y ⟶ Y

Projection to the second curved duplex.

Equations

• X.biprodSnd Y = { f₀ := CategoryTheory.Limits.biprod.snd, f₁ := CategoryTheory.Limits.biprod.snd, comm₀ := ⋯, comm₁ := ⋯ }

noncomputable def TauCeti.CurvedDuplex.biprodLift {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] {R : Type w} [Semiring R] [CategoryTheory.Linear R C] [CategoryTheory.Limits.HasBinaryBiproducts C] {w₀ : R} {Z X Y : CurvedDuplex C w₀} (f : Z ⟶ X) (g : Z ⟶ Y) : Z ⟶ X.biprod Y

A pair of maps into curved duplexes induces a map into their direct sum.

Equations

• TauCeti.CurvedDuplex.biprodLift f g = { f₀ := CategoryTheory.Limits.biprod.lift f.f₀ g.f₀, f₁ := CategoryTheory.Limits.biprod.lift f.f₁ g.f₁, comm₀ := ⋯, comm₁ := ⋯ }

@[simp]

theorem TauCeti.CurvedDuplex.biprodFst_f₀ {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] {R : Type w} [Semiring R] [CategoryTheory.Linear R C] [CategoryTheory.Limits.HasBinaryBiproducts C] {w₀ : R} (X Y : CurvedDuplex C w₀) : (X.biprodFst Y).f₀ = CategoryTheory.Limits.biprod.fst

@[simp]

theorem TauCeti.CurvedDuplex.biprodFst_f₁ {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] {R : Type w} [Semiring R] [CategoryTheory.Linear R C] [CategoryTheory.Limits.HasBinaryBiproducts C] {w₀ : R} (X Y : CurvedDuplex C w₀) : (X.biprodFst Y).f₁ = CategoryTheory.Limits.biprod.fst

@[simp]

theorem TauCeti.CurvedDuplex.biprodSnd_f₀ {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] {R : Type w} [Semiring R] [CategoryTheory.Linear R C] [CategoryTheory.Limits.HasBinaryBiproducts C] {w₀ : R} (X Y : CurvedDuplex C w₀) : (X.biprodSnd Y).f₀ = CategoryTheory.Limits.biprod.snd

@[simp]

theorem TauCeti.CurvedDuplex.biprodSnd_f₁ {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] {R : Type w} [Semiring R] [CategoryTheory.Linear R C] [CategoryTheory.Limits.HasBinaryBiproducts C] {w₀ : R} (X Y : CurvedDuplex C w₀) : (X.biprodSnd Y).f₁ = CategoryTheory.Limits.biprod.snd

@[simp]

theorem TauCeti.CurvedDuplex.biprodLift_f₀ {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] {R : Type w} [Semiring R] [CategoryTheory.Linear R C] [CategoryTheory.Limits.HasBinaryBiproducts C] {w₀ : R} {Z X Y : CurvedDuplex C w₀} (f : Z ⟶ X) (g : Z ⟶ Y) : (biprodLift f g).f₀ = CategoryTheory.Limits.biprod.lift f.f₀ g.f₀

@[simp]

theorem TauCeti.CurvedDuplex.biprodLift_f₁ {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] {R : Type w} [Semiring R] [CategoryTheory.Linear R C] [CategoryTheory.Limits.HasBinaryBiproducts C] {w₀ : R} {Z X Y : CurvedDuplex C w₀} (f : Z ⟶ X) (g : Z ⟶ Y) : (biprodLift f g).f₁ = CategoryTheory.Limits.biprod.lift f.f₁ g.f₁

@[simp]

theorem TauCeti.CurvedDuplex.biprodLift_fst {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] {R : Type w} [Semiring R] [CategoryTheory.Linear R C] [CategoryTheory.Limits.HasBinaryBiproducts C] {w₀ : R} {Z X Y : CurvedDuplex C w₀} (f : Z ⟶ X) (g : Z ⟶ Y) : CategoryTheory.CategoryStruct.comp (biprodLift f g) (X.biprodFst Y) = f

@[simp]

theorem TauCeti.CurvedDuplex.biprodLift_snd {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] {R : Type w} [Semiring R] [CategoryTheory.Linear R C] [CategoryTheory.Limits.HasBinaryBiproducts C] {w₀ : R} {Z X Y : CurvedDuplex C w₀} (f : Z ⟶ X) (g : Z ⟶ Y) : CategoryTheory.CategoryStruct.comp (biprodLift f g) (X.biprodSnd Y) = g

theorem TauCeti.CurvedDuplex.biprod_hom_ext {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] {R : Type w} [Semiring R] [CategoryTheory.Linear R C] [CategoryTheory.Limits.HasBinaryBiproducts C] {w₀ : R} {Z X Y : CurvedDuplex C w₀} {f g : Z ⟶ X.biprod Y} (h₀ : CategoryTheory.CategoryStruct.comp f (X.biprodFst Y) = CategoryTheory.CategoryStruct.comp g (X.biprodFst Y)) (h₁ : CategoryTheory.CategoryStruct.comp f (X.biprodSnd Y) = CategoryTheory.CategoryStruct.comp g (X.biprodSnd Y)) : f = g

Maps into a direct sum are determined by their projections.

noncomputable def TauCeti.CurvedDuplex.biprodInl {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] {R : Type w} [Semiring R] [CategoryTheory.Linear R C] [CategoryTheory.Limits.HasBinaryBiproducts C] {w₀ : R} (X Y : CurvedDuplex C w₀) : X ⟶ X.biprod Y

Inclusion of the first curved duplex into the componentwise direct sum.

Equations

• X.biprodInl Y = { f₀ := CategoryTheory.Limits.biprod.inl, f₁ := CategoryTheory.Limits.biprod.inl, comm₀ := ⋯, comm₁ := ⋯ }

noncomputable def TauCeti.CurvedDuplex.biprodInr {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] {R : Type w} [Semiring R] [CategoryTheory.Linear R C] [CategoryTheory.Limits.HasBinaryBiproducts C] {w₀ : R} (X Y : CurvedDuplex C w₀) : Y ⟶ X.biprod Y

Inclusion of the second curved duplex into the componentwise direct sum.

Equations

• X.biprodInr Y = { f₀ := CategoryTheory.Limits.biprod.inr, f₁ := CategoryTheory.Limits.biprod.inr, comm₀ := ⋯, comm₁ := ⋯ }

noncomputable def TauCeti.CurvedDuplex.biprodDesc {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] {R : Type w} [Semiring R] [CategoryTheory.Linear R C] [CategoryTheory.Limits.HasBinaryBiproducts C] {w₀ : R} {X Y Z : CurvedDuplex C w₀} (f : X ⟶ Z) (g : Y ⟶ Z) : X.biprod Y ⟶ Z

Maps out of both summands induce a map out of their direct sum.

Equations

• TauCeti.CurvedDuplex.biprodDesc f g = { f₀ := CategoryTheory.Limits.biprod.desc f.f₀ g.f₀, f₁ := CategoryTheory.Limits.biprod.desc f.f₁ g.f₁, comm₀ := ⋯, comm₁ := ⋯ }

@[simp]

theorem TauCeti.CurvedDuplex.biprodInl_f₀ {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] {R : Type w} [Semiring R] [CategoryTheory.Linear R C] [CategoryTheory.Limits.HasBinaryBiproducts C] {w₀ : R} (X Y : CurvedDuplex C w₀) : (X.biprodInl Y).f₀ = CategoryTheory.Limits.biprod.inl

@[simp]

theorem TauCeti.CurvedDuplex.biprodInl_f₁ {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] {R : Type w} [Semiring R] [CategoryTheory.Linear R C] [CategoryTheory.Limits.HasBinaryBiproducts C] {w₀ : R} (X Y : CurvedDuplex C w₀) : (X.biprodInl Y).f₁ = CategoryTheory.Limits.biprod.inl

@[simp]

theorem TauCeti.CurvedDuplex.biprodInr_f₀ {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] {R : Type w} [Semiring R] [CategoryTheory.Linear R C] [CategoryTheory.Limits.HasBinaryBiproducts C] {w₀ : R} (X Y : CurvedDuplex C w₀) : (X.biprodInr Y).f₀ = CategoryTheory.Limits.biprod.inr

@[simp]

theorem TauCeti.CurvedDuplex.biprodInr_f₁ {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] {R : Type w} [Semiring R] [CategoryTheory.Linear R C] [CategoryTheory.Limits.HasBinaryBiproducts C] {w₀ : R} (X Y : CurvedDuplex C w₀) : (X.biprodInr Y).f₁ = CategoryTheory.Limits.biprod.inr

@[simp]

theorem TauCeti.CurvedDuplex.biprodDesc_f₀ {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] {R : Type w} [Semiring R] [CategoryTheory.Linear R C] [CategoryTheory.Limits.HasBinaryBiproducts C] {w₀ : R} {X Y Z : CurvedDuplex C w₀} (f : X ⟶ Z) (g : Y ⟶ Z) : (biprodDesc f g).f₀ = CategoryTheory.Limits.biprod.desc f.f₀ g.f₀

@[simp]

theorem TauCeti.CurvedDuplex.biprodDesc_f₁ {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] {R : Type w} [Semiring R] [CategoryTheory.Linear R C] [CategoryTheory.Limits.HasBinaryBiproducts C] {w₀ : R} {X Y Z : CurvedDuplex C w₀} (f : X ⟶ Z) (g : Y ⟶ Z) : (biprodDesc f g).f₁ = CategoryTheory.Limits.biprod.desc f.f₁ g.f₁

@[simp]

theorem TauCeti.CurvedDuplex.biprodInl_desc {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] {R : Type w} [Semiring R] [CategoryTheory.Linear R C] [CategoryTheory.Limits.HasBinaryBiproducts C] {w₀ : R} {X Y Z : CurvedDuplex C w₀} (f : X ⟶ Z) (g : Y ⟶ Z) : CategoryTheory.CategoryStruct.comp (X.biprodInl Y) (biprodDesc f g) = f

@[simp]

theorem TauCeti.CurvedDuplex.biprodInr_desc {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] {R : Type w} [Semiring R] [CategoryTheory.Linear R C] [CategoryTheory.Limits.HasBinaryBiproducts C] {w₀ : R} {X Y Z : CurvedDuplex C w₀} (f : X ⟶ Z) (g : Y ⟶ Z) : CategoryTheory.CategoryStruct.comp (X.biprodInr Y) (biprodDesc f g) = g

@[simp]

theorem TauCeti.CurvedDuplex.biprodInl_fst {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] {R : Type w} [Semiring R] [CategoryTheory.Linear R C] [CategoryTheory.Limits.HasBinaryBiproducts C] {w₀ : R} (X Y : CurvedDuplex C w₀) : CategoryTheory.CategoryStruct.comp (X.biprodInl Y) (X.biprodFst Y) = CategoryTheory.CategoryStruct.id X

@[simp]

theorem TauCeti.CurvedDuplex.biprodInl_snd {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] {R : Type w} [Semiring R] [CategoryTheory.Linear R C] [CategoryTheory.Limits.HasBinaryBiproducts C] {w₀ : R} (X Y : CurvedDuplex C w₀) : CategoryTheory.CategoryStruct.comp (X.biprodInl Y) (X.biprodSnd Y) = 0

@[simp]

theorem TauCeti.CurvedDuplex.biprodInr_fst {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] {R : Type w} [Semiring R] [CategoryTheory.Linear R C] [CategoryTheory.Limits.HasBinaryBiproducts C] {w₀ : R} (X Y : CurvedDuplex C w₀) : CategoryTheory.CategoryStruct.comp (X.biprodInr Y) (X.biprodFst Y) = 0

@[simp]

theorem TauCeti.CurvedDuplex.biprodInr_snd {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] {R : Type w} [Semiring R] [CategoryTheory.Linear R C] [CategoryTheory.Limits.HasBinaryBiproducts C] {w₀ : R} (X Y : CurvedDuplex C w₀) : CategoryTheory.CategoryStruct.comp (X.biprodInr Y) (X.biprodSnd Y) = CategoryTheory.CategoryStruct.id Y

theorem TauCeti.CurvedDuplex.biprod_hom_ext' {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] {R : Type w} [Semiring R] [CategoryTheory.Linear R C] [CategoryTheory.Limits.HasBinaryBiproducts C] {w₀ : R} {X Y Z : CurvedDuplex C w₀} {f g : X.biprod Y ⟶ Z} (h₀ : CategoryTheory.CategoryStruct.comp (X.biprodInl Y) f = CategoryTheory.CategoryStruct.comp (X.biprodInl Y) g) (h₁ : CategoryTheory.CategoryStruct.comp (X.biprodInr Y) f = CategoryTheory.CategoryStruct.comp (X.biprodInr Y) g) : f = g

Maps from a direct sum are determined by their restrictions to both summands.

instance TauCeti.CurvedDuplex.hasBinaryProduct {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] {R : Type w} [Semiring R] [CategoryTheory.Linear R C] [CategoryTheory.Limits.HasBinaryBiproducts C] {w₀ : R} (X Y : CurvedDuplex C w₀) : CategoryTheory.Limits.HasBinaryProduct X Y

Curved duplexes have componentwise binary products.

instance TauCeti.CurvedDuplex.hasBinaryProducts {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] {R : Type w} [Semiring R] [CategoryTheory.Linear R C] [CategoryTheory.Limits.HasBinaryBiproducts C] {w₀ : R} : CategoryTheory.Limits.HasBinaryProducts (CurvedDuplex C w₀)

Curved duplexes have componentwise binary products.

instance TauCeti.CurvedDuplex.hasBinaryBiproducts {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] {R : Type w} [Semiring R] [CategoryTheory.Linear R C] [CategoryTheory.Limits.HasBinaryBiproducts C] {w₀ : R} : CategoryTheory.Limits.HasBinaryBiproducts (CurvedDuplex C w₀)

Curved duplexes have binary biproducts.

theorem TauCeti.CurvedDuplex.isZero_of_components {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] {R : Type w} [Semiring R] [CategoryTheory.Linear R C] {w₀ : R} (X : CurvedDuplex C w₀) (h₀ : CategoryTheory.Limits.IsZero X.X₀) (h₁ : CategoryTheory.Limits.IsZero X.X₁) : CategoryTheory.Limits.IsZero X

A curved duplex with zero objects in both parities is a zero object.

noncomputable def TauCeti.CurvedDuplex.zero {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] {R : Type w} [Semiring R] [CategoryTheory.Linear R C] {w₀ : R} [CategoryTheory.Limits.HasZeroObject C] : CurvedDuplex C w₀

The curved duplex on two zero objects.

Equations

• TauCeti.CurvedDuplex.zero = { X₀ := 0, X₁ := 0, d₀ := 0, d₁ := 0, d₀_comp_d₁ := ⋯, d₁_comp_d₀ := ⋯ }

@[simp]

theorem TauCeti.CurvedDuplex.zero_X₀ {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] {R : Type w} [Semiring R] [CategoryTheory.Linear R C] {w₀ : R} [CategoryTheory.Limits.HasZeroObject C] : zero.X₀ = 0

@[simp]

theorem TauCeti.CurvedDuplex.zero_X₁ {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] {R : Type w} [Semiring R] [CategoryTheory.Linear R C] {w₀ : R} [CategoryTheory.Limits.HasZeroObject C] : zero.X₁ = 0

@[simp]

theorem TauCeti.CurvedDuplex.zero_d₀ {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] {R : Type w} [Semiring R] [CategoryTheory.Linear R C] {w₀ : R} [CategoryTheory.Limits.HasZeroObject C] : zero.d₀ = 0

@[simp]

theorem TauCeti.CurvedDuplex.zero_d₁ {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] {R : Type w} [Semiring R] [CategoryTheory.Linear R C] {w₀ : R} [CategoryTheory.Limits.HasZeroObject C] : zero.d₁ = 0

theorem TauCeti.CurvedDuplex.isZero_zero {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] {R : Type w} [Semiring R] [CategoryTheory.Linear R C] {w₀ : R} [CategoryTheory.Limits.HasZeroObject C] : CategoryTheory.Limits.IsZero zero

The zero curved duplex is both initial and terminal.

instance TauCeti.CurvedDuplex.hasZeroObject {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] {R : Type w} [Semiring R] [CategoryTheory.Linear R C] {w₀ : R} [CategoryTheory.Limits.HasZeroObject C] : CategoryTheory.Limits.HasZeroObject (CurvedDuplex C w₀)

Curved duplexes have a zero object whenever the base category does.

instance TauCeti.CurvedDuplex.hasFiniteProducts {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] {R : Type w} [Semiring R] [CategoryTheory.Linear R C] {w₀ : R} [CategoryTheory.Limits.HasZeroObject C] [CategoryTheory.Limits.HasBinaryBiproducts C] : CategoryTheory.Limits.HasFiniteProducts (CurvedDuplex C w₀)

Curved duplexes have finite products.

instance TauCeti.CurvedDuplex.hasFiniteBiproducts {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] {R : Type w} [Semiring R] [CategoryTheory.Linear R C] {w₀ : R} [CategoryTheory.Limits.HasZeroObject C] [CategoryTheory.Limits.HasBinaryBiproducts C] : CategoryTheory.Limits.HasFiniteBiproducts (CurvedDuplex C w₀)

Curved duplexes have finite biproducts.