Magnitude conjecture

MagnitudeConjecture.Algebra.RightModuleStandardHomogeneousCorners

Degree-zero corners of the actual standard-form algebra #

source
theorem MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.standardCornerMeshHomFinite {k A : Type u} [Field k] [IsAlgClosed k] [Ring A] [Algebra k A] [FiniteDimensional k A] [IsNoetherianRing Aᵐᵒᵖ] (S : FiniteIndecomposableSkeleton k A) (X Y : S.StandardFormMeshCategory) :
FiniteDimensional k (X ⟶ Y)
source
@[instance_reducible]
def MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.standardCornerQuiver {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.standardCornerArrowFintype {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
      noncomputable def MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.standardFormHomogeneousCornerEquiv {k A : Type u} [Field k] [IsAlgClosed k] [Ring A] [Algebra k A] [FiniteDimensional k A] [IsNoetherianRing Aᵐᵒᵖ] (S : FiniteIndecomposableSkeleton k A) (p q : S.StandardFormProjectiveMeshCategory) (d : ℤ) :
      ↥(Graded.cornerComponent (S.standardFormOppositeAlgebraGrading ⋯) (S.standardFormHomogeneousIdempotent p) (S.standardFormHomogeneousIdempotent q) d) ≃ₗ[k] ↥(S.standardFormIntegerHomGrading.component (S.standardFormProjectiveMeshInclusion.obj p) (S.standardFormProjectiveMeshInclusion.obj q) d)

      Homogeneous corners of the standard algebra are exactly the mesh Hom components between the selected projective vertices.

      Instances For
        source
        theorem MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.standardFormHomogeneousCorner_diagonal {k A : Type u} [Field k] [IsAlgClosed k] [Ring A] [Algebra k A] [FiniteDimensional k A] [IsNoetherianRing Aᵐᵒᵖ] (S : FiniteIndecomposableSkeleton k A) (p : S.StandardFormProjectiveMeshCategory) :
        Module.finrank k ↥(Graded.cornerComponent (S.standardFormOppositeAlgebraGrading ⋯) (S.standardFormHomogeneousIdempotent p) (S.standardFormHomogeneousIdempotent p) 0) = 1

        Every diagonal degree-zero corner is one-dimensional.

        source
        theorem MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.standardFormHomogeneousCorner_off_diagonal {k A : Type u} [Field k] [IsAlgClosed k] [Ring A] [Algebra k A] [FiniteDimensional k A] [IsNoetherianRing Aᵐᵒᵖ] (S : FiniteIndecomposableSkeleton k A) (p q : S.StandardFormProjectiveMeshCategory) (hpq : p ≠ q) :
        Graded.cornerComponent (S.standardFormOppositeAlgebraGrading ⋯) (S.standardFormHomogeneousIdempotent p) (S.standardFormHomogeneousIdempotent q) 0 = ⊥

        Distinct primitive labels have no degree-zero corner maps.