Skip to content

Commit 6a058b4

Browse files
mattrobballChrisHughes24
mattrobball
and
ChrisHughes24
committed
feat: port/CategoryTheory.Limits.Shapes.FiniteLimits (#2647)
Co-authored-by: ChrisHughes24 <chrishughes24@gmail.com>
1 parent 187c3ef commit 6a058b4

File tree

2 files changed

+284
-0
lines changed

2 files changed

+284
-0
lines changed

‎Mathlib.lean‎

Lines changed: 1 addition & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -310,6 +310,7 @@ import Mathlib.CategoryTheory.Limits.Shapes.BinaryProducts
310310
import Mathlib.CategoryTheory.Limits.Shapes.DisjointCoproduct
311311
import Mathlib.CategoryTheory.Limits.Shapes.Equalizers
312312
import Mathlib.CategoryTheory.Limits.Shapes.Equivalence
313+
import Mathlib.CategoryTheory.Limits.Shapes.FiniteLimits
313314
import Mathlib.CategoryTheory.Limits.Shapes.Products
314315
import Mathlib.CategoryTheory.Limits.Shapes.Pullbacks
315316
import Mathlib.CategoryTheory.Limits.Shapes.RegularMono

‎Mathlib/CategoryTheory/Limits/Shapes/FiniteLimits.lean‎

Lines changed: 283 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,283 @@
1+
/-
2+
Copyright (c) 2019 Scott Morrison. All rights reserved.
3+
Released under Apache 2.0 license as described in the file LICENSE.
4+
Authors: Scott Morrison
5+
6+
! This file was ported from Lean 3 source module category_theory.limits.shapes.finite_limits
7+
! leanprover-community/mathlib commit c3019c79074b0619edb4b27553a91b2e82242395
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.FinCategory
12+
import Mathlib.CategoryTheory.Limits.Shapes.BinaryProducts
13+
import Mathlib.CategoryTheory.Limits.Shapes.Equalizers
14+
import Mathlib.CategoryTheory.Limits.Shapes.WidePullbacks
15+
import Mathlib.CategoryTheory.Limits.Shapes.Pullbacks
16+
import Mathlib.Data.Fintype.Option
17+
18+
/-!
19+
# Categories with finite limits.
20+
21+
A typeclass for categories with all finite (co)limits.
22+
-/
23+
24+
25+
universe w' w v' u' v u
26+
27+
noncomputable section
28+
29+
open CategoryTheory
30+
31+
namespace CategoryTheory.Limits
32+
33+
variable (C : Type u) [Category.{v} C]
34+
35+
-- We can't just made this an `abbreviation`
36+
-- because of https://github.com/leanprover-community/lean/issues/429
37+
/-- A category has all finite limits if every functor `J ⥤ C` with a `FinCategory J`
38+
instance and `J : Type` has a limit.
39+
40+
This is often called 'finitely complete'.
41+
-/
42+
class HasFiniteLimits : Prop where
43+
/-- `C` has all limits over any type `J` whose objects and morphisms lie in the same universe
44+
and which has `FinType` objects and morphisms-/
45+
out (J : Type) [𝒥 : SmallCategory J] [@FinCategory J 𝒥] : @HasLimitsOfShape J 𝒥 C _
46+
#align category_theory.limits.has_finite_limits CategoryTheory.Limits.HasFiniteLimits
47+
48+
instance (priority := 100) hasLimitsOfShape_of_hasFiniteLimits (J : Type w) [SmallCategory J]
49+
[FinCategory J] [HasFiniteLimits C] : HasLimitsOfShape J C := by
50+
apply @hasLimitsOfShapeOfEquivalence _ _ _ _ _ _ (FinCategory.equivAsType J) ?_
51+
apply HasFiniteLimits.out
52+
#align category_theory.limits.has_limits_of_shape_of_has_finite_limits CategoryTheory.Limits.hasLimitsOfShape_of_hasFiniteLimits
53+
54+
instance (priority := 100) hasFiniteLimits_of_hasLimitsOfSize [HasLimitsOfSize.{v', u'} C] :
55+
HasFiniteLimits C where
56+
out := fun J hJ hJ' =>
57+
haveI := hasLimitsOfSizeShrink.{0, 0} C
58+
let F := @FinCategory.equivAsType J (@FinCategory.fintypeObj J hJ hJ') hJ hJ'
59+
@hasLimitsOfShapeOfEquivalence (@FinCategory.AsType J (@FinCategory.fintypeObj J hJ hJ'))
60+
(@FinCategory.categoryAsType J (@FinCategory.fintypeObj J hJ hJ') hJ hJ') _ _ J hJ F _
61+
#align category_theory.limits.has_finite_limits_of_has_limits_of_size CategoryTheory.Limits.hasFiniteLimits_of_hasLimitsOfSize
62+
63+
/-- If `C` has all limits, it has finite limits. -/
64+
instance (priority := 100) hasFiniteLimits_of_hasLimits [HasLimits C] : HasFiniteLimits C :=
65+
inferInstance
66+
#align category_theory.limits.has_finite_limits_of_has_limits CategoryTheory.Limits.hasFiniteLimits_of_hasLimits
67+
68+
/-- We can always derive `HasFiniteLimits C` by providing limits at an
69+
arbitrary universe. -/
70+
theorem hasFiniteLimits_of_hasFiniteLimits_of_size
71+
(h : ∀ (J : Type w) {𝒥 : SmallCategory J} (_ : @FinCategory J 𝒥), HasLimitsOfShape J C) :
72+
HasFiniteLimits C where
73+
out := fun J hJ hhJ => by
74+
haveI := h (ULiftHom.{w} (ULift.{w} J)) <| @CategoryTheory.finCategoryUlift J hJ hhJ
75+
have l :
76+
@Equivalence J (ULiftHom (ULift J)) hJ (@ULiftHom.category (ULift J) (@uliftCategory J hJ))
77+
:= @ULiftHomULiftCategory.equiv J hJ
78+
apply @hasLimitsOfShapeOfEquivalence (ULiftHom (ULift J))
79+
(@ULiftHom.category (ULift J) (@uliftCategory J hJ)) C _ J hJ
80+
(@Equivalence.symm J hJ (ULiftHom (ULift J))
81+
(@ULiftHom.category (ULift J) (@uliftCategory J hJ)) l) _
82+
/- Porting note: tried to factor out (@instCategoryULiftHom (ULift J) (@uliftCategory J hJ)
83+
but when doing that would then find the instance and say it was not definitionally equal to
84+
to the provide one (the same thing factored out) -/
85+
#align category_theory.limits.has_finite_limits_of_has_finite_limits_of_size CategoryTheory.Limits.hasFiniteLimits_of_hasFiniteLimits_of_size
86+
87+
/-- A category has all finite colimits if every functor `J ⥤ C` with a `FinCategory J`
88+
instance and `J : Type` has a colimit.
89+
90+
This is often called 'finitely cocomplete'.
91+
-/
92+
class HasFiniteColimits : Prop where
93+
/-- `C` has all colimits over any type `J` whose objects and morphisms lie in the same universe
94+
and which has `FinType` objects and morphisms-/
95+
out (J : Type) [𝒥 : SmallCategory J] [@FinCategory J 𝒥] : @HasColimitsOfShape J 𝒥 C _
96+
#align category_theory.limits.has_finite_colimits CategoryTheory.Limits.HasFiniteColimits
97+
98+
instance (priority := 100) hasColimitsOfShape_of_hasFiniteColimits (J : Type w) [SmallCategory J]
99+
[FinCategory J] [HasFiniteColimits C] : HasColimitsOfShape J C := by
100+
refine @hasColimitsOfShape_of_equivalence _ _ _ _ _ _ (FinCategory.equivAsType J) ?_
101+
apply HasFiniteColimits.out
102+
#align category_theory.limits.has_colimits_of_shape_of_has_finite_colimits CategoryTheory.Limits.hasColimitsOfShape_of_hasFiniteColimits
103+
104+
instance (priority := 100) hasFiniteColimits_of_hasColimitsOfSize [HasColimitsOfSize.{v', u'} C] :
105+
HasFiniteColimits C where
106+
out := fun J hJ hJ' =>
107+
haveI := hasColimitsOfSize_shrink.{0, 0} C
108+
let F := @FinCategory.equivAsType J (@FinCategory.fintypeObj J hJ hJ') hJ hJ'
109+
@hasColimitsOfShape_of_equivalence (@FinCategory.AsType J (@FinCategory.fintypeObj J hJ hJ'))
110+
(@FinCategory.categoryAsType J (@FinCategory.fintypeObj J hJ hJ') hJ hJ') _ _ J hJ F _
111+
#align category_theory.limits.has_finite_colimits_of_has_colimits_of_size CategoryTheory.Limits.hasFiniteColimits_of_hasColimitsOfSize
112+
113+
/-- We can always derive `HasFiniteColimits C` by providing colimits at an
114+
arbitrary universe. -/
115+
theorem hasFiniteColimits_of_hasFiniteColimits_of_size
116+
(h : ∀ (J : Type w) {𝒥 : SmallCategory J} (_ : @FinCategory J 𝒥), HasColimitsOfShape J C) :
117+
HasFiniteColimits C where
118+
out := fun J hJ hhJ => by
119+
haveI := h (ULiftHom.{w} (ULift.{w} J)) <| @CategoryTheory.finCategoryUlift J hJ hhJ
120+
have l :
121+
@Equivalence J (ULiftHom (ULift J)) hJ (@ULiftHom.category (ULift J) (@uliftCategory J hJ))
122+
:= @ULiftHomULiftCategory.equiv J hJ
123+
apply @hasColimitsOfShape_of_equivalence (ULiftHom (ULift J))
124+
(@ULiftHom.category (ULift J) (@uliftCategory J hJ)) C _ J hJ
125+
(@Equivalence.symm J hJ (ULiftHom (ULift J))
126+
(@ULiftHom.category (ULift J) (@uliftCategory J hJ)) l) _
127+
#align category_theory.limits.has_finite_colimits_of_has_finite_colimits_of_size CategoryTheory.Limits.hasFiniteColimits_of_hasFiniteColimits_of_size
128+
129+
section
130+
131+
open WalkingParallelPair WalkingParallelPairHom
132+
133+
instance fintypeWalkingParallelPair : Fintype WalkingParallelPair where
134+
elems := [WalkingParallelPair.zero, WalkingParallelPair.one].toFinset
135+
complete x := by cases x <;> simp
136+
#align category_theory.limits.fintype_walking_parallel_pair CategoryTheory.Limits.fintypeWalkingParallelPair
137+
138+
-- attribute [local tidy] tactic.case_bash Porting note: no tidy; no case_bash
139+
140+
instance (j j' : WalkingParallelPair) : Fintype (WalkingParallelPairHom j j') where
141+
elems :=
142+
WalkingParallelPair.recOn j
143+
(WalkingParallelPair.recOn j' [WalkingParallelPairHom.id zero].toFinset
144+
[left, right].toFinset)
145+
(WalkingParallelPair.recOn j' ∅ [WalkingParallelPairHom.id one].toFinset)
146+
complete := by
147+
rintro (_|_) <;> simp
148+
· cases j <;> simp
149+
end
150+
151+
instance : FinCategory WalkingParallelPair where
152+
fintypeObj := fintypeWalkingParallelPair
153+
fintypeHom := instFintypeWalkingParallelPairHom -- Porting note: could not be inferred
154+
155+
/-- Equalizers are finite limits, so if `C` has all finite limits, it also has all equalizers -/
156+
example [HasFiniteLimits C] : HasEqualizers C := by infer_instance
157+
158+
/-- Coequalizers are finite colimits, of if `C` has all finite colimits, it also has all
159+
coequalizers -/
160+
example [HasFiniteColimits C] : HasCoequalizers C := by infer_instance
161+
162+
variable {J : Type v}
163+
164+
-- attribute [local tidy] tactic.case_bash Porting note: no tidy; no case_bash
165+
166+
namespace WidePullbackShape
167+
168+
instance fintypeObj [Fintype J] : Fintype (WidePullbackShape J) := by
169+
rw [WidePullbackShape]
170+
infer_instance
171+
#align category_theory.limits.wide_pullback_shape.fintype_obj CategoryTheory.Limits.WidePullbackShape.fintypeObj
172+
173+
instance fintypeHom (j j' : WidePullbackShape J) : Fintype (j ⟶ j')
174+
where
175+
elems := by
176+
cases' j' with j'
177+
· cases' j with j
178+
· exact {Hom.id none}
179+
· exact {Hom.term j}
180+
· by_cases some j' = j
181+
· rw [h]
182+
exact {Hom.id j}
183+
· exact ∅
184+
complete := by
185+
rintro (_|_)
186+
· cases j <;> simp
187+
· simp
188+
#align category_theory.limits.wide_pullback_shape.fintype_hom CategoryTheory.Limits.WidePullbackShape.fintypeHom
189+
190+
end WidePullbackShape
191+
192+
namespace WidePushoutShape
193+
194+
instance fintypeObj [Fintype J] : Fintype (WidePushoutShape J) := by
195+
rw [WidePushoutShape]; infer_instance
196+
#align category_theory.limits.wide_pushout_shape.fintype_obj CategoryTheory.Limits.WidePushoutShape.fintypeObj
197+
198+
instance fintypeHom (j j' : WidePushoutShape J) : Fintype (j ⟶ j') where
199+
elems := by
200+
cases' j with j
201+
· cases' j' with j'
202+
· exact {Hom.id none}
203+
· exact {Hom.init j'}
204+
· by_cases some j = j'
205+
· rw [h]
206+
exact {Hom.id j'}
207+
· exact ∅
208+
complete := by
209+
rintro (_|_)
210+
· cases j <;> simp
211+
· simp
212+
#align category_theory.limits.wide_pushout_shape.fintype_hom CategoryTheory.Limits.WidePushoutShape.fintypeHom
213+
214+
end WidePushoutShape
215+
216+
instance finCategoryWidePullback [Fintype J] : FinCategory (WidePullbackShape J)
217+
where fintypeHom := WidePullbackShape.fintypeHom
218+
#align category_theory.limits.fin_category_wide_pullback CategoryTheory.Limits.finCategoryWidePullback
219+
220+
instance finCategoryWidePushout [Fintype J] : FinCategory (WidePushoutShape J)
221+
where fintypeHom := WidePushoutShape.fintypeHom
222+
#align category_theory.limits.fin_category_wide_pushout CategoryTheory.Limits.finCategoryWidePushout
223+
224+
-- We can't just made this an `abbreviation`
225+
-- because of https://github.com/leanprover-community/lean/issues/429
226+
/-- `HasFiniteWidePullbacks` represents a choice of wide pullback
227+
for every finite collection of morphisms
228+
-/
229+
class HasFiniteWidePullbacks : Prop where
230+
/-- `C` has all wide pullbacks any Fintype `J`-/
231+
out (J : Type) [Fintype J] : HasLimitsOfShape (WidePullbackShape J) C
232+
#align category_theory.limits.has_finite_wide_pullbacks CategoryTheory.Limits.HasFiniteWidePullbacks
233+
234+
instance hasLimitsOfShape_widePullbackShape (J : Type) [Finite J] [HasFiniteWidePullbacks C] :
235+
HasLimitsOfShape (WidePullbackShape J) C := by
236+
cases nonempty_fintype J
237+
haveI := @HasFiniteWidePullbacks.out C _ _ J
238+
infer_instance
239+
#align category_theory.limits.has_limits_of_shape_wide_pullback_shape CategoryTheory.Limits.hasLimitsOfShape_widePullbackShape
240+
241+
/-- `HasFiniteWidePushouts` represents a choice of wide pushout
242+
for every finite collection of morphisms
243+
-/
244+
class HasFiniteWidePushouts : Prop where
245+
/-- `C` has all wide pushouts any Fintype `J`-/
246+
out (J : Type) [Fintype J] : HasColimitsOfShape (WidePushoutShape J) C
247+
#align category_theory.limits.has_finite_wide_pushouts CategoryTheory.Limits.HasFiniteWidePushouts
248+
249+
instance hasColimitsOfShape_widePushoutShape (J : Type) [Finite J] [HasFiniteWidePushouts C] :
250+
HasColimitsOfShape (WidePushoutShape J) C := by
251+
cases nonempty_fintype J
252+
haveI := @HasFiniteWidePushouts.out C _ _ J
253+
infer_instance
254+
#align category_theory.limits.has_colimits_of_shape_wide_pushout_shape CategoryTheory.Limits.hasColimitsOfShape_widePushoutShape
255+
256+
/-- Finite wide pullbacks are finite limits, so if `C` has all finite limits,
257+
it also has finite wide pullbacks
258+
-/
259+
theorem hasFiniteWidePullbacks_of_hasFiniteLimits [HasFiniteLimits C] : HasFiniteWidePullbacks C :=
260+
⟨fun _ _ => HasFiniteLimits.out _⟩
261+
#align category_theory.limits.has_finite_wide_pullbacks_of_has_finite_limits CategoryTheory.Limits.hasFiniteWidePullbacks_of_hasFiniteLimits
262+
263+
/-- Finite wide pushouts are finite colimits, so if `C` has all finite colimits,
264+
it also has finite wide pushouts
265+
-/
266+
theorem hasFiniteWidePushouts_of_has_finite_limits [HasFiniteColimits C] :
267+
HasFiniteWidePushouts C :=
268+
⟨fun _ _ => HasFiniteColimits.out _⟩
269+
#align category_theory.limits.has_finite_wide_pushouts_of_has_finite_limits CategoryTheory.Limits.hasFiniteWidePushouts_of_has_finite_limits
270+
271+
instance fintypeWalkingPair : Fintype WalkingPair where
272+
elems := {WalkingPair.left, WalkingPair.right}
273+
complete x := by cases x <;> simp
274+
#align category_theory.limits.fintype_walking_pair CategoryTheory.Limits.fintypeWalkingPair
275+
276+
/-- Pullbacks are finite limits, so if `C` has all finite limits, it also has all pullbacks -/
277+
example [HasFiniteWidePullbacks C] : HasPullbacks C := by infer_instance
278+
279+
/-- Pushouts are finite colimits, so if `C` has all finite colimits, it also has all pushouts -/
280+
example [HasFiniteWidePushouts C] : HasPushouts C := by infer_instance
281+
282+
end CategoryTheory.Limits
283+

0 commit comments

Comments
 (0)