Twisted objects of a differential graded category

A twisted object of a differential graded category C is an object X together with a degree-one endomorphism δ satisfying the Maurer–Cartan equation. In Mathlib's enriched factor order, where dgComp f g is f followed by g, that equation reads

d δ = dgComp δ δ.

In Keller's order, δ ∘ δ = (-1)^(1 * 1) • dgComp δ δ = -dgComp δ δ, so it is the familiar d δ + δ ∘ δ = 0 (TauCeti.DGTwistedObject.dgDifferential_twist_add_negOnePow_smul_dgComp_eq_zero).

The twisted objects form a differential graded category TauCeti.DGTwistedObject R C. A morphism (X, δ_X) ⟶ (Y, δ_Y) of degree n is a morphism f : X ⟶ Y of degree n in C, composition and identities are those of C, and the differential is twisted:

D f = d f + (-1)^n • dgComp f δ_Y - dgComp δ_X f.

In Keller's order this is D f = d f + δ_Y ∘ f - (-1)^n • f ∘ δ_X. The twisted differential squares to zero exactly because of the Maurer–Cartan equations of δ_X and δ_Y: expanding D (D f) with the Leibniz rule and associativity leaves dgComp f (d δ_Y - dgComp δ_Y δ_Y) - dgComp (d δ_X - dgComp δ_X δ_X) f. The Leibniz rule for D holds for arbitrary degree-one endomorphisms, by associativity alone.

Twisted objects are the formal analogue of perturbing the differential of a complex by a degree-one endomorphism. Applied to the additive closure of the shift closure of C, whose objects are formal sums ⊕ᵢ Xᵢ[rᵢ], the twisted objects with strictly upper-triangular twisting matrix are the one-sided twisted complexes of Bondal and Kapranov, which form the pretriangulated envelope of C.

Every object X of C is a twisted object with zero twist, and X ↦ (X, 0) is a DG functor TauCeti.DGTwistedObject.embedding which is an isomorphism on Hom complexes. A DG functor F : C ⥤ D preserves the Maurer–Cartan equation, so it induces a DG functor F.mapDGTwistedObject sending (X, δ) to (F X, F δ).

Main definitions

• TauCeti.DGTwistedObject: an object with a degree-one endomorphism satisfying the Maurer–Cartan equation.
• TauCeti.DGTwistedObject.homComplexData: the explicit Hom-complex data of twisted objects, with the twisted differential.
• TauCeti.DGTwistedObject.dgHomEquiv: degree-n morphisms of twisted objects are degree-n morphisms of the underlying objects.
• TauCeti.DGTwistedObject.embedding: the DG functor X ↦ (X, 0).
• CategoryTheory.EnrichedFunctor.mapDGTwistedObject: the DG functor (X, δ) ↦ (F X, F δ) induced by a DG functor F.

Main results

• TauCeti.DGTwistedObject.dgHomEquiv_dgDifferential: the differential is the twisted differential d f + (-1)^n • dgComp f δ_Y - dgComp δ_X f.
• TauCeti.DGTwistedObject.dgHomEquiv_dgComp and TauCeti.DGTwistedObject.dgHomEquiv_dgId: composition and identities are those of C.
• TauCeti.DGTwistedObject.isIso_embedding_map: the embedding is an isomorphism on Hom complexes.

References

• A. I. Bondal and M. M. Kapranov, Enhanced triangulated categories, Section 1.
• V. Drinfeld, DG quotients of DG categories, Section 2.4.
• B. Keller, Introduction to A-infinity algebras and modules, Section 7.6, for the twisting equation d δ + δ ∘ δ = 0 in Keller's order.

structure TauCeti.DGTwistedObject (R : Type v) [CommRing R] (C : Type u) [DGCategory R C] : Type (max u v)

A twisted object of a differential graded category: an object obj with a degree-one endomorphism twist satisfying the Maurer–Cartan equation d δ = dgComp δ δ, which in Keller's order is d δ + δ ∘ δ = 0. The twisted objects form a differential graded category whose Hom complexes carry the twisted differential; see TauCeti.DGTwistedObject.homComplexData.

