Skip to content

Commit db422a2

Browse files
emilyriehlemilyriehl
committed
feat(CategoryTheory): coskeletal simplicial objects (#19492)
A simplicial object `X` is *n-coskeletal* if the identity natural transformation `X` is a right extension of its restriction along `(Truncated.inclusion (n := n)).op` recorded by `rightExtensionInclusion X n`. Co-Authored-By: [Mario Carneiro](https://github.com/digama0) and [Joël Riou](https://github.com/joelriou)
1 parent 6a0cdd1 commit db422a2

File tree

9 files changed

+126
-24
lines changed

9 files changed

+126
-24
lines changed

‎Mathlib.lean‎

Lines changed: 2 additions & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -1042,7 +1042,8 @@ import Mathlib.AlgebraicTopology.Quasicategory.StrictSegal
10421042
import Mathlib.AlgebraicTopology.SimplexCategory
10431043
import Mathlib.AlgebraicTopology.SimplicialCategory.Basic
10441044
import Mathlib.AlgebraicTopology.SimplicialCategory.SimplicialObject
1045-
import Mathlib.AlgebraicTopology.SimplicialObject
1045+
import Mathlib.AlgebraicTopology.SimplicialObject.Basic
1046+
import Mathlib.AlgebraicTopology.SimplicialObject.Coskeletal
10461047
import Mathlib.AlgebraicTopology.SimplicialSet.Basic
10471048
import Mathlib.AlgebraicTopology.SimplicialSet.KanComplex
10481049
import Mathlib.AlgebraicTopology.SimplicialSet.Monoidal

‎Mathlib/AlgebraicTopology/CechNerve.lean‎

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -3,7 +3,7 @@ Copyright (c) 2021 Adam Topaz. All rights reserved.
33
Released under Apache 2.0 license as described in the file LICENSE.
44
Authors: Adam Topaz
55
-/
6-
import Mathlib.AlgebraicTopology.SimplicialObject
6+
import Mathlib.AlgebraicTopology.SimplicialObject.Basic
77
import Mathlib.CategoryTheory.Comma.Arrow
88
import Mathlib.CategoryTheory.Limits.Shapes.WidePullbacks
99
import Mathlib.CategoryTheory.Limits.Shapes.FiniteProducts

‎Mathlib/AlgebraicTopology/MooreComplex.lean‎

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -4,7 +4,7 @@ Released under Apache 2.0 license as described in the file LICENSE.
44
Authors: Kim Morrison
55
-/
66
import Mathlib.Algebra.Homology.HomologicalComplex
7-
import Mathlib.AlgebraicTopology.SimplicialObject
7+
import Mathlib.AlgebraicTopology.SimplicialObject.Basic
88
import Mathlib.CategoryTheory.Abelian.Basic
99

1010
/-!

‎Mathlib/AlgebraicTopology/SimplexCategory.lean‎

Lines changed: 4 additions & 4 deletions
Original file line numberDiff line numberDiff line change
@@ -725,15 +725,15 @@ instance {n} : Inhabited (Truncated n) :=
725725
/-- The fully faithful inclusion of the truncated simplex category into the usual
726726
simplex category.
727727
-/
728-
def inclusion {n : ℕ} : SimplexCategory.Truncated n ⥤ SimplexCategory :=
728+
def inclusion (n : ℕ) : SimplexCategory.Truncated n ⥤ SimplexCategory :=
729729
fullSubcategoryInclusion _
730730

731-
instance (n : ℕ) : (inclusion : Truncated n ⥤ _).Full := FullSubcategory.full _
732-
instance (n : ℕ) : (inclusion : Truncated n ⥤ _).Faithful := FullSubcategory.faithful _
731+
instance (n : ℕ) : (inclusion n : Truncated n ⥤ _).Full := FullSubcategory.full _
732+
instance (n : ℕ) : (inclusion n : Truncated n ⥤ _).Faithful := FullSubcategory.faithful _
733733

734734
/-- A proof that the full subcategory inclusion is fully faithful.-/
735735
noncomputable def inclusion.fullyFaithful (n : ℕ) :
736-
(inclusion : Truncated n ⥤ _).op.FullyFaithful := Functor.FullyFaithful.ofFullyFaithful _
736+
(inclusion n : Truncated n ⥤ _).op.FullyFaithful := Functor.FullyFaithful.ofFullyFaithful _
737737

738738
@[ext]
739739
theorem Hom.ext {n} {a b : Truncated n} (f g : a ⟶ b) :

‎Mathlib/AlgebraicTopology/SimplicialObject.lean‎ renamed to ‎Mathlib/AlgebraicTopology/SimplicialObject/Basic.lean‎

Lines changed: 24 additions & 14 deletions
Original file line numberDiff line numberDiff line change
@@ -250,7 +250,7 @@ section Truncation
250250

251251
/-- The truncation functor from simplicial objects to truncated simplicial objects. -/
252252
def truncation (n : ℕ) : SimplicialObject C ⥤ SimplicialObject.Truncated C n :=
253-
(whiskeringLeft _ _ _).obj SimplexCategory.Truncated.inclusion.op
253+
(whiskeringLeft _ _ _).obj (SimplexCategory.Truncated.inclusion n).op
254254

255255
end Truncation
256256

@@ -259,24 +259,24 @@ noncomputable section
259259

260260
/-- The n-skeleton as a functor `SimplicialObject.Truncated C n ⥤ SimplicialObject C`. -/
261261
protected abbrev Truncated.sk (n : ℕ) [∀ (F : (SimplexCategory.Truncated n)ᵒᵖ ⥤ C),
262-
SimplexCategory.Truncated.inclusion.op.HasLeftKanExtension F] :
262+
(SimplexCategory.Truncated.inclusion n).op.HasLeftKanExtension F] :
263263
SimplicialObject.Truncated C n ⥤ SimplicialObject C :=
264-
lan (SimplexCategory.Truncated.inclusion.op)
264+
lan (SimplexCategory.Truncated.inclusion n).op
265265

266266
/-- The n-coskeleton as a functor `SimplicialObject.Truncated C n ⥤ SimplicialObject C`. -/
267267
protected abbrev Truncated.cosk (n : ℕ) [∀ (F : (SimplexCategory.Truncated n)ᵒᵖ ⥤ C),
268-
SimplexCategory.Truncated.inclusion.op.HasRightKanExtension F] :
268+
(SimplexCategory.Truncated.inclusion n).op.HasRightKanExtension F] :
269269
SimplicialObject.Truncated C n ⥤ SimplicialObject C :=
270-
ran (SimplexCategory.Truncated.inclusion.op)
270+
ran (SimplexCategory.Truncated.inclusion n).op
271271

