feat(AlgebraicTopology): generalize universes for the standard simplex (

#9631)

The PR generalizes universes for `standardSimplex`, which is now a functor `SimplexCategory ⥤ SSet.{u}` for any universe `u`.

Mathlib/AlgebraicTopology/ExtraDegeneracy.lean

@@ -168,7 +168,7 @@ set_option linter.uppercaseLean3 false in
 #align sSet.augmented.standard_simplex.shift_fun_succ SSet.Augmented.StandardSimplex.shiftFun_succ
 
 /-- The shift of a morphism `f : [n] → Δ` in `SimplexCategory` corresponds to
-the monotone map which sends `0` to `0` and `i.succ` to `f.to_order_hom i`. -/
+the monotone map which sends `0` to `0` and `i.succ` to `f.toOrderHom i`. -/
 @[simp]
 def shift {n : ℕ} {Δ : SimplexCategory}
     (f : ([n] : SimplexCategory) ⟶ Δ) : ([n + 1] : SimplexCategory) ⟶ Δ :=
@@ -189,31 +189,38 @@ def shift {n : ℕ} {Δ : SimplexCategory}
 set_option linter.uppercaseLean3 false in
 #align sSet.augmented.standard_simplex.shift SSet.Augmented.StandardSimplex.shift
 
+open SSet.standardSimplex in
 /-- The obvious extra degeneracy on the standard simplex. -/
 protected noncomputable def extraDegeneracy (Δ : SimplexCategory) :
     SimplicialObject.Augmented.ExtraDegeneracy (standardSimplex.obj Δ) where
-  s' _ := SimplexCategory.Hom.mk (OrderHom.const _ 0)
-  s n f := shift f
+  s' _ := objMk (OrderHom.const _ 0)
+  s  n f := (objEquiv _ _).symm
+    (shift (objEquiv _ _ f))
   s'_comp_ε := by
     dsimp
     apply Subsingleton.elim
   s₀_comp_δ₁ := by
+    dsimp
     ext1 x
-    apply SimplexCategory.Hom.ext
+    apply (objEquiv _ _).injective
     ext j
     fin_cases j
     rfl
   s_comp_δ₀ n := by
     ext1 φ
+    apply (objEquiv _ _).injective
     apply SimplexCategory.Hom.ext
     ext i : 2
-    dsimp [SimplicialObject.δ, SimplexCategory.δ, SSet.standardSimplex]
+    dsimp [SimplicialObject.δ, SimplexCategory.δ, SSet.standardSimplex,
+      objEquiv, Equiv.ulift, uliftFunctor]
     simp only [shiftFun_succ]
   s_comp_δ n i := by
     ext1 φ
+    apply (objEquiv _ _).injective
     apply SimplexCategory.Hom.ext
     ext j : 2
-    dsimp [SimplicialObject.δ, SimplexCategory.δ, SSet.standardSimplex]
+    dsimp [SimplicialObject.δ, SimplexCategory.δ, SSet.standardSimplex,
+      objEquiv, Equiv.ulift, uliftFunctor]
     by_cases h : j = 0
     · subst h
       simp only [Fin.succ_succAbove_zero, shiftFun_0]
@@ -222,13 +229,14 @@ protected noncomputable def extraDegeneracy (Δ : SimplexCategory) :
         Fin.succAboveEmb_apply]
   s_comp_σ n i := by
     ext1 φ
+    apply (objEquiv _ _).injective
     apply SimplexCategory.Hom.ext
     ext j : 2
-    dsimp [SimplicialObject.σ, SimplexCategory.σ, SSet.standardSimplex]
+    dsimp [SimplicialObject.σ, SimplexCategory.σ, SSet.standardSimplex,
+      objEquiv, Equiv.ulift, uliftFunctor]
     by_cases h : j = 0
     · subst h
-      simp only [shiftFun_0]
-      exact shiftFun_0 φ.toOrderHom
+      rfl
     · obtain ⟨_, rfl⟩ := Fin.eq_succ_of_ne_zero h
       simp only [Fin.succ_predAbove_succ, shiftFun_succ, Function.comp_apply]
 set_option linter.uppercaseLean3 false in

Mathlib/AlgebraicTopology/Quasicategory.lean

@@ -62,7 +62,7 @@ lemma quasicategory_of_filler (S : SSet)
     Quasicategory S where
   hornFilling' n i σ₀ h₀ hₙ := by
     obtain ⟨σ, h⟩ := filler σ₀ h₀ hₙ
-    use yonedaEquiv.symm σ
+    refine' ⟨(S.yonedaEquiv _).symm σ, _⟩
     apply horn.hom_ext
     intro j hj
     rw [← h j hj, NatTrans.comp_app]

Mathlib/AlgebraicTopology/SimplicialSet.lean

