Magnitude conjecture

MagnitudeConjecture.Algebra.StringArrowRightIdealRangeK

Coefficient-field range of a represented string-arrow map #

The algebra-linear and coefficient-field-linear arrow maps have the same underlying range, which identifies the principal arrow right ideal with its coefficient-field continuation model.

source
def MagnitudeConjecture.BoundQuiver.StringPresentation.representedArrowRangeKLinearEquiv {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.representedArrowLinearMap a).range ≃ₗ[k] ↥(P.representedArrowKLinearMap a).range

The algebra-linear and coefficient-field-linear realizations of the represented arrow map have the same underlying coefficient-field-linear range.

Instances For
    source
    noncomputable def MagnitudeConjecture.BoundQuiver.StringPresentation.arrowRightIdealContinuationLinearEquiv {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) :
    ↥(RightModule.rightIdeal (P.arrowAlgebraCoordinate a)) ≃ₗ[k] ↥(P.representedArrowKLinearMap a).range

    The literal principal arrow right ideal and its continuation model are linearly equivalent over the coefficient field.

    Instances For