Rank functions for pairings

We introduce types of (weak) rank functions for a pairing P of a subcomplex A of a simplicial set X. These are functions f : P.II → α such that P.AncestralRel x y implies f x < f y (in the weak case, we require this only under the additional condition that x and y are of the same dimension). Such rank functions are used in order to show that the ancestrality relation on P.II is well founded, i.e. that P is regular (when we already know P is proper). Conversely, we shall show that if P is regular, then P.RankFunction ℕ is non empty (TODO @joelriou).

(We also introduce similar definitions for the structure PairingCore.)

References

• Sean Moss, Another approach to the Kan-Quillen model structure

structure SSet.Subcomplex.Pairing.RankFunction {X : SSet} {A : X.Subcomplex} (P : A.Pairing) (α : Type v) [PartialOrder α] : Type (max u v)

A rank function for a pairing is a function from the type (II) simplices to a partially ordered type which maps ancestrality relations to strict inequalities.

• rank : ↑P.II → α

  the rank function

• lt {x y : ↑P.II} : P.AncestralRel x y → self.rank x < self.rank y

theorem SSet.Subcomplex.Pairing.RankFunction.wf_ancestralRel {X : SSet} {A : X.Subcomplex} {P : A.Pairing} {α : Type v} [PartialOrder α] [WellFoundedLT α] (f : P.RankFunction α) : WellFounded P.AncestralRel

theorem SSet.Subcomplex.Pairing.RankFunction.isRegular {X : SSet} {A : X.Subcomplex} {P : A.Pairing} {α : Type v} [PartialOrder α] [WellFoundedLT α] (f : P.RankFunction α) [P.IsProper] : P.IsRegular

structure SSet.Subcomplex.Pairing.WeakRankFunction {X : SSet} {A : X.Subcomplex} (P : A.Pairing) (α : Type v) [PartialOrder α] : Type (max u v)

A weak rank function for a pairing is a function from the type (II) simplices to a partially ordered type which maps an ancestrality relation between simplices of the same dimension to a strict inequality.

• rank : ↑P.II → α

  the (weak) rank function

• lt {x y : ↑P.II} : P.AncestralRel x y → (↑x).dim = (↑y).dim → self.rank x < self.rank y

theorem SSet.Subcomplex.Pairing.WeakRankFunction.wf_ancestralRel {X : SSet} {A : X.Subcomplex} {P : A.Pairing} {α : Type v} [PartialOrder α] [WellFoundedLT α] [P.IsProper] (f : P.WeakRankFunction α) : WellFounded P.AncestralRel

theorem SSet.Subcomplex.Pairing.WeakRankFunction.isRegular {X : SSet} {A : X.Subcomplex} {P : A.Pairing} {α : Type v} [PartialOrder α] [WellFoundedLT α] [P.IsProper] (f : P.WeakRankFunction α) : P.IsRegular

def SSet.Subcomplex.Pairing.RankFunction.toWeakRankFunction {X : SSet} {A : X.Subcomplex} (P : A.Pairing) (α : Type v) [PartialOrder α] (f : P.RankFunction α) : P.WeakRankFunction α

The weak rank function attached to a rank function.

Equations

• SSet.Subcomplex.Pairing.RankFunction.toWeakRankFunction P α f = { rank := f.rank, lt := ⋯ }

@[simp]

theorem SSet.Subcomplex.Pairing.RankFunction.toWeakRankFunction_rank {X : SSet} {A : X.Subcomplex} (P : A.Pairing) (α : Type v) [PartialOrder α] (f : P.RankFunction α) (a✝ : ↑P.II) : (toWeakRankFunction P α f).rank a✝ = f.rank a✝

structure SSet.Subcomplex.PairingCore.RankFunction {X : SSet} {A : X.Subcomplex} (h : A.PairingCore) (α : Type v) [PartialOrder α] : Type (max u_1 v)

A rank function for h : A.PairingCore is a function from the index type h.ι to a partially ordered type which maps the ancestrality relations to strict inequalities.

• rank : h.ι → α

  the rank function

• lt {x y : h.ι} : h.AncestralRel x y → self.rank x < self.rank y

structure SSet.Subcomplex.PairingCore.WeakRankFunction {X : SSet} {A : X.Subcomplex} (h : A.PairingCore) (α : Type v) [PartialOrder α] : Type (max u_1 v)

A weak rank function h : A.PairingCore is a function from the index type h.ι to a partially ordered type which maps an ancestrality relation between indices of the same dimension to a strict inequality.

• rank : h.ι → α

  the (weak) rank function

• lt {x y : h.ι} : h.AncestralRel x y → h.dim x = h.dim y → self.rank x < self.rank y

noncomputable def SSet.Subcomplex.PairingCore.rankFunctionEquiv {X : SSet} {A : X.Subcomplex} (h : A.PairingCore) (α : Type v) [PartialOrder α] : h.RankFunction α ≃ h.pairing.RankFunction α

Rank functions for h : A.PairingCore correspond to rank functions for h.pairing : A.Pairing.

Equations

• One or more equations did not get rendered due to their size.

noncomputable def SSet.Subcomplex.PairingCore.weakRankFunctionEquiv {X : SSet} {A : X.Subcomplex} (h : A.PairingCore) (α : Type v) [PartialOrder α] : h.WeakRankFunction α ≃ h.pairing.WeakRankFunction α

Weak rank functions for h : A.PairingCore correspond to weak rank functions for h.pairing : A.Pairing.

Equations

• One or more equations did not get rendered due to their size.