Finite poset spaces and the support chain

This file begins the concrete realization layer used by the frozen manuscript. It defines finite-dimensional spaces equipped with a monotone family of subspaces indexed by a finite poset. It also constructs, from a reverse linear extension, the canonical chain of one-dimensional poset spaces from empty support to full support.

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

A finite-dimensional T-space: a vector space with a monotone family of subspaces indexed by the poset T.

• carrier : Type u
• addCommGroup : AddCommGroup self.carrier
• module : Module k self.carrier
• finiteDimensional : FiniteDimensional k self.carrier
• subspace : T → Submodule k self.carrier
• monotone_subspace ⦃s t : T⦄ : s ≤ t → self.subspace s ≤ self.subspace t

@[instance_reducible]

instance MagnitudeConjecture.PosetSpace.instCoeSortObjType (k T : Type u) [Field k] [PartialOrder T] : CoeSort (Obj k T) (Type u)

structure MagnitudeConjecture.PosetSpace.Hom (k T : Type u) [Field k] [PartialOrder T] (X Y : Obj k T) : Type u

A morphism of T-spaces is a linear map preserving every distinguished subspace.

• linear : X.carrier →ₗ[k] Y.carrier
• map_subspace (t : T) (x : X.carrier) : x ∈ X.subspace t → self.linear x ∈ Y.subspace t

theorem MagnitudeConjecture.PosetSpace.Hom.ext (k T : Type u) [Field k] [PartialOrder T] {X Y : Obj k T} {f g : Hom k T X Y} (h : f.linear = g.linear) : f = g

theorem MagnitudeConjecture.PosetSpace.Hom.ext_iff {k T : Type u} [Field k] [PartialOrder T] {X Y : Obj k T} {f g : Hom k T X Y} : f = g ↔ f.linear = g.linear

@[instance_reducible]

instance MagnitudeConjecture.PosetSpace.instCategoryObj (k T : Type u) [Field k] [PartialOrder T] : CategoryTheory.Category.{u, u + 1} (Obj k T)

@[instance_reducible]

instance MagnitudeConjecture.PosetSpace.instZeroHomObj (k T : Type u) [Field k] [PartialOrder T] {X Y : Obj k T} : Zero (X ⟶ Y)

@[simp]

theorem MagnitudeConjecture.PosetSpace.zero_linear (k T : Type u) [Field k] [PartialOrder T] {X Y : Obj k T} : Hom.linear 0 = 0

@[instance_reducible]

instance MagnitudeConjecture.PosetSpace.instAddHomObj (k T : Type u) [Field k] [PartialOrder T] {X Y : Obj k T} : Add (X ⟶ Y)

@[simp]

theorem MagnitudeConjecture.PosetSpace.add_linear (k T : Type u) [Field k] [PartialOrder T] {X Y : Obj k T} (f g : X ⟶ Y) : (f + g).linear = f.linear + g.linear

@[instance_reducible]

instance MagnitudeConjecture.PosetSpace.instNegHomObj (k T : Type u) [Field k] [PartialOrder T] {X Y : Obj k T} : Neg (X ⟶ Y)

@[simp]

theorem MagnitudeConjecture.PosetSpace.neg_linear (k T : Type u) [Field k] [PartialOrder T] {X Y : Obj k T} (f : X ⟶ Y) : (-f).linear = -f.linear

@[instance_reducible]

instance MagnitudeConjecture.PosetSpace.instSubHomObj (k T : Type u) [Field k] [PartialOrder T] {X Y : Obj k T} : Sub (X ⟶ Y)

@[simp]

theorem MagnitudeConjecture.PosetSpace.sub_linear (k T : Type u) [Field k] [PartialOrder T] {X Y : Obj k T} (f g : X ⟶ Y) : (f - g).linear = f.linear - g.linear

@[instance_reducible]

