Differential graded categories from explicit Hom-complex data

A differential graded category is defined as a category enriched in cochain complexes of R-modules, and TauCeti/CategoryTheory/DG/Basic.lean unpacks that enrichment into homogeneous morphisms, their differential, and their composition. This file goes the other way. Explicit Hom-complex data, TauCeti.DGCategoryData, consists of a Hom complex for every pair of objects, bilinear composition maps on homogeneous degrees, and identities, subject to the graded Leibniz rule, associativity, and the unit laws stated on elements. Such data determines a differential graded category, TauCeti.DGCategoryData.toDGCategory, whose homogeneous morphisms, differential, identities and composition are the given ones.

The two presentations are equivalent: extracting the explicit data from a differential graded category and rebuilding the enrichment recovers the enrichment, and rebuilding the data from the enrichment of explicit data recovers the data. Hence a differential graded category may be specified by elementwise formulas, and a differential graded category built from homogeneous morphisms, such as the one-object category of a differential graded algebra or the category of differential graded modules, needs no monoidal plumbing of its own.

Composition in TauCeti.DGCategoryData is in Mathlib's enriched factor order, so comp f g is f followed by g and the Leibniz sign is carried by the degree of f, exactly as for TauCeti.dgComp. Keller's convention, in which g ∘ f carries the Leibniz sign of g, differs by the Koszul sign (-1) ^ (|f| * |g|); TauCeti.DGCategoryData.ofKeller converts data given in that convention.

Main definitions

• TauCeti.DGCategoryData: explicit Hom-complex data for a differential graded category.
• TauCeti.DGCategoryData.toDGCategory: the differential graded category it determines.
• TauCeti.DGCategoryData.ofKeller: the same data from Keller-ordered composition.
• TauCeti.dgCategoryData: the explicit Hom-complex data of a differential graded category.
• TauCeti.DGCategoryData.equivDGCategory: the two presentations are equivalent.

Main results

• TauCeti.DGCategoryData.dgComp_toDGCategory, TauCeti.DGCategoryData.dgId_toDGCategory, TauCeti.DGCategoryData.dgDifferential_toDGCategory: the homogeneous calculus of the constructed category is the given data.
• TauCeti.DGCategoryData.toDGCategory_dgCategoryData and TauCeti.DGCategoryData.dgCategoryData_toDGCategory: the two round trips.

References

• B. Keller, Deriving DG categories, Section 1.
• B. Keller, Introduction to A-infinity algebras and modules, Section 3.1, for the sign conventions and the comparison sign between the two factor orders.
• TauCeti/Algebra/Homology/LinearHomComplex/Composition.lean.
• TauCeti/Algebra/Homology/LinearHomComplex/Enrichment.lean.

structure TauCeti.DGCategoryData (R : Type v) [CommRing R] (C : Type u) : Type (max u (v + 1))

Explicit Hom-complex data for a differential graded category over R on the objects C: a Hom complex hom X Y for every pair of objects, bilinear composition comp p q n h : (hom X Y).X p →ₗ[R] (hom Y Z).X q →ₗ[R] (hom X Z).X n for p + q = n, in Mathlib's enriched factor order, and identities id X of degree zero, satisfying the graded Leibniz rule, associativity, and the unit laws on homogeneous elements. Such data determines the differential graded category TauCeti.DGCategoryData.toDGCategory.

• hom : C → C → CochainComplex (ModuleCat R) ℤ

  The Hom complex from X to Y.

• comp {X Y Z : C} (p q n : ℤ) (h : p + q = n) : ↑((self.hom X Y).X p) →ₗ[R] ↑((self.hom Y Z).X q) →ₗ[R] ↑((self.hom X Z).X n)

  Composition of a degree-p morphism X ⟶ Y with a degree-q morphism Y ⟶ Z, in Mathlib's enriched factor order: comp p q n h f g is f followed by g.

• id (X : C) : ↑((self.hom X X).X 0)

  The identity of X, a morphism of degree zero.

