Skip to content

Commit 93521b7

Browse files
dagurtomasdagurtomas
committed
feat: condensed sets are equivalent to sheaves on Stonean and Profinite (#6810)
Co-authored-by: Adam Topaz @adamtopaz Co-authored-by: Nick Kuhn @nick-kuhn - [x] depends on: #6809
1 parent 6f69c1a commit 93521b7

File tree

2 files changed

+228
-0
lines changed

2 files changed

+228
-0
lines changed

‎Mathlib.lean‎

Lines changed: 1 addition & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -1332,6 +1332,7 @@ import Mathlib.Computability.TMToPartrec
13321332
import Mathlib.Computability.TuringMachine
13331333
import Mathlib.Condensed.Abelian
13341334
import Mathlib.Condensed.Basic
1335+
import Mathlib.Condensed.Equivalence
13351336
import Mathlib.Control.Applicative
13361337
import Mathlib.Control.Basic
13371338
import Mathlib.Control.Bifunctor

‎Mathlib/Condensed/Equivalence.lean‎

Lines changed: 227 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,227 @@
1+
/-
2+
Copyright (c) 2023 Adam Topaz. All rights reserved.
3+
Released under Apache 2.0 license as described in the file LICENSE.
4+
Authors: Adam Topaz, Nick Kuhn, Dagur Asgeirsson
5+
-/
6+
import Mathlib.Topology.Category.Profinite.EffectiveEpi
7+
import Mathlib.Topology.Category.Stonean.EffectiveEpi
8+
import Mathlib.Condensed.Basic
9+
import Mathlib.CategoryTheory.Sites.DenseSubsite
10+
import Mathlib.CategoryTheory.Sites.InducedTopology
11+
import Mathlib.CategoryTheory.Sites.Closed
12+
/-!
13+
# Sheaves on CompHaus are equivalent to sheaves on Stonean
14+
15+
The forgetful functor from extremally disconnected spaces `Stonean` to compact
16+
Hausdorff spaces `CompHaus` has the marvellous property that it induces an equivalence of categories
17+
between sheaves on these two sites. With the terminology of nLab, `Stonean` is a
18+
*dense subsite* of `CompHaus`: see https://ncatlab.org/nlab/show/dense+sub-site
19+
20+
Mathlib has isolated three properties called `CoverDense`, `CoverPreserving` and `CoverLifting`,
21+
which between them imply that `Stonean` is a dense subsite, and it also has the
22+
construction of the equivalence of the categories of sheaves, given these three properties.
23+
24+
## Main theorems
25+
26+
* `Condensed.StoneanCompHaus.coverDense`, `Condensed.StoneanCompHaus.coverPreserving`,
27+
`Condensed.StoneanCompHaus.coverLifting`: the three conditions needed to guarantee the equivalence
28+
of the categories of sheaves on the coherent site on `Stonean` on the one hand and `CompHaus` on
29+
the other.
30+
* `Condensed.StoneanProfinite.coverDense`, `Condensed.StoneanProfinite.coverPreserving`,
31+
`Condensed.StoneanProfinite.coverLifting`: the corresponding conditions comparing the coherent
32+
sites on `Stonean` and `Profinite`.
33+
* `Condensed.StoneanCompHaus.equivalence`: the equivalence from coherent sheaves on `Stonean` to
34+
coherent sheaves on `CompHaus` (i.e. condensed sets).
35+
* `Condensed.StoneanProfinite.equivalence`: the equivalence from coherent sheaves on `Stonean` to
36+
coherent sheaves on `Profinite`.
37+
* `Condensed.ProfiniteCompHaus.equivalence`: the equivalence from coherent sheaves on `Profinite` to
38+
coherent sheaves on `CompHaus` (i.e. condensed sets).
39+
-/
40+
41+
open CategoryTheory Limits
42+
43+
namespace Condensed
44+
45+
universe u w
46+
47+
namespace StoneanCompHaus
48+
49+
open CompHaus in
50+
lemma generate_singleton_mem_coherentTopology (B : CompHaus) :
51+
Sieve.generate (Presieve.singleton (presentation.π B)) ∈ coherentTopology CompHaus B := by
52+
apply Coverage.saturate.of
53+
refine ⟨Unit, inferInstance, fun _ => (Stonean.toCompHaus.obj B.presentation),
54+
fun _ => (presentation.π B), ?_ , ?_⟩
55+
· funext X f
56+
ext
57+
refine ⟨fun ⟨⟩ ↦ ⟨()⟩, ?_⟩
58+
rintro ⟨⟩
59+
simp only [Presieve.singleton_eq_iff_domain]
60+
· apply ((effectiveEpiFamily_tfae
61+
(fun (_ : Unit) => (Stonean.toCompHaus.obj B.presentation))
62+
(fun (_ : Unit) => (CompHaus.presentation.π B))).out 0 2).mpr
63+
intro b
64+
exact ⟨(), (CompHaus.epi_iff_surjective (presentation.π B)).mp (presentation.epi_π B) b⟩
65+
66+
open CompHaus in
67+
lemma coverDense : CoverDense (coherentTopology _) Stonean.toCompHaus := by
68+
constructor
69+
intro B
70+
convert generate_singleton_mem_coherentTopology B
71+
ext Y f
72+
refine ⟨fun ⟨⟨obj, lift, map, fact⟩⟩ ↦ ?_, fun ⟨Z, h, g, hypo1, hf⟩ ↦ ?_⟩
73+
· have : Projective (Stonean.toCompHaus.obj obj) -- Lean should find this instance?
74+
· simp only [Stonean.toCompHaus, inducedFunctor_obj]
75+
exact inferInstance
76+
obtain ⟨p, p_factors⟩ := Projective.factors map (CompHaus.presentation.π B)
77+
exact ⟨(Stonean.toCompHaus.obj (presentation B)), ⟨lift ≫ p, ⟨(presentation.π B),
78+
⟨Presieve.singleton.mk, by rw [Category.assoc, p_factors, fact]⟩⟩⟩⟩
79+
· cases hypo1
80+
exact ⟨⟨presentation B, h, presentation.π B, hf⟩⟩
81+
82+
theorem coverDense.inducedTopology_Sieve_iff_EffectiveEpiFamily (X : Stonean) (S : Sieve X) :
83+
(∃ (α : Type) (_ : Fintype α) (Y : α → Stonean) (π : (a : α) → (Y a ⟶ X)),
84+
EffectiveEpiFamily Y π ∧ (∀ a : α, (S.arrows) (π a)) ) ↔
85+
(S ∈ coverDense.inducedTopology X) := by
86+
refine ⟨fun ⟨α, _, Y, π, ⟨H₁, H₂⟩⟩ ↦ ?_, fun hS ↦ ?_⟩
87+
· apply (coherentTopology.mem_sieves_iff_hasEffectiveEpiFamily (Sieve.functorPushforward _ S)).mpr
88+
refine ⟨α, inferInstance, fun i => Stonean.toCompHaus.obj (Y i),
89+
fun i => Stonean.toProfinite.map (π i), ⟨?_,
90+
fun a => Sieve.image_mem_functorPushforward Stonean.toCompHaus S (H₂ a)⟩⟩
91+
simp only [(Stonean.effectiveEpiFamily_tfae _ _).out 0 2] at H₁
92+
exact CompHaus.effectiveEpiFamily_of_jointly_surjective
93+
(fun i => Stonean.toCompHaus.obj (Y i)) (fun i => Stonean.toCompHaus.map (π i)) H₁
94+
· obtain ⟨α, _, Y, π, ⟨H₁, H₂⟩⟩ := (coherentTopology.mem_sieves_iff_hasEffectiveEpiFamily _).mp hS
95+
refine ⟨α, inferInstance, ?_⟩
96+
obtain ⟨Y₀, H₂⟩ := Classical.skolem.mp H₂
97+
obtain ⟨π₀, H₂⟩ := Classical.skolem.mp H₂
98+
obtain ⟨f₀, H₂⟩ := Classical.skolem.mp H₂
99+
refine ⟨Y₀ , π₀, ⟨?_, fun i ↦ (H₂ i).1⟩⟩
100+
simp only [(Stonean.effectiveEpiFamily_tfae _ _).out 0 2]
101+
simp only [(CompHaus.effectiveEpiFamily_tfae _ _).out 0 2] at H₁
102+
intro b
103+
obtain ⟨i, x, H₁⟩ := H₁ b
104+
refine ⟨i, f₀ i x, ?_⟩
105+
rw [← H₁, (H₂ i).2]
106+
rfl
107+
108+
lemma coherentTopology_is_induced :
109+
coherentTopology Stonean.{u} = coverDense.inducedTopology := by
110+
ext X S
111+
rw [← coverDense.inducedTopology_Sieve_iff_EffectiveEpiFamily X]
112+
rw [← coherentTopology.mem_sieves_iff_hasEffectiveEpiFamily S]
113+
114+
lemma coverPreserving :
115+
CoverPreserving (coherentTopology _) (coherentTopology _) Stonean.toCompHaus := by
116+
rw [coherentTopology_is_induced]
117+
exact LocallyCoverDense.inducedTopology_coverPreserving (CoverDense.locallyCoverDense coverDense)
118+
119+
lemma coverLifting : CoverLifting (coherentTopology _) (coherentTopology _) Stonean.toCompHaus := by
120+
rw [coherentTopology_is_induced]
121+
exact LocallyCoverDense.inducedTopology_coverLifting (CoverDense.locallyCoverDense coverDense)
122+
123+
/-- The equivalence from coherent sheaves on `Stonean` to coherent sheaves on `CompHaus`
124+
(i.e. condensed sets). -/
125+
noncomputable
126+
def equivalence (A : Type _) [Category.{u+1} A] [HasLimits A] :
127+
Sheaf (coherentTopology Stonean) A ≌ Condensed.{u} A :=
128+
CoverDense.sheafEquivOfCoverPreservingCoverLifting coverDense coverPreserving coverLifting
129+
130+
end StoneanCompHaus
131+
132+
end Condensed
133+
134+
namespace Condensed
135+
136+
universe u w
137+
138+
namespace StoneanProfinite
139+
140+
open Profinite in
141+
lemma generate_singleton_mem_coherentTopology (B : Profinite) :
142+
Sieve.generate (Presieve.singleton (presentation.π B)) ∈ coherentTopology Profinite B := by
143+
apply Coverage.saturate.of
144+
refine ⟨Unit, inferInstance, fun _ => (Stonean.toProfinite.obj B.presentation),
145+
fun _ => (presentation.π B), ?_ , ?_⟩
146+
· funext X f
147+
ext
148+
refine ⟨fun ⟨⟩ ↦ ⟨()⟩, ?_⟩
149+
rintro ⟨⟩
150+
simp only [Presieve.singleton_eq_iff_domain]
151+
· apply ((effectiveEpiFamily_tfae
152+
(fun (_ : Unit) => (Stonean.toProfinite.obj B.presentation))
153+
(fun (_ : Unit) => (Profinite.presentation.π B))).out 0 2).mpr
154+
intro b
155+
exact ⟨(), (Profinite.epi_iff_surjective (presentation.π B)).mp (presentation.epi_π B) b⟩
156+
157+
open Profinite in
158+
lemma coverDense : CoverDense (coherentTopology _) Stonean.toProfinite := by
159+
constructor
160+
intro B
161+
convert generate_singleton_mem_coherentTopology B
162+
ext Y f
163+
refine ⟨fun ⟨⟨obj, lift, map, fact⟩⟩ ↦ ?_, fun ⟨Z, h, g, hypo1, hf⟩ ↦ ?_⟩
164+
· obtain ⟨p, p_factors⟩ := Projective.factors map (Profinite.presentation.π B)
165+
exact ⟨(Stonean.toProfinite.obj (presentation B)), ⟨lift ≫ p, ⟨(presentation.π B),
166+
⟨Presieve.singleton.mk, by rw [Category.assoc, p_factors, fact]⟩⟩⟩⟩
167+
· cases hypo1
168+
exact ⟨⟨presentation B, h, presentation.π B, hf⟩⟩
169+
170+
theorem coverDense.inducedTopology_Sieve_iff_EffectiveEpiFamily (X : Stonean) (S : Sieve X) :
171+
(∃ (α : Type) (_ : Fintype α) (Y : α → Stonean) (π : (a : α) → (Y a ⟶ X)),
172+
EffectiveEpiFamily Y π ∧ (∀ a : α, (S.arrows) (π a)) ) ↔
173+
(S ∈ coverDense.inducedTopology X) := by
174+
refine ⟨fun ⟨α, _, Y, π, ⟨H₁, H₂⟩⟩ ↦ ?_, fun hS ↦ ?_⟩
175+
· apply (coherentTopology.mem_sieves_iff_hasEffectiveEpiFamily (Sieve.functorPushforward _ S)).mpr
176+
refine ⟨α, inferInstance, fun i => Stonean.toProfinite.obj (Y i),
177+
fun i => Stonean.toProfinite.map (π i), ⟨?_,
178+
fun a => Sieve.image_mem_functorPushforward Stonean.toCompHaus S (H₂ a)⟩⟩
179+
simp only [(Stonean.effectiveEpiFamily_tfae _ _).out 0 2] at H₁
180+
exact Profinite.effectiveEpiFamily_of_jointly_surjective
181+
(fun i => Stonean.toProfinite.obj (Y i)) (fun i => Stonean.toProfinite.map (π i)) H₁
182+
· obtain ⟨α, _, Y, π, ⟨H₁, H₂⟩⟩ := (coherentTopology.mem_sieves_iff_hasEffectiveEpiFamily _).mp hS
183+
refine ⟨α, inferInstance, ?_⟩
184+
obtain ⟨Y₀, H₂⟩ := Classical.skolem.mp H₂
185+
obtain ⟨π₀, H₂⟩ := Classical.skolem.mp H₂
186+
obtain ⟨f₀, H₂⟩ := Classical.skolem.mp H₂
187+
refine ⟨Y₀ , π₀, ⟨?_, fun i ↦ (H₂ i).1⟩⟩
188+
simp only [(Stonean.effectiveEpiFamily_tfae _ _).out 0 2]
189+
simp only [(Profinite.effectiveEpiFamily_tfae _ _).out 0 2] at H₁
190+
intro b
191+
obtain ⟨i, x, H₁⟩ := H₁ b
192+
refine ⟨i, f₀ i x, ?_⟩
193+
rw [← H₁, (H₂ i).2]
194+
rfl
195+
196+
lemma coherentTopology_is_induced :
197+
coherentTopology Stonean.{u} = coverDense.inducedTopology := by
198+
ext X S
199+
rw [← coverDense.inducedTopology_Sieve_iff_EffectiveEpiFamily X,
200+
← coherentTopology.mem_sieves_iff_hasEffectiveEpiFamily S]
201+
202+
lemma coverPreserving :
203+
CoverPreserving (coherentTopology _) (coherentTopology _) Stonean.toProfinite := by
204+
rw [coherentTopology_is_induced]
205+
exact LocallyCoverDense.inducedTopology_coverPreserving (CoverDense.locallyCoverDense coverDense)
206+
207+
lemma coverLifting :
208+
CoverLifting (coherentTopology _) (coherentTopology _) Stonean.toProfinite := by
209+
rw [coherentTopology_is_induced]
210+
exact LocallyCoverDense.inducedTopology_coverLifting (CoverDense.locallyCoverDense coverDense)
211+
212+
/-- The equivalence from coherent sheaves on `Stonean` to coherent sheaves on `Profinite`. -/
213+
noncomputable
214+
def equivalence (A : Type _) [Category.{u+1} A] [HasLimits A] :
215+
Sheaf (coherentTopology Stonean) A ≌ Sheaf (coherentTopology Profinite) A :=
216+
CoverDense.sheafEquivOfCoverPreservingCoverLifting coverDense coverPreserving coverLifting
217+
218+
end StoneanProfinite
219+
220+
/-- The equivalence from coherent sheaves on `Profinite` to coherent sheaves on `CompHaus`
221+
(i.e. condensed sets). -/
222+
noncomputable
223+
def ProfiniteCompHaus.equivalence (A : Type _) [Category.{u+1} A] [HasLimits A] :
224+
Sheaf (coherentTopology Profinite) A ≌ Condensed.{u} A :=
225+
(StoneanProfinite.equivalence A).symm.trans (StoneanCompHaus.equivalence A)
226+
227+
end Condensed

0 commit comments

Comments
 (0)