The relative cell complex attached to a rank function for a pairing

Let A be a subcomplex of a simplicial set X. Let P : A.Pairing be a proper pairing (in the sense of Moss) and f : P.RankFunction ι be a rank function. We show that the inclusion A.ι is a relative cell complex with basic cells given by horn inclusions.

References

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

structure SSet.Subcomplex.Pairing.RankFunction.Cell {X : SSet} {A : X.Subcomplex} {P : A.Pairing} {ι : Type v} [LinearOrder ι] (f : P.RankFunction ι) (i : ι) : Type u

Given a rank function f : P.RankFunction ι for a pairing P of a subcomplex A of X : SSet, and i : ι, this is the type of type (II) simplices of rank i.

• s : ↑P.II

  a type (II) simplex

• rank_s : f.rank self.s = i

theorem SSet.Subcomplex.Pairing.RankFunction.Cell.ext {X : SSet} {A : X.Subcomplex} {P : A.Pairing} {ι : Type v} {inst✝ : LinearOrder ι} {f : P.RankFunction ι} {i : ι} {x y : f.Cell i} (s : x.s = y.s) : x = y

theorem SSet.Subcomplex.Pairing.RankFunction.Cell.ext_iff {X : SSet} {A : X.Subcomplex} {P : A.Pairing} {ι : Type v} {inst✝ : LinearOrder ι} {f : P.RankFunction ι} {i : ι} {x y : f.Cell i} : x = y ↔ x.s = y.s

@[reducible, inline]

abbrev SSet.Subcomplex.Pairing.RankFunction.Cell.dim {X : SSet} {A : X.Subcomplex} {P : A.Pairing} {ι : Type v} [LinearOrder ι] {f : P.RankFunction ι} {i : ι} (c : f.Cell i) : ℕ

The dimension c.dim of a cell c of a rank function for a pairing P of a subcomplex of a simplicial set. This is defined as the dimension of the corresponding type (II) simplex. (In the case P is proper, the corresponding type (I) simplex will be of dimension c.dim + 1.)

Equations

• c.dim = (↑c.s).dim

noncomputable def SSet.Subcomplex.Pairing.RankFunction.Cell.index {X : SSet} {A : X.Subcomplex} {P : A.Pairing} {ι : Type v} [LinearOrder ι] {f : P.RankFunction ι} {i : ι} (c : f.Cell i) [P.IsProper] : Fin (c.dim + 2)

If c is a cell of a rank function for a proper pairing P of a subcomplex of a simplicial set, this is the index in Fin (c.dim + 2) of the face of the type (I) simplex given by the corresponding type (II) simplex.

Equations

• c.index = ⋯.index ⋯

@[reducible, inline]

noncomputable abbrev SSet.Subcomplex.Pairing.RankFunction.Cell.horn {X : SSet} {A : X.Subcomplex} {P : A.Pairing} {ι : Type v} [LinearOrder ι] {f : P.RankFunction ι} {i : ι} (c : f.Cell i) [P.IsProper] : (stdSimplex.obj { len := c.dim + 1 }).Subcomplex

The horn in the standard simplex corresponding to a cell of a rank function for a proper pairing of a subcomplex of a simplicial set.

Equations

• c.horn = SSet.horn (c.dim + 1) c.index

@[reducible, inline]

abbrev SSet.Subcomplex.Pairing.RankFunction.Cell.map {X : SSet} {A : X.Subcomplex} {P : A.Pairing} {ι : Type v} [LinearOrder ι] {f : P.RankFunction ι} {i : ι} (c : f.Cell i) [P.IsProper] : stdSimplex.obj { len := c.dim + 1 } ⟶ X

The morphism Δ[c.dim + 1] ⟶ X corresponding to a cell of a rank function for a proper pairing of a subcomplex of X : SSet.

Equations

• c.map = SSet.yonedaEquiv.symm ((↑(P.p c.s)).cast ⋯).simplex

@[simp]

theorem SSet.Subcomplex.Pairing.RankFunction.Cell.range_map {X : SSet} {A : X.Subcomplex} {P : A.Pairing} {ι : Type v} [LinearOrder ι] {f : P.RankFunction ι} {i : ι} (c : f.Cell i) [P.IsProper] : range c.map = (↑(P.p c.s)).subcomplex

theorem SSet.Subcomplex.Pairing.RankFunction.Cell.map_app_objEquiv_symm_δ_index {X : SSet} {A : X.Subcomplex} {P : A.Pairing} {ι : Type v} [LinearOrder ι] {f : P.RankFunction ι} {i : ι} (c : f.Cell i) [P.IsProper] : (CategoryTheory.ConcreteCategory.hom (c.map.app (Opposite.op { len := c.dim }))) (stdSimplex.objEquiv.symm (SimplexCategory.δ c.index)) = (↑c.s).simplex

