The endomorphism differential graded algebra of an object

For an object X of a differential graded category C over R, the homogeneous endomorphisms of X of all degrees form a differential graded algebra End(X) = ⨁ n, Hom^n(X, X): the product is composition, the unit is the identity, and the differential is the differential of the Hom complex. It is the passage from a DG category back to DG algebras: derived Morita theory describes the derived category generated by a compact generator G through modules over the endomorphism DG algebra of G.

The product is Keller-ordered composition, so that for homogeneous g of degree q and f of degree p the product g * f is g ∘ f, "first f, then g". Composition in a TauCeti.DGCategory is in Mathlib's enriched factor order instead, and the two orders differ by the Koszul sign:

g * f = (-1) ^ (p * q) • dgComp f g.

With this sign the Leibniz rule of the Hom complexes becomes the Leibniz rule d (g * f) = d g * f + (-1) ^ |g| • g * d f of a differential graded algebra, and the construction inverts the one-object DG category TauCeti.DGSingleObj of a DG algebra A: the endomorphism DG algebra of its unique object is A again, with no sign twist.

The algebra is the external direct sum of the Hom modules, graded by the copies of the summands (TauCeti.InternalGrading.gradedObjectPiece), and its ring structure is the one Mathlib builds on a direct sum from a graded ring structure on the summands (DirectSum.GRing, DirectSum.GAlgebra).

Main definitions

• TauCeti.DGEnd: the endomorphism algebra ⨁ n, Hom^n(X, X) of an object.
• TauCeti.DGEnd.grading: its grading by the degree of a morphism.
• TauCeti.DGEnd.differential: its differential, the differential of the Hom complex.

Main results

• TauCeti.DGEnd.lof_mul_lof: multiplication is Keller-ordered composition, with the Koszul sign (-1) ^ (p * q) relative to TauCeti.dgComp.
• TauCeti.DGEnd.one_def: the unit is the identity morphism.
• TauCeti.DGEnd.differential_lof: the differential is the differential of the Hom complex.
• TauCeti.DGEnd.isDGAlgebra: the endomorphism algebra is a differential graded algebra.
• TauCeti.DGSingleObj.dgEndAlgEquiv, TauCeti.DGSingleObj.dgEndAlgEquiv_mem_iff and TauCeti.DGSingleObj.dgEndAlgEquiv_differential: the endomorphism DG algebra of the unique object of the one-object DG category of a DG algebra A is isomorphic to A, compatibly with the gradings and the differentials.

References

• B. Keller, Deriving DG categories, Section 1.
• B. Keller, Introduction to A-infinity algebras and modules, Section 3.1.

The graded ring of homogeneous endomorphisms

@[instance_reducible]

noncomputable instance TauCeti.DGEnd.gOne {R : Type v} [CommRing R] {C : Type u} [DGCategory R C] (X : C) : GradedMonoid.GOne fun (n : ℤ) => DGHom R n X X

The unit of the graded ring of homogeneous endomorphisms: the identity.

Equations

• TauCeti.DGEnd.gOne X = { one := TauCeti.dgId R X }

@[instance_reducible]

noncomputable instance TauCeti.DGEnd.gMul {R : Type v} [CommRing R] {C : Type u} [DGCategory R C] (X : C) : GradedMonoid.GMul fun (n : ℤ) => DGHom R n X X

The product of the graded ring of homogeneous endomorphisms: Keller-ordered composition, g * f = (-1) ^ (q * p) • dgComp f g for g of degree q and f of degree p.

Equations

• TauCeti.DGEnd.gMul X = { mul := fun {q p : ℤ} (g : TauCeti.DGHom R q X X) (f : TauCeti.DGHom R p X X) => (q * p).negOnePow • TauCeti.dgComp R f g ⋯ }

theorem TauCeti.DGEnd.gOne_def {R : Type v} [CommRing R] {C : Type u} [DGCategory R C] (X : C) : GradedMonoid.GOne.one = dgId R X

The unit of the graded ring of homogeneous endomorphisms is the identity.

theorem TauCeti.DGEnd.gMul_def {R : Type v} [CommRing R] {C : Type u} [DGCategory R C] (X : C) {q p : ℤ} (g : DGHom R q X X) (f : DGHom R p X X) : GradedMonoid.GMul.mul g f = (q * p).negOnePow • dgComp R f g ⋯

The product of the graded ring of homogeneous endomorphisms is Keller-ordered composition.

@[instance_reducible]

noncomputable instance TauCeti.DGEnd.gMonoid {R : Type v} [CommRing R] {C : Type u} [DGCategory R C] (X : C) : GradedMonoid.GMonoid fun (n : ℤ) => DGHom R n X X

