Magnitude conjecture

MagnitudeConjecture.Algebra.StringArrowRightIdealObjectCoordinate

Object-indexed coordinates for represented string-arrow maps #

Keeping the biproduct coordinates indexed by the objects of the quotient path category avoids transporting a large dependent product along the equivalence with the displayed quiver vertices. Yoneda evaluation is performed directly in each object coordinate.

source
noncomputable def MagnitudeConjecture.BoundQuiver.StringPresentation.representedVertexObjectFiniteHomLinearEquiv {k A Q : Type u} [Field k] [Ring A] [Algebra k A] [Fintype Q] [Quiver Q] [(x y : Q) → Fintype (x ⟶ y)] (P : StringPresentation k A Q) (x : Q) (X : Category P.relations) :
P.representedVertexCoordinateFamily x X ≃ₗ[k] CoveringHom.linearCoyonedaLinearModule X ⟶ (P.quotientRepresentable (obj P.relations x)).obj

Forgetting the finite-dimensional-module subtype identifies a morphism between represented modules with the corresponding natural transformation.

Instances For
    source
    noncomputable def MagnitudeConjecture.BoundQuiver.StringPresentation.representedVertexObjectYonedaLinearEquiv {k A Q : Type u} [Field k] [Ring A] [Algebra k A] [Fintype Q] [Quiver Q] [(x y : Q) → Fintype (x ⟶ y)] (P : StringPresentation k A Q) (x : Q) :
    ((X : Category P.relations) → P.representedVertexCoordinateFamily x X) ≃ₗ[k] (X : Category P.relations) → obj P.relations x ⟶ X

    Linear Yoneda evaluation in coordinates indexed by quotient-category objects.

    Instances For
      source
      noncomputable def MagnitudeConjecture.BoundQuiver.StringPresentation.representedVertexCoordinateLinearEquiv {k A Q : Type u} [Field k] [Ring A] [Algebra k A] [Fintype Q] [Quiver Q] [(x y : Q) → Fintype (x ⟶ y)] (P : StringPresentation k A Q) (x : Q) :
      P.representedVertexHom x ≃ₗ[k] (X : Category P.relations) → obj P.relations x ⟶ X

      Biproduct restriction followed by linear Yoneda evaluation gives coordinates indexed directly by quotient-category objects.

      Instances For
        source
        @[simp]
        theorem MagnitudeConjecture.BoundQuiver.StringPresentation.representedVertexCoordinateLinearEquiv_apply {k A Q : Type u} [Field k] [Ring A] [Algebra k A] [Fintype Q] [Quiver Q] [(x y : Q) → Fintype (x ⟶ y)] (P : StringPresentation k A Q) (x : Q) (X : Category P.relations) (f : P.representedVertexHom x) :
        (P.representedVertexCoordinateLinearEquiv x) f X = (CategoryTheory.ConcreteCategory.hom ((CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.biproduct.ι P.quotientRepresentable X) f).hom.hom.app X)) (CategoryTheory.CategoryStruct.id (Opposite.unop (Opposite.op X)))
        source
        noncomputable def MagnitudeConjecture.BoundQuiver.StringPresentation.leftArrowCompositionLinearMapObj {k A Q : Type u} [Field k] [Ring A] [Algebra k A] [Fintype Q] [Quiver Q] [(x y : Q) → Fintype (x ⟶ y)] (P : StringPresentation k A Q) {x y : Q} (a : x ⟶ y) (X : Category P.relations) :
        (obj P.relations x ⟶ X) →ₗ[k] obj P.relations y ⟶ X

        Left composition by a displayed arrow at an arbitrary quotient-category object.

        Instances For
          source
          @[simp]
          theorem MagnitudeConjecture.BoundQuiver.StringPresentation.leftArrowCompositionLinearMapObj_obj {k A Q : Type u} [Field k] [Ring A] [Algebra k A] [Fintype Q] [Quiver Q] [(x y : Q) → Fintype (x ⟶ y)] (P : StringPresentation k A Q) {x y : Q} (a : x ⟶ y) (z : Q) :
          P.leftArrowCompositionLinearMapObj a (obj P.relations z) = P.leftArrowCompositionLinearMap a z
          source
          theorem MagnitudeConjecture.BoundQuiver.StringPresentation.representedVertexCoordinateLinearEquiv_arrow {k A Q : Type u} [Field k] [Ring A] [Algebra k A] [Fintype Q] [Quiver Q] [(x y : Q) → Fintype (x ⟶ y)] (P : StringPresentation k A Q) {x y : Q} (a : x ⟶ y) (f : P.representedVertexHom x) (X : Category P.relations) :
          (P.representedVertexCoordinateLinearEquiv y) ((P.representedArrowKLinearMap a) f) X = (P.leftArrowCompositionLinearMapObj a X) ((P.representedVertexCoordinateLinearEquiv x) f X)

          In object-indexed coordinates, the represented arrow map is pointwise left composition.

          source
          noncomputable def MagnitudeConjecture.BoundQuiver.StringPresentation.leftArrowCoordinateBasisObj {k A Q : Type u} [Field k] [Ring A] [Algebra k A] [Fintype Q] [Quiver Q] [(x y : Q) → Fintype (x ⟶ y)] (P : StringPresentation k A Q) {x y : Q} (a : x ⟶ y) (X : Category P.relations) :
          Module.Basis (P.LeftContinuationAt a (P.quotientObjectEquiv X)) k ↥(P.leftArrowCompositionLinearMapObj a X).range

          The pointwise continuation basis, stated at an arbitrary quotient-category object.

          Instances For