theorem SSet.Subcomplex.Pairing.RankFunction.Cell.subcomplex_not_le_image_horn {X : SSet} {A : X.Subcomplex} {P : A.Pairing} {ι : Type v} [LinearOrder ι] {f : P.RankFunction ι} {i : ι} (c : f.Cell i) [P.IsProper] : ¬(↑c.s).subcomplex ≤ c.horn.image c.map

theorem SSet.Subcomplex.Pairing.RankFunction.Cell.image_horn_lt_subcomplex {X : SSet} {A : X.Subcomplex} {P : A.Pairing} {ι : Type v} [LinearOrder ι] {f : P.RankFunction ι} {i : ι} (c : f.Cell i) [P.IsProper] : c.horn.image c.map < (↑(P.p c.s)).subcomplex

@[simp]

theorem SSet.Subcomplex.Pairing.RankFunction.Cell.image_face_index_compl {X : SSet} {A : X.Subcomplex} {P : A.Pairing} {ι : Type v} [LinearOrder ι] {f : P.RankFunction ι} {i : ι} (c : f.Cell i) [P.IsProper] : (stdSimplex.face {c.index}ᶜ).image c.map = (↑c.s).subcomplex

@[reducible, inline]

noncomputable abbrev SSet.Subcomplex.Pairing.RankFunction.basicCell {X : SSet} {A : X.Subcomplex} {P : A.Pairing} {ι : Type v} [LinearOrder ι] (f : P.RankFunction ι) [P.IsProper] (i : ι) (c : f.Cell i) : c.horn.toSSet ⟶ stdSimplex.obj { len := c.dim + 1 }

The horn inclusion corresponding to a cell of a rank function for a proper pairing of a subcomplex of a simplicial set.

Equations

• f.basicCell i c = c.horn.ι

def SSet.Subcomplex.Pairing.RankFunction.filtration {X : SSet} {A : X.Subcomplex} {P : A.Pairing} {ι : Type v} [LinearOrder ι] (f : P.RankFunction ι) (i : ι) : X.Subcomplex

The filtration of a simplicial set given by a rank function for a proper pairing of a subcomplex.

Equations

• f.filtration i = A ⊔ ⨆ (j : ι), ⨆ (_ : j < i), ⨆ (c : f.Cell j), (↑(P.p c.s)).subcomplex

theorem SSet.Subcomplex.Pairing.RankFunction.filtration_def {X : SSet} {A : X.Subcomplex} {P : A.Pairing} {ι : Type v} [LinearOrder ι] (f : P.RankFunction ι) (i : ι) : f.filtration i = A ⊔ ⨆ (j : ι), ⨆ (_ : j < i), ⨆ (c : f.Cell j), (↑(P.p c.s)).subcomplex

theorem SSet.Subcomplex.Pairing.RankFunction.subcomplex_le_filtration {X : SSet} {A : X.Subcomplex} {P : A.Pairing} {ι : Type v} [LinearOrder ι] (f : P.RankFunction ι) {j : ι} (c : f.Cell j) {i : ι} (h : j < i) : (↑(P.p c.s)).subcomplex ≤ f.filtration i

@[simp]

theorem SSet.Subcomplex.Pairing.RankFunction.le_filtration {X : SSet} {A : X.Subcomplex} {P : A.Pairing} {ι : Type v} [LinearOrder ι] (f : P.RankFunction ι) (i : ι) : A ≤ f.filtration i

@[simp]

theorem SSet.Subcomplex.Pairing.RankFunction.filtration_bot {X : SSet} {A : X.Subcomplex} {P : A.Pairing} {ι : Type v} [LinearOrder ι] (f : P.RankFunction ι) [OrderBot ι] : f.filtration ⊥ = A

theorem SSet.Subcomplex.Pairing.RankFunction.filtration_monotone {X : SSet} {A : X.Subcomplex} {P : A.Pairing} {ι : Type v} [LinearOrder ι] (f : P.RankFunction ι) : Monotone f.filtration

theorem SSet.Subcomplex.Pairing.RankFunction.filtration_succ {X : SSet} {A : X.Subcomplex} {P : A.Pairing} {ι : Type v} [LinearOrder ι] (f : P.RankFunction ι) [SuccOrder ι] (i : ι) (hi : ¬IsMax i) : f.filtration (Order.succ i) = f.filtration i ⊔ ⨆ (c : f.Cell i), (↑(P.p c.s)).subcomplex

theorem SSet.Subcomplex.Pairing.RankFunction.filtration_of_isSuccLimit {X : SSet} {A : X.Subcomplex} {P : A.Pairing} {ι : Type v} [LinearOrder ι] (f : P.RankFunction ι) [OrderBot ι] [SuccOrder ι] (i : ι) (hi : Order.IsSuccLimit i) : f.filtration i = ⨆ (j : ι), ⨆ (_ : j < i), f.filtration j

theorem SSet.Subcomplex.Pairing.RankFunction.iSup_filtration_iio {X : SSet} {A : X.Subcomplex} {P : A.Pairing} {ι : Type v} [LinearOrder ι] (f : P.RankFunction ι) [OrderBot ι] [SuccOrder ι] (m : ι) (hm : Order.IsSuccLimit m) : ⨆ (i : ↑(Set.Iio m)), f.filtration ↑i = f.filtration m

