Pairings

In this file, we introduce the definition of a pairing for a subcomplex A of a simplicial set X, following the ideas by Sean Moss, Another approach to the Kan-Quillen model structure, who gave a complete combinatorial characterization of strong (inner) anodyne extensions. Strong (inner) anodyne extensions are transfinite compositions of pushouts of coproducts of (inner) horn inclusions, i.e. this is similar to (inner) anodyne extensions but without the stability property under retracts.

A pairing for A consists in the data of a partition of the nondegenerate simplices of X not in A into type (I) simplices and type (II) simplices, and of a bijection between the types of type (I) and type (II) simplices. Indeed, the main observation is that when we attach a simplex along a horn inclusion, exactly two nondegenerate simplices are added: this simplex, and the unique face which is not in the image of the horn. The former shall be considered as of type (I) and the latter as type (II).

We say that a pairing is regular (typeclass Pairing.IsRegular) when

• it is proper (Pairing.IsProper), i.e. any type (II) simplex is uniquely a face of the corresponding type (I) simplex.
• a certain ancestrality relation is well founded. When these conditions are satisfied, the inclusion A.ι : A ⟶ X is a strong anodyne extension (TODO @joelriou), and the converse is also true (if A.ι is a strong anodyne extension, then there is a regular pairing for A (TODO)).

References

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

structure SSet.Subcomplex.Pairing {X : SSet} (A : X.Subcomplex) : Type u

A pairing for a subcomplex A of a simplicial set X consists of a partition of the nondegenerate simplices of X not in A in two types (I) and (II) of simplices, and a bijection between the type (II) simplices and the type (I) simplices. See the introduction of the file AlgebraicTopology.SimplicialSet.AnodyneExtensions.Pairing.

• I : Set A.N

  the set of type (I) simplices

• II : Set A.N

  the set of type (II) simplices

• inter : self.I ∩ self.II = ∅
• union : self.I ∪ self.II = Set.univ
• p : ↑self.II ≃ ↑self.I

  a bijection from the type (II) simplices to the type (I) simplices

class SSet.Subcomplex.Pairing.IsProper {X : SSet} {A : X.Subcomplex} (P : A.Pairing) : Prop

A pairing is regular when each type (II) simplex is uniquely a 1-codimensional face of the corresponding (I) simplex.

• isUniquelyCodimOneFace (x : ↑P.II) : (↑x).IsUniquelyCodimOneFace (↑(P.p x)).toS

theorem SSet.Subcomplex.Pairing.isUniquelyCodimOneFace {X : SSet} {A : X.Subcomplex} (P : A.Pairing) [P.IsProper] (x : ↑P.II) : (↑x).IsUniquelyCodimOneFace (↑(P.p x)).toS

class SSet.Subcomplex.Pairing.IsInner {X : SSet} {A : X.Subcomplex} (P : A.Pairing) [P.IsProper] : Prop

The condition that a pairing only involves inner horns.

• ne_zero (x : ↑P.II) {d : ℕ} (hd : (↑x).dim = d) : ⋯.index hd ≠ 0
• ne_last (x : ↑P.II) {d : ℕ} (hd : (↑x).dim = d) : ⋯.index hd ≠ Fin.last (d + 1)

def SSet.Subcomplex.Pairing.AncestralRel {X : SSet} {A : X.Subcomplex} (P : A.Pairing) (x y : ↑P.II) : Prop

The ancestrality relation on type (II) simplices.

Equations

• P.AncestralRel x y = (x ≠ y ∧ ↑x < ↑(P.p y))

class SSet.Subcomplex.Pairing.IsRegular {X : SSet} {A : X.Subcomplex} (P : A.Pairing) extends P.IsProper : Prop

A proper pairing is regular when the ancestrality relation is well founded.

• isUniquelyCodimOneFace (x : ↑P.II) : (↑x).IsUniquelyCodimOneFace (↑(P.p x)).toS
• wf : WellFounded P.AncestralRel

theorem SSet.Subcomplex.Pairing.wf {X : SSet} {A : X.Subcomplex} (P : A.Pairing) [P.IsRegular] : WellFounded P.AncestralRel

instance SSet.Subcomplex.Pairing.instIsWellFoundedElemNIIAncestralRel {X : SSet} {A : X.Subcomplex} (P : A.Pairing) [P.IsRegular] : IsWellFounded (↑P.II) P.AncestralRel