272272
/-- The n-skeleton as an endofunctor on `SimplicialObject C`. -/
273273
abbrev sk (n : ℕ) [∀ (F : (SimplexCategory.Truncated n)ᵒᵖ ⥤ C),
274-
SimplexCategory.Truncated.inclusion.op.HasLeftKanExtension F] :
274+
(SimplexCategory.Truncated.inclusion n).op.HasLeftKanExtension F] :
275275
SimplicialObject C ⥤ SimplicialObject C := truncation n ⋙ Truncated.sk n
276276

277277
/-- The n-coskeleton as an endofunctor on `SimplicialObject C`. -/
278278
abbrev cosk (n : ℕ) [∀ (F : (SimplexCategory.Truncated n)ᵒᵖ ⥤ C),
279-
SimplexCategory.Truncated.inclusion.op.HasRightKanExtension F] :
279+
(SimplexCategory.Truncated.inclusion n).op.HasRightKanExtension F] :
280280
SimplicialObject C ⥤ SimplicialObject C := truncation n ⋙ Truncated.cosk n
281281

282282
end
@@ -288,9 +288,9 @@ respectively define left and right adjoints to `truncation n`.-/
288288

289289
variable (n : ℕ)
290290
variable [∀ (F : (SimplexCategory.Truncated n)ᵒᵖ ⥤ C),
291-
SimplexCategory.Truncated.inclusion.op.HasRightKanExtension F]
291+
(SimplexCategory.Truncated.inclusion n).op.HasRightKanExtension F]
292292
variable [∀ (F : (SimplexCategory.Truncated n)ᵒᵖ ⥤ C),
293-
SimplexCategory.Truncated.inclusion.op.HasLeftKanExtension F]
293+
(SimplexCategory.Truncated.inclusion n).op.HasLeftKanExtension F]
294294

295295
/-- The adjunction between the n-skeleton and n-truncation.-/
296296
noncomputable def skAdj : Truncated.sk (C := C) n ⊣ truncation n :=
@@ -300,20 +300,30 @@ noncomputable def skAdj : Truncated.sk (C := C) n ⊣ truncation n :=
300300
noncomputable def coskAdj : truncation (C := C) n ⊣ Truncated.cosk n :=
301301
ranAdjunction _ _
302302

