Magnitude conjecture

MagnitudeConjecture.Algebra.RightModuleStandardFormMeshHomCoordinateFactorNamedIncoming

The named incoming-to-factor equality #

source
@[instance_reducible]
def MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.standardFormMeshHomCoordinateNamedIncomingQuiver {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.standardFormMeshHomCoordinateNamedIncomingArrowFintype {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.standardFormSimpleResolutionIncomingYonedaFactorComposite_eq {k A : Type u} [Field k] [IsAlgClosed k] [Ring A] [Algebra k A] [FiniteDimensional k A] [IsNoetherianRing Aᵐᵒᵖ] (S : FiniteIndecomposableSkeleton k A) (hP : S.standardFormRightMeshData.FiniteContravariantRepresentables) (z x : Fin S.n) (t : MeshCategory.obj S.standardFormRightMeshData z ⟶ MeshCategory.obj S.standardFormRightMeshData x) (a : MeshCategory.RightMeshData.IncomingArrow z) :
      S.standardFormSimpleResolutionIncomingYonedaFactorComposite hP z x t a = S.standardFormSimpleResolutionYonedaFactorComposite z x t a

      The named incoming composite is the named Yoneda factor composite.