Existence of a rank function to natural numbers

In this file, we show that if P : A.Pairing is a regular pairing of subcomplex A of a simplicial set X, then there exists a rank function for P with values in ℕ.

instance SSet.Subcomplex.Pairing.instFiniteSubtypeElemNIIAncestralRel {X : SSet} {A : X.Subcomplex} (P : A.Pairing) (y : ↑P.II) : Finite { x : ↑P.II // P.AncestralRel x y }

noncomputable def SSet.Subcomplex.Pairing.rank' {X : SSet} {A : X.Subcomplex} (P : A.Pairing) {y : ↑P.II} (hy : Acc P.AncestralRel y) : ℕ

Auxiliary definition for SSet.Subcomplex.Pairing.Rank.

Equations

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

theorem SSet.Subcomplex.Pairing.rank'_eq {X : SSet} {A : X.Subcomplex} (P : A.Pairing) {y : ↑P.II} (hy : Acc P.AncestralRel y) : P.rank' hy = ⨆ (x : { x : ↑P.II // P.AncestralRel x y }), P.rank' ⋯ + 1

theorem SSet.Subcomplex.Pairing.rank'_lt {X : SSet} {A : X.Subcomplex} (P : A.Pairing) {y : ↑P.II} (hy : Acc P.AncestralRel y) {x : ↑P.II} (r : P.AncestralRel x y) : P.rank' ⋯ < P.rank' hy

noncomputable def SSet.Subcomplex.Pairing.rank {X : SSet} {A : X.Subcomplex} (P : A.Pairing) [P.IsRegular] (x : ↑P.II) : ℕ

The rank function with values in ℕ relative to the well founded ancestrality relation of a regular pairing.

Equations

• P.rank x = P.rank' ⋯

theorem SSet.Subcomplex.Pairing.rank_lt {X : SSet} {A : X.Subcomplex} {P : A.Pairing} [P.IsRegular] {x y : ↑P.II} (h : P.AncestralRel x y) : P.rank x < P.rank y

noncomputable def SSet.Subcomplex.Pairing.rankFunction {X : SSet} {A : X.Subcomplex} (P : A.Pairing) [P.IsRegular] : P.RankFunction ℕ

The canonical rank function with values in ℕ of a regular pairing.

Equations

• P.rankFunction = { rank := P.rank, lt := ⋯ }

instance SSet.Subcomplex.Pairing.instNonemptyRankFunctionNat {X : SSet} {A : X.Subcomplex} (P : A.Pairing) [P.IsRegular] : Nonempty (P.RankFunction ℕ)

instance SSet.Subcomplex.Pairing.instNonemptyWeakRankFunctionNat {X : SSet} {A : X.Subcomplex} (P : A.Pairing) [P.IsRegular] : Nonempty (P.WeakRankFunction ℕ)

theorem SSet.Subcomplex.Pairing.isRegular_iff_nonempty_rankFunction {X : SSet} {A : X.Subcomplex} (P : A.Pairing) [P.IsProper] : P.IsRegular ↔ Nonempty (P.RankFunction ℕ)

theorem SSet.Subcomplex.Pairing.isRegular_iff_nonempty_weakRankFunction {X : SSet} {A : X.Subcomplex} (P : A.Pairing) [P.IsProper] : P.IsRegular ↔ Nonempty (P.WeakRankFunction ℕ)

theorem SSet.Subcomplex.PairingCore.isRegular_iff_nonempty_rankFunction {X : SSet} {A : X.Subcomplex} (P : A.PairingCore) [P.IsProper] : P.IsRegular ↔ Nonempty (P.RankFunction ℕ)

theorem SSet.Subcomplex.PairingCore.isRegular_iff_nonempty_weakRankFunction {X : SSet} {A : X.Subcomplex} (P : A.PairingCore) [P.IsProper] : P.IsRegular ↔ Nonempty (P.WeakRankFunction ℕ)