The additive closure of a differential graded category

For a differential graded category C, the additive closure TauCeti.DGAdditiveClosure C adjoins formal finite direct sums ⊕ᵢ Xᵢ of objects of C. An object is a finite family of objects of C, and the Hom complex between two of them is the complex of matrices of morphisms,

Hom(⊕ᵢ Xᵢ, ⊕ⱼ Yⱼ) = ∏ᵢ ∏ⱼ Hom(Xᵢ, Yⱼ),

with the differential applied entrywise. Composition is matrix multiplication, (f ≫ g)ᵢₖ = ∑ⱼ fᵢⱼ ≫ gⱼₖ, in Mathlib's enriched factor order, and the identity is the diagonal matrix of identities. Since composition in C is bilinear, the Leibniz rule, associativity and the unit laws hold entrywise; no Koszul sign is introduced. This is the DG analogue of Mathlib's CategoryTheory.Mat_.

Every object of C is a one-term sum, and X ↦ X is a DG functor TauCeti.DGAdditiveClosure.embedding which is an isomorphism on Hom complexes. Every object M = ⊕ᵢ Xᵢ of the additive closure is the direct sum of its summands in the DG sense: the inclusions TauCeti.DGAdditiveClosure.single and projections TauCeti.DGAdditiveClosure.proj are closed of degree zero, proj j ∘ single i is the identity for i = j and zero otherwise, and ∑ᵢ single i ∘ proj i is the identity of M.

A DG functor F : C ⥤ D induces a DG functor F.mapDGAdditiveClosure between the additive closures, sending ⊕ᵢ Xᵢ to ⊕ᵢ F Xᵢ and applying F to every matrix entry.

The additive closure of the shift closure is the home of the underlying objects ⊕ᵢ Xᵢ[rᵢ] of the one-sided twisted complexes of Bondal and Kapranov, whose twisting differential is a degree-one matrix of this kind.

Main definitions

• TauCeti.DGAdditiveClosure: the objects ⊕ᵢ Xᵢ of the additive closure.
• TauCeti.DGAdditiveClosure.homComplexData: its explicit Hom-complex data.
• TauCeti.DGAdditiveClosure.dgHomEquiv: degree-n morphisms ⊕ᵢ Xᵢ ⟶ ⊕ⱼ Yⱼ are matrices of degree-n morphisms Xᵢ ⟶ Yⱼ.
• TauCeti.DGAdditiveClosure.embedding: the DG functor sending X to the one-term sum.
• TauCeti.DGAdditiveClosure.single, TauCeti.DGAdditiveClosure.proj: the inclusion of and the projection to a summand.
• TauCeti.DGAdditiveClosure.sum: the direct sum M ⊕ N of two objects, the concatenation of their families of summands.
• CategoryTheory.EnrichedFunctor.mapDGAdditiveClosure: the DG functor between additive closures induced by a DG functor, applied summandwise and entrywise.

Main results

• TauCeti.DGAdditiveClosure.dgHomEquiv_dgDifferential: the differential is entrywise.
• TauCeti.DGAdditiveClosure.dgHomEquiv_dgComp: composition is matrix multiplication.
• TauCeti.DGAdditiveClosure.dgHomEquiv_dgId: the identity is the diagonal matrix of identities.
• TauCeti.DGAdditiveClosure.isIso_embedding_map: the embedding is an isomorphism on Hom complexes.
• TauCeti.DGAdditiveClosure.dgComp_single_proj_self, TauCeti.DGAdditiveClosure.dgComp_single_proj_of_ne and TauCeti.DGAdditiveClosure.sum_dgComp_proj_single: the biproduct equations.

References

• A. I. Bondal and M. M. Kapranov, Enhanced triangulated categories, Section 1.
• V. Drinfeld, DG quotients of DG categories, Section 2.4.
• Kim Morrison and the Mathlib contributors, Mathlib.CategoryTheory.Preadditive.Mat, for the matrix category CategoryTheory.Mat_ of a preadditive category, whose object structure and matrix composition are followed here.

structure TauCeti.DGAdditiveClosure (C : Type u) : Type (max 1 u)

The objects of the additive closure of a differential graded category on the objects C: a finite family X : ι → C, standing for the formal direct sum ⊕ᵢ Xᵢ. The Hom complexes are the complexes of matrices of morphisms; see TauCeti.DGAdditiveClosure.homComplexData.

