Magnitude conjecture

MagnitudeConjecture.Algebra.StringProjectiveRadicalArrowPi

The incoming-arrow product model of a string projective radical #

We retain the incoming-arrow indexing here. Reindexing is performed only after passing to a categorical biproduct, avoiding a large dependent LinearEquiv.piCongrLeft term.

source
theorem MagnitudeConjecture.BoundQuiver.StringPresentation.quotientFGHasFiniteBiproducts {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) :
CategoryTheory.Limits.HasFiniteBiproducts (FGModuleCat P.quotientCategoryAlgebraᵐᵒᵖ)
source
noncomputable def MagnitudeConjecture.BoundQuiver.StringPresentation.representedVertexRadicalArrowPiFGObj {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) (y : Q) :
FGModuleCat P.quotientCategoryAlgebraᵐᵒᵖ

The dependent product of the incoming-arrow ranges, retained as a finitely generated module.

Instances For
    source
    noncomputable def MagnitudeConjecture.BoundQuiver.StringPresentation.representedVertexRadicalToArrowPiIso {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) (y : Q) :
    P.representedVertexRadicalFGObj y ≅ P.representedVertexRadicalArrowPiFGObj y

    The radical is isomorphic to the incoming-arrow dependent product.

    Instances For
      source
      noncomputable def MagnitudeConjecture.BoundQuiver.StringPresentation.representedVertexRadicalArrowPiModuleIso {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) (y : Q) :
      (CategoryTheory.forget₂ (FGModuleCat P.quotientCategoryAlgebraᵐᵒᵖ) (ModuleCat P.quotientCategoryAlgebraᵐᵒᵖ)).obj (P.representedVertexRadicalArrowPiFGObj y) ≅ (CategoryTheory.forget₂ (FGModuleCat P.quotientCategoryAlgebraᵐᵒᵖ) (ModuleCat P.quotientCategoryAlgebraᵐᵒᵖ)).obj (⨁ fun (a : DisplayedIncomingArrow y) => P.incomingArrowRangeFGObj a)

      The incoming-arrow dependent product is the underlying module of the corresponding categorical biproduct.

      Instances For
        source
        noncomputable def MagnitudeConjecture.BoundQuiver.StringPresentation.representedVertexRadicalArrowPiToBiproductIso {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) (y : Q) :
        P.representedVertexRadicalArrowPiFGObj y ≅ ⨁ fun (a : DisplayedIncomingArrow y) => P.incomingArrowRangeFGObj a

        The incoming-arrow dependent product, as an FG-module, is isomorphic to the incoming-arrow categorical biproduct.

        Instances For