303+
instance : ((sk n).obj X).IsLeftKanExtension ((skAdj n).unit.app _) := by
304+
dsimp [sk, skAdj]
305+
rw [lanAdjunction_unit]
306+
infer_instance
307+
308+
instance : ((cosk n).obj X).IsRightKanExtension ((coskAdj n).counit.app _) := by
309+
dsimp [cosk, coskAdj]
310+
rw [ranAdjunction_counit]
311+
infer_instance
312+
303313
namespace Truncated
304314
/- When the left and right Kan extensions exist and are pointwise Kan extensions,
305315
`skAdj n` and `coskAdj n` are respectively coreflective and reflective.-/
306316

307317
variable [∀ (F : (SimplexCategory.Truncated n)ᵒᵖ ⥤ C),
308-
SimplexCategory.Truncated.inclusion.op.HasPointwiseRightKanExtension F]
318+
(SimplexCategory.Truncated.inclusion n).op.HasPointwiseRightKanExtension F]
309319
variable [∀ (F : (SimplexCategory.Truncated n)ᵒᵖ ⥤ C),
310-
SimplexCategory.Truncated.inclusion.op.HasPointwiseLeftKanExtension F]
320+
(SimplexCategory.Truncated.inclusion n).op.HasPointwiseLeftKanExtension F]
311321

312322
instance cosk_reflective : IsIso (coskAdj (C := C) n).counit :=
313-
reflective' SimplexCategory.Truncated.inclusion.op
323+
reflective' (SimplexCategory.Truncated.inclusion n).op
314324

315325
instance sk_coreflective : IsIso (skAdj (C := C) n).unit :=
316-
coreflective' SimplexCategory.Truncated.inclusion.op
326+
coreflective' (SimplexCategory.Truncated.inclusion n).op
317327

318328
/-- Since `Truncated.inclusion` is fully faithful, so is right Kan extension along it.-/
319329
noncomputable def cosk.fullyFaithful :
@@ -675,7 +685,7 @@ section Truncation
675685

676686
/-- The truncation functor from cosimplicial objects to truncated cosimplicial objects. -/
677687
def truncation (n : ℕ) : CosimplicialObject C ⥤ CosimplicialObject.Truncated C n :=
678-
(whiskeringLeft _ _ _).obj SimplexCategory.Truncated.inclusion
688+
(whiskeringLeft _ _ _).obj (SimplexCategory.Truncated.inclusion n)
679689

680690
end Truncation
681691

‎Mathlib/AlgebraicTopology/SimplicialObject/Coskeletal.lean‎

