Magnitude conjecture

MagnitudeConjecture.Algebra.RightModuleStandardFormMeshHomCoordinateFactorUnderlyingEquation

Underlying coordinate equation for the represented mesh factor #

source
@[instance_reducible]
def MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.standardFormMeshHomCoordinateUnderlyingEquationQuiver {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.standardFormMeshHomCoordinateUnderlyingEquationArrowFintype {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.standardFormSimpleResolutionYonedaFactor_coordinate_hom_hom {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 : { z : Fin S.n // z ∉ S.standardFormProjectiveSet }) (x : Fin S.n) (h : S.standardFormRightMeshData.incomingCoefficientFiniteModule hP ↑z ⟶ S.standardFormRightMeshData.contravariantRepresentableFiniteModule hP x) (t : MeshCategory.obj S.standardFormRightMeshData ↑z ⟶ MeshCategory.obj S.standardFormRightMeshData x) (ht : ∀ (a : MeshCategory.RightMeshData.IncomingArrow ↑z), (S.standardFormSimpleResolutionYonedaCoefficient hP z x h a).hom = CategoryTheory.CategoryStruct.comp (S.standardFormRightMeshData.incomingArrowHom a) t) (a : MeshCategory.RightMeshData.IncomingArrow ↑z) :
      (CategoryTheory.CategoryStruct.comp (S.standardFormRightMeshData.incomingSummandInclusionFinite hP (↑z) a) (CategoryTheory.CategoryStruct.comp (S.standardFormRightMeshData.incomingMapFinite hP ↑z) (S.standardFormSimpleResolutionYonedaFactor hP (↑z) x t))).hom.hom = (CategoryTheory.CategoryStruct.comp (S.standardFormRightMeshData.incomingSummandInclusionFinite hP (↑z) a) h).hom.hom

      The coordinate equation after forgetting both finite-dimensional module properties.