theorem SSet.Subcomplex.Pairing.RankFunction.Cell.subcomplex_not_le_filtration {X : SSet} {A : X.Subcomplex} {P : A.Pairing} {ι : Type v} [LinearOrder ι] {f : P.RankFunction ι} {j : ι} (c : f.Cell j) : ¬(↑c.s).subcomplex ≤ f.filtration j

theorem SSet.Subcomplex.Pairing.RankFunction.iSup_filtration {X : SSet} {A : X.Subcomplex} {P : A.Pairing} {ι : Type v} [LinearOrder ι] (f : P.RankFunction ι) [P.IsProper] [OrderBot ι] [SuccOrder ι] [NoMaxOrder ι] : ⨆ (i : ι), f.filtration i = ⊤

def SSet.Subcomplex.Pairing.RankFunction.Cell.mapToSucc {X : SSet} {A : X.Subcomplex} {P : A.Pairing} {ι : Type v} [LinearOrder ι] {f : P.RankFunction ι} [P.IsProper] {j : ι} [SuccOrder ι] [NoMaxOrder ι] (c : f.Cell j) : stdSimplex.obj { len := c.dim + 1 } ⟶ (f.filtration (Order.succ j)).toSSet

The morphism Δ[c.dim + 1] ⟶ f.filtration (Order.succ j) given by c : f.Cell j, when f is a rank function for a proper pairing of a subcomplex of a simplicial set.

Equations

• c.mapToSucc = SSet.Subcomplex.lift c.map ⋯

@[simp]

theorem SSet.Subcomplex.Pairing.RankFunction.Cell.mapToSucc_ι {X : SSet} {A : X.Subcomplex} {P : A.Pairing} {ι : Type v} [LinearOrder ι] {f : P.RankFunction ι} [P.IsProper] {j : ι} [SuccOrder ι] [NoMaxOrder ι] (c : f.Cell j) : CategoryTheory.CategoryStruct.comp c.mapToSucc (f.filtration (Order.succ j)).ι = c.map

@[simp]

theorem SSet.Subcomplex.Pairing.RankFunction.Cell.mapToSucc_ι_assoc {X : SSet} {A : X.Subcomplex} {P : A.Pairing} {ι : Type v} [LinearOrder ι] {f : P.RankFunction ι} [P.IsProper] {j : ι} [SuccOrder ι] [NoMaxOrder ι] (c : f.Cell j) {Z : SSet} (h : X ⟶ Z) : CategoryTheory.CategoryStruct.comp c.mapToSucc (CategoryTheory.CategoryStruct.comp (f.filtration (Order.succ j)).ι h) = CategoryTheory.CategoryStruct.comp c.map h

The main technical result in this section is SSet.Subcomplex.Pairing.RankFunction.isPushout which states that there is a pushout square:

                                      f.t j
∐ fun (c : f.Cell j) ↦ c.horn  -------------> f.filtration j
               |                                   |
         f.m j |                                   |
               v                      f.b j        v
∐ fun (c : f.Cell j) ↦ Δ[c.dim + 1]  -------> f.filtration (Order.succ j)

The map on the left is a coproduct of horn inclusions (the source and target of the morphism f.m j are denoted f.sigmaHorn j and f.sigmaStdSimplex j).

@[reducible, inline]

noncomputable abbrev SSet.Subcomplex.Pairing.RankFunction.sigmaHorn {X : SSet} {A : X.Subcomplex} {P : A.Pairing} {ι : Type v} [LinearOrder ι] (f : P.RankFunction ι) [P.IsProper] (j : ι) : SSet

Given a rank function for a proper pairing of a subcomplex of a simplicial set, this is the coproduct of the horns corresponding to all cells of rank j.

Equations

• f.sigmaHorn j = ∐ fun (c : f.Cell j) => c.horn.toSSet

@[reducible, inline]

noncomputable abbrev SSet.Subcomplex.Pairing.RankFunction.Cell.ιSigmaHorn {X : SSet} {A : X.Subcomplex} {P : A.Pairing} {ι : Type v} [LinearOrder ι] {f : P.RankFunction ι} [P.IsProper] {j : ι} (c : f.Cell j) : c.horn.toSSet ⟶ f.sigmaHorn j

Given a cell c of rank j for a rank function f for a proper pairing of a subcomplex of a simplicial set, this is the inclusion of c.horn into f.sigmaHorn j.

Equations

• c.ιSigmaHorn = CategoryTheory.Limits.Sigma.ι (fun (c : f.Cell j) => c.horn.toSSet) c

@[reducible, inline]

noncomputable abbrev SSet.Subcomplex.Pairing.RankFunction.sigmaStdSimplex {X : SSet} {A : X.Subcomplex} {P : A.Pairing} {ι : Type v} [LinearOrder ι] (f : P.RankFunction ι) (j : ι) : SSet