@@ -71,10 +71,14 @@ instance hasColimits : HasColimits SSet := by
 lemma hom_ext {X Y : SSet} {f g : X ⟶ Y} (w : ∀ n, f.app n = g.app n) : f = g :=
   SimplicialObject.hom_ext _ _ w
 
+/-- The ulift functor `SSet.{u} ⥤ SSet.{max u v}` on simplicial sets. -/
+def uliftFunctor : SSet.{u} ⥤ SSet.{max u v} :=
+  (SimplicialObject.whiskering _ _).obj CategoryTheory.uliftFunctor.{v, u}
+
 /-- The `n`-th standard simplex `Δ[n]` associated with a nonempty finite linear order `n`
 is the Yoneda embedding of `n`. -/
-def standardSimplex : SimplexCategory ⥤ SSet :=
-  yoneda
+def standardSimplex : SimplexCategory ⥤ SSet.{u} :=
+  yoneda ⋙ uliftFunctor
 set_option linter.uppercaseLean3 false in
 #align sSet.standard_simplex SSet.standardSimplex
 
@@ -88,36 +92,62 @@ namespace standardSimplex
 
 open Finset Opposite SimplexCategory
 
+@[simp]
+lemma map_id (n : SimplexCategory) :
+    (SSet.standardSimplex.map (SimplexCategory.Hom.mk OrderHom.id : n ⟶ n)) = 𝟙 _ :=
+  CategoryTheory.Functor.map_id _ _
+
+/-- Simplices of the standard simplex identify to morphisms in `SimplexCategory`. -/
+def objEquiv (n : SimplexCategory) (m : SimplexCategoryᵒᵖ) :
+    (standardSimplex.{u}.obj n).obj m ≃ (m.unop ⟶ n) :=
+  Equiv.ulift.{u, 0}
+
+/-- Constructor for simplices of the standard simplex which takes a `OrderHom` as an input. -/
+abbrev objMk {n : SimplexCategory} {m : SimplexCategoryᵒᵖ}
+    (f : Fin (len m.unop + 1) →o Fin (n.len + 1)) :
+    (standardSimplex.{u}.obj n).obj m :=
+  (objEquiv _ _).symm (Hom.mk f)
+
+lemma map_apply {m₁ m₂ : SimplexCategoryᵒᵖ} (f : m₁ ⟶ m₂) {n : SimplexCategory}
+    (x : (standardSimplex.{u}.obj n).obj m₁) :
+    (standardSimplex.{u}.obj n).map f x = (objEquiv _ _).symm (f.unop ≫ (objEquiv _ _) x) := by
+  rfl
+
+/-- The canonical bijection `(standardSimplex.obj n ⟶ X) ≃ X.obj (op n)`. -/
+def _root_.SSet.yonedaEquiv (X : SSet.{u}) (n : SimplexCategory) :
+    (standardSimplex.obj n ⟶ X) ≃ X.obj (op n) :=
+  yonedaCompUliftFunctorEquiv X n
+
 /-- The (degenerate) `m`-simplex in the standard simplex concentrated in vertex `k`. -/
 def const (n : ℕ) (k : Fin (n+1)) (m : SimplexCategoryᵒᵖ) : Δ[n].obj m :=
-  Hom.mk <| OrderHom.const _ k
+  objMk (OrderHom.const _ k )
 
 @[simp]
-lemma const_toOrderHom (n : ℕ) (k : Fin (n+1)) (m : SimplexCategoryᵒᵖ) :
-    (const n k m).toOrderHom = OrderHom.const _ k :=
+lemma const_down_toOrderHom (n : ℕ) (k : Fin (n+1)) (m : SimplexCategoryᵒᵖ) :
+    (const n k m).down.toOrderHom = OrderHom.const _ k :=
   rfl
 
 /-- The edge of the standard simplex with endpoints `a` and `b`. -/
 def edge (n : ℕ) (a b : Fin (n+1)) (hab : a ≤ b) : Δ[n] _[1] := by
-  refine Hom.mk ⟨![a, b], ?_⟩
+  refine objMk ⟨![a, b], ?_⟩
   rw [Fin.monotone_iff_le_succ]
   simp only [unop_op, len_mk, Fin.forall_fin_one]
   apply Fin.mk_le_mk.mpr hab
 
-lemma coe_edge_toOrderHom (n : ℕ) (a b : Fin (n+1)) (hab : a ≤ b) :
-    ↑(edge n a b hab).toOrderHom = ![a, b] :=
+lemma coe_edge_down_toOrderHom (n : ℕ) (a b : Fin (n+1)) (hab : a ≤ b) :
+    ↑(edge n a b hab).down.toOrderHom = ![a, b] :=
   rfl
 
 /-- The triangle in the standard simplex with vertices `a`, `b`, and `c`. -/
 def triangle {n : ℕ} (a b c : Fin (n+1)) (hab : a ≤ b) (hbc : b ≤ c) : Δ[n] _[2] := by