• d_comp {X Y Z : C} {p q n : ℤ} (h : p + q = n) (f : ↑((self.hom X Y).X p)) (g : ↑((self.hom Y Z).X q)) : (ModuleCat.Hom.hom ((self.hom X Z).d n (n + 1))) (((self.comp p q n h) f) g) = ((self.comp (p + 1) q (n + 1) ⋯) ((ModuleCat.Hom.hom ((self.hom X Y).d p (p + 1))) f)) g + p.negOnePow • ((self.comp p (q + 1) (n + 1) ⋯) f) ((ModuleCat.Hom.hom ((self.hom Y Z).d q (q + 1))) g)

  The graded Leibniz rule, with the Koszul sign carried by the degree of the first factor.

• comp_assoc {W X Y Z : C} {p q r pq qr n : ℤ} (hpq : p + q = pq) (hqr : q + r = qr) (h : p + q + r = n) (f : ↑((self.hom W X).X p)) (g : ↑((self.hom X Y).X q)) (k : ↑((self.hom Y Z).X r)) : ((self.comp pq r n ⋯) (((self.comp p q pq hpq) f) g)) k = ((self.comp p qr n ⋯) f) (((self.comp q r qr hqr) g) k)

  Composition is associative.

• id_comp {X Y : C} {q : ℤ} (g : ↑((self.hom X Y).X q)) : ((self.comp 0 q q ⋯) (self.id X)) g = g

  The identity is a left unit.

• comp_id {X Y : C} {p : ℤ} (f : ↑((self.hom X Y).X p)) : ((self.comp p 0 p ⋯) f) (self.id Y) = f

  The identity is a right unit.

@[simp]

theorem TauCeti.DGCategoryData.d_id {R : Type v} [CommRing R] {C : Type u} (D : DGCategoryData R C) (X : C) : (ModuleCat.Hom.hom ((D.hom X X).d 0 1)) (D.id X) = 0

The identity is a cycle.

The enriched composition and identity

noncomputable def TauCeti.DGCategoryData.compMap {R : Type v} [CommRing R] {C : Type u} (D : DGCategoryData R C) (X Y Z : C) (p q n : ℤ) (h : p + q = n) : CategoryTheory.MonoidalCategoryStruct.tensorObj ((D.hom X Y).X p) ((D.hom Y Z).X q) ⟶ (D.hom X Z).X n

The bidegree-(p, q) component of composition, as a morphism out of the tensor product of the two homogeneous modules.

Equations

• D.compMap X Y Z p q n h = ModuleCat.ofHom (TensorProduct.lift (D.comp p q n h))

@[simp]

theorem TauCeti.DGCategoryData.compMap_tmul {R : Type v} [CommRing R] {C : Type u} (D : DGCategoryData R C) (X Y Z : C) (p q n : ℤ) (h : p + q = n) (f : ↑((D.hom X Y).X p)) (g : ↑((D.hom Y Z).X q)) : (ModuleCat.Hom.hom (D.compMap X Y Z p q n h)) (f ⊗ₜ[R] g) = ((D.comp p q n h) f) g

noncomputable def TauCeti.DGCategoryData.enrichedComp {R : Type v} [CommRing R] {C : Type u} (D : DGCategoryData R C) (X Y Z : C) : CategoryTheory.MonoidalCategoryStruct.tensorObj (D.hom X Y) (D.hom Y Z) ⟶ D.hom X Z

Composition as a morphism of cochain complexes out of the totalized tensor product of the two Hom complexes. The Leibniz rule makes it a chain map.

Equations

• One or more equations did not get rendered due to their size.

theorem TauCeti.DGCategoryData.enrichedComp_f {R : Type v} [CommRing R] {C : Type u} (D : DGCategoryData R C) (X Y Z : C) (n : ℤ) : (D.enrichedComp X Y Z).f n = HomologicalComplex.mapBifunctorDesc fun (p q : ℤ) (h : (ComplexShape.up ℤ).π (ComplexShape.up ℤ) (ComplexShape.up ℤ) (p, q) = n) => D.compMap X Y Z p q n h

The degree-n component of the enriched composition is assembled from the bidegree components.

@[simp]

theorem TauCeti.DGCategoryData.ι_enrichedComp {R : Type v} [CommRing R] {C : Type u} (D : DGCategoryData R C) (X Y Z : C) (p q n : ℤ) (h : p + q = n) : CategoryTheory.CategoryStruct.comp (HomologicalComplex.ιTensorObj (D.hom X Y) (D.hom Y Z) p q n h) ((D.enrichedComp X Y Z).f n) = D.compMap X Y Z p q n h

