Magnitude conjecture

MagnitudeConjecture.Algebra.RightModuleStandardFormMeshYonedaFactorComposition

Composition of an incoming mesh coordinate with a Yoneda factor #

source
@[instance_reducible]
def MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.standardFormMeshYonedaFactorCompositionQuiver {k A : Type u} [Field k] [Ring A] [Algebra k A] [FiniteDimensional k A] [IsNoetherianRing Aᵐᵒᵖ] (S : FiniteIndecomposableSkeleton k A) :
Quiver (Fin S.n)
Instances For
    source
    @[instance_reducible]
    noncomputable def MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.standardFormMeshYonedaFactorCompositionArrowFintype {k A : Type u} [Field k] [Ring A] [Algebra k A] [FiniteDimensional k A] [IsNoetherianRing Aᵐᵒᵖ] (S : FiniteIndecomposableSkeleton k A) (x y : Fin S.n) :
    Fintype (x ⟶ y)
    Instances For
      source
      theorem MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.standardFormIncoming_comp_yonedaFactor {k A : Type u} [Field k] [IsAlgClosed k] [Ring A] [Algebra k A] [FiniteDimensional k A] [IsNoetherianRing Aᵐᵒᵖ] (S : FiniteIndecomposableSkeleton k A) (z x : Fin S.n) (a : MeshCategory.RightMeshData.IncomingArrow z) (t : MeshCategory.obj S.standardFormRightMeshData z ⟶ MeshCategory.obj S.standardFormRightMeshData x) :
      let T := S.standardFormRightMeshData; let Y := CategoryTheory.linearYoneda k T.VertexCategory; CategoryTheory.CategoryStruct.comp (T.incomingSummandInclusion z a) (CategoryTheory.CategoryStruct.comp (T.incomingMap z) (Y.map (CategoryTheory.InducedCategory.homMk t))) = Y.map (CategoryTheory.CategoryStruct.comp (CategoryTheory.InducedCategory.homMk (T.incomingArrowHom a)) (CategoryTheory.InducedCategory.homMk t))

      Composition with an incoming mesh coordinate is carried by linear Yoneda to composition in the induced vertex category.