Magnitude conjecture

MagnitudeConjecture.Combinatorics.PosetSpaceBoundarySocle

The boundary-socle criterion for poset diagrams #

For a contravariant diagram on the augmented boundary, the maps from the non-root values into the root are injective exactly when the diagram has no nonzero subdiagram supported away from the root. This is the diagrammatic content of the manuscript's elementary projective-socle argument: a kernel at a non-root point generates a submodule invisible at the root, while any submodule invisible at the root lies in those kernels.

The ring-theoretic identification of root-supported simples with the projective boundary simple is deliberately kept separate. The result here is the intrinsic criterion needed on the incidence-diagram side.

source
structure MagnitudeConjecture.PosetSpace.BoundarySubdiagram (k T : Type u) [Field k] [PartialOrder T] (F : CategoryTheory.Functor (BoundaryIndex T)ᵒᵖ (ModuleCat k)) :
Type u

A pointwise linear subdiagram of a boundary diagram.

  • obj (q : (BoundaryIndex T)ᵒᵖ) : Submodule k ↑(F.obj q)

    The chosen subspace at each boundary point.

  • map {q r : (BoundaryIndex T)ᵒᵖ} (f : q ⟶ r) : self.obj q ≤ Submodule.comap (ModuleCat.Hom.hom (F.map f)) (self.obj r)

    Every structure map preserves the chosen subspaces.