On the bidegree-(p, q) summand, the enriched composition is the bilinear composition of the data.

@[simp]

theorem TauCeti.DGCategoryData.ι_enrichedComp_assoc {R : Type v} [CommRing R] {C : Type u} (D : DGCategoryData R C) (X Y Z : C) (p q n : ℤ) (h : p + q = n) {Z✝ : ModuleCat R} (h✝ : (D.hom X Z).X n ⟶ Z✝) : CategoryTheory.CategoryStruct.comp (HomologicalComplex.ιTensorObj (D.hom X Y) (D.hom Y Z) p q n h) (CategoryTheory.CategoryStruct.comp ((D.enrichedComp X Y Z).f n) h✝) = CategoryTheory.CategoryStruct.comp (D.compMap X Y Z p q n h) h✝

On the bidegree-(p, q) summand, the enriched composition is the bilinear composition of the data.

noncomputable def TauCeti.DGCategoryData.enrichedId {R : Type v} [CommRing R] {C : Type u} (D : DGCategoryData R C) (X : C) : CategoryTheory.MonoidalCategoryStruct.tensorUnit (CochainComplex (ModuleCat R) ℤ) ⟶ D.hom X X

The identity of X, as a morphism from the tensor unit to the Hom complex of X with itself.

Equations

• D.enrichedId X = HomologicalComplex.mkHomFromSingle (ModuleCat.ofHom (LinearMap.toSpanSingleton R (↑((D.hom X X).1 0)) (D.id X))) ⋯

theorem TauCeti.DGCategoryData.enrichedId_f_zero {R : Type v} [CommRing R] {C : Type u} (D : DGCategoryData R C) (X : C) : (D.enrichedId X).f 0 = CategoryTheory.CategoryStruct.comp (HomologicalComplex.singleObjXSelf (ComplexShape.up ℤ) 0 (CategoryTheory.MonoidalCategoryStruct.tensorUnit (ModuleCat R))).hom (ModuleCat.ofHom (LinearMap.toSpanSingleton R (↑((D.hom X X).X 0)) (D.id X)))

The degree-zero component of the enriched identity.

@[simp]

theorem TauCeti.DGCategoryData.enrichedId_f_zero_apply {R : Type v} [CommRing R] {C : Type u} (D : DGCategoryData R C) (X : C) (r : R) : (ModuleCat.Hom.hom ((D.enrichedId X).f 0)) ((CategoryTheory.ConcreteCategory.hom (HomologicalComplex.singleObjXSelf (ComplexShape.up ℤ) 0 (CategoryTheory.MonoidalCategoryStruct.tensorUnit (ModuleCat R))).inv) r) = r • D.id X

The degree-zero component of the enriched identity sends a scalar to that multiple of the identity.

The differential graded category

@[simp]

theorem TauCeti.DGCategoryData.leftUnitor_inv_enrichedId_enrichedComp {R : Type v} [CommRing R] {C : Type u} (D : DGCategoryData R C) (X Y : C) : CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.leftUnitor (D.hom X Y)).inv (CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.whiskerRight (D.enrichedId X) (D.hom X Y)) (D.enrichedComp X X Y)) = CategoryTheory.CategoryStruct.id (D.hom X Y)

The enriched identity is a left unit for the enriched composition.

@[simp]

theorem TauCeti.DGCategoryData.leftUnitor_inv_enrichedId_enrichedComp_assoc {R : Type v} [CommRing R] {C : Type u} (D : DGCategoryData R C) (X Y : C) {Z : CochainComplex (ModuleCat R) ℤ} (h : D.hom X Y ⟶ Z) : CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.leftUnitor (D.hom X Y)).inv (CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.whiskerRight (D.enrichedId X) (D.hom X Y)) (CategoryTheory.CategoryStruct.comp (D.enrichedComp X X Y) h)) = h

The enriched identity is a left unit for the enriched composition.

@[simp]

theorem TauCeti.DGCategoryData.rightUnitor_inv_enrichedId_enrichedComp {R : Type v} [CommRing R] {C : Type u} (D : DGCategoryData R C) (X Y : C) : CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.rightUnitor (D.hom X Y)).inv (CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.whiskerLeft (D.hom X Y) (D.enrichedId Y)) (D.enrichedComp X Y Y)) = CategoryTheory.CategoryStruct.id (D.hom X Y)

