Magnitude conjecture

MagnitudeConjecture.Algebra.StringArrowRepresentedMap

Represented string-arrow maps #

This file records the coefficient-field-linear realization of a represented arrow map and its underlying range.

source
noncomputable def MagnitudeConjecture.BoundQuiver.StringPresentation.quotientObjectEquiv {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) :
Category P.relations ≃ Q

The objects of the quotient path category are exactly its displayed quiver vertices.

Instances For
    source
    @[simp]
    theorem MagnitudeConjecture.BoundQuiver.StringPresentation.quotientObjectEquiv_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) (z : Q) :
    P.quotientObjectEquiv (obj P.relations z) = z
    source
    @[simp]
    theorem MagnitudeConjecture.BoundQuiver.StringPresentation.quotientObjectEquiv_symm_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) (z : Q) :
    P.quotientObjectEquiv.symm z = obj P.relations z
    source
    @[reducible, inline]
    abbrev MagnitudeConjecture.BoundQuiver.StringPresentation.representedVertexHom {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) :
    Type u

    The underlying coefficient-field Hom space of a represented vertex module.

    Instances For
      source
      noncomputable def MagnitudeConjecture.BoundQuiver.StringPresentation.representedArrowKLinearMap {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) :
      P.representedVertexHom x →ₗ[k] P.representedVertexHom y

      Postcomposition with the arrow transformation as a coefficient-field linear map.

      Instances For
        source
        @[simp]
        theorem MagnitudeConjecture.BoundQuiver.StringPresentation.representedArrowLinearMap_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 y : Q} (a : x ⟶ y) (f : ↑(P.representedVertexModule x)) :
        (P.representedArrowLinearMap a) f = (P.representedArrowKLinearMap a) f
        source
        @[instance_reducible]
        noncomputable instance MagnitudeConjecture.BoundQuiver.StringPresentation.representedArrowLinearRangeModule {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) :
        Module k ↥(P.representedArrowLinearMap a).range
        source
        instance MagnitudeConjecture.BoundQuiver.StringPresentation.representedArrowLinearRangeIsScalarTower {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) :
        IsScalarTower k P.quotientCategoryAlgebraᵐᵒᵖ ↥(P.representedArrowLinearMap a).range