• ι : Type

  The index type of the summands.

• fintype : Fintype self.ι
• X : self.ι → C

  The summands.

The Hom-complex data

noncomputable def TauCeti.DGAdditiveClosure.homComplexData (R : Type v) [CommRing R] {C : Type u} [DGCategory R C] : DGCategoryData R (DGAdditiveClosure C)

The explicit Hom-complex data of the additive closure: matrices of morphisms with the entrywise differential, matrix multiplication as composition, and the diagonal matrix of identities as identity.

@[instance_reducible]

noncomputable instance TauCeti.DGAdditiveClosure.instDGCategory (R : Type v) [CommRing R] {C : Type u} [DGCategory R C] : DGCategory R (DGAdditiveClosure C)

The additive closure of a differential graded category: formal finite direct sums ⊕ᵢ Xᵢ, with the complexes of matrices of morphisms as Hom complexes.

Morphisms, differential, composition and identity

noncomputable def TauCeti.DGAdditiveClosure.dgHomEquiv (R : Type v) [CommRing R] {C : Type u} [DGCategory R C] (M N : DGAdditiveClosure C) (n : ℤ) : DGHom R n M N ≃ₗ[R] (i : M.ι) → (j : N.ι) → DGHom R n (M.X i) (N.X j)

A morphism ⊕ᵢ Xᵢ ⟶ ⊕ⱼ Yⱼ of degree n in the additive closure is a matrix of morphisms Xᵢ ⟶ Yⱼ of degree n in C.

theorem TauCeti.DGAdditiveClosure.dgHom_ext (R : Type v) [CommRing R] {C : Type u} [DGCategory R C] {M N : DGAdditiveClosure C} {n : ℤ} {f g : DGHom R n M N} (h : ∀ (i : M.ι) (j : N.ι), (dgHomEquiv R M N n) f i j = (dgHomEquiv R M N n) g i j) : f = g

Morphisms of the additive closure are determined by their matrix entries.

@[simp]

theorem TauCeti.DGAdditiveClosure.dgHomEquiv_dgDifferential (R : Type v) [CommRing R] {C : Type u} [DGCategory R C] {M N : DGAdditiveClosure C} (n : ℤ) (f : DGHom R n M N) (i : M.ι) (j : N.ι) : (dgHomEquiv R M N (n + 1)) ((dgDifferential R n) f) i j = (dgDifferential R n) ((dgHomEquiv R M N n) f i j)

The differential of the additive closure is the differential of C, applied entrywise.

@[simp]

theorem TauCeti.DGAdditiveClosure.dgHomEquiv_dgComp (R : Type v) [CommRing R] {C : Type u} [DGCategory R C] {M N K : DGAdditiveClosure C} {p q n : ℤ} (f : DGHom R p M N) (g : DGHom R q N K) (h : p + q = n) (i : M.ι) (k : K.ι) : (dgHomEquiv R M K n) (dgComp R f g h) i k = ∑ j : N.ι, dgComp R ((dgHomEquiv R M N p) f i j) ((dgHomEquiv R N K q) g j k) h

Composition in the additive closure is matrix multiplication: the (i, k) entry of f followed by g is ∑ⱼ fᵢⱼ followed by gⱼₖ.

theorem TauCeti.DGAdditiveClosure.dgHomEquiv_dgId (R : Type v) [CommRing R] {C : Type u} [DGCategory R C] (M : DGAdditiveClosure C) [DecidableEq M.ι] (i : M.ι) : (dgHomEquiv R M M 0) (dgId R M) i = Pi.single i (dgId R (M.X i))

The identity of the additive closure is the diagonal matrix of identities.

@[simp]

theorem TauCeti.DGAdditiveClosure.dgHomEquiv_dgId_self (R : Type v) [CommRing R] {C : Type u} [DGCategory R C] (M : DGAdditiveClosure C) (i : M.ι) : (dgHomEquiv R M M 0) (dgId R M) i i = dgId R (M.X i)

The diagonal entries of the identity are identities.

@[simp]

theorem TauCeti.DGAdditiveClosure.dgHomEquiv_dgId_of_ne (R : Type v) [CommRing R] {C : Type u} [DGCategory R C] (M : DGAdditiveClosure C) {i j : M.ι} (h : i ≠ j) : (dgHomEquiv R M M 0) (dgId R M) i j = 0