Given a rank function for a proper pairing of a subcomplex of a simplicial set, this is coproduct of the standard simplices corresponding to all cells of rank j.

Equations

• f.sigmaStdSimplex j = ∐ fun (i : f.Cell j) => SSet.stdSimplex.obj { len := i.dim + 1 }

@[reducible, inline]

noncomputable abbrev SSet.Subcomplex.Pairing.RankFunction.Cell.ιSigmaStdSimplex {X : SSet} {A : X.Subcomplex} {P : A.Pairing} {ι : Type v} [LinearOrder ι] {f : P.RankFunction ι} {j : ι} (c : f.Cell j) : stdSimplex.obj { len := c.dim + 1 } ⟶ f.sigmaStdSimplex j

Given a cell c of rank j for a rank function f for a proper pairing of a subcomplex of a simplicial set, this is the inclusion of Δ[c.dim + 1] into f.sigmaStdSimplex j.

Equations

• c.ιSigmaStdSimplex = CategoryTheory.Limits.Sigma.ι (fun (c : f.Cell j) => SSet.stdSimplex.obj { len := c.dim + 1 }) c

theorem SSet.Subcomplex.Pairing.RankFunction.ιSigmaHorn_jointly_surjective {X : SSet} {A : X.Subcomplex} {P : A.Pairing} {ι : Type v} [LinearOrder ι] (f : P.RankFunction ι) [P.IsProper] {d : ℕ} {j : ι} (a : (f.sigmaHorn j).obj (Opposite.op { len := d })) : ∃ (c : f.Cell j) (x : c.horn.toSSet.obj (Opposite.op { len := d })), (CategoryTheory.ConcreteCategory.hom (c.ιSigmaHorn.app (Opposite.op { len := d }))) x = a

theorem SSet.Subcomplex.Pairing.RankFunction.ιSigmaStdSimplex_jointly_surjective {X : SSet} {A : X.Subcomplex} {P : A.Pairing} {ι : Type v} [LinearOrder ι] (f : P.RankFunction ι) {d : ℕ} {j : ι} (a : (f.sigmaStdSimplex j).obj (Opposite.op { len := d })) : ∃ (c : f.Cell j) (x : (stdSimplex.obj { len := c.dim + 1 }).obj (Opposite.op { len := d })), (CategoryTheory.ConcreteCategory.hom (c.ιSigmaStdSimplex.app (Opposite.op { len := d }))) x = a

theorem SSet.Subcomplex.Pairing.RankFunction.ιSigmaStdSimplex_eq_iff {X : SSet} {A : X.Subcomplex} {P : A.Pairing} {ι : Type v} [LinearOrder ι] (f : P.RankFunction ι) {j : ι} {d : ℕ} (x : f.Cell j) (s : (stdSimplex.obj { len := x.dim + 1 }).obj (Opposite.op { len := d })) (y : f.Cell j) (t : (stdSimplex.obj { len := y.dim + 1 }).obj (Opposite.op { len := d })) : (CategoryTheory.ConcreteCategory.hom (x.ιSigmaStdSimplex.app (Opposite.op { len := d }))) s = (CategoryTheory.ConcreteCategory.hom (y.ιSigmaStdSimplex.app (Opposite.op { len := d }))) t ↔ ∃ (h : x = y), t = cast ⋯ s

instance SSet.Subcomplex.Pairing.RankFunction.instMonoιSigmaStdSimplex {X : SSet} {A : X.Subcomplex} {P : A.Pairing} {ι : Type v} [LinearOrder ι] (f : P.RankFunction ι) {j : ι} (c : f.Cell j) : CategoryTheory.Mono c.ιSigmaStdSimplex

noncomputable def SSet.Subcomplex.Pairing.RankFunction.m {X : SSet} {A : X.Subcomplex} {P : A.Pairing} {ι : Type v} [LinearOrder ι] (f : P.RankFunction ι) [P.IsProper] (j : ι) : f.sigmaHorn j ⟶ f.sigmaStdSimplex j

The coproduct of the horn inclusions corresponding to all the cells of rank j for a rank function for a proper pairing of a subcomplex of a simplicial set.

Equations

• f.m j = CategoryTheory.Limits.Sigma.map (f.basicCell j)

instance SSet.Subcomplex.Pairing.RankFunction.instMonoM {X : SSet} {A : X.Subcomplex} {P : A.Pairing} {ι : Type v} [LinearOrder ι] (f : P.RankFunction ι) [P.IsProper] (j : ι) : CategoryTheory.Mono (f.m j)

@[simp]

theorem SSet.Subcomplex.Pairing.RankFunction.Cell.ι_m {X : SSet} {A : X.Subcomplex} {P : A.Pairing} {ι : Type v} [LinearOrder ι] (f : P.RankFunction ι) [P.IsProper] {j : ι} (c : f.Cell j) : CategoryTheory.CategoryStruct.comp c.ιSigmaHorn (f.m j) = CategoryTheory.CategoryStruct.comp c.horn.ι c.ιSigmaStdSimplex