The enriched identity is a right unit for the enriched composition.

@[simp]

theorem TauCeti.DGCategoryData.rightUnitor_inv_enrichedId_enrichedComp_assoc {R : Type v} [CommRing R] {C : Type u} (D : DGCategoryData R C) (X Y : C) {Z : CochainComplex (ModuleCat R) ℤ} (h : D.hom X Y ⟶ Z) : CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.rightUnitor (D.hom X Y)).inv (CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.whiskerLeft (D.hom X Y) (D.enrichedId Y)) (CategoryTheory.CategoryStruct.comp (D.enrichedComp X Y Y) h)) = h

The enriched identity is a right unit for the enriched composition.

@[simp]

theorem TauCeti.DGCategoryData.enrichedComp_assoc {R : Type v} [CommRing R] {C : Type u} (D : DGCategoryData R C) (W X Y Z : C) : CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.associator (D.hom W X) (D.hom X Y) (D.hom Y Z)).inv (CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.whiskerRight (D.enrichedComp W X Y) (D.hom Y Z)) (D.enrichedComp W Y Z)) = CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.whiskerLeft (D.hom W X) (D.enrichedComp X Y Z)) (D.enrichedComp W X Z)

The enriched composition is associative, with the tensor products identified by the monoidal associator.

@[simp]

theorem TauCeti.DGCategoryData.enrichedComp_assoc_assoc {R : Type v} [CommRing R] {C : Type u} (D : DGCategoryData R C) (W X Y Z : C) {Z✝ : CochainComplex (ModuleCat R) ℤ} (h : D.hom W Z ⟶ Z✝) : CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.associator (D.hom W X) (D.hom X Y) (D.hom Y Z)).inv (CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.whiskerRight (D.enrichedComp W X Y) (D.hom Y Z)) (CategoryTheory.CategoryStruct.comp (D.enrichedComp W Y Z) h)) = CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.whiskerLeft (D.hom W X) (D.enrichedComp X Y Z)) (CategoryTheory.CategoryStruct.comp (D.enrichedComp W X Z) h)

The enriched composition is associative, with the tensor products identified by the monoidal associator.

@[instance_reducible]

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

The differential graded category determined by explicit Hom-complex data. Its body is exposed so that its homogeneous morphisms TauCeti.DGHom remain definitionally the given (D.hom X Y).X n.

Equations

• D.toDGCategory = { Hom := D.hom, id := D.enrichedId, comp := D.enrichedComp, id_comp := ⋯, comp_id := ⋯, assoc := ⋯ }

@[simp]

theorem TauCeti.DGCategoryData.dgHomComplex_toDGCategory {R : Type v} [CommRing R] {C : Type u} (D : DGCategoryData R C) (X Y : C) : dgHomComplex R X Y = D.hom X Y

The Hom complex of the constructed category is the given one.

@[simp]

theorem TauCeti.DGCategoryData.eId_toDGCategory {R : Type v} [CommRing R] {C : Type u} (D : DGCategoryData R C) (X : C) : CategoryTheory.eId (CochainComplex (ModuleCat R) ℤ) X = D.enrichedId X

The enriched identity of the constructed category is the given one.

@[simp]

theorem TauCeti.DGCategoryData.eComp_toDGCategory {R : Type v} [CommRing R] {C : Type u} (D : DGCategoryData R C) (X Y Z : C) : CategoryTheory.eComp (CochainComplex (ModuleCat R) ℤ) X Y Z = D.enrichedComp X Y Z

The enriched composition of the constructed category is the given one.

@[simp]

theorem TauCeti.DGCategoryData.dgDifferential_toDGCategory {R : Type v} [CommRing R] {C : Type u} (D : DGCategoryData R C) {X Y : C} (n : ℤ) (f : ↑((D.hom X Y).X n)) : (dgDifferential R n) f = (ModuleCat.Hom.hom ((D.hom X Y).d n (n + 1))) f

The differential of the constructed category is the differential of the given Hom complexes.

@[simp]

theorem TauCeti.DGCategoryData.dgCompMap_toDGCategory {R : Type v} [CommRing R] {C : Type u} (D : DGCategoryData R C) (X Y Z : C) (p q n : ℤ) (h : p + q = n) : dgCompMap R X Y Z p q n h = D.compMap X Y Z p q n h

