Documentation

TauCeti.CategoryTheory.DG.SingleObj

The one-object differential graded category of a differential graded algebra #

A differential graded algebra (A, d) over R determines a differential graded category with a single object: the Hom complex of that object is the underlying cochain complex of A, the identity is 1, and composition is multiplication. This file constructs that category, TauCeti.DGSingleObj h, for a DG algebra h : IsDGAlgebra π’œ d.

Multiplication is Keller-ordered composition: for homogeneous a and b, the product a * b is a ∘ b, "first b, then a", so that the Leibniz rule d (a * b) = d a * b + (-1) ^ |a| β€’ a * d b is the Leibniz rule of Keller composition. Composition in a TauCeti.DGCategory is in Mathlib's enriched factor order instead, and the two orders differ by the Koszul sign: for f of degree p and g of degree q,

dgComp f g = (-1) ^ (p * q) β€’ (g * f).

This is TauCeti.DGSingleObj.dgHomEquiv_dgComp, the sign-bridge between the algebra and the category conventions.

The degree-n morphisms of the single object are the degree-n part of A, TauCeti.DGSingleObj.dgHomEquiv, and under this identification the differential, the identity and composition are d, 1 and signed multiplication. These are the public interface to the construction.

Main definitions #

Main results #

References #

source
structure TauCeti.DGSingleObj {R A : Type u} [CommRing R] [Ring A] [Algebra R A] {π’œ : β„€ β†’ Submodule R A} [GradedAlgebra π’œ] {d : A β†’β‚—[R] A} (h : IsDGAlgebra π’œ d) :
Type

The objects of the one-object differential graded category of a DG algebra h : IsDGAlgebra π’œ d: a single object TauCeti.DGSingleObj.star h, whose Hom complex is the underlying cochain complex of A and whose composition is multiplication.

The type is a structure indexed by h, so that objects of the categories of different DG algebras are not interchangeable.

    Instances For
      source
      def TauCeti.DGSingleObj.star {R A : Type u} [CommRing R] [Ring A] [Algebra R A] {π’œ : β„€ β†’ Submodule R A} [GradedAlgebra π’œ] {d : A β†’β‚—[R] A} (h : IsDGAlgebra π’œ d) :
      DGSingleObj h

      The unique object of the one-object differential graded category.

      Equations
      Instances For
        source
        @[instance_reducible]
        instance TauCeti.DGSingleObj.instUnique {R A : Type u} [CommRing R] [Ring A] [Algebra R A] {π’œ : β„€ β†’ Submodule R A} [GradedAlgebra π’œ] {d : A β†’β‚—[R] A} (h : IsDGAlgebra π’œ d) :
        Unique (DGSingleObj h)
        Equations

        The Hom complex #

        source
        noncomputable def TauCeti.DGSingleObj.homComplexData {R A : Type u} [CommRing R] [Ring A] [Algebra R A] {π’œ : β„€ β†’ Submodule R A} [GradedAlgebra π’œ] {d : A β†’β‚—[R] A} (h : IsDGAlgebra π’œ d) :
        DGCategoryData R (DGSingleObj h)

        The explicit Hom-complex data of the one-object differential graded category, from Keller-ordered composition given by multiplication.

        Equations
        • One or more equations did not get rendered due to their size.
        Instances For
          source
          @[instance_reducible]
          noncomputable instance TauCeti.DGSingleObj.instDGCategory {R A : Type u} [CommRing R] [Ring A] [Algebra R A] {π’œ : β„€ β†’ Submodule R A} [GradedAlgebra π’œ] {d : A β†’β‚—[R] A} (h : IsDGAlgebra π’œ d) :
          DGCategory R (DGSingleObj h)

          The one-object differential graded category of a DG algebra.

          Equations

          Morphisms, differential, identity and composition #

          source
          theorem TauCeti.DGSingleObj.dgHomComplex_eq {R A : Type u} [CommRing R] [Ring A] [Algebra R A] {π’œ : β„€ β†’ Submodule R A} [GradedAlgebra π’œ] {d : A β†’β‚—[R] A} {h : IsDGAlgebra π’œ d} (X Y : DGSingleObj h) :
          dgHomComplex R X Y = gradedCochainComplex π’œ d β‹― β‹―

          The Hom complex of the one-object differential graded category is the underlying cochain complex of the algebra.

          source
          noncomputable def TauCeti.DGSingleObj.dgHomEquiv {R A : Type u} [CommRing R] [Ring A] [Algebra R A] {π’œ : β„€ β†’ Submodule R A} [GradedAlgebra π’œ] {d : A β†’β‚—[R] A} {h : IsDGAlgebra π’œ d} (X Y : DGSingleObj h) (n : β„€) :
          DGHom R n X Y ≃ₗ[R] β†₯(π’œ n)

          The degree-n morphisms of the one-object differential graded category are the degree-n part of the algebra.

          Equations
          Instances For
            source
            @[simp]
            theorem TauCeti.DGSingleObj.dgHomEquiv_dgDifferential {R A : Type u} [CommRing R] [Ring A] [Algebra R A] {π’œ : β„€ β†’ Submodule R A} [GradedAlgebra π’œ] {d : A β†’β‚—[R] A} {h : IsDGAlgebra π’œ d} {X Y : DGSingleObj h} (n : β„€) (f : DGHom R n X Y) :
            ↑((X.dgHomEquiv Y (n + 1)) ((dgDifferential R n) f)) = d ↑((X.dgHomEquiv Y n) f)

            The differential of the one-object differential graded category is the differential of the algebra.

            source
            @[simp]
            theorem TauCeti.DGSingleObj.dgHomEquiv_dgId {R A : Type u} [CommRing R] [Ring A] [Algebra R A] {π’œ : β„€ β†’ Submodule R A} [GradedAlgebra π’œ] {d : A β†’β‚—[R] A} {h : IsDGAlgebra π’œ d} (X : DGSingleObj h) :
            ↑((X.dgHomEquiv X 0) (dgId R X)) = 1

            The identity of the one-object differential graded category is the unit of the algebra.

            source
            @[simp]
            theorem TauCeti.DGSingleObj.dgHomEquiv_dgComp {R A : Type u} [CommRing R] [Ring A] [Algebra R A] {π’œ : β„€ β†’ Submodule R A} [GradedAlgebra π’œ] {d : A β†’β‚—[R] A} {h : IsDGAlgebra π’œ d} {X Y Z : DGSingleObj h} {p q n : β„€} (f : DGHom R p X Y) (g : DGHom R q Y Z) (hpq : p + q = n) :
            ↑((X.dgHomEquiv Z n) (dgComp R f g hpq)) = (p * q).negOnePow β€’ (↑((Y.dgHomEquiv Z q) g) * ↑((X.dgHomEquiv Y p) f))

            Composition in the one-object differential graded category is multiplication. Since dgComp f g is f followed by g while g * f is the Keller composite "first f, then g", the two differ by the Koszul sign (-1) ^ (p * q).