Magnitude conjecture

MagnitudeConjecture.Combinatorics.PosetSpaceBoundary

The augmented boundary poset of a poset space #

The incidence boundary of a T-space is obtained by adjoining a new root below OrderDual T. We use a dedicated inductive type so that the index is universe-polymorphic and its root/non-root decomposition remains literal.

source
def MagnitudeConjecture.PosetSpace.boundaryLE {T : Type u} [LE T] :
Option T → Option T → Prop

The incidence relation on the root followed by the points of T.

Instances For
    source
    theorem MagnitudeConjecture.PosetSpace.boundaryLE_refl {T : Type u} [Preorder T] (q : Option T) :
    boundaryLE q q
    source
    theorem MagnitudeConjecture.PosetSpace.boundaryLE_trans {T : Type u} [Preorder T] {q r s : Option T} :
    boundaryLE q r → boundaryLE r s → boundaryLE q s
    source
    theorem MagnitudeConjecture.PosetSpace.boundaryLE_antisymm {T : Type u} [PartialOrder T] {q r : Option T} (hqr : boundaryLE q r) (hrq : boundaryLE r q) :
    q = r
    source
    inductive MagnitudeConjecture.PosetSpace.BoundaryIndex (T : Type u) :
    Type u

    A root adjoined below the dual of T.

    Instances For
      source
      def MagnitudeConjecture.PosetSpace.instDecidableEqBoundaryIndex.decEq {T✝ : Type u_1} [DecidableEq T✝] (x✝ x✝¹ : BoundaryIndex T✝) :
      Decidable (x✝ = x✝¹)
      Instances For
        source
        @[instance_reducible]
        instance MagnitudeConjecture.PosetSpace.instDecidableEqBoundaryIndex {T✝ : Type u_1} [DecidableEq T✝] :
        DecidableEq (BoundaryIndex T✝)
        source
        def MagnitudeConjecture.PosetSpace.BoundaryIndex.toOption {T : Type u} :
        BoundaryIndex T → Option T

        Forget the order tag on an augmented boundary index.

        Instances For
          source
          def MagnitudeConjecture.PosetSpace.BoundaryIndex.equivOption {T : Type u} :
          BoundaryIndex T ≃ Option T

          The underlying finite type is just Option T.

          Instances For
            source
            @[instance_reducible]
            noncomputable instance MagnitudeConjecture.PosetSpace.instFintypeBoundaryIndex {T : Type u} [Fintype T] :
            Fintype (BoundaryIndex T)
            source
            @[simp]
            theorem MagnitudeConjecture.PosetSpace.BoundaryIndex.toOption_root {T : Type u} :
            root.toOption = none
            source
            @[simp]
            theorem MagnitudeConjecture.PosetSpace.BoundaryIndex.toOption_nonroot {T : Type u} (t : T) :
            (nonroot t).toOption = some t
            source
            theorem MagnitudeConjecture.PosetSpace.BoundaryIndex.toOption_injective {T : Type u} :
            Function.Injective toOption
            source
            @[instance_reducible]
            instance MagnitudeConjecture.PosetSpace.instPartialOrderBoundaryIndex {T : Type u} [PartialOrder T] :
            PartialOrder (BoundaryIndex T)

            The augmented order is the boundary incidence relation. Its non-root part is OrderDual T.

            source
            theorem MagnitudeConjecture.PosetSpace.boundaryLE_toOption_iff_le {T : Type u} [PartialOrder T] (q r : BoundaryIndex T) :
            boundaryLE q.toOption r.toOption ↔ q ≤ r