The off-diagonal entries of the identity vanish.

The embedding of C

noncomputable def TauCeti.DGAdditiveClosure.embeddingHomEquiv (R : Type v) [CommRing R] {C : Type u} [DGCategory R C] (X Y : C) (n : ℤ) : DGHom R n X Y ≃ₗ[R] DGHom R n { ι := PUnit.{1}, fintype := PUnit.fintype, X := fun (x : PUnit.{1}) => X } { ι := PUnit.{1}, fintype := PUnit.fintype, X := fun (x : PUnit.{1}) => Y }

The action of the embedding on morphisms of degree n: a degree-n morphism X ⟶ Y of C is the one-by-one matrix it fills.

@[simp]

theorem TauCeti.DGAdditiveClosure.dgHomEquiv_embeddingHomEquiv (R : Type v) [CommRing R] {C : Type u} [DGCategory R C] {X Y : C} {n : ℤ} (f : DGHom R n X Y) (i j : PUnit.{1}) : (dgHomEquiv R { ι := PUnit.{1}, fintype := PUnit.fintype, X := fun (x : PUnit.{1}) => X } { ι := PUnit.{1}, fintype := PUnit.fintype, X := fun (x : PUnit.{1}) => Y } n) ((embeddingHomEquiv R X Y n) f) i j = f

The one-by-one matrix filled by a morphism has that morphism as its entry.

theorem TauCeti.DGAdditiveClosure.embeddingHomEquiv_dgDifferential (R : Type v) [CommRing R] {C : Type u} [DGCategory R C] {X Y : C} (n : ℤ) (f : DGHom R n X Y) : (embeddingHomEquiv R X Y (n + 1)) ((dgDifferential R n) f) = (dgDifferential R n) ((embeddingHomEquiv R X Y n) f)

The one-by-one matrix filled by a morphism commutes with the differential.

theorem TauCeti.DGAdditiveClosure.embeddingHomEquiv_dgId (R : Type v) [CommRing R] {C : Type u} [DGCategory R C] (X : C) : (embeddingHomEquiv R X X 0) (dgId R X) = dgId R { ι := PUnit.{1}, fintype := PUnit.fintype, X := fun (x : PUnit.{1}) => X }

The one-by-one matrix filled by the identity is the identity.

theorem TauCeti.DGAdditiveClosure.embeddingHomEquiv_dgComp (R : Type v) [CommRing R] {C : Type u} [DGCategory R C] {X Y Z : C} {p q n : ℤ} (f : DGHom R p X Y) (g : DGHom R q Y Z) (h : p + q = n) : (embeddingHomEquiv R X Z n) (dgComp R f g h) = dgComp R ((embeddingHomEquiv R X Y p) f) ((embeddingHomEquiv R Y Z q) g) h

One-by-one matrices compose by the composition of their entries.

noncomputable def TauCeti.DGAdditiveClosure.embedding (R : Type v) [CommRing R] {C : Type u} [DGCategory R C] : CategoryTheory.EnrichedFunctor (CochainComplex (ModuleCat R) ℤ) C (DGAdditiveClosure C)

The DG functor from a differential graded category to its additive closure sending X to the one-term sum.

@[simp]

theorem TauCeti.DGAdditiveClosure.embedding_obj (R : Type v) [CommRing R] {C : Type u} [DGCategory R C] (X : C) : (embedding R).obj X = { ι := PUnit.{1}, fintype := PUnit.fintype, X := fun (x : PUnit.{1}) => X }

The embedding sends X to the one-term sum.

@[simp]

theorem TauCeti.DGAdditiveClosure.dgMap_embedding (R : Type v) [CommRing R] {C : Type u} [DGCategory R C] {X Y : C} {n : ℤ} (f : DGHom R n X Y) : ((embedding R).dgMap n) f = (embeddingHomEquiv R X Y n) f

The embedding acts on morphisms by TauCeti.DGAdditiveClosure.embeddingHomEquiv.

instance TauCeti.DGAdditiveClosure.isIso_embedding_map (R : Type v) [CommRing R] {C : Type u} [DGCategory R C] (X Y : C) : CategoryTheory.IsIso ((embedding R).map X Y)

