Skip to content

Commit 72ff023

Browse files
mattrobballmattrobball
committed
feat: port CategoryTheory.Skeletal (#2432)
Co-authored-by: Matthew Robert Ballard <100034030+mattrobball@users.noreply.github.com>
1 parent 2576ab9 commit 72ff023

File tree

2 files changed

+374
-0
lines changed

2 files changed

+374
-0
lines changed

‎Mathlib.lean‎

Lines changed: 1 addition & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -275,6 +275,7 @@ import Mathlib.CategoryTheory.Products.Associator
275275
import Mathlib.CategoryTheory.Products.Basic
276276
import Mathlib.CategoryTheory.Products.Bifunctor
277277
import Mathlib.CategoryTheory.Sigma.Basic
278+
import Mathlib.CategoryTheory.Skeletal
278279
import Mathlib.CategoryTheory.Sums.Basic
279280
import Mathlib.CategoryTheory.Thin
280281
import Mathlib.CategoryTheory.Types

‎Mathlib/CategoryTheory/Skeletal.lean‎

Lines changed: 373 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,373 @@
1+
/-
2+
Copyright (c) 2020 Bhavik Mehta. All rights reserved.
3+
Released under Apache 2.0 license as described in the file LICENSE.
4+
Authors: Bhavik Mehta
5+
6+
! This file was ported from Lean 3 source module category_theory.skeletal
7+
! leanprover-community/mathlib commit 28aa996fc6fb4317f0083c4e6daf79878d81be33
8+
! Please do not edit these lines, except to modify the commit id
9+
! if you have ported upstream changes.
10+
-/
11+
import Mathlib.CategoryTheory.Adjunction.Basic
12+
import Mathlib.CategoryTheory.Category.Preorder
13+
import Mathlib.CategoryTheory.IsomorphismClasses
14+
import Mathlib.CategoryTheory.Thin
15+
16+
/-!
17+
# Skeleton of a category
18+
19+
Define skeletal categories as categories in which any two isomorphic objects are equal.
20+
21+
Construct the skeleton of an arbitrary category by taking isomorphism classes, and show it is a
22+
skeleton of the original category.
23+
24+
In addition, construct the skeleton of a thin category as a partial ordering, and (noncomputably)
25+
show it is a skeleton of the original category. The advantage of this special case being handled
26+
separately is that lemmas and definitions about orderings can be used directly, for example for the
27+
subobject lattice. In addition, some of the commutative diagrams about the functors commute
28+
definitionally on the nose which is convenient in practice.
29+
-/
30+
31+
32+
universe v₁ v₂ v₃ u₁ u₂ u₃
33+
34+
namespace CategoryTheory
35+
36+
open Category
37+
38+
variable (C : Type u₁) [Category.{v₁} C]
39+
40+
variable (D : Type u₂) [Category.{v₂} D]
41+
42+
variable {E : Type u₃} [Category.{v₃} E]
43+
44+
/-- A category is skeletal if isomorphic objects are equal. -/
45+
def Skeletal : Prop :=
46+
∀ ⦃X Y : C⦄, IsIsomorphic X Y → X = Y
47+
#align category_theory.skeletal CategoryTheory.Skeletal
48+
49+
/-- `IsSkeletonOf C D F` says that `F : D ⥤ C` exhibits `D` as a skeletal full subcategory of `C`,
50+
in particular `F` is a (strong) equivalence and `D` is skeletal.
51+
-/
52+
structure IsSkeletonOf (F : D ⥤ C) where
53+
/-- The category `D` has isomorphic objects equal -/
54+
skel : Skeletal D
55+
/-- The functor `F` is an equivalence -/
56+
eqv : IsEquivalence F
57+
#align category_theory.is_skeleton_of CategoryTheory.IsSkeletonOf
58+
59+
attribute [local instance] isIsomorphicSetoid
60+
61+
variable {C D}
62+
63+
/-- If `C` is thin and skeletal, then any naturally isomorphic functors to `C` are equal. -/
64+
theorem Functor.eq_of_iso {F₁ F₂ : D ⥤ C} [Quiver.IsThin C] (hC : Skeletal C) (hF : F₁ ≅ F₂) :
65+
F₁ = F₂ :=
66+
Functor.ext (fun X => hC ⟨hF.app X⟩) fun _ _ _ => Subsingleton.elim _ _
67+
#align category_theory.functor.eq_of_iso CategoryTheory.Functor.eq_of_iso
68+
69+
/-- If `C` is thin and skeletal, `D ⥤ C` is skeletal.
70+
`CategoryTheory.functor_thin` shows it is thin also.
71+
-/
72+
theorem functor_skeletal [Quiver.IsThin C] (hC : Skeletal C) : Skeletal (D ⥤ C) := fun _ _ h =>
73+
h.elim (Functor.eq_of_iso hC)
74+
#align category_theory.functor_skeletal CategoryTheory.functor_skeletal
75+
76+
variable (C D)
77+
78+
/-- Construct the skeleton category as the induced category on the isomorphism classes, and derive
79+
its category structure.
80+
-/
81+
def Skeleton : Type u₁ := InducedCategory C Quotient.out
82+
#align category_theory.skeleton CategoryTheory.Skeleton
83+
84+
instance [Inhabited C] : Inhabited (Skeleton C) :=
85+
⟨⟦default⟧⟩
86+
87+
-- Porting note: previously `Skeleton` used `deriving Category`
88+
noncomputable instance : Category (Skeleton C) := by
89+
apply InducedCategory.category
90+
91+
/-- The functor from the skeleton of `C` to `C`. -/
92+
@[simps!]
93+
noncomputable def fromSkeleton : Skeleton C ⥤ C :=
94+
inducedFunctor _
95+
#align category_theory.from_skeleton CategoryTheory.fromSkeleton
96+
97+
-- Porting note: previously `fromSkeleton` used `deriving Faithful, Full`
98+
noncomputable instance : Full <| fromSkeleton C := by
99+
apply InducedCategory.full
100+
noncomputable instance : Faithful <| fromSkeleton C := by
101+
apply InducedCategory.faithful
102+
103+
instance : EssSurj (fromSkeleton C) where mem_essImage X := ⟨Quotient.mk' X, Quotient.mk_out X⟩
104+
105+
-- Porting note: named this instance
106+
noncomputable instance fromSkeleton.isEquivalence : IsEquivalence (fromSkeleton C) :=
107+
Equivalence.ofFullyFaithfullyEssSurj (fromSkeleton C)
108+
109+
/-- The equivalence between the skeleton and the category itself. -/
110+
noncomputable def skeletonEquivalence : Skeleton C ≌ C :=
111+
(fromSkeleton C).asEquivalence
112+
#align category_theory.skeleton_equivalence CategoryTheory.skeletonEquivalence
113+
114+
theorem skeleton_skeletal : Skeletal (Skeleton C) := by
115+
rintro X Y ⟨h⟩
116+
have : X.out ≈ Y.out := ⟨(fromSkeleton C).mapIso h⟩
117+
simpa using Quotient.sound this
118+
#align category_theory.skeleton_skeletal CategoryTheory.skeleton_skeletal
119+
120+
/-- The `skeleton` of `C` given by choice is a skeleton of `C`. -/
121+
noncomputable def skeletonIsSkeleton : IsSkeletonOf C (Skeleton C) (fromSkeleton C) where
122+
skel := skeleton_skeletal C
123+
eqv := fromSkeleton.isEquivalence C
124+
#align category_theory.skeleton_is_skeleton CategoryTheory.skeletonIsSkeleton
125+
126+
section
127+
128+
variable {C D}
129+
130+
/-- Two categories which are categorically equivalent have skeletons with equivalent objects.
131+
-/
132+
noncomputable def Equivalence.skeletonEquiv (e : C ≌ D) : Skeleton C ≃ Skeleton D :=
133+
let f := ((skeletonEquivalence C).trans e).trans (skeletonEquivalence D).symm
134+
{ toFun := f.functor.obj
135+
invFun := f.inverse.obj
136+
left_inv := fun X => skeleton_skeletal C ⟨(f.unitIso.app X).symm⟩
137+
right_inv := fun Y => skeleton_skeletal D ⟨f.counitIso.app Y⟩ }
138+
#align category_theory.equivalence.skeleton_equiv CategoryTheory.Equivalence.skeletonEquiv
139+
140+
end
141+
142+
/-- Construct the skeleton category by taking the quotient of objects. This construction gives a
143+
preorder with nice definitional properties, but is only really appropriate for thin categories.
144+
If your original category is not thin, you probably want to be using `skeleton` instead of this.
145+
-/
146+
def ThinSkeleton : Type u₁ :=
147+
Quotient (isIsomorphicSetoid C)
148+
#align category_theory.thin_skeleton CategoryTheory.ThinSkeleton
149+
150+
instance inhabitedThinSkeleton [Inhabited C] : Inhabited (ThinSkeleton C) :=
151+
⟨@Quotient.mk' C (isIsomorphicSetoid C) default⟩
152+
#align category_theory.inhabited_thin_skeleton CategoryTheory.inhabitedThinSkeleton
153+
154+
instance ThinSkeleton.preorder : Preorder (ThinSkeleton C)
155+
where
156+
le :=
157+
@Quotient.lift₂ C C _ (isIsomorphicSetoid C) (isIsomorphicSetoid C)
158+
(fun X Y => Nonempty (X ⟶ Y))
159+
(by
160+
rintro _ _ _ _ ⟨i₁⟩ ⟨i₂⟩
161+
exact
162+
propext
163+
⟨Nonempty.map fun f => i₁.inv ≫ f ≫ i₂.hom,
164+
Nonempty.map fun f => i₁.hom ≫ f ≫ i₂.inv⟩)
165+
le_refl := by
166+
refine' Quotient.ind fun a => _
167+
exact ⟨𝟙 _⟩
168+
le_trans a b c := Quotient.inductionOn₃ a b c fun A B C => Nonempty.map2 (· ≫ ·)
169+
#align category_theory.thin_skeleton.preorder CategoryTheory.ThinSkeleton.preorder
170+
171+
/-- The functor from a category to its thin skeleton. -/
172+
@[simps]
173+
def toThinSkeleton : C ⥤ ThinSkeleton C where
174+
obj := @Quotient.mk' C _
175+
map f := homOfLE (Nonempty.intro f)
176+
#align category_theory.to_thin_skeleton CategoryTheory.toThinSkeleton
177+
178+
/-!
179+
The constructions here are intended to be used when the category `C` is thin, even though
180+
some of the statements can be shown without this assumption.
181+
-/
182+
183+
184+
namespace ThinSkeleton
185+
186+
/-- The thin skeleton is thin. -/
187+
instance thin : Quiver.IsThin (ThinSkeleton C) := fun _ _ =>
188+
⟨by
189+
rintro ⟨⟨f₁⟩⟩ ⟨⟨_⟩⟩
190+
rfl⟩
191+
#align category_theory.thin_skeleton.thin CategoryTheory.ThinSkeleton.thin
192+
193+
variable {C} {D}
194+
195+
/-- A functor `C ⥤ D` computably lowers to a functor `ThinSkeleton C ⥤ ThinSkeleton D`. -/
196+
@[simps]
197+
def map (F : C ⥤ D) : ThinSkeleton C ⥤ ThinSkeleton D where
198+
obj := Quotient.map F.obj fun X₁ X₂ ⟨hX⟩ => ⟨F.mapIso hX⟩
199+
map {X} {Y} := Quotient.recOnSubsingleton₂ X Y fun x y k => homOfLE (k.le.elim fun t => ⟨F.map t⟩)
200+
#align category_theory.thin_skeleton.map CategoryTheory.ThinSkeleton.map
201+
202+
theorem comp_toThinSkeleton (F : C ⥤ D) : F ⋙ toThinSkeleton D = toThinSkeleton C ⋙ map F :=
203+
rfl
204+
#align category_theory.thin_skeleton.comp_to_thin_skeleton CategoryTheory.ThinSkeleton.comp_toThinSkeleton
205+
206+
/-- Given a natural transformation `F₁ ⟶ F₂`, induce a natural transformation `map F₁ ⟶ map F₂`.-/
207+
def mapNatTrans {F₁ F₂ : C ⥤ D} (k : F₁ ⟶ F₂) : map F₁ ⟶ map F₂
208+
where app X := Quotient.recOnSubsingleton X fun x => ⟨⟨⟨k.app x⟩⟩⟩
209+
#align category_theory.thin_skeleton.map_nat_trans CategoryTheory.ThinSkeleton.mapNatTrans
210+
211+
/- Porting note: `map₂ObjMap`, `map₂Functor`, and `map₂NatTrans` were all extracted
212+
from the original `map₂` proof. Lean needed an extensive amount explicit type
213+
annotations to figure things out. This also translated into repeated deterministic
214+
timeouts. The extracted defs allow for explicit motives for the multiple
215+
descents to the quotients.
216+
217+
It would be better to prove that
218+
`ThinSkeleton (C × D) ≌ ThinSkeleton C × ThinSkeleton D`
219+
which is more immediate from comparing the preorders. Then one could get
220+
`map₂` by currying.
221+
-/
222+
/-- Given a bifunctor, we descend to a function on objects of `ThinSkeleton` -/
223+
def map₂ObjMap (F : C ⥤ D ⥤ E) : ThinSkeleton C → ThinSkeleton D → ThinSkeleton E :=
224+
fun x y =>
225+
@Quotient.map₂ C D (isIsomorphicSetoid C) (isIsomorphicSetoid D) E (isIsomorphicSetoid E)
226+
(fun X Y => (F.obj X).obj Y)
227+
(fun X₁ _ ⟨hX⟩ _ Y₂ ⟨hY⟩ => ⟨(F.obj X₁).mapIso hY ≪≫ (F.mapIso hX).app Y₂⟩) x y
228+
229+
/-- For each `x : ThinSkeleton C`, we promote `map₂ObjMap F x` to a functor -/
230+
def map₂Functor (F : C ⥤ D ⥤ E) : ThinSkeleton C → ThinSkeleton D ⥤ ThinSkeleton E :=
231+
fun x =>
232+
{ obj := fun y => map₂ObjMap F x y
233+
map := fun {y₁} {y₂} => @Quotient.recOnSubsingleton C (isIsomorphicSetoid C)
234+
(fun x => (y₁ ⟶ y₂) → (map₂ObjMap F x y₁ ⟶ map₂ObjMap F x y₂)) _ x fun X
235+
=> Quotient.recOnSubsingleton₂ y₁ y₂ fun Y₁ Y₂ hY =>
236+
homOfLE (hY.le.elim fun g => ⟨(F.obj X).map g⟩) }
237+
238+
/-- This provides natural transformations `map₂Functor F x₁ ⟶ map₂Functor F x₂` given
239+
`x₁ ⟶ x₂` -/
240+
def map₂NatTrans (F : C ⥤ D ⥤ E) : {x₁ x₂ : ThinSkeleton C} → (x₁ ⟶ x₂) →
241+
(map₂Functor F x₁ ⟶ map₂Functor F x₂) := fun {x₁} {x₂} =>
242+
@Quotient.recOnSubsingleton₂ C C (isIsomorphicSetoid C) (isIsomorphicSetoid C)
243+
(fun x x' : ThinSkeleton C => (x ⟶ x') → (map₂Functor F x ⟶ map₂Functor F x')) _ x₁ x₂
244+
(fun X₁ X₂ f => { app := fun y =>
245+
Quotient.recOnSubsingleton y fun Y => homOfLE (f.le.elim fun f' => ⟨(F.map f').app Y⟩) })
246+
247+
-- TODO: state the lemmas about what happens when you compose with `toThinSkeleton`
248+
/-- A functor `C ⥤ D ⥤ E` computably lowers to a functor
249+
`ThinSkeleton C ⥤ ThinSkeleton D ⥤ ThinSkeleton E` -/
250+
@[simps]
251+
def map₂ (F : C ⥤ D ⥤ E) : ThinSkeleton C ⥤ ThinSkeleton D ⥤ ThinSkeleton E where
252+
obj := map₂Functor F
253+
map := map₂NatTrans F
254+
#align category_theory.thin_skeleton.map₂ CategoryTheory.ThinSkeleton.map₂
255+
256+
variable (C)
257+
258+
section
259+
260+
variable [Quiver.IsThin C]
261+
262+
instance toThinSkeleton_faithful : Faithful (toThinSkeleton C) where
263+
#align category_theory.thin_skeleton.to_thin_skeleton_faithful CategoryTheory.ThinSkeleton.toThinSkeleton_faithful
264+
265+
/-- Use `Quotient.out` to create a functor out of the thin skeleton. -/
266+
@[simps]
267+
noncomputable def fromThinSkeleton : ThinSkeleton C ⥤ C where
268+
obj := Quotient.out
269+
map {x} {y} :=
270+
Quotient.recOnSubsingleton₂ x y fun X Y f =>
271+
(Nonempty.some (Quotient.mk_out X)).hom ≫ f.le.some ≫ (Nonempty.some (Quotient.mk_out Y)).inv
272+
#align category_theory.thin_skeleton.from_thin_skeleton CategoryTheory.ThinSkeleton.fromThinSkeleton
273+
274+
noncomputable instance fromThinSkeletonEquivalence : IsEquivalence (fromThinSkeleton C) where
275+
inverse := toThinSkeleton C
276+
counitIso := NatIso.ofComponents (fun X => Nonempty.some (Quotient.mk_out X)) (by aesop_cat)
277+
unitIso := NatIso.ofComponents (fun x => Quotient.recOnSubsingleton x fun X =>
278+
eqToIso (Quotient.sound ⟨(Nonempty.some (Quotient.mk_out X)).symm⟩)) (fun _ => rfl)
279+
#align category_theory.thin_skeleton.from_thin_skeleton_equivalence CategoryTheory.ThinSkeleton.fromThinSkeletonEquivalence
280+
281+
/-- The equivalence between the thin skeleton and the category itself. -/
282+
noncomputable def equivalence : ThinSkeleton C ≌ C :=
283+
(fromThinSkeleton C).asEquivalence
284+
#align category_theory.thin_skeleton.equivalence CategoryTheory.ThinSkeleton.equivalence
285+
286+
variable {C}
287+
288+
theorem equiv_of_both_ways {X Y : C} (f : X ⟶ Y) (g : Y ⟶ X) : X ≈ Y :=
289+
⟨iso_of_both_ways f g⟩
290+
#align category_theory.thin_skeleton.equiv_of_both_ways CategoryTheory.ThinSkeleton.equiv_of_both_ways
291+
292+
instance thinSkeletonPartialOrder : PartialOrder (ThinSkeleton C) :=
293+
{ CategoryTheory.ThinSkeleton.preorder C with
294+
le_antisymm :=
295+
Quotient.ind₂
296+
(by
297+
rintro _ _ ⟨f⟩ ⟨g⟩
298+
apply Quotient.sound (equiv_of_both_ways f g)) }
299+
#align category_theory.thin_skeleton.thin_skeleton_partial_order CategoryTheory.ThinSkeleton.thinSkeletonPartialOrder
300+
301+
theorem skeletal : Skeletal (ThinSkeleton C) := fun X Y =>
302+
Quotient.inductionOn₂ X Y fun _ _ h => h.elim fun i => i.1.le.antisymm i.2.le
303+
#align category_theory.thin_skeleton.skeletal CategoryTheory.ThinSkeleton.skeletal
304+
305+
theorem map_comp_eq (F : E ⥤ D) (G : D ⥤ C) : map (F ⋙ G) = map F ⋙ map G :=
306+
Functor.eq_of_iso skeletal <|
307+
NatIso.ofComponents (fun X => Quotient.recOnSubsingleton X fun x => Iso.refl _) (by aesop_cat)
308+
#align category_theory.thin_skeleton.map_comp_eq CategoryTheory.ThinSkeleton.map_comp_eq
309+
310+
theorem map_id_eq : map (𝟭 C) = 𝟭 (ThinSkeleton C) :=
311+
Functor.eq_of_iso skeletal <|
312+
NatIso.ofComponents (fun X => Quotient.recOnSubsingleton X fun x => Iso.refl _) (by aesop_cat)
313+
#align category_theory.thin_skeleton.map_id_eq CategoryTheory.ThinSkeleton.map_id_eq
314+
315+
theorem map_iso_eq {F₁ F₂ : D ⥤ C} (h : F₁ ≅ F₂) : map F₁ = map F₂ :=
316+
Functor.eq_of_iso skeletal
317+
{ hom := mapNatTrans h.hom
318+
inv := mapNatTrans h.inv }
319+
#align category_theory.thin_skeleton.map_iso_eq CategoryTheory.ThinSkeleton.map_iso_eq
320+
321+
/-- `fromThinSkeleton C` exhibits the thin skeleton as a skeleton. -/
322+
noncomputable def thinSkeletonIsSkeleton : IsSkeletonOf C (ThinSkeleton C) (fromThinSkeleton C)
323+
where
324+
skel := skeletal
325+
eqv := ThinSkeleton.fromThinSkeletonEquivalence C
326+
#align category_theory.thin_skeleton.thin_skeleton_is_skeleton CategoryTheory.ThinSkeleton.thinSkeletonIsSkeleton
327+
328+
noncomputable instance isSkeletonOfInhabited :
329+
Inhabited (IsSkeletonOf C (ThinSkeleton C) (fromThinSkeleton C)) :=
330+
⟨thinSkeletonIsSkeleton⟩
331+
#align category_theory.thin_skeleton.is_skeleton_of_inhabited CategoryTheory.ThinSkeleton.isSkeletonOfInhabited
332+
333+
end
334+
335+
variable {C}
336+
337+
/-- An adjunction between thin categories gives an adjunction between their thin skeletons. -/
338+
def lowerAdjunction (R : D ⥤ C) (L : C ⥤ D) (h : L ⊣ R) : ThinSkeleton.map L ⊣ ThinSkeleton.map R :=
339+
Adjunction.mkOfUnitCounit
340+
{ unit :=
341+
{
342+
app := fun X => by
343+
letI := isIsomorphicSetoid C
344+
refine' Quotient.recOnSubsingleton X fun x => homOfLE ⟨h.unit.app x⟩ }
345+
-- TODO: make quotient.rec_on_subsingleton' so the letI isn't needed
346+
counit :=
347+
{
348+
app := fun X => by
349+
letI := isIsomorphicSetoid D
350+
refine' Quotient.recOnSubsingleton X fun x => homOfLE ⟨h.counit.app x⟩ } }
351+
#align category_theory.thin_skeleton.lower_adjunction CategoryTheory.ThinSkeleton.lowerAdjunction
352+
353+
end ThinSkeleton
354+
355+
open ThinSkeleton
356+
357+
section
358+
359+
variable {C} {α : Type _} [PartialOrder α]
360+
361+
/--
362+
When `e : C ≌ α` is a categorical equivalence from a thin category `C` to some partial order `α`,
363+
the `ThinSkeleton C` is order isomorphic to `α`.
364+
-/
365+
noncomputable def Equivalence.thinSkeletonOrderIso [Quiver.IsThin C] (e : C ≌ α) :
366+
ThinSkeleton C ≃o α :=
367+
((ThinSkeleton.equivalence C).trans e).toOrderIso
368+
#align category_theory.equivalence.thin_skeleton_order_iso CategoryTheory.Equivalence.thinSkeletonOrderIso
369+
370+
end
371+
372+
end CategoryTheory
373+

0 commit comments

Comments
 (0)