The bidegree components of composition in the constructed category are the given ones.

@[simp]

theorem TauCeti.DGCategoryData.dgComp_toDGCategory {R : Type v} [CommRing R] {C : Type u} (D : DGCategoryData R C) {X Y Z : C} {p q n : ℤ} (f : ↑((D.hom X Y).X p)) (g : ↑((D.hom Y Z).X q)) (h : p + q = n) : dgComp R f g h = ((D.comp p q n h) f) g

Composition in the constructed category is the given composition.

@[simp]

theorem TauCeti.DGCategoryData.dgId_toDGCategory {R : Type v} [CommRing R] {C : Type u} (D : DGCategoryData R C) (X : C) : dgId R X = D.id X

The identity of the constructed category is the given identity.

Keller-ordered data

noncomputable def TauCeti.DGCategoryData.ofKeller {R : Type v} [CommRing R] {C : Type u} (hom : C → C → CochainComplex (ModuleCat R) ℤ) (comp : {X Y Z : C} → (q p n : ℤ) → q + p = n → ↑((hom Y Z).X q) →ₗ[R] ↑((hom X Y).X p) →ₗ[R] ↑((hom X Z).X n)) (id : (X : C) → ↑((hom X X).X 0)) (d_comp : ∀ {X Y Z : C} {q p n : ℤ} (h : q + p = n) (g : ↑((hom Y Z).X q)) (f : ↑((hom X Y).X p)), (ModuleCat.Hom.hom ((hom X Z).d n (n + 1))) (((comp q p n h) g) f) = ((comp (q + 1) p (n + 1) ⋯) ((ModuleCat.Hom.hom ((hom Y Z).d q (q + 1))) g)) f + q.negOnePow • ((comp q (p + 1) (n + 1) ⋯) g) ((ModuleCat.Hom.hom ((hom X Y).d p (p + 1))) f)) (comp_assoc : ∀ {W X Y Z : C} {r q p rq qp n : ℤ} (hrq : r + q = rq) (hqp : q + p = qp) (h : r + q + p = n) (k : ↑((hom Y Z).X r)) (g : ↑((hom X Y).X q)) (f : ↑((hom W X).X p)), ((comp rq p n ⋯) (((comp r q rq hrq) k) g)) f = ((comp r qp n ⋯) k) (((comp q p qp hqp) g) f)) (comp_id : ∀ {X Y : C} {q : ℤ} (g : ↑((hom X Y).X q)), ((comp q 0 q ⋯) g) (id X) = g) (id_comp : ∀ {X Y : C} {p : ℤ} (f : ↑((hom X Y).X p)), ((comp 0 p p ⋯) (id Y)) f = f) : DGCategoryData R C

Explicit Hom-complex data from Keller-ordered composition. Here comp q p n h g f is g ∘ f for g : Y ⟶ Z of degree q and f : X ⟶ Y of degree p, the Leibniz rule d (g ∘ f) = d g ∘ f + (-1) ^ q • g ∘ d f carries the sign of g, and associativity and the unit laws are the usual ones. The enriched-order composition of the resulting data is (-1) ^ (p * q) • g ∘ f, the Koszul sign converting between the two factor orders. The body is exposed so that the homogeneous morphisms of the resulting data remain definitionally the given (hom X Y).X n.

Equations

• One or more equations did not get rendered due to their size.

@[simp]