@[simp]

theorem SSet.Subcomplex.Pairing.RankFunction.Cell.ι_m_assoc {X : SSet} {A : X.Subcomplex} {P : A.Pairing} {ι : Type v} [LinearOrder ι] (f : P.RankFunction ι) [P.IsProper] {j : ι} (c : f.Cell j) {Z : SSet} (h : f.sigmaStdSimplex j ⟶ Z) : CategoryTheory.CategoryStruct.comp c.ιSigmaHorn (CategoryTheory.CategoryStruct.comp (f.m j) h) = CategoryTheory.CategoryStruct.comp c.horn.ι (CategoryTheory.CategoryStruct.comp c.ιSigmaStdSimplex h)

@[simp]

theorem SSet.Subcomplex.Pairing.RankFunction.Cell.preimage_filtration_map {X : SSet} {A : X.Subcomplex} {P : A.Pairing} {ι : Type v} [LinearOrder ι] (f : P.RankFunction ι) [P.IsProper] {j : ι} (c : f.Cell j) : (f.filtration j).preimage c.map = c.horn

noncomputable def SSet.Subcomplex.Pairing.RankFunction.Cell.mapHorn {X : SSet} {A : X.Subcomplex} {P : A.Pairing} {ι : Type v} [LinearOrder ι] (f : P.RankFunction ι) [P.IsProper] {j : ι} (c : f.Cell j) : c.horn.toSSet ⟶ (f.filtration j).toSSet

Given a cell c of rank j for a rank function f for a proper pairing of a subcomplex of a simplicial set, this is the induced morphism c.horn ⟶ f.filtration j.

Equations

• SSet.Subcomplex.Pairing.RankFunction.Cell.mapHorn f c = SSet.Subcomplex.lift (CategoryTheory.CategoryStruct.comp c.horn.ι c.map) ⋯

@[simp]

theorem SSet.Subcomplex.Pairing.RankFunction.Cell.mapHorn_ι {X : SSet} {A : X.Subcomplex} {P : A.Pairing} {ι : Type v} [LinearOrder ι] (f : P.RankFunction ι) [P.IsProper] {j : ι} (c : f.Cell j) : CategoryTheory.CategoryStruct.comp (mapHorn f c) (f.filtration j).ι = CategoryTheory.CategoryStruct.comp c.horn.ι c.map

@[simp]

theorem SSet.Subcomplex.Pairing.RankFunction.Cell.mapHorn_ι_assoc {X : SSet} {A : X.Subcomplex} {P : A.Pairing} {ι : Type v} [LinearOrder ι] (f : P.RankFunction ι) [P.IsProper] {j : ι} (c : f.Cell j) {Z : SSet} (h : X ⟶ Z) : CategoryTheory.CategoryStruct.comp (mapHorn f c) (CategoryTheory.CategoryStruct.comp (f.filtration j).ι h) = CategoryTheory.CategoryStruct.comp c.horn.ι (CategoryTheory.CategoryStruct.comp c.map h)

noncomputable def SSet.Subcomplex.Pairing.RankFunction.t {X : SSet} {A : X.Subcomplex} {P : A.Pairing} {ι : Type v} [LinearOrder ι] (f : P.RankFunction ι) [P.IsProper] (j : ι) : f.sigmaHorn j ⟶ (f.filtration j).toSSet

Given a rank function f : P.RankFunction ι for a proper pairing P of a subcomplex of a simplicial set, this is the induced morphism f.sigmaHorn j ⟶ f.filtration j for any j : ι.

Equations

• f.t j = CategoryTheory.Limits.Sigma.desc fun (c : f.Cell j) => SSet.Subcomplex.Pairing.RankFunction.Cell.mapHorn f c

@[simp]

theorem SSet.Subcomplex.Pairing.RankFunction.Cell.ι_t {X : SSet} {A : X.Subcomplex} {P : A.Pairing} {ι : Type v} [LinearOrder ι] {f : P.RankFunction ι} [P.IsProper] {j : ι} (c : f.Cell j) : CategoryTheory.CategoryStruct.comp c.ιSigmaHorn (f.t j) = mapHorn f c

@[simp]

theorem SSet.Subcomplex.Pairing.RankFunction.Cell.ι_t_assoc {X : SSet} {A : X.Subcomplex} {P : A.Pairing} {ι : Type v} [LinearOrder ι] {f : P.RankFunction ι} [P.IsProper] {j : ι} (c : f.Cell j) {Z : SSet} (h : (f.filtration j).toSSet ⟶ Z) : CategoryTheory.CategoryStruct.comp c.ιSigmaHorn (CategoryTheory.CategoryStruct.comp (f.t j) h) = CategoryTheory.CategoryStruct.comp (mapHorn f c) h

@[simp]

