-
Notifications
You must be signed in to change notification settings - Fork 259
/
Filtered.lean
100 lines (74 loc) · 3.82 KB
/
Filtered.lean
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
/-
Copyright (c) 2022 Markus Himmel. All rights reserved.
Released under Apache 2.0 license as described in the file LICENSE.
Authors: Markus Himmel
-/
import Mathlib.CategoryTheory.Filtered.Basic
import Mathlib.CategoryTheory.Limits.HasLimits
import Mathlib.CategoryTheory.Limits.Types
#align_import category_theory.limits.filtered from "leanprover-community/mathlib"@"e4ee4e30418efcb8cf304ba76ad653aeec04ba6e"
/-!
# Filtered categories and limits
In this file , we show that `C` is filtered if and only if for every functor `F : J ⥤ C` from a
finite category there is some `X : C` such that `lim Hom(F·, X)` is nonempty.
Furthermore, we define the type classes `HasCofilteredLimitsOfSize` and `HasFilteredColimitsOfSize`.
-/
universe w' w v u
noncomputable section
open CategoryTheory
variable {C : Type u} [Category.{v} C]
namespace CategoryTheory
section NonemptyLimit
open CategoryTheory.Limits Opposite
/-- `C` is filtered if and only if for every functor `F : J ⥤ C` from a finite category there is
some `X : C` such that `lim Hom(F·, X)` is nonempty.
Lemma 3.1.2 of [Kashiwara2006] -/
theorem IsFiltered.iff_nonempty_limit : IsFiltered C ↔
∀ {J : Type v} [SmallCategory J] [FinCategory J] (F : J ⥤ C),
∃ (X : C), Nonempty (limit (F.op ⋙ yoneda.obj X)) := by
rw [IsFiltered.iff_cocone_nonempty.{v}]
refine ⟨fun h J _ _ F => ?_, fun h J _ _ F => ?_⟩
· obtain ⟨c⟩ := h F
exact ⟨c.pt, ⟨(limitCompYonedaIsoCocone F c.pt).inv c.ι⟩⟩
· obtain ⟨pt, ⟨ι⟩⟩ := h F
exact ⟨⟨pt, (limitCompYonedaIsoCocone F pt).hom ι⟩⟩
/-- `C` is cofiltered if and only if for every functor `F : J ⥤ C` from a finite category there is
some `X : C` such that `lim Hom(X, F·)` is nonempty. -/
theorem IsCofiltered.iff_nonempty_limit : IsCofiltered C ↔
∀ {J : Type v} [SmallCategory J] [FinCategory J] (F : J ⥤ C),
∃ (X : C), Nonempty (limit (F ⋙ coyoneda.obj (op X))) := by
rw [IsCofiltered.iff_cone_nonempty.{v}]
refine ⟨fun h J _ _ F => ?_, fun h J _ _ F => ?_⟩
· obtain ⟨c⟩ := h F
exact ⟨c.pt, ⟨(limitCompCoyonedaIsoCone F c.pt).inv c.π⟩⟩
· obtain ⟨pt, ⟨π⟩⟩ := h F
exact ⟨⟨pt, (limitCompCoyonedaIsoCone F pt).hom π⟩⟩
end NonemptyLimit
namespace Limits
section
variable (C)
/-- Class for having all cofiltered limits of a given size. -/
@[pp_with_univ]
class HasCofilteredLimitsOfSize : Prop where
/-- For all filtered types of size `w`, we have limits -/
HasLimitsOfShape : ∀ (I : Type w) [Category.{w'} I] [IsCofiltered I], HasLimitsOfShape I C
#align category_theory.limits.has_cofiltered_limits_of_size CategoryTheory.Limits.HasCofilteredLimitsOfSize
/-- Class for having all filtered colimits of a given size. -/
@[pp_with_univ]
class HasFilteredColimitsOfSize : Prop where
/-- For all filtered types of a size `w`, we have colimits -/
HasColimitsOfShape : ∀ (I : Type w) [Category.{w'} I] [IsFiltered I], HasColimitsOfShape I C
#align category_theory.limits.has_filtered_colimits_of_size CategoryTheory.Limits.HasFilteredColimitsOfSize
end
instance (priority := 100) hasLimitsOfShape_of_has_cofiltered_limits
[HasCofilteredLimitsOfSize.{w', w} C] (I : Type w) [Category.{w'} I] [IsCofiltered I] :
HasLimitsOfShape I C :=
HasCofilteredLimitsOfSize.HasLimitsOfShape _
#align category_theory.limits.has_limits_of_shape_of_has_cofiltered_limits CategoryTheory.Limits.hasLimitsOfShape_of_has_cofiltered_limits
instance (priority := 100) hasColimitsOfShape_of_has_filtered_colimits
[HasFilteredColimitsOfSize.{w', w} C] (I : Type w) [Category.{w'} I] [IsFiltered I] :
HasColimitsOfShape I C :=
HasFilteredColimitsOfSize.HasColimitsOfShape _
#align category_theory.limits.has_colimits_of_shape_of_has_filtered_colimits CategoryTheory.Limits.hasColimitsOfShape_of_has_filtered_colimits
end Limits
end CategoryTheory