theorem TauCeti.DGCategoryData.ofKeller_hom {R : Type v} [CommRing R] {C : Type u} {hom : C → C → CochainComplex (ModuleCat R) ℤ} {comp : {X Y Z : C} → (q p n : ℤ) → q + p = n → ↑((hom Y Z).X q) →ₗ[R] ↑((hom X Y).X p) →ₗ[R] ↑((hom X Z).X n)} {id : (X : C) → ↑((hom X X).X 0)} {d_comp : ∀ {X Y Z : C} {q p n : ℤ} (h : q + p = n) (g : ↑((hom Y Z).X q)) (f : ↑((hom X Y).X p)), (ModuleCat.Hom.hom ((hom X Z).d n (n + 1))) (((comp q p n h) g) f) = ((comp (q + 1) p (n + 1) ⋯) ((ModuleCat.Hom.hom ((hom Y Z).d q (q + 1))) g)) f + q.negOnePow • ((comp q (p + 1) (n + 1) ⋯) g) ((ModuleCat.Hom.hom ((hom X Y).d p (p + 1))) f)} {comp_assoc : ∀ {W X Y Z : C} {r q p rq qp n : ℤ} (hrq : r + q = rq) (hqp : q + p = qp) (h : r + q + p = n) (k : ↑((hom Y Z).X r)) (g : ↑((hom X Y).X q)) (f : ↑((hom W X).X p)), ((comp rq p n ⋯) (((comp r q rq hrq) k) g)) f = ((comp r qp n ⋯) k) (((comp q p qp hqp) g) f)} {comp_id : ∀ {X Y : C} {q : ℤ} (g : ↑((hom X Y).X q)), ((comp q 0 q ⋯) g) (id X) = g} {id_comp : ∀ {X Y : C} {p : ℤ} (f : ↑((hom X Y).X p)), ((comp 0 p p ⋯) (id Y)) f = f} (X Y : C) : (ofKeller hom (fun {X Y Z : C} => comp) id ⋯ ⋯ ⋯ ⋯).hom X Y = hom X Y

@[simp]

theorem TauCeti.DGCategoryData.ofKeller_comp {R : Type v} [CommRing R] {C : Type u} {hom : C → C → CochainComplex (ModuleCat R) ℤ} {comp : {X Y Z : C} → (q p n : ℤ) → q + p = n → ↑((hom Y Z).X q) →ₗ[R] ↑((hom X Y).X p) →ₗ[R] ↑((hom X Z).X n)} {id : (X : C) → ↑((hom X X).X 0)} {d_comp : ∀ {X Y Z : C} {q p n : ℤ} (h : q + p = n) (g : ↑((hom Y Z).X q)) (f : ↑((hom X Y).X p)), (ModuleCat.Hom.hom ((hom X Z).d n (n + 1))) (((comp q p n h) g) f) = ((comp (q + 1) p (n + 1) ⋯) ((ModuleCat.Hom.hom ((hom Y Z).d q (q + 1))) g)) f + q.negOnePow • ((comp q (p + 1) (n + 1) ⋯) g) ((ModuleCat.Hom.hom ((hom X Y).d p (p + 1))) f)} {comp_assoc : ∀ {W X Y Z : C} {r q p rq qp n : ℤ} (hrq : r + q = rq) (hqp : q + p = qp) (h : r + q + p = n) (k : ↑((hom Y Z).X r)) (g : ↑((hom X Y).X q)) (f : ↑((hom W X).X p)), ((comp rq p n ⋯) (((comp r q rq hrq) k) g)) f = ((comp r qp n ⋯) k) (((comp q p qp hqp) g) f)} {comp_id : ∀ {X Y : C} {q : ℤ} (g : ↑((hom X Y).X q)), ((comp q 0 q ⋯) g) (id X) = g} {id_comp : ∀ {X Y : C} {p : ℤ} (f : ↑((hom X Y).X p)), ((comp 0 p p ⋯) (id Y)) f = f} {X Y Z : C} (p q n : ℤ) (h : p + q = n) (f : ↑((hom X Y).X p)) (g : ↑((hom Y Z).X q)) : (((ofKeller hom (fun {X Y Z : C} => comp) id ⋯ ⋯ ⋯ ⋯).comp p q n h) f) g = (p * q).negOnePow • ((comp q p n ⋯) g) f

The enriched-order composition of Keller-ordered data is Keller composition in reversed order, with the Koszul sign (-1) ^ (p * q).

@[simp]