theorem SSet.Subcomplex.Pairing.RankFunction.Cell.ι_t_app {X : SSet} {A : X.Subcomplex} {P : A.Pairing} {ι : Type v} [LinearOrder ι] {f : P.RankFunction ι} [P.IsProper] {j : ι} (c : f.Cell j) (x : SimplexCategoryᵒᵖ) : CategoryTheory.CategoryStruct.comp (c.ιSigmaHorn.app x) ((f.t j).app x) = (mapHorn f c).app x

@[simp]

theorem SSet.Subcomplex.Pairing.RankFunction.Cell.ι_t_app_assoc {X : SSet} {A : X.Subcomplex} {P : A.Pairing} {ι : Type v} [LinearOrder ι] {f : P.RankFunction ι} [P.IsProper] {j : ι} (c : f.Cell j) (x : SimplexCategoryᵒᵖ) {Z : Type u} (h : (f.filtration j).toSSet.obj x ⟶ Z) : CategoryTheory.CategoryStruct.comp (c.ιSigmaHorn.app x) (CategoryTheory.CategoryStruct.comp ((f.t j).app x) h) = CategoryTheory.CategoryStruct.comp ((mapHorn f c).app x) h

@[simp]

theorem SSet.Subcomplex.Pairing.RankFunction.Cell.ι_t_app_apply {X : SSet} {A : X.Subcomplex} {P : A.Pairing} {ι : Type v} [LinearOrder ι] {f : P.RankFunction ι} [P.IsProper] {j : ι} (c : f.Cell j) (x : SimplexCategoryᵒᵖ) (x✝ : c.horn.toSSet.obj x) : (CategoryTheory.ConcreteCategory.hom ((f.t j).app x)) ((CategoryTheory.ConcreteCategory.hom (c.ιSigmaHorn.app x)) x✝) = (CategoryTheory.ConcreteCategory.hom ((mapHorn f c).app x)) x✝

noncomputable def SSet.Subcomplex.Pairing.RankFunction.Cell.type₁ {X : SSet} {A : X.Subcomplex} {P : A.Pairing} {ι : Type v} [LinearOrder ι] (f : P.RankFunction ι) [P.IsProper] {j : ι} (c : f.Cell j) : (range (f.m j)).N

Given a rank j cell c for a rank function f for a proper pairing of a subcomplex of a simplicial set, this is the nondegenerate simplex in f.sigmaStdSimplex j not in the image of f.m j : f.sigmaHorn j ⟶ f.sigmaStdSimplex j which corresponds to c.ιSigmaStdSimplex.

Equations

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

@[simp]

theorem SSet.Subcomplex.Pairing.RankFunction.Cell.type₁_simplex {X : SSet} {A : X.Subcomplex} {P : A.Pairing} {ι : Type v} [LinearOrder ι] (f : P.RankFunction ι) [P.IsProper] {j : ι} (c : f.Cell j) : (type₁ f c).simplex = (CategoryTheory.ConcreteCategory.hom (c.ιSigmaStdSimplex.app (Opposite.op { len := c.dim + 1 }))) (stdSimplex.objEquiv.symm (CategoryTheory.CategoryStruct.id (Opposite.unop (Opposite.op { len := c.dim + 1 }))))

@[simp]

theorem SSet.Subcomplex.Pairing.RankFunction.Cell.type₁_dim {X : SSet} {A : X.Subcomplex} {P : A.Pairing} {ι : Type v} [LinearOrder ι] (f : P.RankFunction ι) [P.IsProper] {j : ι} (c : f.Cell j) : (type₁ f c).dim = c.dim + 1

noncomputable def SSet.Subcomplex.Pairing.RankFunction.Cell.type₂ {X : SSet} {A : X.Subcomplex} {P : A.Pairing} {ι : Type v} [LinearOrder ι] (f : P.RankFunction ι) [P.IsProper] {j : ι} (c : f.Cell j) : (range (f.m j)).N

Given a rank j cell c for a rank function f for a proper pairing of a subcomplex of a simplicial set, this is the nondegenerate simplex in f.sigmaStdSimplex j not in the image of f.m j : f.sigmaHorn j ⟶ f.sigmaStdSimplex j which corresponds to the c.indexth-face of c.type₁.

Equations

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

@[simp]

theorem SSet.Subcomplex.Pairing.RankFunction.Cell.type₂_dim {X : SSet} {A : X.Subcomplex} {P : A.Pairing} {ι : Type v} [LinearOrder ι] (f : P.RankFunction ι) [P.IsProper] {j : ι} (c : f.Cell j) : (type₂ f c).dim = c.dim

@[simp]

theorem SSet.Subcomplex.Pairing.RankFunction.Cell.type₂_simplex {X : SSet} {A : X.Subcomplex} {P : A.Pairing} {ι : Type v} [LinearOrder ι] (f : P.RankFunction ι) [P.IsProper] {j : ι} (c : f.Cell j) : (type₂ f c).simplex = (CategoryTheory.ConcreteCategory.hom (c.ιSigmaStdSimplex.app (Opposite.op { len := c.dim }))) (stdSimplex.objEquiv.symm (SimplexCategory.δ c.index))

