quasicategory_ifftheoremProved here from basic factspropext, Classical.choice, Quot.sound
quasicategory_iffLean 4Proved here from basic factsFormally verified
/-- **What a quasi-category is.** A simplicial set `S` is a quasi-category exactly when every*inner* horn `Λ[n, i] ⟶ S` (with `0 < i < n`) extends along the inclusion `Λ[n, i] ⟶ Δ[n]`.Mathlib's class `SSet.Quasicategory` states this for `n + 2` (inner horns only exist fromdimension 2); here it is unfolded into the form used in the lesson. -/theorem quasicategory_iff (S : SSet) : S.Quasicategory ↔ ∀ (n : ℕ) (i : Fin (n + 1)) (σ₀ : (Λ[n, i] : SSet) ⟶ S), 0 < i → i < Fin.last n → ∃ σ : Δ[n] ⟶ S, σ₀ = Λ[n, i].ι ≫ σ := by constructor · intro hS n i σ₀ h0 hn exact Quasicategory.hornFilling h0 hn σ₀ · intro h exact ⟨fun n i σ₀ h0 hn => h (n + 2) i σ₀ h0 hn⟩
kan_is_quasicategorytheoremApplies a library theorempropext, Classical.choice, Quot.sound
kan_is_quasicategoryLean 4Applies a library theoremFormally verified
/-- Every Kan complex (all horns fill, inner and outer) is a quasi-category: ∞-groupoids arespecial ∞-categories. This is Mathlib's instance in `Mathlib.AlgebraicTopology.Quasicategory.Basic`. -/theorem kan_is_quasicategory (S : SSet) [KanComplex S] : S.Quasicategory := inferInstance
nerve_is_quasicategorytheoremApplies a library theorempropext, Classical.choice, Quot.sound
nerve_is_quasicategoryLean 4Applies a library theoremFormally verified
/-- **The nerve of a category is a quasi-category.** Mathlib proves this(`CategoryTheory.Nerve.quasicategory`) by showing that nerves satisfy the strict Segalcondition: every simplex is determined by its spine of composable arrows. -/theorem nerve_is_quasicategory (C : Type) [Category C] : (nerve C).Quasicategory := inferInstance
nerve_composite_uniquetheoremProved here from basic factspropext, Classical.choice, Quot.sound
nerve_composite_uniqueLean 4Proved here from basic factsFormally verified
/-- **Inner horns in a nerve fill uniquely.** Given composable edges `f` and `g` (a horn`Λ[2, 1]`), there is exactly one edge `h` that can be the third side of a 2-simplex, namely`f ≫ g`. In a general quasi-category a filler exists but is unique only up to homotopy; nervesare exactly the simplicial sets whose inner horns fill uniquely. -/theorem nerve_composite_unique {C : Type} [Category C] {x₀ x₁ x₂ : C} (f : x₀ ⟶ x₁) (g : x₁ ⟶ x₂) : ∃! h : x₀ ⟶ x₂, Nonempty (Edge.CompStruct (nerve.edgeMk f) (nerve.edgeMk g) (nerve.edgeMk h)) := by refine ⟨f ≫ g, (nerve_triangle_iff f g (f ≫ g)).2 rfl, fun h hh => ?_⟩ exact ((nerve_triangle_iff f g h).1 hh).symm
groupoid_outer_horntheoremProved here from basic factspropext, Classical.choice, Quot.sound
groupoid_outer_hornLean 4Proved here from basic factsFormally verified
/-- **Outer horns in the nerve of a groupoid fill.** Given `f : x₀ ⟶ x₁` and `h : x₀ ⟶ x₂` (ahorn `Λ[2, 0]`), there is exactly one `g : x₁ ⟶ x₂` making a 2-simplex, namely `f⁻¹ ≫ h`. Thisis the dimension-2 shadow of the fact that nerves of groupoids are Kan complexes: filling outerhorns is *inverting* arrows. -/theorem groupoid_outer_horn {G : Type} [Groupoid G] {x₀ x₁ x₂ : G} (f : x₀ ⟶ x₁) (h : x₀ ⟶ x₂) : ∃! g : x₁ ⟶ x₂, Nonempty (Edge.CompStruct (nerve.edgeMk f) (nerve.edgeMk g) (nerve.edgeMk h)) := by refine ⟨Groupoid.inv f ≫ h, (nerve_triangle_iff _ _ _).2 (by simp), fun g hg => ?_⟩ have hfg : f ≫ g = h := (nerve_triangle_iff f g h).1 hg rw [← hfg] simp
nerve_fin_two_not_kantheoremProved here from basic factspropext, Classical.choice, Quot.sound
nerve_fin_two_not_kanLean 4Proved here from basic factsFormally verified
/-- **A quasi-category that is not a Kan complex**: the nerve of the poset `0 < 1` (the"walking arrow" `Fin 2`). The horn `Λ[2, 0]` with edges `0 ⟶ 1` (from vertex 0 to vertex 1) and`𝟙 0` (from vertex 0 to vertex 2) has no filler: the missing edge would be an arrow `1 ⟶ 0`, i.e.a proof of `1 ≤ 0`. Proof: glue the two edges into a horn (`horn₂₀.isPushout`), fill it usingthe Kan property, read off the vertices of the filling 2-simplex from its faces, and apply itsmiddle-to-last arrow. -/theorem nerve_fin_two_not_kan : ¬ KanComplex (nerve (Fin 2)) := by intro hK -- The two edges of the horn: `0 ⟶ 1` and the identity of `0`. let e₀₁ : (nerve (Fin 2)) _⦋1⦌ := ComposableArrows.mk₁ (homOfLE (show (0 : Fin 2) ≤ 1 by decide)) let e₀₂ : (nerve (Fin 2)) _⦋1⦌ := ComposableArrows.mk₁ (𝟙 (0 : Fin 2)) -- They share their source vertex 0, so they glue to a map `Λ[2, 0] ⟶ nerve (Fin 2)`. have hsrc : (nerve (Fin 2)).δ 1 e₀₁ = (nerve (Fin 2)).δ 1 e₀₂ := ComposableArrows.ext₀ rfl obtain ⟨σ, hσ₁, hσ₂⟩ := horn₂₀.isPushout.exists_desc (SSet.yonedaEquiv.symm e₀₁) (SSet.yonedaEquiv.symm e₀₂) (by rw [stdSimplex.δ_comp_yonedaEquiv_symm, stdSimplex.δ_comp_yonedaEquiv_symm, hsrc]) -- The Kan property fills the horn with a 2-simplex `s`. obtain ⟨s, hs⟩ := KanComplex.hornFilling σ have hs₂ : stdSimplex.δ 2 ≫ s = SSet.yonedaEquiv.symm e₀₁ := by simp [← hσ₁, hs] have hs₁ : stdSimplex.δ 1 ≫ s = SSet.yonedaEquiv.symm e₀₂ := by simp [← hσ₂, hs] obtain ⟨t, rfl⟩ := SSet.yonedaEquiv.symm.surjective s rw [stdSimplex.δ_comp_yonedaEquiv_symm] at hs₂ hs₁ have ht₂ : (nerve (Fin 2)).δ 2 t = e₀₁ := SSet.yonedaEquiv.symm.injective hs₂ have ht₁ : (nerve (Fin 2)).δ 1 t = e₀₂ := SSet.yonedaEquiv.symm.injective hs₁ -- Vertex 1 of `t` is `1` (read off face 2) and vertex 2 of `t` is `0` (read off face 1). have v₁ : t.obj 1 = 1 := congrArg (fun x : ComposableArrows (Fin 2) 1 => x.obj 1) ht₂ have v₂ : t.obj 2 = 0 := congrArg (fun x : ComposableArrows (Fin 2) 1 => x.obj 1) ht₁ -- The arrow of `t` from vertex 1 to vertex 2 would prove `1 ≤ 0`. have hle : t.obj 1 ≤ t.obj 2 := leOfHom (t.map' 1 2) rw [v₁, v₂] at hle exact absurd hle (by decide)
/-- The **homotopy category** functor `hoFunctor : SSet ⥤ Cat` is left adjoint to the nerve.For a quasi-category `S`, `hoFunctor S` has the vertices as objects and homotopy classes ofedges as morphisms; composition is defined by filling inner 2-horns. This is Mathlib's`CategoryTheory.nerveAdjunction`. -/noncomputable def nerveAdjunction : hoFunctor ⊣ nerveFunctor := CategoryTheory.nerveAdjunction
/-- The homotopy category of the nerve of a category is that category again (naturally): thenerve loses no information, and categories sit inside ∞-categories as a full subcategory. Thisis Mathlib's `CategoryTheory.nerveFunctorCompHoFunctorIso`. -/noncomputable def hoNerveIso : nerveFunctor.{0, 0} ⋙ hoFunctor ≅ 𝟭 Cat := CategoryTheory.nerveFunctorCompHoFunctorIso
/-- Fill the outer horn `Λ[2, 2]` in the nerve of a groupoid: given `g : x₁ ⟶ x₂` and`h : x₀ ⟶ x₂`, there is exactly one `f` with a 2-simplex `(f, g, h)`. Hint: use`nerve_triangle_iff` to turn "there is a 2-simplex" into `f ≫ g = h`, take`f := h ≫ Groupoid.inv g`, and finish the computations with `simp`. -/theorem groupoid_outer_horn_right {G : Type} [Groupoid G] {x₀ x₁ x₂ : G} (g : x₁ ⟶ x₂) (h : x₀ ⟶ x₂) : ∃! f : x₀ ⟶ x₁, Nonempty (Edge.CompStruct (nerve.edgeMk f) (nerve.edgeMk g) (nerve.edgeMk h)) := by sorry
Show the compiled solution
groupoid_outer_horn_rightLean 4Proved here from basic factsFormally verified
/-- The other outer horn, `Λ[2, 2]`: in the nerve of a groupoid, given `g : x₁ ⟶ x₂` and`h : x₀ ⟶ x₂` there is exactly one `f : x₀ ⟶ x₁` making a 2-simplex, namely `h ≫ g⁻¹`. -/theorem groupoid_outer_horn_right {G : Type} [Groupoid G] {x₀ x₁ x₂ : G} (g : x₁ ⟶ x₂) (h : x₀ ⟶ x₂) : ∃! f : x₀ ⟶ x₁, Nonempty (Edge.CompStruct (nerve.edgeMk f) (nerve.edgeMk g) (nerve.edgeMk h)) := by refine ⟨h ≫ Groupoid.inv g, (nerve_triangle_iff _ _ _).2 (by simp), fun f hf => ?_⟩ have hfg : f ≫ g = h := (nerve_triangle_iff f g h).1 hf rw [← hfg] simp