Support chains for selectable reverse enumerations

This file transports the support-prefix chain and Schur-detour arithmetic from the package's canonical reverse extension to an arbitrary selectable reverse enumeration.

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

The upper support consisting of the first j elements of the selected reverse enumeration.

theorem MagnitudeConjecture.PosetSpace.supportAtFor_isUpperSet (T : Type u) [PartialOrder T] [Fintype T] (R : ReverseEnumeration T) (j : Fin (Fintype.card T + 1)) : IsUpperSet (supportAtFor T R j)

Every selected support prefix is an upper set in the original poset.

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

Selected support prefixes are monotone in their length.

theorem MagnitudeConjecture.PosetSpace.supportAtFor_strictMono (T : Type u) [PartialOrder T] [Fintype T] (R : ReverseEnumeration T) (j : Fin (Fintype.card T)) : supportAtFor T R j.castSucc ⊂ supportAtFor T R j.succ

Consecutive selected support prefixes are strictly increasing.

@[reducible, inline]

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

The one-dimensional poset space at a selected support prefix.

@[reducible, inline]

noncomputable abbrev MagnitudeConjecture.PosetSpace.supportLineStepFor (k T : Type u) [Field k] [PartialOrder T] [Fintype T] (R : ReverseEnumeration T) (j : Fin (Fintype.card T)) : supportLineFor k T R j.castSucc ⟶ supportLineFor k T R j.succ

A consecutive map in the selected support chain.

theorem MagnitudeConjecture.PosetSpace.supportLineStepFor_ne_zero (k T : Type u) [Field k] [PartialOrder T] [Fintype T] (R : ReverseEnumeration T) (j : Fin (Fintype.card T)) : supportLineStepFor k T R j ≠ 0

theorem MagnitudeConjecture.PosetSpace.supportLineStepFor_not_isIso (k T : Type u) [Field k] [PartialOrder T] [Fintype T] (R : ReverseEnumeration T) (j : Fin (Fintype.card T)) : ¬CategoryTheory.IsIso (supportLineStepFor k T R j)

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

Along any selected support chain, a Schur-positive grading grows by at least the difference of support indices.

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

A two-step Schur detour replacing one inclusion in a selected support chain.

• middle : Obj k T
• middle_schur : IsSchur k T self.middle
• inMap : supportLineFor k T R ⟨q + 1, ⋯⟩ ⟶ self.middle
• outMap : self.middle ⟶ supportLineFor k T R ⟨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_selectableSchurDetour (k T : Type u) [Field k] [PartialOrder T] [Fintype T] (R : ReverseEnumeration T) {L q : ℕ} (G : PositiveGrading (Obj k T) (IsSchur k T) L) {hq : q + 2 < Fintype.card T} (D : SelectableSchurDetour k T R q hq) : Fintype.card T + 1 ≤ L

Splicing a two-step Schur detour into any selected support chain forces the strict realization bound |T|+1 ≤ L.