Poset spaces as injective diagrams on the augmented boundary

The augmented boundary is a root adjoined below OrderDual T. A T-space gives a contravariant diagram on this boundary: its value at the root is the ambient vector space, its value at t is the distinguished subspace at t, and every structure map into the root is the subtype inclusion.

This file proves the converse. A finite-dimensional boundary diagram whose maps into the root are injective is recovered by taking their ranges in the root. Thus finite T-spaces are equivalent to precisely these diagrams.

def MagnitudeConjecture.PosetSpace.boundarySpace (k T : Type u) [Field k] [PartialOrder T] (Y : Obj k T) : BoundaryIndex T → ModuleCat k

The module attached by a T-space to a boundary index.

def MagnitudeConjecture.PosetSpace.boundaryRestriction (k T : Type u) [Field k] [PartialOrder T] (Y : Obj k T) {q r : BoundaryIndex T} (h : q ≤ r) : boundarySpace k T Y r ⟶ boundarySpace k T Y q

The contravariant restriction map attached to an inequality in the augmented boundary.

@[simp]

theorem MagnitudeConjecture.PosetSpace.boundaryRestriction_root_root (k T : Type u) [Field k] [PartialOrder T] (Y : Obj k T) (h : BoundaryIndex.root ≤ BoundaryIndex.root) : boundaryRestriction k T Y h = CategoryTheory.CategoryStruct.id (boundarySpace k T Y BoundaryIndex.root)

@[simp]

theorem MagnitudeConjecture.PosetSpace.boundaryRestriction_root_nonroot (k T : Type u) [Field k] [PartialOrder T] (Y : Obj k T) (t : T) (h : BoundaryIndex.root ≤ BoundaryIndex.nonroot t) : ModuleCat.Hom.hom (boundaryRestriction k T Y h) = (Y.subspace t).subtype

@[simp]

theorem MagnitudeConjecture.PosetSpace.boundaryRestriction_nonroot_nonroot (k T : Type u) [Field k] [PartialOrder T] (Y : Obj k T) (s t : T) (h : BoundaryIndex.nonroot t ≤ BoundaryIndex.nonroot s) : ModuleCat.Hom.hom (boundaryRestriction k T Y h) = Submodule.inclusion ⋯

theorem MagnitudeConjecture.PosetSpace.boundaryRestriction_refl (k T : Type u) [Field k] [PartialOrder T] (Y : Obj k T) (q : BoundaryIndex T) : boundaryRestriction k T Y ⋯ = CategoryTheory.CategoryStruct.id (boundarySpace k T Y q)

theorem MagnitudeConjecture.PosetSpace.boundaryRestriction_trans (k T : Type u) [Field k] [PartialOrder T] (Y : Obj k T) {q r s : BoundaryIndex T} (hqr : q ≤ r) (hrs : r ≤ s) : boundaryRestriction k T Y ⋯ = CategoryTheory.CategoryStruct.comp (boundaryRestriction k T Y hrs) (boundaryRestriction k T Y hqr)

def MagnitudeConjecture.PosetSpace.boundaryDiagram (k T : Type u) [Field k] [PartialOrder T] (Y : Obj k T) : CategoryTheory.Functor (BoundaryIndex T)ᵒᵖ (ModuleCat k)

The contravariant boundary diagram of a T-space.

@[simp]

theorem MagnitudeConjecture.PosetSpace.boundaryDiagram_obj_root (k T : Type u) [Field k] [PartialOrder T] (Y : Obj k T) : (boundaryDiagram k T Y).obj (Opposite.op BoundaryIndex.root) = ModuleCat.of k Y.carrier

@[simp]

theorem MagnitudeConjecture.PosetSpace.boundaryDiagram_obj_nonroot (k T : Type u) [Field k] [PartialOrder T] (Y : Obj k T) (t : T) : (boundaryDiagram k T Y).obj (Opposite.op (BoundaryIndex.nonroot t)) = ModuleCat.of k ↥(Y.subspace t)

def MagnitudeConjecture.PosetSpace.boundaryRootArrow (T : Type u) [PartialOrder T] (t : T) : Opposite.op (BoundaryIndex.nonroot t) ⟶ Opposite.op BoundaryIndex.root

The canonical arrow from a non-root boundary point to the root in the opposite boundary category.

def MagnitudeConjecture.PosetSpace.boundaryNonrootArrow (T : Type u) [PartialOrder T] {s t : T} (hst : s ≤ t) : Opposite.op (BoundaryIndex.nonroot s) ⟶ Opposite.op (BoundaryIndex.nonroot t)

If s ≤ t in T, contravariance gives an arrow from the value at s to the value at t.

