CompositionSite.lean

1 import Mathlib.CategoryTheory.Sites.Grothendieck
2 import Mathlib.CategoryTheory.Category.Preorder
3 import Mathlib.Data.Set.Lattice.Bounded
4 
5 set_option autoImplicit false
6 
7 /-!
8 # A Grothendieck topology on full patches of views
9 
10 A sieve covers a patch exactly when it contains the support of every
11 composable pair of arrows in that patch. All three topology axioms are
12 proved. This is a specified topology, not a universal view doctrine.
13 -/
14 universe u v z t
15 namespace KomorebiSpace
16 open CategoryTheory
17 namespace CompositionSite
18 variable {V : Type u} [Category.{v} V]
19 
20 /-- A composable pair, with its three endpoint views. -/
21 structure Triangle (V : Type u) [Category.{v} V] where
22   a : V
23   b : V
24   c : V
25   first : a ⟶ b
26   second : b ⟶ c
27 
28 namespace Triangle
29 variable (q : Triangle V)
30 
31 def support : Set V := {x | x = q.a ∨ x = q.b ∨ x = q.c}
32 
33 @[simp] theorem a_mem : q.a ∈ q.support := Or.inl rfl
34 @[simp] theorem b_mem : q.b ∈ q.support := Or.inr (Or.inl rfl)
35 @[simp] theorem c_mem : q.c ∈ q.support := Or.inr (Or.inr rfl)
36 
37 theorem support_le_iff (W : Set V) :
38     q.support ⊆ W ↔ q.a ∈ W ∧ q.b ∈ W ∧ q.c ∈ W := by
39   constructor
40   · intro h
41     exact ⟨h q.a_mem, h q.b_mem, h q.c_mem⟩
42   · rintro ⟨ha, hb, hc⟩ x (rfl | rfl | rfl)
43     · exact ha
44     · exact hb
45     · exact hc
46 
47 /-- A degenerate triangle detects a single view. -/
48 def point (a : V) : Triangle V := ⟨a, a, a, 𝟙 a, 𝟙 a⟩
49 
50 end Triangle
51 
52 /-- Covering means that every composition support is a member of the sieve. -/
53 def Covers (W : Set V) (s : Sieve W) : Prop :=
54   ∀ (q : Triangle V) (h : q.support ⊆ W), s (homOfLE h)
55 
56 /-- The composition topology, constructed using mathlib's actual sieve API. -/
57 def topology (V : Type u) [Category.{v} V] : GrothendieckTopology (Set V) where
58   sieves W := {s | Covers W s}
59   top_mem' := by intro W q h; trivial
60   pullback_stable' := by
61     intro W Z s f hs q hq
62     exact hs q (hq.trans (leOfHom f))
63   transitive' := by
64     intro W s hs r hr q hq
65     have ht := hr (hs q hq)
66     exact ht q (Set.Subset.refl q.support)
67 
68 @[simp] theorem covering_iff (W : Set V) (s : Sieve W) :
69     s ∈ topology V W ↔ Covers W s := Iff.rfl
70 
71 /-- The downward closure of a family of subpatches. -/
72 def familySieve {I : Type z} (W : Set V) (U : I → Set V)
73     (_hU : ∀ i, U i ⊆ W) : Sieve W where
74   arrows := fun {Z} _ => ∃ i, Z ⊆ U i
75   downward_closed := by
76     intro Z Z' f hf g
77     obtain ⟨i, hi⟩ := hf
78     exact ⟨i, (leOfHom g).trans hi⟩
79 
80 /-- The relative composition-cover predicate, with containment separated. -/
81 def FamilyCovers {I : Type z} (W : Set V) (U : I → Set V) : Prop :=
82   ∀ (q : Triangle V), q.support ⊆ W → ∃ i, q.support ⊆ U i
83 
84 theorem familySieve_covering_iff {I : Type z} (W : Set V) (U : I → Set V)
85     (hU : ∀ i, U i ⊆ W) :
86     familySieve W U hU ∈ topology V W ↔ FamilyCovers W U := Iff.rfl
87 
88 /-- Identity covers. -/
89 theorem identity_cover (W : Set V) : FamilyCovers W (fun _ : Unit => W) := by
90   intro q hq
91   exact ⟨(), hq⟩
92 
93 /-- Pullback of a family is intersection with the smaller full patch. -/
94 theorem intersection_cover {I : Type z} {W Z : Set V} {U : I → Set V}
95     (hZW : Z ⊆ W) (h : FamilyCovers W U) :
96     FamilyCovers Z (fun i => U i ∩ Z) := by
97   intro q hq
98   obtain ⟨i, hi⟩ := h q (hq.trans hZW)
99   exact ⟨i, fun x hx => ⟨hi hx, hq hx⟩⟩
100 
101 /-- Composite covering families still see every composition relation. -/
102 theorem composite_cover {I : Type z} {J : I → Type t} {W : Set V}
103     {U : I → Set V} {T : ∀ i, J i → Set V}
104     (h : FamilyCovers W U) (k : ∀ i, FamilyCovers (U i) (T i)) :
105     FamilyCovers W (fun ij : Sigma J => T ij.1 ij.2) := by
106   intro q hq
107   obtain ⟨i, hi⟩ := h q hq
108   obtain ⟨j, hj⟩ := k i q hi
109   exact ⟨⟨i, j⟩, hj⟩
110 
111 /-- A composition cover is necessarily an object cover. -/
112 theorem covers_objects {I : Type z} {W : Set V} {U : I → Set V}
113     (h : FamilyCovers W U) {a : V} (ha : a ∈ W) : ∃ i, a ∈ U i := by
114   have hq : (Triangle.point a).support ⊆ W :=
115     ((Triangle.point a).support_le_iff W).mpr ⟨ha, ha, ha⟩
116   obtain ⟨i, hi⟩ := h (Triangle.point a) hq
117   exact ⟨i, hi (Triangle.a_mem _)⟩
118 
119 /-- Every covering sieve supplies its own covering family, not only chosen generators. -/
120 def sievePatches {W : Set V} (s : Sieve W) :=
121   {Z : Set V // ∃ h : Z ⊆ W, s (homOfLE h)}
122 
123 theorem sieve_family_covers {W : Set V} {s : Sieve W}
124     (hs : s ∈ topology V W) :
125     FamilyCovers W (fun Z : sievePatches s => Z.val) := by
126   intro q hq
127   exact ⟨⟨q.support, hq, hs q hq⟩, Set.Subset.refl _⟩
128 
129 omit [Category.{v} V] in
130 /-- The explicit downward closure is the standard sieve generated by the family. -/
131 theorem familySieve_eq_ofArrows {I : Type z} (W : Set V) (U : I → Set V)
132     (hU : ∀ i, U i ⊆ W) :
133     familySieve W U hU = Sieve.ofArrows U (fun i => homOfLE (hU i)) := by
134   apply Sieve.ext
135   intro Z f
136   rw [Sieve.mem_ofArrows_iff]
137   constructor
138   · rintro ⟨i, hi⟩
139     exact ⟨i, homOfLE hi, Subsingleton.elim _ _⟩
140   · rintro ⟨i, a, _⟩
141     exact ⟨i, leOfHom a⟩
142 
143 theorem ofArrows_covering_iff {I : Type z} (W : Set V) (U : I → Set V)
144     (hU : ∀ i, U i ⊆ W) :
145     Sieve.ofArrows U (fun i => homOfLE (hU i)) ∈ topology V W ↔ FamilyCovers W U := by
146   rw [← familySieve_eq_ofArrows]
147   exact Iff.rfl
148 
149 /-- Covering sieve membership is local at the composable-pair supports. -/
150 theorem support_covering_iff_top (q : Triangle V) (s : Sieve q.support) :
151     s ∈ topology V q.support ↔ s = ⊤ := by
152   constructor
153   · intro hs
154     have hi : s (𝟙 q.support) := hs q (Set.Subset.refl _)
155     apply Sieve.ext
156     intro Z f
157     constructor
158     · intro _; trivial
159     · intro _
160       simpa only [Category.comp_id] using s.downward_closed hi f
161   · intro hs
162     rw [hs]
163     exact (topology V).top_mem _
164 
165 /-- The empty patch has its required empty cover. -/
166 theorem empty_cover : FamilyCovers (∅ : Set V) (fun i : Empty => nomatch i) := by
167   intro q hq
168   exact False.elim (hq q.a_mem)
169 
170 end CompositionSite
171 end KomorebiSpace

Back to source controls