theorem SSet.Subcomplex.Pairing.RankFunction.exists_or_of_range_m_N {X : SSet} {A : X.Subcomplex} {P : A.Pairing} {ι : Type v} [LinearOrder ι] (f : P.RankFunction ι) [P.IsProper] {j : ι} (s : (range (f.m j)).N) : ∃ (c : f.Cell j), s = Cell.type₁ f c ∨ s = Cell.type₂ f c

noncomputable def SSet.Subcomplex.Pairing.RankFunction.b {X : SSet} {A : X.Subcomplex} {P : A.Pairing} {ι : Type v} [LinearOrder ι] (f : P.RankFunction ι) [P.IsProper] [SuccOrder ι] [NoMaxOrder ι] (j : ι) : f.sigmaStdSimplex j ⟶ (f.filtration (Order.succ j)).toSSet

Given a rank function f : P.RankFunction ι for a proper pairing P of a subcomplex of a simplicial set, this is the induced morphism f.sigmaStdSimplex j ⟶ f.filtration (Order.succ j) for any j : ι.

Equations

• f.b j = CategoryTheory.Limits.Sigma.desc fun (c : f.Cell j) => c.mapToSucc

@[simp]

theorem SSet.Subcomplex.Pairing.RankFunction.Cell.ι_b {X : SSet} {A : X.Subcomplex} {P : A.Pairing} {ι : Type v} [LinearOrder ι] {f : P.RankFunction ι} [P.IsProper] [SuccOrder ι] [NoMaxOrder ι] {j : ι} (c : f.Cell j) : CategoryTheory.CategoryStruct.comp c.ιSigmaStdSimplex (f.b j) = c.mapToSucc

@[simp]

theorem SSet.Subcomplex.Pairing.RankFunction.Cell.ι_b_assoc {X : SSet} {A : X.Subcomplex} {P : A.Pairing} {ι : Type v} [LinearOrder ι] {f : P.RankFunction ι} [P.IsProper] [SuccOrder ι] [NoMaxOrder ι] {j : ι} (c : f.Cell j) {Z : SSet} (h : (f.filtration (Order.succ j)).toSSet ⟶ Z) : CategoryTheory.CategoryStruct.comp c.ιSigmaStdSimplex (CategoryTheory.CategoryStruct.comp (f.b j) h) = CategoryTheory.CategoryStruct.comp c.mapToSucc h

@[simp]

theorem SSet.Subcomplex.Pairing.RankFunction.Cell.ι_b_app {X : SSet} {A : X.Subcomplex} {P : A.Pairing} {ι : Type v} [LinearOrder ι] {f : P.RankFunction ι} [P.IsProper] [SuccOrder ι] [NoMaxOrder ι] {j : ι} (c : f.Cell j) (x : SimplexCategoryᵒᵖ) : CategoryTheory.CategoryStruct.comp (c.ιSigmaStdSimplex.app x) ((f.b j).app x) = c.mapToSucc.app x

@[simp]

theorem SSet.Subcomplex.Pairing.RankFunction.Cell.ι_b_app_assoc {X : SSet} {A : X.Subcomplex} {P : A.Pairing} {ι : Type v} [LinearOrder ι] {f : P.RankFunction ι} [P.IsProper] [SuccOrder ι] [NoMaxOrder ι] {j : ι} (c : f.Cell j) (x : SimplexCategoryᵒᵖ) {Z : Type u} (h : (f.filtration (Order.succ j)).toSSet.obj x ⟶ Z) : CategoryTheory.CategoryStruct.comp (c.ιSigmaStdSimplex.app x) (CategoryTheory.CategoryStruct.comp ((f.b j).app x) h) = CategoryTheory.CategoryStruct.comp (c.mapToSucc.app x) h

@[simp]

theorem SSet.Subcomplex.Pairing.RankFunction.Cell.ι_b_app_apply {X : SSet} {A : X.Subcomplex} {P : A.Pairing} {ι : Type v} [LinearOrder ι] {f : P.RankFunction ι} [P.IsProper] [SuccOrder ι] [NoMaxOrder ι] {j : ι} (c : f.Cell j) (x : SimplexCategoryᵒᵖ) (x✝ : (stdSimplex.obj { len := c.dim + 1 }).obj x) : (CategoryTheory.ConcreteCategory.hom ((f.b j).app x)) ((CategoryTheory.ConcreteCategory.hom (c.ιSigmaStdSimplex.app x)) x✝) = (CategoryTheory.ConcreteCategory.hom (c.mapToSucc.app x)) x✝

theorem SSet.Subcomplex.Pairing.RankFunction.w {X : SSet} {A : X.Subcomplex} {P : A.Pairing} {ι : Type v} [LinearOrder ι] (f : P.RankFunction ι) [P.IsProper] [SuccOrder ι] [NoMaxOrder ι] (j : ι) : CategoryTheory.CategoryStruct.comp (f.t j) (homOfLE ⋯) = CategoryTheory.CategoryStruct.comp (f.m j) (f.b j)