The homogeneous endomorphisms of an object form a graded monoid under Keller-ordered composition.

Equations

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

@[instance_reducible]

noncomputable instance TauCeti.DGEnd.gRing {R : Type v} [CommRing R] {C : Type u} [DGCategory R C] (X : C) : DirectSum.GRing fun (n : ℤ) => DGHom R n X X

The homogeneous endomorphisms of an object form a graded ring under Keller-ordered composition.

Equations

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

@[instance_reducible]

noncomputable instance TauCeti.DGEnd.gAlgebra {R : Type v} [CommRing R] {C : Type u} [DGCategory R C] (X : C) : DirectSum.GAlgebra R fun (n : ℤ) => DGHom R n X X

The homogeneous endomorphisms of an object form a graded R-algebra: a scalar r acts as the degree-zero endomorphism r • dgId R X.

Equations

• TauCeti.DGEnd.gAlgebra X = { toFun := (LinearMap.toSpanSingleton R (TauCeti.DGHom R 0 X X) (TauCeti.dgId R X)).toAddMonoidHom, map_one := ⋯, map_mul := ⋯, commutes := ⋯, smul_def := ⋯ }

The endomorphism algebra

@[reducible, inline]

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

The endomorphism algebra of an object X of a differential graded category: the direct sum ⨁ n, Hom^n(X, X) of its homogeneous endomorphisms, with Keller-ordered composition as product and the identity as unit.

Equations

• TauCeti.DGEnd R X = DirectSum ℤ fun (n : ℤ) => TauCeti.DGHom R n X X

@[simp]

theorem TauCeti.DGEnd.lof_mul_lof {R : Type v} [CommRing R] {C : Type u} [DGCategory R C] {X : C} {p q n : ℤ} (g : DGHom R q X X) (f : DGHom R p X X) (h : p + q = n) : (DirectSum.lof R ℤ (fun (n : ℤ) => DGHom R n X X) q) g * (DirectSum.lof R ℤ (fun (n : ℤ) => DGHom R n X X) p) f = (DirectSum.lof R ℤ (fun (n : ℤ) => DGHom R n X X) n) ((p * q).negOnePow • dgComp R f g h)

Multiplication in the endomorphism algebra is Keller-ordered composition: for g of degree q and f of degree p, the product g * f is "first f, then g", which is the enriched composite dgComp f g up to the Koszul sign (-1) ^ (p * q).

theorem TauCeti.DGEnd.one_def {R : Type v} [CommRing R] {C : Type u} [DGCategory R C] {X : C} : 1 = (DirectSum.lof R ℤ (fun (n : ℤ) => DGHom R n X X) 0) (dgId R X)

The unit of the endomorphism algebra is the identity morphism.

theorem TauCeti.DGEnd.algebraMap_apply {R : Type v} [CommRing R] {C : Type u} [DGCategory R C] {X : C} (r : R) : (algebraMap R (DGEnd R X)) r = (DirectSum.lof R ℤ (fun (n : ℤ) => DGHom R n X X) 0) (r • dgId R X)

A scalar acts on the endomorphism algebra as a multiple of the identity morphism.

The grading

@[reducible, inline]

abbrev TauCeti.DGEnd.grading (R : Type v) [CommRing R] {C : Type u} [DGCategory R C] (X : C) (n : ℤ) : Submodule R (DGEnd R X)

The grading of the endomorphism algebra by the degree of a morphism: the degree-n part is the copy of Hom^n(X, X).

Equations

• TauCeti.DGEnd.grading R X n = TauCeti.InternalGrading.gradedObjectPiece R (TauCeti.dgHomComplex R X X).X n

theorem TauCeti.DGEnd.lof_mem_grading {R : Type v} [CommRing R] {C : Type u} [DGCategory R C] {X : C} {n : ℤ} (f : DGHom R n X X) : (DirectSum.lof R ℤ (fun (n : ℤ) => DGHom R n X X) n) f ∈ grading R X n

A homogeneous endomorphism of degree n lies in the degree-n part.

theorem TauCeti.DGEnd.mem_grading_iff {R : Type v} [CommRing R] {C : Type u} [DGCategory R C] {X : C} {n : ℤ} {a : DGEnd R X} : a ∈ grading R X n ↔ ∃ (f : DGHom R n X X), (DirectSum.lof R ℤ (fun (n : ℤ) => DGHom R n X X) n) f = a

The degree-n part consists of the homogeneous endomorphisms of degree n.

instance TauCeti.DGEnd.instGradedMonoidIntSubmoduleGrading {R : Type v} [CommRing R] {C : Type u} [DGCategory R C] {X : C} : SetLike.GradedMonoid (grading R X)

