Magnitude conjecture

MagnitudeConjecture.Combinatorics.PosetSpaceBoundaryPresentation

Two-term boundary presentations of finite poset spaces #

The boundary cover of a poset space is surjective both on its ambient vector space and on every distinguished subspace. Its ordinary linear kernel, equipped with the induced distinguished subspaces, is therefore its kernel in the category of poset spaces. Covering that kernel once more gives a two-term presentation by boundary-projective objects.

This is the target-side exact presentation used in Iyama realization. It does not assert that its relation map already has a weak cokernel in the finite strict tau-category.

source
def MagnitudeConjecture.PosetSpace.kernelObj {k T : Type u} [Field k] [PartialOrder T] {X Y : Obj k T} (f : X ⟶ Y) :
Obj k T

The kernel of a poset-space morphism, formed on the ambient linear map and equipped with the induced distinguished subspaces.

Instances For
    source
    def MagnitudeConjecture.PosetSpace.kernelInclusion {k T : Type u} [Field k] [PartialOrder T] {X Y : Obj k T} (f : X ⟶ Y) :
    kernelObj f ⟶ X

    The canonical inclusion of the induced kernel poset space.

    Instances For
      source
      @[simp]
      theorem MagnitudeConjecture.PosetSpace.kernelInclusion_linear {k T : Type u} [Field k] [PartialOrder T] {X Y : Obj k T} (f : X ⟶ Y) :
      (kernelInclusion f).linear = f.linear.ker.subtype
      source
      theorem MagnitudeConjecture.PosetSpace.kernelInclusion_comp {k T : Type u} [Field k] [PartialOrder T] {X Y : Obj k T} (f : X ⟶ Y) :
      CategoryTheory.CategoryStruct.comp (kernelInclusion f) f = 0

      The kernel inclusion is annihilated by the original morphism.

      source
      def MagnitudeConjecture.PosetSpace.kernelLift {k T : Type u} [Field k] [PartialOrder T] {W X Y : Obj k T} (f : X ⟶ Y) (g : W ⟶ X) (hgf : CategoryTheory.CategoryStruct.comp g f = 0) :
      W ⟶ kernelObj f

      A map annihilating f factors through the induced kernel object.

      Instances For
        source
        @[simp]
        theorem MagnitudeConjecture.PosetSpace.kernelLift_comp_inclusion {k T : Type u} [Field k] [PartialOrder T] {W X Y : Obj k T} (f : X ⟶ Y) (g : W ⟶ X) (hgf : CategoryTheory.CategoryStruct.comp g f = 0) :
        CategoryTheory.CategoryStruct.comp (kernelLift f g hgf) (kernelInclusion f) = g
        source
        noncomputable def MagnitudeConjecture.PosetSpace.BoundarySurjective.desc {k T : Type u} [Field k] [PartialOrder T] {X Y Z : Obj k T} {f : X ⟶ Y} (hf : BoundarySurjective f) (q : X ⟶ Z) (hq : CategoryTheory.CategoryStruct.comp (kernelInclusion f) q = 0) :
        Y ⟶ Z

        A boundary-surjective morphism is the categorical cokernel of its induced kernel inclusion. The distinguished-subspace condition is exactly what makes the linear quotient factor preserve every subspace.

        Instances For
          source
          theorem MagnitudeConjecture.PosetSpace.BoundarySurjective.comp_desc {k T : Type u} [Field k] [PartialOrder T] {X Y Z : Obj k T} {f : X ⟶ Y} (hf : BoundarySurjective f) (q : X ⟶ Z) (hq : CategoryTheory.CategoryStruct.comp (kernelInclusion f) q = 0) :
          CategoryTheory.CategoryStruct.comp f (hf.desc q hq) = q

          The quotient factor supplied by boundary surjectivity has the requested composite.

          source
          @[reducible, inline]
          abbrev MagnitudeConjecture.PosetSpace.boundaryKernel {k T : Type u} [Field k] [PartialOrder T] [Fintype T] (Y : Obj k T) :
          Obj k T

          The kernel poset space of the canonical boundary cover.

          Instances For
            source
            @[reducible, inline]
            abbrev MagnitudeConjecture.PosetSpace.boundaryRelationObject {k T : Type u} [Field k] [PartialOrder T] [Fintype T] (Y : Obj k T) :
            Obj k T

            Covering the kernel supplies the degree-one boundary-projective object.

            Instances For
              source
              def MagnitudeConjecture.PosetSpace.boundaryRelationMap {k T : Type u} [Field k] [PartialOrder T] [Fintype T] (Y : Obj k T) :
              boundaryRelationObject Y ⟶ boundaryCover Y

              The relation map in the canonical two-term boundary presentation.

              Instances For
                source
                theorem MagnitudeConjecture.PosetSpace.boundaryRelationMap_comp {k T : Type u} [Field k] [PartialOrder T] [Fintype T] (Y : Obj k T) :
                CategoryTheory.CategoryStruct.comp (boundaryRelationMap Y) (boundaryCoverMap Y) = 0

                The relation map is annihilated by the boundary-cover projection.

                source
                theorem MagnitudeConjecture.PosetSpace.boundaryCoverMap_weakCokernel {k T : Type u} [Field k] [PartialOrder T] [Fintype T] (Y : Obj k T) {Z : Obj k T} (q : boundaryCover Y ⟶ Z) (hq : CategoryTheory.CategoryStruct.comp (boundaryRelationMap Y) q = 0) :
                ∃ (s : Y ⟶ Z), CategoryTheory.CategoryStruct.comp (boundaryCoverMap Y) s = q

                The canonical boundary-cover projection is a weak cokernel of the relation map. Thus every finite poset space has a two-term presentation by explicit boundary-projective objects.