@[simp]

theorem MagnitudeConjecture.PosetSpace.boundaryDiagram_map_rootArrow_hom (k T : Type u) [Field k] [PartialOrder T] (Y : Obj k T) (t : T) : ModuleCat.Hom.hom ((boundaryDiagram k T Y).map (boundaryRootArrow T t)) = (Y.subspace t).subtype

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

The component of a morphism of T-spaces on its boundary diagram.

@[simp]

theorem MagnitudeConjecture.PosetSpace.boundaryDiagramMap_app_root_linear (k T : Type u) [Field k] [PartialOrder T] {X Y : Obj k T} (f : X ⟶ Y) : ModuleCat.Hom.hom ((boundaryDiagramMap k T f).app (Opposite.op BoundaryIndex.root)) = f.linear

noncomputable def MagnitudeConjecture.PosetSpace.boundaryDiagramFunctor (k T : Type u) [Field k] [PartialOrder T] : CategoryTheory.Functor (Obj k T) (CategoryTheory.Functor (BoundaryIndex T)ᵒᵖ (ModuleCat k))

Sending a poset space to its boundary diagram is functorial.

def MagnitudeConjecture.PosetSpace.IsFiniteInjectiveBoundaryDiagram (k T : Type u) [Field k] [PartialOrder T] : CategoryTheory.ObjectProperty (CategoryTheory.Functor (BoundaryIndex T)ᵒᵖ (ModuleCat k))

A boundary diagram has the form required by a finite poset space when all its values are finite-dimensional and every structure map from a non-root value into the root is injective.

@[reducible, inline]

abbrev MagnitudeConjecture.PosetSpace.FiniteInjectiveBoundaryDiagram (k T : Type u) [Field k] [PartialOrder T] : Type (u + 1)

The full category of finite-dimensional boundary diagrams with injective maps into the root.

theorem MagnitudeConjecture.PosetSpace.boundaryDiagram_isFiniteInjective (k T : Type u) [Field k] [PartialOrder T] (Y : Obj k T) : IsFiniteInjectiveBoundaryDiagram k T (boundaryDiagram k T Y)

noncomputable def MagnitudeConjecture.PosetSpace.finiteInjectiveBoundaryDiagramFunctor (k T : Type u) [Field k] [PartialOrder T] : CategoryTheory.Functor (Obj k T) (FiniteInjectiveBoundaryDiagram k T)

The boundary-diagram functor with its codomain restricted to the exact finite injective image condition.

def MagnitudeConjecture.PosetSpace.boundaryDiagramMapRoot (k T : Type u) [Field k] [PartialOrder T] {X Y : Obj k T} (α : boundaryDiagram k T X ⟶ boundaryDiagram k T Y) : X.carrier →ₗ[k] Y.carrier

The root component of a natural transformation of boundary diagrams.

def MagnitudeConjecture.PosetSpace.boundaryDiagramMapNonroot (k T : Type u) [Field k] [PartialOrder T] {X Y : Obj k T} (α : boundaryDiagram k T X ⟶ boundaryDiagram k T Y) (t : T) : ↥(X.subspace t) →ₗ[k] ↥(Y.subspace t)

A non-root component of a natural transformation of boundary diagrams.

theorem MagnitudeConjecture.PosetSpace.boundaryDiagramMap_root_eq_nonroot (k T : Type u) [Field k] [PartialOrder T] {X Y : Obj k T} (α : boundaryDiagram k T X ⟶ boundaryDiagram k T Y) (t : T) (x : ↥(X.subspace t)) : (boundaryDiagramMapRoot k T α) ↑x = ↑((boundaryDiagramMapNonroot k T α t) x)

Naturality at the arrow into the root says that the root component restricts to each non-root component.

def MagnitudeConjecture.PosetSpace.homOfBoundaryDiagramMap (k T : Type u) [Field k] [PartialOrder T] {X Y : Obj k T} (α : boundaryDiagram k T X ⟶ boundaryDiagram k T Y) : X ⟶ Y

A natural transformation between boundary diagrams is determined at the root and therefore induces a morphism of the underlying poset spaces.

theorem MagnitudeConjecture.PosetSpace.boundaryDiagramMap_homOfBoundaryDiagramMap (k T : Type u) [Field k] [PartialOrder T] {X Y : Obj k T} (α : boundaryDiagram k T X ⟶ boundaryDiagram k T Y) : boundaryDiagramMap k T (homOfBoundaryDiagramMap k T α) = α

instance MagnitudeConjecture.PosetSpace.finiteInjectiveBoundaryDiagramFunctor_faithful (k T : Type u) [Field k] [PartialOrder T] : (finiteInjectiveBoundaryDiagramFunctor k T).Faithful