theorem TauCeti.DGCategoryData.ofKeller_id {R : Type v} [CommRing R] {C : Type u} {hom : C → C → CochainComplex (ModuleCat R) ℤ} {comp : {X Y Z : C} → (q p n : ℤ) → q + p = n → ↑((hom Y Z).X q) →ₗ[R] ↑((hom X Y).X p) →ₗ[R] ↑((hom X Z).X n)} {id : (X : C) → ↑((hom X X).X 0)} {d_comp : ∀ {X Y Z : C} {q p n : ℤ} (h : q + p = n) (g : ↑((hom Y Z).X q)) (f : ↑((hom X Y).X p)), (ModuleCat.Hom.hom ((hom X Z).d n (n + 1))) (((comp q p n h) g) f) = ((comp (q + 1) p (n + 1) ⋯) ((ModuleCat.Hom.hom ((hom Y Z).d q (q + 1))) g)) f + q.negOnePow • ((comp q (p + 1) (n + 1) ⋯) g) ((ModuleCat.Hom.hom ((hom X Y).d p (p + 1))) f)} {comp_assoc : ∀ {W X Y Z : C} {r q p rq qp n : ℤ} (hrq : r + q = rq) (hqp : q + p = qp) (h : r + q + p = n) (k : ↑((hom Y Z).X r)) (g : ↑((hom X Y).X q)) (f : ↑((hom W X).X p)), ((comp rq p n ⋯) (((comp r q rq hrq) k) g)) f = ((comp r qp n ⋯) k) (((comp q p qp hqp) g) f)} {comp_id : ∀ {X Y : C} {q : ℤ} (g : ↑((hom X Y).X q)), ((comp q 0 q ⋯) g) (id X) = g} {id_comp : ∀ {X Y : C} {p : ℤ} (f : ↑((hom X Y).X p)), ((comp 0 p p ⋯) (id Y)) f = f} (X : C) : (ofKeller hom (fun {X Y Z : C} => comp) id ⋯ ⋯ ⋯ ⋯).id X = id X

The explicit data of a differential graded category

noncomputable def TauCeti.dgCategoryData (R : Type v) [CommRing R] (C : Type u) [DGCategory R C] : DGCategoryData R C

The explicit Hom-complex data of a differential graded category: its Hom complexes, homogeneous composition, and identities. Its body is exposed so that its Hom complexes remain definitionally those of the category.

Equations

• One or more equations did not get rendered due to their size.

@[simp]

theorem TauCeti.dgCategoryData_hom (R : Type v) [CommRing R] (C : Type u) [DGCategory R C] (X Y : C) : (dgCategoryData R C).hom X Y = dgHomComplex R X Y

@[simp]

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

@[simp]

theorem TauCeti.dgCategoryData_id (R : Type v) [CommRing R] (C : Type u) [DGCategory R C] (X : C) : (dgCategoryData R C).id X = dgId R X

@[simp]

theorem TauCeti.DGCategoryData.enrichedId_dgCategoryData {R : Type v} [CommRing R] {C : Type u} [DGCategory R C] (X : C) : (dgCategoryData R C).enrichedId X = CategoryTheory.eId (CochainComplex (ModuleCat R) ℤ) X

The enriched identity of a differential graded category is the enriched identity of its explicit data.

@[simp]

theorem TauCeti.DGCategoryData.enrichedComp_dgCategoryData {R : Type v} [CommRing R] {C : Type u} [DGCategory R C] (X Y Z : C) : (dgCategoryData R C).enrichedComp X Y Z = CategoryTheory.eComp (CochainComplex (ModuleCat R) ℤ) X Y Z

The enriched composition of a differential graded category is the enriched composition of its explicit data.

@[simp]

theorem TauCeti.DGCategoryData.toDGCategory_dgCategoryData {R : Type v} [CommRing R] {C : Type u} [inst : DGCategory R C] : (dgCategoryData R C).toDGCategory = inst

Rebuilding a differential graded category from its explicit Hom-complex data recovers the category.

@[simp]

theorem TauCeti.DGCategoryData.dgCategoryData_toDGCategory {R : Type v} [CommRing R] {C : Type u} (D : DGCategoryData R C) : dgCategoryData R C = D

Extracting the explicit Hom-complex data of the category built from explicit data recovers the data.

noncomputable def TauCeti.DGCategoryData.equivDGCategory {R : Type v} [CommRing R] {C : Type u} : DGCategoryData R C ≃ DGCategory R C

The two presentations of a differential graded category agree: explicit Hom-complex data on C is the same as an enrichment of C in cochain complexes of R-modules.

Equations

• One or more equations did not get rendered due to their size.

@[simp]

theorem TauCeti.DGCategoryData.equivDGCategory_apply {R : Type v} [CommRing R] {C : Type u} (D : DGCategoryData R C) : equivDGCategory D = D.toDGCategory

@[simp]

theorem TauCeti.DGCategoryData.equivDGCategory_symm_apply {R : Type v} [CommRing R] {C : Type u} [inst : DGCategory R C] : equivDGCategory.symm inst = dgCategoryData R C