Magnitude conjecture

MagnitudeConjecture.CategoryTheory.LinearPathCategory

The free linear category on a quiver #

This constructs a linear category whose objects are the vertices of a quiver and whose morphisms are finite linear combinations of paths. The construction uses the representable projective quiver representations, so associativity and linearity of composition come from the functor category. It is adapted from the Tau Ceti-derived quiver foundation used by the sibling subcat-research formalization, with only the path-category interface retained here.

source
@[reducible, inline]
abbrev MagnitudeConjecture.LinearPathCategory.QuiverRep (k : Type u) (Q : Type v) [Field k] [Quiver Q] :
Type (max (max v u_1) u_2 v u (u_2 + 1))

Representations of a quiver over k.

Instances For
    source
    @[simp]
    theorem MagnitudeConjecture.LinearPathCategory.QuiverRep.map_nil {k : Type u} [Field k] {Q : Type v} [Quiver Q] (M : QuiverRep k Q) (a : Q) :
    M.map Quiver.Path.nil = CategoryTheory.CategoryStruct.id (M.obj (have this := a; this))

    The trivial path acts as the identity in every quiver representation.

    source
    noncomputable def MagnitudeConjecture.LinearPathCategory.representable (k : Type u) (Q : Type v) [Field k] [Quiver Q] (i : Q) :
    QuiverRep k Q

    The representable projective at i, with path basis in every component.

    Instances For
      source
      noncomputable def MagnitudeConjecture.LinearPathCategory.representableBasis {k : Type u} [Field k] {Q : Type v} [Quiver Q] (i j : Q) :
      Module.Basis (Quiver.Path i j) k ↑((representable k Q i).obj (have this := j; this))

      Paths i ⟶ j form a basis of the j component of the representable at i.

      Instances For
        source
        @[simp]
        theorem MagnitudeConjecture.LinearPathCategory.representable_map_basis {k : Type u} [Field k] {Q : Type v} [Quiver Q] (i : Q) {a b : Q} (p : Quiver.Path a b) (q : Quiver.Path i a) :
        (CategoryTheory.ConcreteCategory.hom ((representable k Q i).map p)) ((representableBasis i a) q) = (representableBasis i b) (q.comp p)

        A path acts on a representable by concatenation.

        source
        instance MagnitudeConjecture.LinearPathCategory.finiteDimensional_representable_obj {k : Type u} [Field k] {Q : Type v} [Quiver Q] (i j : Q) [Finite (Quiver.Path i j)] :
        FiniteDimensional k ↑((representable k Q i).obj (have this := j; this))
        source
        noncomputable def MagnitudeConjecture.LinearPathCategory.representableHom {k : Type u} [Field k] {Q : Type v} [Quiver Q] (i : Q) (M : QuiverRep k Q) (x : ↑(M.obj (have this := i; this))) :
        representable k Q i ⟶ M

        The morphism from a representable determined by an element at its representing vertex.

        Instances For
          source
          @[simp]
          theorem MagnitudeConjecture.LinearPathCategory.representableHom_app_basis {k : Type u} [Field k] {Q : Type v} [Quiver Q] (i : Q) (M : QuiverRep k Q) (x : ↑(M.obj (have this := i; this))) (j : Q) (p : Quiver.Path i j) :
          (CategoryTheory.ConcreteCategory.hom ((representableHom i M x).app j)) ((representableBasis i j) p) = (CategoryTheory.ConcreteCategory.hom (M.map p)) x
          source
          theorem MagnitudeConjecture.LinearPathCategory.representableHom_app_nil {k : Type u} [Field k] {Q : Type v} [Quiver Q] (i : Q) (M : QuiverRep k Q) (x : ↑(M.obj (have this := i; this))) :
          (CategoryTheory.ConcreteCategory.hom ((representableHom i M x).app i)) ((representableBasis i i) Quiver.Path.nil) = x
          source
          @[simp]
          theorem MagnitudeConjecture.LinearPathCategory.representableHom_app_nil_self {k : Type u} [Field k] {Q : Type v} [Quiver Q] {i : Q} {M : QuiverRep k Q} (f : representable k Q i ⟶ M) :
          representableHom i M ((CategoryTheory.ConcreteCategory.hom (f.app i)) ((representableBasis i i) Quiver.Path.nil)) = f
          source
          noncomputable def MagnitudeConjecture.LinearPathCategory.representableHomEquiv {k : Type u} [Field k] {Q : Type v} [Quiver Q] (i : Q) (M : QuiverRep k Q) :
          (representable k Q i ⟶ M) ≃ₗ[k] ↑(M.obj (have this := i; this))

          The Yoneda-style linear equivalence between morphisms out of a representable and the corresponding vertex component.

          Instances For
            source
            @[simp]
            theorem MagnitudeConjecture.LinearPathCategory.representableHomEquiv_apply {k : Type u} [Field k] {Q : Type v} [Quiver Q] (i : Q) (M : QuiverRep k Q) (f : representable k Q i ⟶ M) :
            (representableHomEquiv i M) f = (CategoryTheory.ConcreteCategory.hom (f.app i)) ((representableBasis i i) Quiver.Path.nil)
            source
            @[simp]
            theorem MagnitudeConjecture.LinearPathCategory.representableHomEquiv_symm_apply {k : Type u} [Field k] {Q : Type v} [Quiver Q] (i : Q) (M : QuiverRep k Q) (x : ↑(M.obj (have this := i; this))) :
            (representableHomEquiv i M).symm x = representableHom i M x
            source
            @[reducible, inline]
            abbrev MagnitudeConjecture.LinearPathCategory.Category (k : Type u) [Field k] (Q : Type v) [Quiver Q] :
            Type v

            The free linear path category, realized as the full subcategory of quiver representations on the representables.

            Instances For
              source
              def MagnitudeConjecture.LinearPathCategory.obj (k : Type u) [Field k] (Q : Type v) [Quiver Q] (x : Q) :
              Category k Q

              A quiver vertex as an object of the free linear path category.

              Instances For
                source
                def MagnitudeConjecture.LinearPathCategory.vertex {k : Type u} [Field k] {Q : Type v} [Quiver Q] (x : Category k Q) :
                Q

                The underlying quiver vertex of an object of the free linear category.

                Instances For
                  source
                  noncomputable def MagnitudeConjecture.LinearPathCategory.homPathLinearEquiv {k : Type u} [Field k] {Q : Type v} [Quiver Q] (x y : Category k Q) :
                  (x ⟶ y) ≃ₗ[k] Quiver.Path (vertex y) (vertex x) →₀ k

                  Morphisms in the free linear category are finite linear combinations of paths, with the path direction reversed by the representable convention.

                  Instances For
                    source
                    noncomputable def MagnitudeConjecture.LinearPathCategory.pathHom {k : Type u} [Field k] {Q : Type v} [Quiver Q] {x y : Category k Q} (p : Quiver.Path (vertex y) (vertex x)) :
                    x ⟶ y

                    The morphism represented by one path.

                    Instances For
                      source
                      noncomputable def MagnitudeConjecture.LinearPathCategory.homPathBasis {k : Type u} [Field k] {Q : Type v} [Quiver Q] (x y : Category k Q) :
                      Module.Basis (Quiver.Path (vertex y) (vertex x)) k (x ⟶ y)

                      Paths form a basis of every Hom space.

                      Instances For
                        source
                        @[simp]
                        theorem MagnitudeConjecture.LinearPathCategory.homPathBasis_apply {k : Type u} [Field k] {Q : Type v} [Quiver Q] (x y : Category k Q) (p : Quiver.Path (vertex y) (vertex x)) :
                        (homPathBasis x y) p = pathHom p
                        source
                        instance MagnitudeConjecture.LinearPathCategory.homModuleFinite {k : Type u} [Field k] {Q : Type v} [Quiver Q] (x y : Category k Q) [Finite (Quiver.Path (vertex y) (vertex x))] :
                        Module.Finite k (x ⟶ y)
                        source
                        @[simp]
                        theorem MagnitudeConjecture.LinearPathCategory.homPathLinearEquiv_pathHom {k : Type u} [Field k] {Q : Type v} [Quiver Q] {x y : Category k Q} (p : Quiver.Path (vertex y) (vertex x)) :
                        (homPathLinearEquiv x y) (pathHom p) = Finsupp.single p 1
                        source
                        @[simp]
                        theorem MagnitudeConjecture.LinearPathCategory.homPathLinearEquiv_id {k : Type u} [Field k] {Q : Type v} [Quiver Q] (x : Category k Q) :
                        (homPathLinearEquiv x x) (CategoryTheory.CategoryStruct.id x) = Finsupp.single Quiver.Path.nil 1
                        source
                        @[simp]
                        theorem MagnitudeConjecture.LinearPathCategory.pathHom_nil {k : Type u} [Field k] {Q : Type v} [Quiver Q] (x : Category k Q) :
                        pathHom Quiver.Path.nil = CategoryTheory.CategoryStruct.id x
                        source
                        theorem MagnitudeConjecture.LinearPathCategory.pathHom_hom {k : Type u} [Field k] {Q : Type v} [Quiver Q] {x y : Category k Q} (p : Quiver.Path (vertex y) (vertex x)) :
                        (pathHom p).hom = representableHom (vertex x) (representable k Q (vertex y)) ((representableBasis (vertex y) (vertex x)) p)

                        The natural transformation underlying a path-basis morphism.

                        source
                        @[simp]
                        theorem MagnitudeConjecture.LinearPathCategory.pathHom_comp {k : Type u} [Field k] {Q : Type v} [Quiver Q] {x y z : Category k Q} (p : Quiver.Path (vertex y) (vertex x)) (q : Quiver.Path (vertex z) (vertex y)) :
                        CategoryTheory.CategoryStruct.comp (pathHom p) (pathHom q) = pathHom (q.comp p)
                        source
                        theorem MagnitudeConjecture.LinearPathCategory.pathHom_comp_assoc {k : Type u} [Field k] {Q : Type v} [Quiver Q] {x y z : Category k Q} (p : Quiver.Path (vertex y) (vertex x)) (q : Quiver.Path (vertex z) (vertex y)) {Z : Category k Q} (h : z ⟶ Z) :
                        CategoryTheory.CategoryStruct.comp (pathHom p) (CategoryTheory.CategoryStruct.comp (pathHom q) h) = CategoryTheory.CategoryStruct.comp (pathHom (q.comp p)) h