• obj : C

  The underlying object.

• twist : DGHom R 1 self.obj self.obj

  The twisting endomorphism δ, of degree one.

• dgDifferential_twist : (dgDifferential R 1) self.twist = dgComp R self.twist self.twist ⋯

  The Maurer–Cartan equation d δ = dgComp δ δ, in Mathlib's enriched factor order.

theorem TauCeti.DGTwistedObject.dgDifferential_twist_add_negOnePow_smul_dgComp_eq_zero (R : Type v) [CommRing R] {C : Type u} [DGCategory R C] (X : DGTwistedObject R C) : (dgDifferential R 1) X.twist + (1 * 1).negOnePow • dgComp R X.twist X.twist ⋯ = 0

The Maurer–Cartan equation in Keller's order: d δ + δ ∘ δ = 0, where the Keller-ordered composite is δ ∘ δ = (-1)^(1 * 1) • dgComp δ δ.

The twisted differential

The Hom-complex data

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

The explicit Hom-complex data of twisted objects: the morphisms of C with the twisted differential d f + (-1)^n • dgComp f δ_Y - dgComp δ_X f, and the composition and identities of C.

@[instance_reducible]

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

The differential graded category of twisted objects of a differential graded category, with the twisted differential on Hom complexes.

Morphisms, differential, composition and identity

noncomputable def TauCeti.DGTwistedObject.dgHomEquiv (R : Type v) [CommRing R] {C : Type u} [DGCategory R C] (X Y : DGTwistedObject R C) (n : ℤ) : DGHom R n X Y ≃ₗ[R] DGHom R n X.obj Y.obj

A morphism (X, δ_X) ⟶ (Y, δ_Y) of degree n of twisted objects is a morphism X ⟶ Y of degree n in C.

@[simp]

theorem TauCeti.DGTwistedObject.dgHomEquiv_dgDifferential (R : Type v) [CommRing R] {C : Type u} [DGCategory R C] {X Y : DGTwistedObject R C} (n : ℤ) (f : DGHom R n X Y) : (dgHomEquiv R X Y (n + 1)) ((dgDifferential R n) f) = (dgDifferential R n) ((dgHomEquiv R X Y n) f) + n.negOnePow • dgComp R ((dgHomEquiv R X Y n) f) Y.twist ⋯ - dgComp R X.twist ((dgHomEquiv R X Y n) f) ⋯

The twisted differential: the differential of a degree-n morphism of twisted objects is d f + (-1)^n • dgComp f δ_Y - dgComp δ_X f.

@[simp]

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

Composition of twisted objects is the composition of C.

@[simp]

theorem TauCeti.DGTwistedObject.dgHomEquiv_dgId (R : Type v) [CommRing R] {C : Type u} [DGCategory R C] (X : DGTwistedObject R C) : (dgHomEquiv R X X 0) (dgId R X) = dgId R X.obj

The identity of a twisted object is the identity of its underlying object.

The embedding X ↦ (X, 0)

@[reducible, inline]

abbrev TauCeti.DGTwistedObject.ofObj (R : Type v) [CommRing R] {C : Type u} [DGCategory R C] (X : C) : DGTwistedObject R C

An object of C with the zero twist, which satisfies the Maurer–Cartan equation since both sides vanish.

theorem TauCeti.DGTwistedObject.eq_ofObj_of_twist_eq_zero (R : Type v) [CommRing R] {C : Type u} [DGCategory R C] {X : DGTwistedObject R C} (h : X.twist = 0) : X = ofObj R X.obj

A twisted object with zero twist is its underlying object with the zero twist.

noncomputable def TauCeti.DGTwistedObject.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 (ofObj R X) (ofObj R Y)

The action of the embedding on morphisms of degree n: a degree-n morphism X ⟶ Y of C is a degree-n morphism (X, 0) ⟶ (Y, 0) of twisted objects.

@[simp]