The embedding is an isomorphism on Hom complexes: C is a full DG subcategory of its additive closure.

Summands

noncomputable def TauCeti.DGAdditiveClosure.single (R : Type v) [CommRing R] {C : Type u} [DGCategory R C] (M : DGAdditiveClosure C) (i : M.ι) : DGHom R 0 { ι := PUnit.{1}, fintype := PUnit.fintype, X := fun (x : PUnit.{1}) => M.X i } M

The inclusion of the summand Xᵢ, as the one-term sum (embedding R).obj (M.X i), into ⊕ᵢ Xᵢ: the i-th row of the identity matrix.

noncomputable def TauCeti.DGAdditiveClosure.proj (R : Type v) [CommRing R] {C : Type u} [DGCategory R C] (M : DGAdditiveClosure C) (i : M.ι) : DGHom R 0 M { ι := PUnit.{1}, fintype := PUnit.fintype, X := fun (x : PUnit.{1}) => M.X i }

The projection of ⊕ᵢ Xᵢ onto the summand Xᵢ, as the one-term sum (embedding R).obj (M.X i): the i-th column of the identity matrix.

@[simp]

theorem TauCeti.DGAdditiveClosure.dgHomEquiv_single (R : Type v) [CommRing R] {C : Type u} [DGCategory R C] (M : DGAdditiveClosure C) (i : M.ι) (u : PUnit.{1}) (j : M.ι) : (dgHomEquiv R { ι := PUnit.{1}, fintype := PUnit.fintype, X := fun (x : PUnit.{1}) => M.X i } M 0) (single R M i) u j = (dgHomEquiv R M M 0) (dgId R M) i j

The entries of the inclusion of the summand Xᵢ are the entries of the i-th row of the identity.

@[simp]

theorem TauCeti.DGAdditiveClosure.dgHomEquiv_proj (R : Type v) [CommRing R] {C : Type u} [DGCategory R C] (M : DGAdditiveClosure C) (i j : M.ι) (u : PUnit.{1}) : (dgHomEquiv R M { ι := PUnit.{1}, fintype := PUnit.fintype, X := fun (x : PUnit.{1}) => M.X i } 0) (proj R M i) j u = (dgHomEquiv R M M 0) (dgId R M) j i

The entries of the projection onto the summand Xᵢ are the entries of the i-th column of the identity.

@[simp]

theorem TauCeti.DGAdditiveClosure.dgDifferential_dgHomEquiv_dgId (R : Type v) [CommRing R] {C : Type u} [DGCategory R C] (M : DGAdditiveClosure C) (i j : M.ι) : (dgDifferential R 0) ((dgHomEquiv R M M 0) (dgId R M) i j) = 0

The entries of the identity are closed.

@[simp]

theorem TauCeti.DGAdditiveClosure.sum_dgHomEquiv_dgId_dgComp (R : Type v) [CommRing R] {C : Type u} [DGCategory R C] {M : DGAdditiveClosure C} {Z : C} {q : ℤ} (F : (j : M.ι) → DGHom R q (M.X j) Z) (i : M.ι) : ∑ j : M.ι, dgComp R ((dgHomEquiv R M M 0) (dgId R M) i j) (F j) ⋯ = F i

Multiplying a row of morphisms out of the summands of M on the left by a row of the identity of M picks out one of them.

@[simp]

theorem TauCeti.DGAdditiveClosure.sum_dgComp_dgHomEquiv_dgId (R : Type v) [CommRing R] {C : Type u} [DGCategory R C] {M : DGAdditiveClosure C} {Z : C} {p : ℤ} (F : (j : M.ι) → DGHom R p Z (M.X j)) (k : M.ι) : ∑ j : M.ι, dgComp R (F j) ((dgHomEquiv R M M 0) (dgId R M) j k) ⋯ = F k

Multiplying a column of morphisms into the summands of M on the right by a column of the identity of M picks out one of them.

@[simp]

theorem TauCeti.DGAdditiveClosure.dgDifferential_single (R : Type v) [CommRing R] {C : Type u} [DGCategory R C] (M : DGAdditiveClosure C) (i : M.ι) : (dgDifferential R 0) (single R M i) = 0

The inclusion of a summand is closed.

@[simp]