Instances For
    source
    theorem MagnitudeConjecture.PosetSpace.BoundarySubdiagram.ext {k T : Type u} [Field k] [PartialOrder T] {F : CategoryTheory.Functor (BoundaryIndex T)ᵒᵖ (ModuleCat k)} {N L : BoundarySubdiagram k T F} (h : ∀ (q : (BoundaryIndex T)ᵒᵖ), N.obj q = L.obj q) :
    N = L
    source
    theorem MagnitudeConjecture.PosetSpace.BoundarySubdiagram.ext_iff {k T : Type u} [Field k] [PartialOrder T] {F : CategoryTheory.Functor (BoundaryIndex T)ᵒᵖ (ModuleCat k)} {N L : BoundarySubdiagram k T F} :
    N = L ↔ ∀ (q : (BoundaryIndex T)ᵒᵖ), N.obj q = L.obj q
    source
    def MagnitudeConjecture.PosetSpace.BoundarySubdiagram.IsZero {k T : Type u} [Field k] [PartialOrder T] {F : CategoryTheory.Functor (BoundaryIndex T)ᵒᵖ (ModuleCat k)} (N : BoundarySubdiagram k T F) :
    Prop

    A boundary subdiagram is zero when every pointwise subspace is zero.

    Instances For
      source
      def MagnitudeConjecture.PosetSpace.BoundarySubdiagram.SupportedAwayFromRoot {k T : Type u} [Field k] [PartialOrder T] {F : CategoryTheory.Functor (BoundaryIndex T)ᵒᵖ (ModuleCat k)} (N : BoundarySubdiagram k T F) :
      Prop

      A boundary subdiagram is supported away from the root when its root component vanishes.

      Instances For
        source
        def MagnitudeConjecture.PosetSpace.BoundarySubdiagram.IsSubdiagramOf {k T : Type u} [Field k] [PartialOrder T] {F : CategoryTheory.Functor (BoundaryIndex T)ᵒᵖ (ModuleCat k)} (N L : BoundarySubdiagram k T F) :
        Prop

        Pointwise containment of boundary subdiagrams.

        Instances For
          source
          def MagnitudeConjecture.PosetSpace.BoundarySubdiagram.IsSimple {k T : Type u} [Field k] [PartialOrder T] {F : CategoryTheory.Functor (BoundaryIndex T)ᵒᵖ (ModuleCat k)} (N : BoundarySubdiagram k T F) :
          Prop

          A nonzero boundary subdiagram is simple when it has no proper nonzero boundary subdiagram.

          Instances For
            source
            def MagnitudeConjecture.PosetSpace.BoundarySubdiagram.MeetsRoot {k T : Type u} [Field k] [PartialOrder T] {F : CategoryTheory.Functor (BoundaryIndex T)ᵒᵖ (ModuleCat k)} (N : BoundarySubdiagram k T F) :
            Prop

            A boundary subdiagram meets the root when its root component is nonzero.

            Instances For
              source
              theorem MagnitudeConjecture.PosetSpace.BoundarySubdiagram.isSubdiagramOf_refl {k T : Type u} [Field k] [PartialOrder T] {F : CategoryTheory.Functor (BoundaryIndex T)ᵒᵖ (ModuleCat k)} (N : BoundarySubdiagram k T F) :
              N.IsSubdiagramOf N
              source
              theorem MagnitudeConjecture.PosetSpace.BoundarySubdiagram.IsSubdiagramOf.trans {k T : Type u} [Field k] [PartialOrder T] {F : CategoryTheory.Functor (BoundaryIndex T)ᵒᵖ (ModuleCat k)} {N L M : BoundarySubdiagram k T F} (hNL : N.IsSubdiagramOf L) (hLM : L.IsSubdiagramOf M) :
              N.IsSubdiagramOf M
              source
              theorem MagnitudeConjecture.PosetSpace.BoundarySubdiagram.IsSubdiagramOf.supportedAwayFromRoot {k T : Type u} [Field k] [PartialOrder T] {F : CategoryTheory.Functor (BoundaryIndex T)ᵒᵖ (ModuleCat k)} {N L : BoundarySubdiagram k T F} (hNL : N.IsSubdiagramOf L) (hL : L.SupportedAwayFromRoot) :
              N.SupportedAwayFromRoot
              source
              noncomputable def MagnitudeConjecture.PosetSpace.BoundarySubdiagram.totalFinrank {k T : Type u} [Field k] [PartialOrder T] {F : CategoryTheory.Functor (BoundaryIndex T)ᵒᵖ (ModuleCat k)} [Fintype T] (N : BoundarySubdiagram k T F) :
              ℕ

              The sum of the dimensions of the pointwise subspaces of a finite boundary subdiagram.

              Instances For
                source
                theorem MagnitudeConjecture.PosetSpace.BoundarySubdiagram.totalFinrank_mono {k T : Type u} [Field k] [PartialOrder T] {F : CategoryTheory.Functor (BoundaryIndex T)ᵒᵖ (ModuleCat k)} [Fintype T] (hfinite : ∀ (q : BoundaryIndex T), Module.Finite k ↑(F.obj (Opposite.op q))) {N L : BoundarySubdiagram k T F} (hNL : N.IsSubdiagramOf L) :
                N.totalFinrank ≤ L.totalFinrank
                source
                theorem MagnitudeConjecture.PosetSpace.BoundarySubdiagram.eq_of_isSubdiagramOf_of_totalFinrank_eq {k T : Type u} [Field k] [PartialOrder T] {F : CategoryTheory.Functor (BoundaryIndex T)ᵒᵖ (ModuleCat k)} [Fintype T] (hfinite : ∀ (q : BoundaryIndex T), Module.Finite k ↑(F.obj (Opposite.op q))) {N L : BoundarySubdiagram k T F} (hNL : N.IsSubdiagramOf L) (hrank : N.totalFinrank = L.totalFinrank) :
                N = L
                source
                theorem MagnitudeConjecture.PosetSpace.BoundarySubdiagram.exists_simple_subdiagram {k T : Type u} [Field k] [PartialOrder T] {F : CategoryTheory.Functor (BoundaryIndex T)ᵒᵖ (ModuleCat k)} [Fintype T] (hfinite : ∀ (q : BoundaryIndex T), Module.Finite k ↑(F.obj (Opposite.op q))) (N : BoundarySubdiagram k T F) (hN : ¬N.IsZero) :
                ∃ (L : BoundarySubdiagram k T F), L.IsSubdiagramOf N ∧ L.IsSimple

                Every nonzero subdiagram of a finite-dimensional finite boundary diagram contains a simple subdiagram.

                source
                noncomputable def MagnitudeConjecture.PosetSpace.BoundarySubdiagram.rootKernel {k T : Type u} [Field k] [PartialOrder T] (F : CategoryTheory.Functor (BoundaryIndex T)ᵒᵖ (ModuleCat k)) :
                BoundarySubdiagram k T F

                The pointwise kernels of all maps to the root form a subdiagram.

                Instances For
                  source
                  @[simp]
                  theorem MagnitudeConjecture.PosetSpace.BoundarySubdiagram.rootKernel_obj_root {k T : Type u} [Field k] [PartialOrder T] (F : CategoryTheory.Functor (BoundaryIndex T)ᵒᵖ (ModuleCat k)) :
                  (rootKernel F).obj (Opposite.op BoundaryIndex.root) = ⊥
                  source
                  @[simp]
                  theorem MagnitudeConjecture.PosetSpace.BoundarySubdiagram.rootKernel_obj_nonroot {k T : Type u} [Field k] [PartialOrder T] (F : CategoryTheory.Functor (BoundaryIndex T)ᵒᵖ (ModuleCat k)) (t : T) :
                  (rootKernel F).obj (Opposite.op (BoundaryIndex.nonroot t)) = (boundaryDiagramRootMap k T F t).ker
                  source
                  theorem MagnitudeConjecture.PosetSpace.BoundarySubdiagram.rootKernel_supportedAwayFromRoot {k T : Type u} [Field k] [PartialOrder T] (F : CategoryTheory.Functor (BoundaryIndex T)ᵒᵖ (ModuleCat k)) :
                  (rootKernel F).SupportedAwayFromRoot
                  source
                  theorem MagnitudeConjecture.PosetSpace.BoundarySubdiagram.rootKernel_isZero_iff {k T : Type u} [Field k] [PartialOrder T] (F : CategoryTheory.Functor (BoundaryIndex T)ᵒᵖ (ModuleCat k)) :
                  (rootKernel F).IsZero ↔ ∀ (t : T), Function.Injective ⇑(boundaryDiagramRootMap k T F t)

                  The root-kernel subdiagram is zero exactly when all maps into the root are injective.

                  source
                  theorem MagnitudeConjecture.PosetSpace.BoundarySubdiagram.injective_rootMaps_iff_no_supportedAwaySubdiagram {k T : Type u} [Field k] [PartialOrder T] (F : CategoryTheory.Functor (BoundaryIndex T)ᵒᵖ (ModuleCat k)) :
                  (∀ (t : T), Function.Injective ⇑(boundaryDiagramRootMap k T F t)) ↔ ∀ (N : BoundarySubdiagram k T F), N.SupportedAwayFromRoot → N.IsZero

                  Injectivity of all maps into the root is equivalent to the absence of a nonzero subdiagram supported away from the root.

                  source
                  theorem MagnitudeConjecture.PosetSpace.BoundarySubdiagram.no_supportedAwaySubdiagram_iff_every_simple_meetsRoot {k T : Type u} [Field k] [PartialOrder T] [Fintype T] (F : CategoryTheory.Functor (BoundaryIndex T)ᵒᵖ (ModuleCat k)) (hfinite : ∀ (q : BoundaryIndex T), Module.Finite k ↑(F.obj (Opposite.op q))) :
                  (∀ (N : BoundarySubdiagram k T F), N.SupportedAwayFromRoot → N.IsZero) ↔ ∀ (L : BoundarySubdiagram k T F), L.IsSimple → L.MeetsRoot

                  On a finite-dimensional finite boundary diagram, having no nonzero subdiagram supported away from the root is equivalent to every simple subdiagram meeting the root. This is the intrinsic socle formulation of the root-injectivity criterion.

                  source
                  theorem MagnitudeConjecture.PosetSpace.isFiniteInjectiveBoundaryDiagram_iff_no_supportedAwaySubdiagram (k T : Type u) [Field k] [PartialOrder T] (F : CategoryTheory.Functor (BoundaryIndex T)ᵒᵖ (ModuleCat k)) :
                  IsFiniteInjectiveBoundaryDiagram k T F ↔ (∀ (q : BoundaryIndex T), Module.Finite k ↑(F.obj (Opposite.op q))) ∧ ∀ (N : BoundarySubdiagram k T F), N.SupportedAwayFromRoot → N.IsZero

                  Finite injective boundary diagrams can equivalently be characterized by finite-dimensional values and the absence of nonzero subdiagrams supported away from the root.

                  source
                  theorem MagnitudeConjecture.PosetSpace.isFiniteInjectiveBoundaryDiagram_iff_every_simple_meetsRoot (k T : Type u) [Field k] [PartialOrder T] [Fintype T] (F : CategoryTheory.Functor (BoundaryIndex T)ᵒᵖ (ModuleCat k)) :
                  IsFiniteInjectiveBoundaryDiagram k T F ↔ (∀ (q : BoundaryIndex T), Module.Finite k ↑(F.obj (Opposite.op q))) ∧ ∀ (L : BoundarySubdiagram k T F), L.IsSimple → L.MeetsRoot

                  Finite injective boundary diagrams are equivalently the finite diagrams whose every simple subdiagram meets the root. Under the incidence-module interpretation, the root simple is the projective boundary simple, so this is the manuscript's projective-socle criterion.