Magnitude conjecture

MagnitudeConjecture.Algebra.RightModuleIyamaBoundaryPresentation

Lifting the two-term boundary presentation #

Covering the kernel of the represented boundary cover gives a second represented boundary object. Fullness of restricted Yoneda lifts the relation map between these two objects back to the primitive factor category. On the poset-space side the original cover is a weak cokernel of that lifted relation.

This file deliberately stops before the remaining Iyama theorem: constructing inside the finite strict tau-category a realization whose restricted Yoneda object is that weak cokernel.

source
@[reducible, inline]
noncomputable abbrev MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.PrimitiveProjectivePosetData.categoricalBoundaryRelationObject {k A : Type u} [Field k] [Ring A] [Algebra k A] [FiniteDimensional k A] [IsNoetherianRing Aᵐᵒᵖ] {S : FiniteIndecomposableSkeleton k A} {K : Set (Fin S.n)} {D : S.PrimitiveMultiplicityInput K} {T : Type u} [Fintype T] [PartialOrder T] (R : S.PrimitiveProjectivePosetData D T) (Y : PosetSpace.Obj k T) :
S.FactorCategory K

The categorical boundary object representing the relation space in the canonical two-term presentation of Y.

Instances For
    source
    noncomputable def MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.PrimitiveProjectivePosetData.representedBoundaryRelationMap {k A : Type u} [Field k] [Ring A] [Algebra k A] [FiniteDimensional k A] [IsNoetherianRing Aᵐᵒᵖ] {S : FiniteIndecomposableSkeleton k A} {K : Set (Fin S.n)} {D : S.PrimitiveMultiplicityInput K} {T : Type u} [Fintype T] [PartialOrder T] (R : S.PrimitiveProjectivePosetData D T) (H : S.HasAcyclicNonzeroNonisomorphisms) (Y : PosetSpace.Obj k T) :
    R.representableData.obj (R.categoricalBoundaryRelationObject Y) ⟶ R.representableData.obj (R.boundaryCoverObject Y)

    The relation map transported between the two represented boundary-cover objects.

    Instances For
      source
      theorem MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.PrimitiveProjectivePosetData.representedBoundaryRelationMap_comp {k A : Type u} [Field k] [Ring A] [Algebra k A] [FiniteDimensional k A] [IsNoetherianRing Aᵐᵒᵖ] {S : FiniteIndecomposableSkeleton k A} {K : Set (Fin S.n)} {D : S.PrimitiveMultiplicityInput K} {T : Type u} [Fintype T] [PartialOrder T] (R : S.PrimitiveProjectivePosetData D T) (H : S.HasAcyclicNonzeroNonisomorphisms) (Y : PosetSpace.Obj k T) :
      CategoryTheory.CategoryStruct.comp (R.representedBoundaryRelationMap H Y) (R.representedBoundaryCoverMap H Y) = 0

      The represented relation is annihilated by the represented boundary cover.

      source
      theorem MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.PrimitiveProjectivePosetData.representedBoundaryCoverMap_weakCokernel {k A : Type u} [Field k] [Ring A] [Algebra k A] [FiniteDimensional k A] [IsNoetherianRing Aᵐᵒᵖ] {S : FiniteIndecomposableSkeleton k A} {K : Set (Fin S.n)} {D : S.PrimitiveMultiplicityInput K} {T : Type u} [Fintype T] [PartialOrder T] (R : S.PrimitiveProjectivePosetData D T) (H : S.HasAcyclicNonzeroNonisomorphisms) (Y : PosetSpace.Obj k T) {Z : PosetSpace.Obj k T} (q : R.representableData.obj (R.boundaryCoverObject Y) ⟶ Z) (hq : CategoryTheory.CategoryStruct.comp (R.representedBoundaryRelationMap H Y) q = 0) :
      ∃ (s : Y ⟶ Z), CategoryTheory.CategoryStruct.comp (R.representedBoundaryCoverMap H Y) s = q

      On the poset-space side, the represented boundary cover is a weak cokernel of the represented relation map.

      source
      noncomputable def MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.PrimitiveProjectivePosetData.liftedBoundaryRelationMap {k A : Type u} [Field k] [Ring A] [Algebra k A] [FiniteDimensional k A] [IsNoetherianRing Aᵐᵒᵖ] {S : FiniteIndecomposableSkeleton k A} {K : Set (Fin S.n)} {D : S.PrimitiveMultiplicityInput K} {T : Type u} [Fintype T] [PartialOrder T] (R : S.PrimitiveProjectivePosetData D T) (H : S.HasAcyclicNonzeroNonisomorphisms) (Y : PosetSpace.Obj k T) :
      R.categoricalBoundaryRelationObject Y ⟶ R.boundaryCoverObject Y

      Fullness lifts the relation map of the boundary presentation to the primitive factor category.

      Instances For
        source
        theorem MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.PrimitiveProjectivePosetData.map_liftedBoundaryRelationMap {k A : Type u} [Field k] [Ring A] [Algebra k A] [FiniteDimensional k A] [IsNoetherianRing Aᵐᵒᵖ] {S : FiniteIndecomposableSkeleton k A} {K : Set (Fin S.n)} {D : S.PrimitiveMultiplicityInput K} {T : Type u} [Fintype T] [PartialOrder T] (R : S.PrimitiveProjectivePosetData D T) (H : S.HasAcyclicNonzeroNonisomorphisms) (Y : PosetSpace.Obj k T) :
        R.representableData.map (R.liftedBoundaryRelationMap H Y) = R.representedBoundaryRelationMap H Y

        Restricted Yoneda sends the lifted categorical relation to the explicit relation map between the represented boundary covers.

        source
        theorem MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.PrimitiveProjectivePosetData.representedBoundaryCoverMap_weakCokernel_lifted {k A : Type u} [Field k] [Ring A] [Algebra k A] [FiniteDimensional k A] [IsNoetherianRing Aᵐᵒᵖ] {S : FiniteIndecomposableSkeleton k A} {K : Set (Fin S.n)} {D : S.PrimitiveMultiplicityInput K} {T : Type u} [Fintype T] [PartialOrder T] (R : S.PrimitiveProjectivePosetData D T) (H : S.HasAcyclicNonzeroNonisomorphisms) (Y : PosetSpace.Obj k T) {Z : PosetSpace.Obj k T} (q : R.representableData.obj (R.boundaryCoverObject Y) ⟶ Z) (hq : CategoryTheory.CategoryStruct.comp (R.representableData.map (R.liftedBoundaryRelationMap H Y)) q = 0) :
        ∃ (s : Y ⟶ Z), CategoryTheory.CategoryStruct.comp (R.representedBoundaryCoverMap H Y) s = q

        The represented boundary cover is therefore a weak cokernel of the image of the lifted categorical relation.