Magnitude conjecture

MagnitudeConjecture.Algebra.RightModuleStandardFormARIncoming

Recovered incoming maps for the standard-form algebra #

This file identifies the recovered incoming map with its biproduct formula and proves right minimality at every standard-form label.

source
@[instance_reducible]
def MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.standardFormARIncomingQuiver {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.standardFormARIncomingArrowFintype {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.standardFormRecoveredIncomingMap {k A : Type u} [Field k] [IsAlgClosed k] [Ring A] [Algebra k A] [FiniteDimensional k A] [IsNoetherianRing Aᵐᵒᵖ] (S : FiniteIndecomposableSkeleton k A) (z : Fin S.n) :
      S.standardFormAdditiveRestrictedYonedaFunctor.obj (S.standardFormRightMeshData.additiveIncomingObj z) ⟶ S.standardFormProjectiveVertexModuleIndecomposableSkeleton.obj z

      The recovered complete incoming map at any standard-form label, with its singleton endpoint identified with the literal recovered indecomposable skeleton object.

      Instances For
        source
        theorem MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.standardFormRecoveredIncomingMap_eq_biproduct_desc {k A : Type u} [Field k] [IsAlgClosed k] [Ring A] [Algebra k A] [FiniteDimensional k A] [IsNoetherianRing Aᵐᵒᵖ] (S : FiniteIndecomposableSkeleton k A) (z : Fin S.n) :
        S.standardFormRecoveredIncomingMap z = CategoryTheory.Limits.biproduct.desc fun (a : MeshCategory.RightMeshData.IncomingArrow z) => (S.standardFormRestrictedYonedaFunctor ⋯).map (S.standardFormRightMeshData.incomingArrowHom a)

        The recovered incoming map is literally the biproduct descendant of the restricted-Yoneda images of all incoming mesh arrows.

        source
        theorem MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.standardFormRecoveredIncomingMap_eq_map_additiveIncoming_comp_singletonIso {k A : Type u} [Field k] [IsAlgClosed k] [Ring A] [Algebra k A] [FiniteDimensional k A] [IsNoetherianRing Aᵐᵒᵖ] (S : FiniteIndecomposableSkeleton k A) (z : Fin S.n) :
        S.standardFormRecoveredIncomingMap z = CategoryTheory.CategoryStruct.comp (S.standardFormAdditiveRestrictedYonedaFunctor.map (S.standardFormRightMeshData.additiveIncomingMap z)) (S.standardFormAdditiveRestrictedYonedaSingletonIso z).hom

        The biproduct-defined recovered incoming map is the restricted-Yoneda image of the additive incoming mesh map, followed by the singleton endpoint identification.

        source
        theorem MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.standardFormRecoveredIncomingMap_mono_of_projective {k A : Type u} [Field k] [IsAlgClosed k] [Ring A] [Algebra k A] [FiniteDimensional k A] [IsNoetherianRing Aᵐᵒᵖ] (S : FiniteIndecomposableSkeleton k A) (z : Fin S.n) (hz : CategoryTheory.Projective (S.fgObj z)) :
        CategoryTheory.Mono (S.standardFormRecoveredIncomingMap z)

        At an original projective label, the recovered incoming map is monic.

        source
        theorem MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.standardFormRecoveredIncomingMap_rightMinimal {k A : Type u} [Field k] [IsAlgClosed k] [Ring A] [Algebra k A] [FiniteDimensional k A] [IsNoetherianRing Aᵐᵒᵖ] (S : FiniteIndecomposableSkeleton k A) (z : Fin S.n) :
        QuotientSubmoduleEquidistribution.IsRightMinimal (S.standardFormRecoveredIncomingMap z)

        The recovered incoming map is right minimal at every label. At a projective label this follows from monicity; at a nonprojective label it is the terminal map of the recovered short exact mesh.