instance MagnitudeConjecture.PosetSpace.instSMulNatHomObj (k T : Type u) [Field k] [PartialOrder T] {X Y : Obj k T} : SMul ℕ (X ⟶ Y)

@[simp]

theorem MagnitudeConjecture.PosetSpace.nsmul_linear (k T : Type u) [Field k] [PartialOrder T] {X Y : Obj k T} (n : ℕ) (f : X ⟶ Y) : (n • f).linear = n • f.linear

@[instance_reducible]

instance MagnitudeConjecture.PosetSpace.instSMulIntHomObj (k T : Type u) [Field k] [PartialOrder T] {X Y : Obj k T} : SMul ℤ (X ⟶ Y)

@[simp]

theorem MagnitudeConjecture.PosetSpace.zsmul_linear (k T : Type u) [Field k] [PartialOrder T] {X Y : Obj k T} (n : ℤ) (f : X ⟶ Y) : (n • f).linear = n • f.linear

@[instance_reducible]

instance MagnitudeConjecture.PosetSpace.instAddCommGroupHomObj (k T : Type u) [Field k] [PartialOrder T] {X Y : Obj k T} : AddCommGroup (X ⟶ Y)

@[instance_reducible]

instance MagnitudeConjecture.PosetSpace.instSMulHomObj (k T : Type u) [Field k] [PartialOrder T] {X Y : Obj k T} : SMul k (X ⟶ Y)

@[simp]

theorem MagnitudeConjecture.PosetSpace.smul_linear (k T : Type u) [Field k] [PartialOrder T] {X Y : Obj k T} (c : k) (f : X ⟶ Y) : (c • f).linear = c • f.linear

@[instance_reducible]

instance MagnitudeConjecture.PosetSpace.instModuleHomObj (k T : Type u) [Field k] [PartialOrder T] {X Y : Obj k T} : Module k (X ⟶ Y)

@[instance_reducible]

instance MagnitudeConjecture.PosetSpace.instPreadditiveObj (k T : Type u) [Field k] [PartialOrder T] : CategoryTheory.Preadditive (Obj k T)

@[instance_reducible]

instance MagnitudeConjecture.PosetSpace.instLinearObj (k T : Type u) [Field k] [PartialOrder T] : CategoryTheory.Linear k (Obj k T)

@[instance_reducible]

instance MagnitudeConjecture.PosetSpace.instHasZeroMorphismsObj (k T : Type u) [Field k] [PartialOrder T] : CategoryTheory.Limits.HasZeroMorphisms (Obj k T)

@[simp]

theorem MagnitudeConjecture.PosetSpace.id_linear (k T : Type u) [Field k] [PartialOrder T] (X : Obj k T) : (CategoryTheory.CategoryStruct.id X).linear = LinearMap.id

@[simp]

theorem MagnitudeConjecture.PosetSpace.comp_linear (k T : Type u) [Field k] [PartialOrder T] {X Y Z : Obj k T} (f : X ⟶ Y) (g : Y ⟶ Z) : (CategoryTheory.CategoryStruct.comp f g).linear = g.linear ∘ₗ f.linear

@[reducible, inline]

noncomputable abbrev MagnitudeConjecture.PosetSpace.line (k T : Type u) [Field k] [PartialOrder T] (U : Set T) (hU : IsUpperSet U) : Obj k T

The one-dimensional T-space whose distinguished subspace is k exactly on the upper set U.

@[simp]

theorem MagnitudeConjecture.PosetSpace.line_subspace_of_mem (k T : Type u) [Field k] [PartialOrder T] (U : Set T) (hU : IsUpperSet U) (t : T) (ht : t ∈ U) : (line k T U hU).subspace t = ⊤

@[simp]

theorem MagnitudeConjecture.PosetSpace.line_subspace_of_not_mem (k T : Type u) [Field k] [PartialOrder T] (U : Set T) (hU : IsUpperSet U) (t : T) (ht : t ∉ U) : (line k T U hU).subspace t = ⊥