theorem TauCeti.DGAdditiveClosure.dgDifferential_proj (R : Type v) [CommRing R] {C : Type u} [DGCategory R C] (M : DGAdditiveClosure C) (i : M.ι) : (dgDifferential R 0) (proj R M i) = 0

The projection to a summand is closed.

@[simp]

theorem TauCeti.DGAdditiveClosure.dgComp_single_proj_self (R : Type v) [CommRing R] {C : Type u} [DGCategory R C] (M : DGAdditiveClosure C) (i : M.ι) : dgComp R (single R M i) (proj R M i) ⋯ = dgId R { ι := PUnit.{1}, fintype := PUnit.fintype, X := fun (x : PUnit.{1}) => M.X i }

The inclusion of a summand followed by the projection to it is the identity.

@[simp]

theorem TauCeti.DGAdditiveClosure.dgComp_single_proj_of_ne (R : Type v) [CommRing R] {C : Type u} [DGCategory R C] (M : DGAdditiveClosure C) {i j : M.ι} (h : i ≠ j) : dgComp R (single R M i) (proj R M j) ⋯ = 0

The inclusion of a summand followed by the projection to a different summand vanishes.

theorem TauCeti.DGAdditiveClosure.sum_dgComp_proj_single (R : Type v) [CommRing R] {C : Type u} [DGCategory R C] (M : DGAdditiveClosure C) : ∑ i : M.ι, dgComp R (proj R M i) (single R M i) ⋯ = dgId R M

⊕ᵢ Xᵢ is the direct sum of its summands: the sum over all summands of the projection followed by the inclusion is the identity.

theorem TauCeti.DGAdditiveClosure.dgComp_proj_single_of_subsingleton (R : Type v) [CommRing R] {C : Type u} [DGCategory R C] (M : DGAdditiveClosure C) [Subsingleton M.ι] (i : M.ι) : dgComp R (proj R M i) (single R M i) ⋯ = dgId R M

If M has at most one summand, the projection onto the summand Xᵢ followed by the inclusion of it is the identity of M.

Restriction to a set of summands

@[simp]

