Documentation

TauCeti.CategoryTheory.Graded.Basic

Graded linear quivers #

A graded linear quiver over a commutative ring R is a collection of objects such that every ordered pair of objects carries an R-module of morphisms with an internal ℤ-grading. That is the whole of the data: there is no composition, no identity, and no law relating the morphisms of different pairs of objects.

The higher theories of this library are built on such a quiver rather than assumed in it. A differential graded category is a graded linear quiver together with a graded composition and identities which are unital and associative, and an A∞ category is a graded linear quiver together with operations mₙ of degree 2 - n in arity n for n ≥ 1. Composition is the operation m₂ of that structure and not a datum of the quiver, so a differential graded category is the subcase of an A∞ category in which m₂ is a strictly unital and strictly associative composition and the operations mₙ vanish for n ≥ 3. The differential is part of that structure rather than of the quiver as well: it is the degree-one operation d = m₁, and a differential graded category requires that it square to zero and be a graded derivation of the composition, d (f ∘ g) = d f ∘ g + (-1)^{|f|} f ∘ d g for morphisms f and g of degrees |f| and |g|.

The grading is internal: the morphisms of degree n are the submodule grHom X Y n of the hom module X → Y, and the submodule family is an internal direct sum, so every morphism is a finite and uniquely determined sum of morphisms of definite degrees, its degree-n component being DirectSum.decompose of the grading, as in TauCeti.InternalGrading. The same data is a CategoryTheory.GradedObject ℤ (ModuleCat R), which presents the homogeneous modules separately, through TauCeti.GradedLinearQuiver.gradedHom and the constructor TauCeti.GradedLinearQuiver.ofGradedHom; TauCeti.InternalGrading.toGradedObject and TauCeti.InternalGrading.ofGradedObject convert between the two presentations, and TauCeti.InternalGrading.ofGradedObjectToGradedObjectIso recovers the components F X Y of ofGradedHom F from its grading, degree by degree.

Main definitions #

Main results #

References #

source
class TauCeti.GradedLinearQuiver (R : Type w) [CommRing R] (C : Type u) :
Type (max (max u (v + 1)) w)

A graded linear quiver over a commutative ring R: a collection of objects C with, for each ordered pair of objects, an R-module homModule X Y of morphisms carrying an internal ℤ grading grading X Y.

There is no composition and no identity, and no law relating the data of different pairs of objects: they belong to the structure which a graded linear quiver carries, such as the A∞ structure whose operation m₂ is the composition.

The base ring is a commutative ring, as for the differential graded categories of TauCeti.

  • homModule : C → C → ModuleCat R

    The R-module of morphisms from X to Y.

  • grading (X Y : C) : InternalGrading R ↑(homModule X Y)

    The internal ℤ-grading of the hom module from X to Y.

Instances
    source
    @[instance_reducible]
    noncomputable def TauCeti.GradedLinearQuiver.ofGradedHom (R : Type w) [CommRing R] {C : Type u} (F : C → C → CategoryTheory.GradedObject ℤ (ModuleCat R)) :
    GradedLinearQuiver R C

    The graded linear quiver whose hom modules are the components of a graded object: the total module of morphisms X → Y is the external direct sum of the components of F X Y.

    The two fields of this quiver are homModule_ofGradedHom and grading_ofGradedHom, and InternalGrading.ofGradedObjectToGradedObjectIso recovers the graded object F itself, degree by degree, from the second of them.

    Equations
    • One or more equations did not get rendered due to their size.
    Instances For
      source
      @[simp]
      theorem TauCeti.GradedLinearQuiver.homModule_ofGradedHom (R : Type w) [CommRing R] {C : Type u} {F : C → C → CategoryTheory.GradedObject ℤ (ModuleCat R)} (X Y : C) :
      homModule X Y = ↧(DirectSum ℤ fun (p : ℤ) => ↑(F X Y p))

      The hom module between two objects of the graded linear quiver ofGradedHom F: the external direct sum of the components of F X Y.

      source
      @[simp]
      theorem TauCeti.GradedLinearQuiver.grading_ofGradedHom (R : Type w) [CommRing R] {C : Type u} {F : C → C → CategoryTheory.GradedObject ℤ (ModuleCat R)} (X Y : C) :
      grading X Y = InternalGrading.ofGradedObject R (F X Y)

      The internal grading between two objects of the graded linear quiver ofGradedHom F is the canonical grading of the external direct sum of the components of F X Y.

      source
      @[reducible, inline]
      abbrev TauCeti.GradedLinearQuiver.grHom (R : Type w) [CommRing R] {C : Type u} [GradedLinearQuiver R C] (X Y : C) (n : ℤ) :
      Type v

      The morphisms from X to Y of cohomological degree n, as the R-module (grading X Y).piece n.

      Equations
      Instances For
        source
        @[reducible, inline]
        abbrev TauCeti.GradedLinearQuiver.gradedHom (R : Type w) [CommRing R] {C : Type u} [GradedLinearQuiver R C] (X Y : C) :
        CategoryTheory.GradedObject ℤ (ModuleCat R)

        The hom modules of a graded linear quiver as a graded object: the component in the degree n is the module of the morphisms of that degree.

        Equations
        Instances For
          source
          def TauCeti.GradedLinearQuiver.grHomReindex (R : Type w) [CommRing R] {C : Type u} [GradedLinearQuiver R C] {X Y : C} {n k : ℤ} (h : n = k) (f : grHom R X Y n) :
          grHom R X Y k

          Record a morphism of degree n as a morphism of degree k, along an equation h : n = k of degrees. The underlying morphism is unchanged.

          Equations
          Instances For
            source
            @[simp]
            theorem TauCeti.GradedLinearQuiver.val_grHomReindex (R : Type w) [CommRing R] {C : Type u} [GradedLinearQuiver R C] {X Y : C} {n k : ℤ} (h : n = k) (f : grHom R X Y n) :
            ↑(grHomReindex R h f) = ↑f

            Reindexing a homogeneous morphism does not change the underlying morphism.

            source
            @[simp]
            theorem TauCeti.GradedLinearQuiver.grHomReindex_refl (R : Type w) [CommRing R] {C : Type u} [GradedLinearQuiver R C] {X Y : C} {n : ℤ} (f : grHom R X Y n) :
            grHomReindex R ⋯ f = f

            A homogeneous morphism reindexed by reflexivity is the morphism itself.

            source
            @[simp]
            theorem TauCeti.GradedLinearQuiver.grHomReindex_trans (R : Type w) [CommRing R] {C : Type u} [GradedLinearQuiver R C] {X Y : C} {n k l : ℤ} (h₁ : n = k) (h₂ : k = l) (f : grHom R X Y n) :
            grHomReindex R h₂ (grHomReindex R h₁ f) = grHomReindex R ⋯ f

            A homogeneous morphism reindexed successively along two equations of degrees is the morphism reindexed along their composition.

            An example #

            A graded linear quiver with two objects, carrying a copy of R in each of the degrees 0 and 1 and no morphism in any other degree. The same graded object of components is assigned to every ordered pair of objects, so the total hom module of such a pair is the external direct sum ⨁ p, twoObjModule R p. The ring of the example is taken in the universe of the hom modules, so that a copy of R is one of their components.