noncomputable def MagnitudeConjecture.PosetSpace.lineHom (k T : Type u) [Field k] [PartialOrder T] {U V : Set T} {hU : IsUpperSet U} {hV : IsUpperSet V} (hUV : U ⊆ V) : line k T U hU ⟶ line k T V hV

Inclusion of upper supports gives a morphism of one-dimensional T-spaces with underlying identity map.

@[simp]

theorem MagnitudeConjecture.PosetSpace.lineHom_linear (k T : Type u) [Field k] [PartialOrder T] {U V : Set T} {hU : IsUpperSet U} {hV : IsUpperSet V} (hUV : U ⊆ V) : (lineHom k T hUV).linear = LinearMap.id

theorem MagnitudeConjecture.PosetSpace.lineHom_ne_zero (k T : Type u) [Field k] [PartialOrder T] {U V : Set T} {hU : IsUpperSet U} {hV : IsUpperSet V} (hUV : U ⊆ V) : lineHom k T hUV ≠ 0

Every support-inclusion map is nonzero.

theorem MagnitudeConjecture.PosetSpace.lineHom_not_isIso (k T : Type u) [Field k] [PartialOrder T] {U V : Set T} {hU : IsUpperSet U} {hV : IsUpperSet V} (hUV : U ⊂ V) : ¬CategoryTheory.IsIso (lineHom k T ⋯)

A strict inclusion of upper supports gives a nonisomorphism between the corresponding one-dimensional T-spaces.

def MagnitudeConjecture.PosetSpace.IsSchur (k T : Type u) [Field k] [PartialOrder T] (X : Obj k T) : Prop

A T-space is Schur when its total space is nonzero and every endomorphism is scalar. In the directed realization this is the concrete property enjoyed by every indecomposable object.

theorem MagnitudeConjecture.PosetSpace.line_isSchur (k T : Type u) [Field k] [PartialOrder T] (U : Set T) (hU : IsUpperSet U) : IsSchur k T (line k T U hU)

Every one-dimensional support object is Schur.

@[reducible, inline]

abbrev MagnitudeConjecture.PosetSpace.ReverseExtension (T : Type u) : Type u

The reverse linear extension used in the manuscript: an increasing linear extension of the dual poset.

@[instance_reducible]

instance MagnitudeConjecture.PosetSpace.instFintypeReverseExtension (T : Type u) [Fintype T] : Fintype (ReverseExtension T)

noncomputable def MagnitudeConjecture.PosetSpace.reverseOrderIso (T : Type u) [PartialOrder T] [Fintype T] : Fin (Fintype.card T) ≃o ReverseExtension T

Increasing enumeration of the chosen reverse linear extension.

noncomputable def MagnitudeConjecture.PosetSpace.reverseIndex (T : Type u) [PartialOrder T] [Fintype T] (t : T) : Fin (Fintype.card T)

The position of a poset element in the chosen reverse linear extension.

theorem MagnitudeConjecture.PosetSpace.reverseIndex_anti (T : Type u) [PartialOrder T] [Fintype T] {s t : T} (hst : s ≤ t) : reverseIndex T t ≤ reverseIndex T s

The reverse-extension index reverses the original partial order.

def MagnitudeConjecture.PosetSpace.supportAt (T : Type u) [PartialOrder T] [Fintype T] (j : Fin (Fintype.card T + 1)) : Set T

The upper support consisting of the first j elements of the reverse linear extension.

theorem MagnitudeConjecture.PosetSpace.supportAt_isUpperSet (T : Type u) [PartialOrder T] [Fintype T] (j : Fin (Fintype.card T + 1)) : IsUpperSet (supportAt T j)

Every prefix of the reverse linear extension is an upper set in the original poset.

theorem MagnitudeConjecture.PosetSpace.supportAt_mono (T : Type u) [PartialOrder T] [Fintype T] {i j : Fin (Fintype.card T + 1)} (hij : i ≤ j) : supportAt T i ⊆ supportAt T j