-  refine Hom.mk ⟨![a, b, c], ?_⟩
+  refine objMk ⟨![a, b, c], ?_⟩
   rw [Fin.monotone_iff_le_succ]
   simp only [unop_op, len_mk, Fin.forall_fin_two]
   dsimp
   simp only [*, Matrix.tail_cons, Matrix.head_cons, true_and]
 
-lemma coe_triangle_toOrderHom {n : ℕ} (a b c : Fin (n+1)) (hab : a ≤ b) (hbc : b ≤ c) :
-    ↑(triangle a b c hab hbc).toOrderHom = ![a, b, c] :=
+lemma coe_triangle_down_toOrderHom {n : ℕ} (a b c : Fin (n+1)) (hab : a ≤ b) (hbc : b ≤ c) :
+    ↑(triangle a b c hab hbc).down.toOrderHom = ![a, b, c] :=
   rfl
 
 end standardSimplex
@@ -127,7 +157,7 @@ section
 /-- The `m`-simplices of the `n`-th standard simplex are
 the monotone maps from `Fin (m+1)` to `Fin (n+1)`. -/
 def asOrderHom {n} {m} (α : Δ[n].obj m) : OrderHom (Fin (m.unop.len + 1)) (Fin (n + 1)) :=
-  α.toOrderHom
+  α.down.toOrderHom
 set_option linter.uppercaseLean3 false in
 #align sSet.as_order_hom SSet.asOrderHom
 
@@ -136,10 +166,10 @@ end
 /-- The boundary `∂Δ[n]` of the `n`-th standard simplex consists of
 all `m`-simplices of `standardSimplex n` that are not surjective
 (when viewed as monotone function `m → n`). -/
-def boundary (n : ℕ) : SSet where
+def boundary (n : ℕ) : SSet.{u} where
   obj m := { α : Δ[n].obj m // ¬Function.Surjective (asOrderHom α) }
   map {m₁ m₂} f α :=
-    ⟨f.unop ≫ (α : Δ[n].obj m₁), by
+    ⟨Δ[n].map f α.1, by
       intro h
       apply α.property
       exact Function.Surjective.of_comp h⟩
@@ -161,7 +191,7 @@ for which the union of `{i}` and the range of `α` is not all of `n`
 def horn (n : ℕ) (i : Fin (n + 1)) : SSet where
   obj m := { α : Δ[n].obj m // Set.range (asOrderHom α) ∪ {i} ≠ Set.univ }
   map {m₁ m₂} f α :=
-    ⟨f.unop ≫ (α : Δ[n].obj m₁), by
+    ⟨Δ[n].map f α.1, by
       intro h; apply α.property
       rw [Set.eq_univ_iff_forall] at h ⊢; intro j
       apply Or.imp _ id (h j)
@@ -253,7 +283,8 @@ def primitiveTriangle {n : ℕ} (i : Fin (n+4))
     OrderHom.const_coe_coe, Set.union_singleton, ne_eq, ← Set.univ_subset_iff, Set.subset_def,
     Set.mem_univ, Set.mem_insert_iff, Set.mem_range, Function.const_apply, exists_const,
     forall_true_left, not_forall, not_or, unop_op, not_exists,
-    standardSimplex.triangle, OrderHom.coe_mk, @eq_comm _ _ i]
+    standardSimplex.triangle, OrderHom.coe_mk, @eq_comm _ _ i,
+    standardSimplex.objMk, standardSimplex.objEquiv, Equiv.ulift]
   dsimp
   by_cases hk0 : k = 0
   · subst hk0
@@ -268,9 +299,10 @@ def primitiveTriangle {n : ℕ} (i : Fin (n+4))
 
 /-- The `j`th subface of the `i`-th horn. -/
 @[simps]
-def face {n : ℕ} (i j : Fin (n+2)) (h : j ≠ i) : Λ[n+1, i] _[n] := by
-  refine ⟨SimplexCategory.δ j, ?_⟩
-  simpa [← Set.univ_subset_iff, Set.subset_def, asOrderHom, SimplexCategory.δ, not_or]
+def face {n : ℕ} (i j : Fin (n+2)) (h : j ≠ i) : Λ[n+1, i] _[n] :=
+  ⟨(standardSimplex.objEquiv _ _).symm (SimplexCategory.δ j), by
+    simpa [← Set.univ_subset_iff, Set.subset_def, asOrderHom, SimplexCategory.δ, not_or,
+      standardSimplex.objEquiv, asOrderHom, Equiv.ulift]⟩
 
 /-- Two morphisms from a horn are equal if they are equal on all suitable faces. -/
 protected
