Lifting against horn inclusions

A map of simplicial sets Λ[n + 1, i] ⟶ X out of a horn is the same as a compatible family of n-simplices of X, one for each face j ≠ i (SSet.horn.IsCompatible). Accordingly, a map p : X ⟶ Y has the right lifting property with respect to the horn inclusion Λ[n + 1, i] ⟶ Δ[n + 1] exactly when every compatible family of faces lying over the faces of an (n + 1)-simplex of Y extends to an (n + 1)-simplex of X over it (SSet.hasLiftingProperty_horn_ι_iff). This is the relative form of Mathlib's criterion SSet.KanComplex.iff for Kan complexes. It reduces horn-lifting conditions to statements about simplices and their faces, which is how such conditions are transported along constructions that act on simplices, such as universe lifts.

Kan fibrations and inner fibrations are the maps with the right lifting property with respect to all horn inclusions, respectively all inner horn inclusions (SSet.modelCategoryQuillen.rlp_J_iff, SSet.mem_innerFibrations_iff).

The map SSet.horn.IsCompatible.desc induced by a compatible family f sends a simplex of the face j to its image under f j (SSet.horn.IsCompatible.desc_app_ι_app), and when it extends to a simplex σ, the faces of σ are the members of f (SSet.horn.IsCompatible.δ_yonedaEquiv_of_desc_eq). An edge of a face of a horn is an edge of the horn (SSet.horn.ι_app_edge).

theorem SSet.horn.ι_app_edge {n : ℕ} (i j : Fin (n + 2)) (hj : j ≠ i) (a b : Fin (n + 1)) (hab : a ≤ b) : (CategoryTheory.ConcreteCategory.hom ((ι i j hj).app (Opposite.op { len := 1 }))) (stdSimplex.edge n a b hab) = edge (n + 1) i (j.succAbove a) (j.succAbove b) ⋯ ⋯

The edge from a to b of the face j of a horn Λ[n + 1, i] is the edge of the horn between the corresponding vertices j.succAbove a and j.succAbove b.

theorem SSet.horn.IsCompatible.desc_app_ι_app {X : SSet} {n : ℕ} {i : Fin (n + 2)} {f : (j : Fin (n + 2)) → j ≠ i → (stdSimplex.obj { len := n } ⟶ X)} (hf : horn.IsCompatible f) (j : Fin (n + 2)) (hj : j ≠ i) {d : SimplexCategoryᵒᵖ} (x : (stdSimplex.obj { len := n }).obj d) : (CategoryTheory.ConcreteCategory.hom (hf.desc.app d)) ((CategoryTheory.ConcreteCategory.hom ((ι i j hj).app d)) x) = (CategoryTheory.ConcreteCategory.hom ((f j hj).app d)) x

The map out of a horn induced by a compatible family f sends a simplex x of the face j to its image under f j.

theorem SSet.horn.IsCompatible.δ_yonedaEquiv_of_desc_eq {X : SSet} {n : ℕ} {i : Fin (n + 2)} {f : (j : Fin (n + 2)) → j ≠ i → (stdSimplex.obj { len := n } ⟶ X)} (hf : horn.IsCompatible f) {σ : stdSimplex.obj { len := n + 1 } ⟶ X} (hσ : hf.desc = CategoryTheory.CategoryStruct.comp (horn (n + 1) i).ι σ) (j : Fin (n + 2)) (hj : j ≠ i) : (CategoryTheory.ConcreteCategory.hom (CategoryTheory.SimplicialObject.δ X j)) (yonedaEquiv σ) = yonedaEquiv (f j hj)

If the map out of a horn induced by a compatible family f extends along Λ[n + 1, i] ⟶ Δ[n + 1] to a simplex σ, then the faces of σ are the members of f.

theorem SSet.hasLiftingProperty_horn_ι_iff {X Y : SSet} (p : X ⟶ Y) {n : ℕ} (i : Fin (n + 2)) : CategoryTheory.HasLiftingProperty (horn (n + 1) i).ι p ↔ ∀ (f : (j : Fin (n + 2)) → j ≠ i → (stdSimplex.obj { len := n } ⟶ X)), horn.IsCompatible f → ∀ (b : stdSimplex.obj { len := n + 1 } ⟶ Y), (∀ (j : Fin (n + 2)) (hj : j ≠ i), CategoryTheory.CategoryStruct.comp (f j hj) p = CategoryTheory.CategoryStruct.comp (stdSimplex.δ j) b) → ∃ (φ : stdSimplex.obj { len := n + 1 } ⟶ X), (∀ (j : Fin (n + 2)) (hj : j ≠ i), CategoryTheory.CategoryStruct.comp (stdSimplex.δ j) φ = f j hj) ∧ CategoryTheory.CategoryStruct.comp φ p = b

A map p has the right lifting property with respect to the horn inclusion Λ[n + 1, i] ⟶ Δ[n + 1] exactly when every compatible family of faces in the source of p, lying over the faces of an (n + 1)-simplex b of the target, extends to an (n + 1)-simplex over b.

theorem SSet.modelCategoryQuillen.rlp_J_iff {X Y : SSet} (p : X ⟶ Y) : J.rlp p ↔ ∀ (n : ℕ) (i : Fin (n + 2)), CategoryTheory.HasLiftingProperty (horn (n + 1) i).ι p

A map is a Kan fibration exactly when it has the right lifting property with respect to every horn inclusion.

theorem SSet.mem_innerFibrations_iff {X Y : SSet} (p : X ⟶ Y) : innerFibrations p ↔ ∀ (n : ℕ) (i : Fin (n + 3)), 0 < i → i < Fin.last (n + 2) → CategoryTheory.HasLiftingProperty (horn (n + 2) i).ι p

A map is an inner fibration exactly when it has the right lifting property with respect to every inner horn inclusion.