The support prefixes are monotone in the prefix length.

noncomputable def MagnitudeConjecture.PosetSpace.reverseElement (T : Type u) [PartialOrder T] [Fintype T] (j : Fin (Fintype.card T)) : T

The element occupying position j in the reverse linear extension.

@[simp]

theorem MagnitudeConjecture.PosetSpace.reverseIndex_reverseElement (T : Type u) [PartialOrder T] [Fintype T] (j : Fin (Fintype.card T)) : reverseIndex T (reverseElement T j) = j

structure MagnitudeConjecture.PosetSpace.ReverseEnumeration (T : Type u) [PartialOrder T] [Fintype T] : Type u

A selectable reverse linear enumeration of a finite poset. Unlike the canonical choice above, this interface can carry order extensions chosen to put a specified antichain in consecutive positions.

• equiv : Fin (Fintype.card T) ≃ T
• index_anti {s t : T} : s ≤ t → self.equiv.symm t ≤ self.equiv.symm s

def MagnitudeConjecture.PosetSpace.ReverseEnumeration.index (T : Type u) [PartialOrder T] [Fintype T] (R : ReverseEnumeration T) (t : T) : Fin (Fintype.card T)

The position of an element in a selectable reverse enumeration.

@[simp]

theorem MagnitudeConjecture.PosetSpace.ReverseEnumeration.index_equiv (T : Type u) [PartialOrder T] [Fintype T] (R : ReverseEnumeration T) (j : Fin (Fintype.card T)) : index T R (R.equiv j) = j

theorem MagnitudeConjecture.PosetSpace.ReverseEnumeration.index_injective (T : Type u) [PartialOrder T] [Fintype T] (R : ReverseEnumeration T) : Function.Injective (index T R)

theorem MagnitudeConjecture.PosetSpace.supportAt_zero (T : Type u) [PartialOrder T] [Fintype T] : supportAt T 0 = ∅

The support chain starts at the empty set.

theorem MagnitudeConjecture.PosetSpace.supportAt_last (T : Type u) [PartialOrder T] [Fintype T] : supportAt T (Fin.last (Fintype.card T)) = Set.univ

The support chain ends at the full set.

theorem MagnitudeConjecture.PosetSpace.supportAt_strictMono (T : Type u) [PartialOrder T] [Fintype T] (j : Fin (Fintype.card T)) : supportAt T j.castSucc ⊂ supportAt T j.succ

Consecutive supports in the reverse-linear-extension chain are strictly increasing.

@[reducible, inline]

noncomputable abbrev MagnitudeConjecture.PosetSpace.supportLine (k T : Type u) [Field k] [PartialOrder T] [Fintype T] (j : Fin (Fintype.card T + 1)) : Obj k T

The manuscript's canonical chain of one-dimensional T-spaces has one strict nonisomorphism for every element of T.

@[reducible, inline]

noncomputable abbrev MagnitudeConjecture.PosetSpace.supportLineStep (k T : Type u) [Field k] [PartialOrder T] [Fintype T] (j : Fin (Fintype.card T)) : supportLine k T j.castSucc ⟶ supportLine k T j.succ

The consecutive morphisms in the canonical support chain.

theorem MagnitudeConjecture.PosetSpace.supportLineStep_not_isIso (k T : Type u) [Field k] [PartialOrder T] [Fintype T] (j : Fin (Fintype.card T)) : ¬CategoryTheory.IsIso (supportLineStep k T j)

Every step in the canonical support chain is a nonisomorphism.

@[reducible, inline]

noncomputable abbrev MagnitudeConjecture.PosetSpace.supportLineChain (k T : Type u) [Field k] [PartialOrder T] [Fintype T] : CategoryTheory.ComposableArrows (Obj k T) (Fintype.card T)

The full canonical support chain, viewed as a composable string of |T| morphisms.