theorem TauCeti.DGAdditiveClosure.dgHomEquiv_dgId_subtype (R : Type v) [CommRing R] {C : Type u} [DGCategory R C] (M : DGAdditiveClosure C) (q : M.ι → Prop) [DecidablePred q] (i j : { i : M.ι // q i }) : (dgHomEquiv R { ι := { i : M.ι // q i }, fintype := Subtype.fintype q, X := fun (i : { i : M.ι // q i }) => M.X ↑i } { ι := { i : M.ι // q i }, fintype := Subtype.fintype q, X := fun (i : { i : M.ι // q i }) => M.X ↑i } 0) (dgId R { ι := { i : M.ι // q i }, fintype := Subtype.fintype q, X := fun (i : { i : M.ι // q i }) => M.X ↑i }) i j = (dgHomEquiv R M M 0) (dgId R M) ↑i ↑j

The identity of the sum of the summands of M satisfying q is the restriction of the identity of M.

Binary sums

@[reducible, inline]

abbrev TauCeti.DGAdditiveClosure.sum {C : Type u} (M N : DGAdditiveClosure C) : DGAdditiveClosure C

The direct sum M ⊕ N of two objects of the additive closure: the concatenation of their families of summands.

@[simp]

theorem TauCeti.DGAdditiveClosure.dgHomEquiv_dgId_sum_inl_inl (R : Type v) [CommRing R] {C : Type u} [DGCategory R C] (M N : DGAdditiveClosure C) (i j : M.ι) : (dgHomEquiv R (M.sum N) (M.sum N) 0) (dgId R (M.sum N)) (Sum.inl i) (Sum.inl j) = (dgHomEquiv R M M 0) (dgId R M) i j

The block of the identity of M ⊕ N on the summands of M is the identity of M.

@[simp]

theorem TauCeti.DGAdditiveClosure.dgHomEquiv_dgId_sum_inl_inr (R : Type v) [CommRing R] {C : Type u} [DGCategory R C] (M N : DGAdditiveClosure C) (i : M.ι) (j : N.ι) : (dgHomEquiv R (M.sum N) (M.sum N) 0) (dgId R (M.sum N)) (Sum.inl i) (Sum.inr j) = 0

The block of the identity of M ⊕ N from the summands of M to those of N vanishes.

@[simp]

theorem TauCeti.DGAdditiveClosure.dgHomEquiv_dgId_sum_inr_inl (R : Type v) [CommRing R] {C : Type u} [DGCategory R C] (M N : DGAdditiveClosure C) (i : N.ι) (j : M.ι) : (dgHomEquiv R (M.sum N) (M.sum N) 0) (dgId R (M.sum N)) (Sum.inr i) (Sum.inl j) = 0

The block of the identity of M ⊕ N from the summands of N to those of M vanishes.

@[simp]

theorem TauCeti.DGAdditiveClosure.dgHomEquiv_dgId_sum_inr_inr (R : Type v) [CommRing R] {C : Type u} [DGCategory R C] (M N : DGAdditiveClosure C) (i j : N.ι) : (dgHomEquiv R (M.sum N) (M.sum N) 0) (dgId R (M.sum N)) (Sum.inr i) (Sum.inr j) = (dgHomEquiv R N N 0) (dgId R N) i j

The block of the identity of M ⊕ N on the summands of N is the identity of N.

Functoriality

noncomputable def CategoryTheory.EnrichedFunctor.mapDGAdditiveClosureHom {R : Type v} [CommRing R] {C : Type u} {D : Type u₂} [TauCeti.DGCategory R C] [TauCeti.DGCategory R D] (F : EnrichedFunctor (CochainComplex (ModuleCat R) ℤ) C D) (M N : TauCeti.DGAdditiveClosure C) (n : ℤ) : TauCeti.DGHom R n M N →ₗ[R] TauCeti.DGHom R n { ι := M.ι, fintype := M.fintype, X := fun (i : M.ι) => F.obj (M.X i) } { ι := N.ι, fintype := N.fintype, X := fun (j : N.ι) => F.obj (N.X j) }

The action of a DG functor on matrices of morphisms of degree n: it is applied entrywise.

@[simp]

theorem CategoryTheory.EnrichedFunctor.dgHomEquiv_mapDGAdditiveClosureHom {R : Type v} [CommRing R] {C : Type u} {D : Type u₂} [TauCeti.DGCategory R C] [TauCeti.DGCategory R D] (F : EnrichedFunctor (CochainComplex (ModuleCat R) ℤ) C D) {M N : TauCeti.DGAdditiveClosure C} {n : ℤ} (f : TauCeti.DGHom R n M N) (i : M.ι) (j : N.ι) : (TauCeti.DGAdditiveClosure.dgHomEquiv R { ι := M.ι, fintype := M.fintype, X := fun (i : M.ι) => F.obj (M.X i) } { ι := N.ι, fintype := N.fintype, X := fun (j : N.ι) => F.obj (N.X j) } n) ((F.mapDGAdditiveClosureHom M N n) f) i j = (F.dgMap n) ((TauCeti.DGAdditiveClosure.dgHomEquiv R M N n) f i j)

The entries of the image of a matrix are the images of its entries.

@[reducible, inline]

noncomputable abbrev CategoryTheory.EnrichedFunctor.mapDGAdditiveClosure {R : Type v} [CommRing R] {C : Type u} {D : Type u₂} [TauCeti.DGCategory R C] [TauCeti.DGCategory R D] (F : EnrichedFunctor (CochainComplex (ModuleCat R) ℤ) C D) : EnrichedFunctor (CochainComplex (ModuleCat R) ℤ) (TauCeti.DGAdditiveClosure C) (TauCeti.DGAdditiveClosure D)

The DG functor between additive closures induced by a DG functor F, sending ⊕ᵢ Xᵢ to ⊕ᵢ F Xᵢ and applying F to every matrix entry.

@[simp]

theorem CategoryTheory.EnrichedFunctor.dgMap_mapDGAdditiveClosure {R : Type v} [CommRing R] {C : Type u} {D : Type u₂} [TauCeti.DGCategory R C] [TauCeti.DGCategory R D] (F : EnrichedFunctor (CochainComplex (ModuleCat R) ℤ) C D) {M N : TauCeti.DGAdditiveClosure C} {n : ℤ} (f : TauCeti.DGHom R n M N) : (F.mapDGAdditiveClosure.dgMap n) f = (F.mapDGAdditiveClosureHom M N n) f

The induced DG functor acts on matrices by CategoryTheory.EnrichedFunctor.mapDGAdditiveClosureHom.