The grading of the endomorphism algebra respects the unit and the multiplication: the identity has degree 0, and a product of homogeneous endomorphisms of degrees q and p has degree q + p.

@[instance_reducible]

noncomputable instance TauCeti.DGEnd.gradedAlgebra (R : Type v) [CommRing R] {C : Type u} [DGCategory R C] (X : C) : GradedAlgebra (grading R X)

The endomorphism algebra is graded by the degree of a morphism.

Equations

• TauCeti.DGEnd.gradedAlgebra R X = ⋯.gradedAlgebra

The differential

noncomputable def TauCeti.DGEnd.differential (R : Type v) [CommRing R] {C : Type u} [DGCategory R C] (X : C) : DGEnd R X →ₗ[R] DGEnd R X

The differential of the endomorphism algebra: the differential of the Hom complex, applied in every degree.

Equations

• TauCeti.DGEnd.differential R X = DirectSum.toModule R ℤ (TauCeti.DGEnd R X) fun (n : ℤ) => DirectSum.lof R ℤ (fun (n : ℤ) => TauCeti.DGHom R n X X) (n + 1) ∘ₗ TauCeti.dgDifferential R n

@[simp]

theorem TauCeti.DGEnd.differential_lof {R : Type v} [CommRing R] {C : Type u} [DGCategory R C] {X : C} {n : ℤ} (f : DGHom R n X X) : (differential R X) ((DirectSum.lof R ℤ (fun (n : ℤ) => DGHom R n X X) n) f) = (DirectSum.lof R ℤ (fun (n : ℤ) => DGHom R n X X) (n + 1)) ((dgDifferential R n) f)

The differential of the endomorphism algebra is the differential of the Hom complex.

theorem TauCeti.DGEnd.isDGAlgebra {R : Type v} [CommRing R] {C : Type u} [DGCategory R C] {X : C} : IsDGAlgebra (grading R X) (differential R X)

The endomorphism algebra of an object is a differential graded algebra.

The endomorphism algebra of the one-object category of a DG algebra

noncomputable def TauCeti.DGSingleObj.dgEndAlgEquiv {R A : Type v} [CommRing R] [Ring A] [Algebra R A] {𝒜 : ℤ → Submodule R A} [GradedAlgebra 𝒜] {d : A →ₗ[R] A} (h : IsDGAlgebra 𝒜 d) : DGEnd R (star h) ≃ₐ[R] A

The endomorphism algebra of the one-object DG category of a DG algebra A is A. A degree-n endomorphism of the unique object is sent to the element of 𝒜 n it names; with the Keller-ordered product of TauCeti.DGEnd this is multiplicative, with no sign twist.

Equations

• TauCeti.DGSingleObj.dgEndAlgEquiv h = AlgEquiv.ofLinearEquiv (TauCeti.DGSingleObj.dgEndLinearEquiv✝ h) ⋯ ⋯

@[simp]

theorem TauCeti.DGSingleObj.dgEndAlgEquiv_lof {R A : Type v} [CommRing R] [Ring A] [Algebra R A] {𝒜 : ℤ → Submodule R A} [GradedAlgebra 𝒜] {d : A →ₗ[R] A} (h : IsDGAlgebra 𝒜 d) {n : ℤ} (f : DGHom R n (star h) (star h)) : (dgEndAlgEquiv h) ((DirectSum.lof R ℤ (fun (n : ℤ) => DGHom R n (star h) (star h)) n) f) = ↑(((star h).dgHomEquiv (star h) n) f)

The comparison sends a homogeneous endomorphism to the element of the algebra it names.

@[simp]

theorem TauCeti.DGSingleObj.dgEndAlgEquiv_mem_iff {R A : Type v} [CommRing R] [Ring A] [Algebra R A] {𝒜 : ℤ → Submodule R A} [GradedAlgebra 𝒜] {d : A →ₗ[R] A} (h : IsDGAlgebra 𝒜 d) {n : ℤ} {x : DGEnd R (star h)} : (dgEndAlgEquiv h) x ∈ 𝒜 n ↔ x ∈ DGEnd.grading R (star h) n

The comparison identifies the degree-n part of the endomorphism algebra with 𝒜 n.

@[simp]

theorem TauCeti.DGSingleObj.dgEndAlgEquiv_differential {R A : Type v} [CommRing R] [Ring A] [Algebra R A] {𝒜 : ℤ → Submodule R A} [GradedAlgebra 𝒜] {d : A →ₗ[R] A} (h : IsDGAlgebra 𝒜 d) (x : DGEnd R (star h)) : (dgEndAlgEquiv h) ((DGEnd.differential R (star h)) x) = d ((dgEndAlgEquiv h) x)

The comparison intertwines the differential of the endomorphism algebra with the differential of the algebra.