Kan complexes

In this file, the abbreviation KanComplex is introduced for fibrant objects in the category SSet which is equipped with Kan fibrations.

In Mathlib/AlgebraicTopology/Quasicategory/Basic.lean we show that every Kan complex is a quasicategory.

TODO

• Show that the singular simplicial set of a topological space is a Kan complex.

@[reducible, inline]

abbrev SSet.KanComplex (S : SSet) : Prop

A simplicial set S is a Kan complex if it is fibrant, which means that the projection S ⟶ ⊤_ _ has the right lifting property with respect to horn inclusions.

Equations

• S.KanComplex = HomotopicalAlgebra.IsFibrant S

theorem SSet.KanComplex.hornFilling {S : SSet} [S.KanComplex] {n : ℕ} {i : Fin (n + 2)} (σ₀ : (horn (n + 1) i).toSSet ⟶ S) : ∃ (σ : stdSimplex.obj { len := n + 1 } ⟶ S), σ₀ = CategoryTheory.CategoryStruct.comp (horn (n + 1) i).ι σ

A Kan complex S satisfies the following horn-filling condition: for every nonzero n : ℕ and 0 ≤ i ≤ n, every map of simplicial sets σ₀ : Λ[n, i] → S can be extended to a map σ : Δ[n] → S.

theorem SSet.horn.IsCompatible.exists_lift_of_kanComplex {X : SSet} {n : ℕ} {i : Fin (n + 2)} {f : (j : Fin (n + 2)) → j ≠ i → (stdSimplex.obj { len := n } ⟶ X)} [X.KanComplex] (hf : horn.IsCompatible f) : ∃ (φ : stdSimplex.obj { len := n + 1 } ⟶ X), ∀ (j : Fin (n + 2)) (hj : j ≠ i), CategoryTheory.CategoryStruct.comp (stdSimplex.δ j) φ = f j hj

noncomputable def SSet.horn.IsCompatible.liftOfKanComplex {X : SSet} {n : ℕ} {i : Fin (n + 2)} {f : (j : Fin (n + 2)) → j ≠ i → (stdSimplex.obj { len := n } ⟶ X)} [X.KanComplex] (hf : horn.IsCompatible f) : stdSimplex.obj { len := n + 1 } ⟶ X

If X is a Kan complex and f : ∀ (j : Fin (n + 2)) (_ : j ≠ i), Δ[n] ⟶ X is a compatible family of morphisms (which defines a morphism Λ[n + 1, i] ⟶ X), then this is a lifting Δ[n + 1] ⟶ X.

Equations

• hf.liftOfKanComplex = ⋯.choose

theorem SSet.horn.IsCompatible.δ_liftOfKanComplex {X : SSet} {n : ℕ} {i : Fin (n + 2)} {f : (j : Fin (n + 2)) → j ≠ i → (stdSimplex.obj { len := n } ⟶ X)} [X.KanComplex] (hf : horn.IsCompatible f) (j : Fin (n + 2)) (hj : j ≠ i := by grind) : CategoryTheory.CategoryStruct.comp (stdSimplex.δ j) hf.liftOfKanComplex = f j hj

theorem SSet.horn.IsCompatible.δ_liftOfKanComplex_assoc {X : SSet} {n : ℕ} {i : Fin (n + 2)} {f : (j : Fin (n + 2)) → j ≠ i → (stdSimplex.obj { len := n } ⟶ X)} [X.KanComplex] (hf : horn.IsCompatible f) (j : Fin (n + 2)) (hj : j ≠ i := by grind) {Z : SSet} (h : X ⟶ Z) : CategoryTheory.CategoryStruct.comp (stdSimplex.δ j) (CategoryTheory.CategoryStruct.comp hf.liftOfKanComplex h) = CategoryTheory.CategoryStruct.comp (f j hj) h

theorem SSet.KanComplex.iff {Z : SSet} : Z.KanComplex ↔ ∀ ⦃n : ℕ⦄ ⦃i : Fin (n + 2)⦄ (f : (j : Fin (n + 2)) → j ≠ i → (stdSimplex.obj { len := n } ⟶ Z)), horn.IsCompatible f → ∃ (φ : stdSimplex.obj { len := n + 1 } ⟶ Z), ∀ (j : Fin (n + 2)) (hj : j ≠ i), CategoryTheory.CategoryStruct.comp (stdSimplex.δ j) φ = f j hj

A simplicial set X is a Kan complex iff for any n : ℕ, i : Fin (n + 2), and any family of morphisms Δ[n] ⟶ Z for all j ≠ i that is compatible (in the sense that it extends to a morphism Λ[n + 1, i] ⟶ X), there exists a morphism Δ[n + 1] ⟶ Z which induces the given family of morphisms on the faces j ≠ i.