@[simp]

theorem MagnitudeConjecture.PosetSpace.supportLineChain_hom_linear (k T : Type u) [Field k] [PartialOrder T] [Fintype T] : (supportLineChain k T).hom.linear = LinearMap.id

The total composite of the canonical support chain is the identity on its one-dimensional underlying vector space.

theorem MagnitudeConjecture.PosetSpace.supportLineChain_hom_ne_zero (k T : Type u) [Field k] [PartialOrder T] [Fintype T] : (supportLineChain k T).hom ≠ 0

Hence the total composite of the support chain is nonzero.

theorem MagnitudeConjecture.PosetSpace.supportLineChain_map_succ (k T : Type u) [Field k] [PartialOrder T] [Fintype T] (j : Fin (Fintype.card T)) : (supportLineChain k T).map' (↑j) (↑j + 1) ⋯ ⋯ = supportLineStep k T j

The adjacent arrow of the full support chain is the previously defined strict support-inclusion morphism.

theorem MagnitudeConjecture.PosetSpace.supportLineChain_map_succ_not_isIso (k T : Type u) [Field k] [PartialOrder T] [Fintype T] (j : Fin (Fintype.card T)) : ¬CategoryTheory.IsIso ((supportLineChain k T).map' (↑j) (↑j + 1) ⋯ ⋯)

Every adjacent arrow in the full support chain is a nonisomorphism.

theorem MagnitudeConjecture.PosetSpace.supportLineChain_map_succ_ne_zero (k T : Type u) [Field k] [PartialOrder T] [Fintype T] (j : Fin (Fintype.card T)) : (supportLineChain k T).map' (↑j) (↑j + 1) ⋯ ⋯ ≠ 0

Every adjacent arrow in the full support chain is nonzero.

def MagnitudeConjecture.PosetSpace.IsNonzeroNonisomorphismChain {C : Type u} [CategoryTheory.Category.{u_1, u} C] [CategoryTheory.Limits.HasZeroMorphisms C] (P : C → Prop) {n : ℕ} (F : CategoryTheory.ComposableArrows C n) : Prop

A composable chain through objects satisfying P is a nonzero nonisomorphism chain when every adjacent arrow is a nonzero nonisomorphism and its total composite is nonzero. In the manuscript, P selects the indecomposable objects.

def MagnitudeConjecture.PosetSpace.HasNonzeroNonisomorphismLengthAtMost (C : Type u) [CategoryTheory.Category.{u_1, u} C] [CategoryTheory.Limits.HasZeroMorphisms C] (P : C → Prop) (L : ℕ) : Prop

A category has nonzero nonisomorphism paths of length at most L when every such finite composable chain has at most L arrows. This is the exact categorical consequence of the manuscript's positive path-length grading.

structure MagnitudeConjecture.PosetSpace.PositiveGrading (C : Type u) [CategoryTheory.Category.{u_1, u} C] [CategoryTheory.Limits.HasZeroMorphisms C] (P : C → Prop) (L : ℕ) : Type u

A positive grading on the objects satisfying P: nonzero nonisomorphisms between admissible objects strictly raise level, and every admissible object has level at most L.

• level : C → ℕ
• level_le (X : C) : P X → self.level X ≤ L
• lt_of_nonzero_not_isIso {X Y : C} (f : X ⟶ Y) : P X → P Y → f ≠ 0 → ¬CategoryTheory.IsIso f → self.level X < self.level Y

theorem MagnitudeConjecture.PosetSpace.PositiveGrading.hasNonzeroNonisomorphismLengthAtMost {C : Type u} [CategoryTheory.Category.{u_1, u} C] [CategoryTheory.Limits.HasZeroMorphisms C] {P : C → Prop} {L : ℕ} (G : PositiveGrading C P L) : HasNonzeroNonisomorphismLengthAtMost C P L

A positive grading bounds the length of every nonzero chain of nonisomorphisms.

theorem MagnitudeConjecture.PosetSpace.supportLineChain_isNonzeroNonisomorphismChain (k T : Type u) [Field k] [PartialOrder T] [Fintype T] {P : Obj k T → Prop} : (∀ (j : Fin (Fintype.card T + 1)), P (supportLine k T j)) → IsNonzeroNonisomorphismChain P (supportLineChain k T)

The canonical support chain is a nonzero nonisomorphism chain of length exactly |T|.

theorem MagnitudeConjecture.PosetSpace.card_le_of_nonzeroNonisomorphismLengthAtMost (k T : Type u) [Field k] [PartialOrder T] [Fintype T] {L : ℕ} {P : Obj k T → Prop} (support_admissible : ∀ (j : Fin (Fintype.card T + 1)), P (supportLine k T j)) (hLength : HasNonzeroNonisomorphismLengthAtMost (Obj k T) P L) : Fintype.card T ≤ L

The path-length bound in the poset-space category forces the manuscript's realization inequality |T| ≤ L.

theorem MagnitudeConjecture.PosetSpace.card_le_of_positiveGrading (k T : Type u) [Field k] [PartialOrder T] [Fintype T] {L : ℕ} {P : Obj k T → Prop} (support_admissible : ∀ (j : Fin (Fintype.card T + 1)), P (supportLine k T j)) (G : PositiveGrading (Obj k T) P L) : Fintype.card T ≤ L

In particular, a positive grading on the poset-space category gives the realization-length inequality |T| ≤ L.

theorem MagnitudeConjecture.PosetSpace.card_le_of_schurPositiveGrading (k T : Type u) [Field k] [PartialOrder T] [Fintype T] {L : ℕ} (G : PositiveGrading (Obj k T) (IsSchur k T) L) : Fintype.card T ≤ L

The manuscript-shaped specialization: a positive grading on the Schur T-spaces forces |T| ≤ L, since every canonical support object is Schur.

theorem MagnitudeConjecture.PosetSpace.supportLine_level_add_index_le (k T : Type u) [Field k] [PartialOrder T] [Fintype T] {L : ℕ} (G : PositiveGrading (Obj k T) (IsSchur k T) L) {i j : Fin (Fintype.card T + 1)} (hij : i ≤ j) : G.level (supportLine k T i) + ↑j ≤ G.level (supportLine k T j) + ↑i

Along the canonical support chain, a Schur-positive grading grows by at least the difference of the support indices. The subtraction-free statement is convenient for natural-number arithmetic.

structure MagnitudeConjecture.PosetSpace.SchurDetour (k T : Type u) [Field k] [PartialOrder T] [Fintype T] (q : ℕ) (hq : q + 2 < Fintype.card T) : Type (u + 1)

A two-step Schur detour replacing one ordinary support inclusion. The three-antichain construction supplies this data with the two-dimensional three-line space as middle.

• middle : Obj k T
• middle_schur : IsSchur k T self.middle
• inMap : supportLine k T ⟨q + 1, ⋯⟩ ⟶ self.middle
• outMap : self.middle ⟶ supportLine k T ⟨q + 2, ⋯⟩
• inMap_ne_zero : self.inMap ≠ 0
• outMap_ne_zero : self.outMap ≠ 0
• inMap_not_isIso : ¬CategoryTheory.IsIso self.inMap
• outMap_not_isIso : ¬CategoryTheory.IsIso self.outMap

theorem MagnitudeConjecture.PosetSpace.card_add_one_le_of_schurDetour (k T : Type u) [Field k] [PartialOrder T] [Fintype T] {L q : ℕ} (G : PositiveGrading (Obj k T) (IsSchur k T) L) {hq : q + 2 < Fintype.card T} (D : SchurDetour k T q hq) : Fintype.card T + 1 ≤ L

Splicing a two-step Schur detour into the |T|-step support chain forces the strict equality obstruction |T|+1 ≤ L.