@@ -279,13 +311,18 @@ lemma hom_ext {n : ℕ} {i : Fin (n+2)} {S : SSet} (σ₁ σ₂ : Λ[n+1, i] ⟶
     σ₁ = σ₂ := by
   apply NatTrans.ext; apply funext; apply Opposite.rec; apply SimplexCategory.rec
   intro m; ext f
-  obtain ⟨j, hji, hfj⟩ : ∃ j, ¬j = i ∧ ∀ k, f.1.toOrderHom k ≠ j := by
-    simpa [← Set.univ_subset_iff, Set.subset_def, asOrderHom, not_or] using f.2
-  have H : f = (Λ[n+1, i].map (factor_δ f.1 j).op) (face i j hji) := by
+  obtain ⟨f', hf⟩ := (standardSimplex.objEquiv _ _).symm.surjective f.1
+  obtain ⟨j, hji, hfj⟩ : ∃ j, ¬j = i ∧ ∀ k, f'.toOrderHom k ≠ j := by
+    obtain ⟨f, hf'⟩ := f
+    subst hf
+    simpa [← Set.univ_subset_iff, Set.subset_def, asOrderHom, not_or] using hf'
+  have H : f = (Λ[n+1, i].map (factor_δ f' j).op) (face i j hji) := by
     apply Subtype.ext
-    exact (factor_δ_spec f.1 j hfj).symm
-  have H₁ := congrFun (σ₁.naturality (factor_δ f.1 j).op) (face i j hji)
-  have H₂ := congrFun (σ₂.naturality (factor_δ f.1 j).op) (face i j hji)
+    apply (standardSimplex.objEquiv _ _).injective
+    rw [← hf]
+    exact (factor_δ_spec f' j hfj).symm
+  have H₁ := congrFun (σ₁.naturality (factor_δ f' j).op) (face i j hji)
+  have H₂ := congrFun (σ₂.naturality (factor_δ f' j).op) (face i j hji)
   dsimp at H₁ H₂
   erw [H, H₁, H₂, h _ hji]
 
@@ -347,16 +384,12 @@ set_option linter.uppercaseLean3 false in
 
 namespace Augmented
 
--- porting note: added to ease the automation of the proofs in the definition
--- of `standardSimplex`
-attribute [local simp] SSet.standardSimplex
-
 -- porting note: an instance of `Subsingleton (⊤_ (Type u))` was added in
 -- `CategoryTheory.Limits.Types` to ease the automation in this definition
 /-- The functor which sends `[n]` to the simplicial set `Δ[n]` equipped by
 the obvious augmentation towards the terminal object of the category of sets. -/
 @[simps]
-noncomputable def standardSimplex : SimplexCategory ⥤ SSet.Augmented where
+noncomputable def standardSimplex : SimplexCategory ⥤ SSet.Augmented.{u} where
   obj Δ :=
     { left := SSet.standardSimplex.obj Δ
       right := terminal _

Mathlib/AlgebraicTopology/SingularSet.lean

@@ -28,6 +28,7 @@ It is the left Kan extension of `SimplexCategory.toTop` along the Yoneda embeddi
 
 ## TODO
 
+- Generalize to an adjunction between `SSet.{u}` and `TopCat.{u}` for any universe `u`
 - Show that the singular simplicial set is a Kan complex.
 - Show the adjunction `sSetTopAdj` is a Quillen adjunction.
 

Mathlib/CategoryTheory/Yoneda.lean

@@ -337,6 +337,23 @@ theorem yonedaPairing_map (P Q : Cᵒᵖ × (Cᵒᵖ ⥤ Type v₁)) (α : P ⟶
   rfl
 #align category_theory.yoneda_pairing_map CategoryTheory.yonedaPairing_map
 
+variable {C} in
+/-- A bijection `(yoneda.obj X ⋙ uliftFunctor ⟶ F) ≃ F.obj (op X)` which is a variant
+of `yonedaEquiv` with heterogeneous universes. -/
+def yonedaCompUliftFunctorEquiv (F : Cᵒᵖ ⥤ Type max v₁ w) (X : C) :
+    (yoneda.obj X ⋙ uliftFunctor.{w} ⟶ F) ≃ F.obj (op X) where
+  toFun φ := φ.app (op X) (ULift.up (𝟙 _))
+  invFun f :=
+    { app := fun Y x => F.map (ULift.down x).op f }
+  left_inv φ := by
+    ext Y f
+    dsimp
+    rw [← FunctorToTypes.naturality]
+    dsimp
+    rw [Category.comp_id]
+    rfl
+  right_inv f := by aesop_cat
+
 /-- The Yoneda lemma asserts that the Yoneda pairing
 `(X : Cᵒᵖ, F : Cᵒᵖ ⥤ Type) ↦ (yoneda.obj (unop X) ⟶ F)`
 is naturally isomorphic to the evaluation `(X, F) ↦ F.obj X`.