Lines changed: 91 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,91 @@
1+
/-
2+
Copyright (c) 2024 Emily Riehl. All rights reserved.
3+
Released under Apache 2.0 license as described in the file LICENSE.
4+
Authors: Mario Carneiro, Emily Riehl, Joël Riou
5+
-/
6+
import Mathlib.AlgebraicTopology.SimplicialObject.Basic
7+
import Mathlib.CategoryTheory.Functor.KanExtension.Adjunction
8+
import Mathlib.CategoryTheory.Functor.KanExtension.Basic
9+
10+
/-!
11+
# Coskeletal simplicial objects
12+
13+
The identity natural transformation exhibits a simplicial object `X` as a right extension of its
14+
restriction along `(Truncated.inclusion n).op` recorded by `rightExtensionInclusion X n`.
15+
16+
The simplicial object `X` is *n-coskeletal* if `rightExtensionInclusion X n` is a right Kan
17+
extension.
18+
19+
When the ambient category admits right Kan extensions along `(Truncated.inclusion n).op`,
20+
then when `X` is `n`-coskeletal, the unit of `coskAdj n` defines an isomorphism:
21+
`isoCoskOfIsCoskeletal : X ≅ (cosk n).obj X`.
22+
23+
TODO: Prove that `X` is `n`-coskeletal whenever a certain canonical cone is a limit cone.
24+
-/
25+
26+
open Opposite
27+
28+
open CategoryTheory
29+
30+
open CategoryTheory.Limits CategoryTheory.Functor SimplexCategory
31+
32+
universe v u v' u'
33+
34+
namespace CategoryTheory
35+
36+
namespace SimplicialObject
37+
variable {C : Type u} [Category.{v} C]
38+
variable (X : SimplicialObject C) (n : ℕ)
39+
40+
namespace Truncated
41+
42+
/-- The identity natural transformation exhibits a simplicial set as a right extension of its
43+
restriction along `(Truncated.inclusion n).op`.-/
44+
@[simps!]
45+
def rightExtensionInclusion :
46+
RightExtension (Truncated.inclusion n).op
47+
((Truncated.inclusion n).op ⋙ X) := RightExtension.mk _ (𝟙 _)
48+
49+
end Truncated
50+
51+
open Truncated
52+
53+
/-- A simplicial object `X` is `n`-coskeletal when it is the right Kan extension of its restriction
54+
along `(Truncated.inclusion n).op` via the identity natural transformation. -/
55+
@[mk_iff]
56+
class IsCoskeletal : Prop where
57+
isRightKanExtension : IsRightKanExtension X (𝟙 ((Truncated.inclusion n).op ⋙ X))
58+
59+
attribute [instance] IsCoskeletal.isRightKanExtension
60+
61+
section
62+
63+
variable [∀ (F : (SimplexCategory.Truncated n)ᵒᵖ ⥤ C),
64+
(SimplexCategory.Truncated.inclusion n).op.HasRightKanExtension F]
65+
66+
/-- If `X` is `n`-coskeletal, then `Truncated.rightExtensionInclusion X n` is a terminal object in
67+
the category `RightExtension (Truncated.inclusion n).op (Truncated.inclusion.op ⋙ X)`. -/
68+
noncomputable def IsCoskeletal.isUniversalOfIsRightKanExtension [X.IsCoskeletal n] :
69+
(rightExtensionInclusion X n).IsUniversal := by
70+
apply Functor.isUniversalOfIsRightKanExtension
71+
72+
theorem isCoskeletal_iff_isIso : X.IsCoskeletal n ↔ IsIso ((coskAdj n).unit.app X) := by
73+
rw [isCoskeletal_iff]
74+
exact isRightKanExtension_iff_isIso ((coskAdj n).unit.app X)
75+
((coskAdj n).counit.app _) (𝟙 _) ((coskAdj n).left_triangle_components X)
76+
77+
instance [X.IsCoskeletal n] : IsIso ((coskAdj n).unit.app X) := by
78+
rw [← isCoskeletal_iff_isIso]
79+
infer_instance
80+
81+
/-- The canonical isomorphism `X ≅ (cosk n).obj X` defined when `X` is coskeletal and the
82+
`n`-coskeleton functor exists.-/
83+
@[simps! hom]
84+
noncomputable def isoCoskOfIsCoskeletal [X.IsCoskeletal n] : X ≅ (cosk n).obj X :=
85+
asIso ((coskAdj n).unit.app X)
86+
87+
end
88+
89+
end SimplicialObject
90+
91+
end CategoryTheory

‎Mathlib/AlgebraicTopology/SimplicialSet/Basic.lean‎

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -3,7 +3,7 @@ Copyright (c) 2021 Kim Morrison. All rights reserved.
33
Released under Apache 2.0 license as described in the file LICENSE.
44
Authors: Johan Commelin, Kim Morrison, Adam Topaz
55
-/
6-
import Mathlib.AlgebraicTopology.SimplicialObject
6+
import Mathlib.AlgebraicTopology.SimplicialObject.Basic
77
import Mathlib.CategoryTheory.Limits.Shapes.Types
88
import Mathlib.CategoryTheory.Yoneda
99
import Mathlib.Data.Fin.VecNotation

‎Mathlib/AlgebraicTopology/SplitSimplicialObject.lean‎

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -3,7 +3,7 @@ Copyright (c) 2022 Joël Riou. All rights reserved.
33
Released under Apache 2.0 license as described in the file LICENSE.
44
Authors: Joël Riou
55
-/
6-
import Mathlib.AlgebraicTopology.SimplicialObject
6+
import Mathlib.AlgebraicTopology.SimplicialObject.Basic
77
import Mathlib.CategoryTheory.Limits.Shapes.Products
88
import Mathlib.Data.Fintype.Sigma
99

‎Mathlib/CategoryTheory/Idempotents/SimplicialObject.lean‎

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -3,7 +3,7 @@ Copyright (c) 2022 Joël Riou. All rights reserved.
33
Released under Apache 2.0 license as described in the file LICENSE.
44
Authors: Joël Riou
55
-/
6-
import Mathlib.AlgebraicTopology.SimplicialObject
6+
import Mathlib.AlgebraicTopology.SimplicialObject.Basic
77
import Mathlib.CategoryTheory.Idempotents.FunctorCategories
88

99
/-!

0 commit comments

Comments
 (0)