instance MagnitudeConjecture.PosetSpace.finiteInjectiveBoundaryDiagramFunctor_full (k T : Type u) [Field k] [PartialOrder T] : (finiteInjectiveBoundaryDiagramFunctor k T).Full

def MagnitudeConjecture.PosetSpace.boundaryDiagramRootMap (k T : Type u) [Field k] [PartialOrder T] (F : CategoryTheory.Functor (BoundaryIndex T)ᵒᵖ (ModuleCat k)) (t : T) : ↑(F.obj (Opposite.op (BoundaryIndex.nonroot t))) →ₗ[k] ↑(F.obj (Opposite.op BoundaryIndex.root))

The structure map of an arbitrary boundary diagram into its root.

theorem MagnitudeConjecture.PosetSpace.boundaryDiagramRootMap_map_nonroot (k T : Type u) [Field k] [PartialOrder T] (F : CategoryTheory.Functor (BoundaryIndex T)ᵒᵖ (ModuleCat k)) {s t : T} (hst : s ≤ t) (y : ↑(F.obj (Opposite.op (BoundaryIndex.nonroot s)))) : (boundaryDiagramRootMap k T F t) ((ModuleCat.Hom.hom (F.map (boundaryNonrootArrow T hst))) y) = (boundaryDiagramRootMap k T F s) y

The map along a comparable pair of non-root points commutes with the two maps into the root.

def MagnitudeConjecture.PosetSpace.posetSpaceOfBoundaryDiagram (k T : Type u) [Field k] [PartialOrder T] (F : FiniteInjectiveBoundaryDiagram k T) : Obj k T

Reconstruct a poset space from a finite injective boundary diagram by taking the ranges of all structure maps inside the root value.

noncomputable def MagnitudeConjecture.PosetSpace.boundaryRangeLinearEquiv (k T : Type u) [Field k] [PartialOrder T] (F : FiniteInjectiveBoundaryDiagram k T) (t : T) : ↑(F.obj.obj (Opposite.op (BoundaryIndex.nonroot t))) ≃ₗ[k] ↥(boundaryDiagramRootMap k T F.obj t).range

An injective root map identifies a non-root value with its range in the root.

noncomputable def MagnitudeConjecture.PosetSpace.boundaryReconstructionComponent (k T : Type u) [Field k] [PartialOrder T] (F : FiniteInjectiveBoundaryDiagram k T) (q : (BoundaryIndex T)ᵒᵖ) : (boundaryDiagram k T (posetSpaceOfBoundaryDiagram k T F)).obj q ≅ F.obj.obj q

Componentwise identification of the reconstructed diagram with the original finite injective diagram.

theorem MagnitudeConjecture.PosetSpace.boundaryReconstructionComponent_rootMap (k T : Type u) [Field k] [PartialOrder T] (F : FiniteInjectiveBoundaryDiagram k T) (t : T) (x : ↥(boundaryDiagramRootMap k T F.obj t).range) : (boundaryDiagramRootMap k T F.obj t) ((ModuleCat.Hom.hom (boundaryReconstructionComponent k T F (Opposite.op (BoundaryIndex.nonroot t))).hom) x) = ↑x

The non-root reconstruction component is inverse to range restriction, so applying the original root map recovers the underlying root vector.

noncomputable def MagnitudeConjecture.PosetSpace.boundaryReconstructionIso (k T : Type u) [Field k] [PartialOrder T] (F : FiniteInjectiveBoundaryDiagram k T) : boundaryDiagram k T (posetSpaceOfBoundaryDiagram k T F) ≅ F.obj

The canonical isomorphism from the diagram reconstructed from ranges to the original finite injective boundary diagram.

instance MagnitudeConjecture.PosetSpace.finiteInjectiveBoundaryDiagramFunctor_essSurj (k T : Type u) [Field k] [PartialOrder T] : (finiteInjectiveBoundaryDiagramFunctor k T).EssSurj

instance MagnitudeConjecture.PosetSpace.finiteInjectiveBoundaryDiagramFunctor_isEquivalence (k T : Type u) [Field k] [PartialOrder T] : (finiteInjectiveBoundaryDiagramFunctor k T).IsEquivalence

noncomputable def MagnitudeConjecture.PosetSpace.finitePosetSpaceBoundaryEquivalence (k T : Type u) [Field k] [PartialOrder T] : Obj k T ≌ FiniteInjectiveBoundaryDiagram k T

Finite T-spaces are exactly finite-dimensional contravariant diagrams on the augmented boundary whose maps into the root are injective.