theorem TauCeti.DGTwistedObject.dgHomEquiv_embeddingHomEquiv (R : Type v) [CommRing R] {C : Type u} [DGCategory R C] {X Y : C} {n : ℤ} (f : DGHom R n X Y) : (dgHomEquiv R (ofObj R X) (ofObj R Y) n) ((embeddingHomEquiv R X Y n) f) = f

The embedding does not change the underlying morphism.

theorem TauCeti.DGTwistedObject.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)

With zero twists, the twisted differential is the differential of C.

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

The DG functor from a differential graded category to its twisted objects sending X to the twisted object (X, 0).

@[simp]

theorem TauCeti.DGTwistedObject.embedding_obj (R : Type v) [CommRing R] {C : Type u} [DGCategory R C] (X : C) : (embedding R).obj X = ofObj R X

The embedding sends X to the twisted object (X, 0).

@[simp]

theorem TauCeti.DGTwistedObject.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.DGTwistedObject.embeddingHomEquiv.

instance TauCeti.DGTwistedObject.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 twisted objects.

Functoriality

@[reducible, inline]

noncomputable abbrev CategoryTheory.EnrichedFunctor.mapDGTwistedObjectObj {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) (X : TauCeti.DGTwistedObject R C) : TauCeti.DGTwistedObject R D

The image (F X, F δ) of a twisted object under a DG functor: F preserves the Maurer–Cartan equation since it commutes with the differential and with composition.

noncomputable def CategoryTheory.EnrichedFunctor.mapDGTwistedObjectHom {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) (X Y : TauCeti.DGTwistedObject R C) (n : ℤ) : TauCeti.DGHom R n X Y →ₗ[R] TauCeti.DGHom R n (F.mapDGTwistedObjectObj X) (F.mapDGTwistedObjectObj Y)

The action of a DG functor on morphisms of twisted objects of degree n: its action on the underlying morphisms.

@[simp]

theorem CategoryTheory.EnrichedFunctor.dgHomEquiv_mapDGTwistedObjectHom {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) {X Y : TauCeti.DGTwistedObject R C} {n : ℤ} (f : TauCeti.DGHom R n X Y) : (TauCeti.DGTwistedObject.dgHomEquiv R (F.mapDGTwistedObjectObj X) (F.mapDGTwistedObjectObj Y) n) ((F.mapDGTwistedObjectHom X Y n) f) = (F.dgMap n) ((TauCeti.DGTwistedObject.dgHomEquiv R X Y n) f)

The underlying morphism of the image of a morphism is the image of its underlying morphism.

@[reducible, inline]

noncomputable abbrev CategoryTheory.EnrichedFunctor.mapDGTwistedObject {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.DGTwistedObject R C) (TauCeti.DGTwistedObject R D)

The DG functor between twisted objects induced by a DG functor F, sending (X, δ) to (F X, F δ) and acting by F on the underlying morphisms.

@[simp]

theorem CategoryTheory.EnrichedFunctor.dgMap_mapDGTwistedObject {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) {X Y : TauCeti.DGTwistedObject R C} {n : ℤ} (f : TauCeti.DGHom R n X Y) : (F.mapDGTwistedObject.dgMap n) f = (F.mapDGTwistedObjectHom X Y n) f

The induced DG functor acts on morphisms by CategoryTheory.EnrichedFunctor.mapDGTwistedObjectHom.

theorem CategoryTheory.EnrichedFunctor.dgHomEquiv_dgMap_mapDGTwistedObject {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) {X Y : TauCeti.DGTwistedObject R C} {n : ℤ} (f : TauCeti.DGHom R n X Y) : (TauCeti.DGTwistedObject.dgHomEquiv R (F.mapDGTwistedObject.obj X) (F.mapDGTwistedObject.obj Y) n) ((F.mapDGTwistedObject.dgMap n) f) = (F.dgMap n) ((TauCeti.DGTwistedObject.dgHomEquiv R X Y n) f)

The underlying morphism of the image of a morphism under the induced DG functor is the image of its underlying morphism.