theorem SSet.Subcomplex.Pairing.RankFunction.w_assoc {X : SSet} {A : X.Subcomplex} {P : A.Pairing} {ι : Type v} [LinearOrder ι] (f : P.RankFunction ι) [P.IsProper] [SuccOrder ι] [NoMaxOrder ι] (j : ι) {Z : SSet} (h : (f.filtration (Order.succ j)).toSSet ⟶ Z) : CategoryTheory.CategoryStruct.comp (f.t j) (CategoryTheory.CategoryStruct.comp (homOfLE ⋯) h) = CategoryTheory.CategoryStruct.comp (f.m j) (CategoryTheory.CategoryStruct.comp (f.b j) h)

theorem SSet.Subcomplex.Pairing.RankFunction.isPullback {X : SSet} {A : X.Subcomplex} {P : A.Pairing} {ι : Type v} [LinearOrder ι] (f : P.RankFunction ι) [P.IsProper] [SuccOrder ι] [NoMaxOrder ι] (j : ι) : CategoryTheory.IsPullback (f.t j) (f.m j) (homOfLE ⋯) (f.b j)

theorem SSet.Subcomplex.Pairing.RankFunction.range_homOfLE_app_union_range_b_app {X : SSet} {A : X.Subcomplex} {P : A.Pairing} {ι : Type v} [LinearOrder ι] (f : P.RankFunction ι) [P.IsProper] [SuccOrder ι] [NoMaxOrder ι] (j : ι) (d : SimplexCategoryᵒᵖ) : Set.range ⇑(CategoryTheory.ConcreteCategory.hom ((homOfLE ⋯).app d)) ⊔ Set.range ⇑(CategoryTheory.ConcreteCategory.hom ((f.b j).app d)) = Set.univ

noncomputable def SSet.Subcomplex.Pairing.RankFunction.mapN {X : SSet} {A : X.Subcomplex} {P : A.Pairing} {ι : Type v} [LinearOrder ι] (f : P.RankFunction ι) [P.IsProper] [SuccOrder ι] [NoMaxOrder ι] {j : ι} (x : (range (f.m j)).N) : X.S

Given a rank function f : P.RankFunction ι for a proper pairing of a subcomplex of a simplicial set X, this is the simplex of X corresponding to an element in (Subcomplex.range (f.m j)).N.

Equations

• f.mapN x = { dim := x.dim, simplex := ↑((CategoryTheory.ConcreteCategory.hom ((f.b j).app (Opposite.op { len := x.dim }))) x.simplex) }

@[simp]

theorem SSet.Subcomplex.Pairing.RankFunction.mapN_type₁ {X : SSet} {A : X.Subcomplex} {P : A.Pairing} {ι : Type v} [LinearOrder ι] (f : P.RankFunction ι) [P.IsProper] [SuccOrder ι] [NoMaxOrder ι] {j : ι} (c : f.Cell j) : f.mapN (Cell.type₁ f c) = { dim := (↑(P.p c.s)).dim, simplex := (↑(P.p c.s)).simplex }

@[simp]

theorem SSet.Subcomplex.Pairing.RankFunction.mapN_type₂ {X : SSet} {A : X.Subcomplex} {P : A.Pairing} {ι : Type v} [LinearOrder ι] (f : P.RankFunction ι) [P.IsProper] [SuccOrder ι] [NoMaxOrder ι] {j : ι} (c : f.Cell j) : f.mapN (Cell.type₂ f c) = { dim := (↑c.s).dim, simplex := (↑c.s).simplex }

theorem SSet.Subcomplex.Pairing.RankFunction.isPushout {X : SSet} {A : X.Subcomplex} {P : A.Pairing} {ι : Type v} [LinearOrder ι] (f : P.RankFunction ι) [P.IsProper] [SuccOrder ι] [NoMaxOrder ι] (j : ι) : CategoryTheory.IsPushout (f.t j) (f.m j) (homOfLE ⋯) (f.b j)

instance SSet.Subcomplex.Pairing.RankFunction.instIsWellOrderContinuousFunctor {X : SSet} {A : X.Subcomplex} {P : A.Pairing} {ι : Type v} [LinearOrder ι] (f : P.RankFunction ι) [SuccOrder ι] [OrderBot ι] : ⋯.functor.IsWellOrderContinuous

noncomputable def SSet.Subcomplex.Pairing.RankFunction.relativeCellComplex {X : SSet} {A : X.Subcomplex} {P : A.Pairing} {ι : Type v} [LinearOrder ι] (f : P.RankFunction ι) [P.IsProper] [SuccOrder ι] [OrderBot ι] [NoMaxOrder ι] [WellFoundedLT ι] : HomotopicalAlgebra.RelativeCellComplex f.basicCell A.ι

Given a rank function f : P.RankFunction ι for a proper pairing P of a subcomplex A of simplicial set X, the inclusion A.ι is a relative cell complex with basic cells given by horn inclusions.

Equations

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