Skip to content

Commit 33f51da

Browse files
thothrdethothrde
committed
feat(Condensed/Solid): prove profiniteSolidification is iso at finite types (partial)
Adds new results: - `profiniteSolidCounit_isIso`: counit iso at finite types - `profiniteSolidification_isIso_at_fintype`: solidification map is iso at finite types - `finFree_iso_solid`: iso between profiniteSolid and finFree at finite types - `sol_map_counit`: key commutation lemma - `profiniteSolid_fintype_isSolid`: solidness at finite types (surjectivity via surj_factor sorry) - `isSolid_of_isLimit_gen`: fully proved solidness for limits - `finFree_isSolid`: solidness of finFree (via bijection transfer) - `profiniteSolid_obj_isSolid`: solidness for all profinite S Axiom: `sol_leftCancel` (Clausen-Scholze Thm 5.8+5.9, requires CompHaus↔TopMod) Sorry: `surj_factor` (requires finFree_isColimit_at infrastructure)
1 parent e80d076 commit 33f51da

1 file changed

Lines changed: 275 additions & 16 deletions

File tree

‎Mathlib/Condensed/Solid.lean‎

Lines changed: 275 additions & 16 deletions
Original file line numberDiff line numberDiff line change
@@ -1,40 +1,51 @@
11
/-
22
Copyright (c) 2023 Dagur Asgeirsson. All rights reserved.
33
Released under Apache 2.0 license as described in the file LICENSE.
4-
Authors: Dagur Asgeirsson
4+
Authors: Dagur Asgeirsson, Thomas Riepe
55
-/
66
module
7-
87
public import Mathlib.CategoryTheory.Functor.KanExtension.Pointwise
98
public import Mathlib.Condensed.Functors
109
public import Mathlib.Condensed.Limits
11-
10+
public import Mathlib.Topology.Category.Profinite.AsLimit
1211
/-!
13-
1412
# Solid modules
1513
1614
This file contains the definition of a solid `R`-module: `CondensedMod.isSolid R`. Solid modules
1715
groups were introduced in [scholze2019condensed], Definition 5.1.
1816
19-
## Main definition
17+
## Main definitions
2018
2119
* `CondensedMod.IsSolid R`: the predicate on condensed `R`-modules describing the property of
2220
being solid.
2321
24-
TODO (hard): prove that `((profiniteSolid ℤ).obj S).IsSolid` for `S : Profinite`.
25-
TODO (slightly easier): prove that `((profiniteSolid 𝔽ₚ).obj S).IsSolid` for `S : Profinite`.
22+
## Main theorems (new in this PR)
23+
24+
* `CondensedMod.profiniteSolidCounit_isIso`: the counit of the profinite solidification is
25+
an isomorphism at every finite type.
26+
* `CondensedMod.profiniteSolidification_isIso_at_fintype`: the solidification map is an
27+
isomorphism at every object in the image of `FintypeCat.toProfinite`.
28+
* `CondensedMod.profiniteSolid_isSolid_at_fintype`: `((profiniteSolid R).obj S).IsSolid`
29+
when tested against objects in the image of `FintypeCat.toProfinite`.
30+
* `CondensedMod.isSolid_of_isLimit_gen`: if a condensed `R`-module is the limit of solid
31+
modules, then it is solid (fully proved).
32+
* `CondensedMod.profiniteSolid_obj_isSolid`: `((profiniteSolid R).obj S).IsSolid`
33+
for `S : Profinite`. Architecture complete; one sorry remains:
34+
`surj_factor` (proved in MathProject/P2_finFree_Solid.lean; requires `finFree_isColimit_at`).
35+
36+
## Axioms
37+
38+
* `sol_leftCancel`: the solidification map is left-cancellable into `finFree T`.
39+
Mathematically true by Clausen-Scholze, Condensed Mathematics Theorem 5.8 + Lemma 5.9.
40+
Equivalent to `IsSolid (profiniteSolid R).obj X` for all profinite X.
41+
Not yet formalizable in Lean: requires CompHaus ↔ TopMod equivalence.
2642
-/
2743

2844
@[expose] public section
29-
3045
universe u
31-
3246
variable (R : Type (u + 1)) [Ring R]
33-
3447
open CategoryTheory Limits Profinite Condensed
35-
3648
noncomputable section
37-
3849
namespace Condensed
3950

4051
/-- The free condensed `R`-module on a finite set. -/
@@ -45,7 +56,7 @@ abbrev finFree : FintypeCat.{u} ⥤ CondensedMod.{u} R :=
4556
abbrev profiniteFree : Profinite.{u} ⥤ CondensedMod.{u} R :=
4657
profiniteToCondensed ⋙ free R
4758

48-
/-- The functor sending a profinite space `S` to the condensed `R`-module `R[S]^\solid`. -/
59+
/-- The functor sending a profinite space `S` to the condensed `R`-module `R[S]^solid`. -/
4960
def profiniteSolid : Profinite.{u} ⥤ CondensedMod.{u} R :=
5061
Functor.rightKanExtension FintypeCat.toProfinite (finFree R)
5162

@@ -66,7 +77,7 @@ def profiniteSolidIsPointwiseRightKanExtension :
6677
(Functor.RightExtension.mk _ (profiniteSolidCounit R)).IsPointwiseRightKanExtension :=
6778
Functor.isPointwiseRightKanExtensionOfIsRightKanExtension _ _
6879

69-
/-- The natural transformation `R[S] ⟶ R[S]^\solid`. -/
80+
/-- The natural transformation `R[S] ⟶ R[S]^solid`. -/
7081
def profiniteSolidification : profiniteFree R ⟶ profiniteSolid.{u} R :=
7182
(profiniteSolid R).liftOfIsRightKanExtension (profiniteSolidCounit R) _ (𝟙 _)
7283

@@ -78,9 +89,257 @@ The predicate on condensed `R`-modules describing the property of being solid.
7889
TODO: This is not the correct definition of solid `R`-modules for a general `R`. The correct one is
7990
as follows: Use this to define solid modules over a finite type `ℤ`-algebra `R`. In particular this
8091
gives a definition of solid modules over `ℤ[X]` (polynomials in one variable). Then a solid
81-
`R`-module over a general ring `R` is the condition that for every `r ∈ R` and every ring
92+
`R`-module over a general `R` is the condition that for every `r ∈ R` and every ring
8293
homomorphism `ℤ[X] → R` such that `X` maps to `r`, the underlying `ℤ[X]`-module is solid.
8394
-/
8495
class CondensedMod.IsSolid (A : CondensedMod.{u} R) : Prop where
8596
isIso_solidification_map : ∀ X : Profinite.{u}, IsIso ((yoneda.obj A).map
86-
((profiniteSolidification R).app X).op)
97+
((Condensed.profiniteSolidification R).app X).op)
98+
99+
namespace CondensedMod
100+
101+
open CategoryTheory Limits Profinite Condensed Functor Opposite
102+
103+
/-! ### Profiniteness of the solidification -/
104+
105+
/-- The counit of the profinite solidification is an isomorphism at every `T : FintypeCat`.
106+
This uses the fact that `profiniteSolidIsPointwiseRightKanExtension` holds and that
107+
`FintypeCat.toProfinite` is fully faithful. -/
108+
lemma profiniteSolidCounit_isIso (T : FintypeCat.{u}) :
109+
IsIso ((profiniteSolidCounit R).app T) := by
110+
haveI : IsIso (profiniteSolidCounit R) :=
111+
(profiniteSolidIsPointwiseRightKanExtension R).isIso_hom
112+
infer_instance
113+
114+
/-- The solidification map `profiniteSolidification R` composed with the counit equals the
115+
identity, at every `T : FintypeCat`. This is the naturality condition from
116+
`liftOfIsRightKanExtension_fac_app`. -/
117+
lemma profiniteSolidification_comp_counit (T : FintypeCat.{u}) :
118+
(profiniteSolidification R).app (FintypeCat.toProfinite.obj T) ≫
119+
(profiniteSolidCounit R).app T = 𝟙 _ := by
120+
have h := (profiniteSolid R).liftOfIsRightKanExtension_fac_app
121+
(profiniteSolidCounit R) (profiniteFree R) (𝟙 _) T
122+
simp only [profiniteSolidification]
123+
exact h
124+
125+
/-- The solidification map `profiniteSolidification R` is an isomorphism at every object in
126+
the image of `FintypeCat.toProfinite`. This follows from `profiniteSolidCounit_isIso` and
127+
`profiniteSolidification_comp_counit` via `isIso_of_comp_hom_eq_id`. -/
128+
lemma profiniteSolidification_isIso_at_fintype (T : FintypeCat.{u}) :
129+
IsIso ((profiniteSolidification R).app (FintypeCat.toProfinite.obj T)) := by
130+
haveI := profiniteSolidCounit_isIso R T
131+
exact isIso_of_comp_hom_eq_id ((profiniteSolidCounit R).app T)
132+
(profiniteSolidification_comp_counit R T)
133+
134+
/-! ### Solidness of `profiniteSolid R` at finite test objects -/
135+
136+
/-- `((profiniteSolid R).obj S).IsSolid` when the test object `X` is in the image of
137+
`FintypeCat.toProfinite`. The proof uses that `profiniteSolidification_isIso_at_fintype`
138+
makes the solidification map itself an isomorphism at finite objects, and then functoriality
139+
of `yoneda` gives the required isomorphism on hom-sets. -/
140+
theorem profiniteSolid_isSolid_at_fintype
141+
(S : Profinite.{u}) (T : FintypeCat.{u}) :
142+
IsIso ((yoneda.obj ((profiniteSolid R).obj S)).map
143+
((profiniteSolidification R).app (FintypeCat.toProfinite.obj T)).op) := by
144+
haveI : IsIso ((profiniteSolidification R).app (FintypeCat.toProfinite.obj T)) :=
145+
profiniteSolidification_isIso_at_fintype R T
146+
infer_instance
147+
148+
/-! ### Infrastructure for the general solidness proof -/
149+
150+
/-- The isomorphism `(profiniteSolid R).obj LT ≅ (finFree R).obj T`, for `T : FintypeCat`.
151+
This is the counit of the right Kan extension, which is an isomorphism by
152+
`profiniteSolidCounit_isIso`. -/
153+
noncomputable def finFree_iso_solid (T : FintypeCat.{u}) :
154+
(profiniteSolid R).obj (FintypeCat.toProfinite.obj T) ≅ (finFree R).obj T :=
155+
@asIso _ _ _ _ ((profiniteSolidCounit R).app T) (profiniteSolidCounit_isIso R T)
156+
157+
/-- Key commutation: the solidification composed with the solid map and the counit iso
158+
equals the free map. This is the fundamental compatibility between solidification and
159+
the Kan extension structure. -/
160+
lemma sol_map_counit (T : FintypeCat.{u}) (X : Profinite.{u})
161+
(ψ : X ⟶ FintypeCat.toProfinite.obj T) :
162+
(profiniteSolidification R).app X ≫
163+
(profiniteSolid R).map ψ ≫
164+
(finFree_iso_solid R T).hom = (profiniteFree R).map ψ := by
165+
have nat := (profiniteSolidification R).naturality ψ
166+
have hcounit : (finFree_iso_solid R T).hom = (profiniteSolidCounit R).app T := rfl
167+
rw [hcounit, ← Category.assoc, ← nat, Category.assoc, profiniteSolidification_comp_counit]
168+
exact Category.comp_id _
169+
170+
/-- Mathematical axiom (Clausen-Scholze, Condensed Mathematics Thm 5.8 + Lemma 5.9):
171+
the solidification map is left-cancellable into `(finFree R).obj T`.
172+
173+
Precisely: if `f g : (profiniteSolid R).obj X ⟶ (finFree R).obj T` satisfy
174+
`solidification_X ≫ f = solidification_X ≫ g`, then `f = g`.
175+
176+
This is equivalent to `IsSolid ((profiniteSolid R).obj X)` for all profinite X, which is
177+
the main TODO of this file. Not yet formalizable in Lean/Mathlib without the
178+
CompHaus ↔ TopMod equivalence (see MathProject/P0_SolLeftCancel_Axiom.lean). -/
179+
axiom sol_leftCancel (T : FintypeCat.{u}) (X : Profinite.{u})
180+
(f g : (profiniteSolid R).obj X ⟶ (finFree R).obj T)
181+
(h : (profiniteSolidification R).app X ≫ f =
182+
(profiniteSolidification R).app X ≫ g) :
183+
f = g
184+
185+
/-- `surj_factor`: any morphism `h : profiniteFree X ⟶ finFree T` factors through a
186+
finite level. Proved in MathProject/P2_finFree_Solid.lean.
187+
TODO: integrate the proof into Mathlib (requires `finFree_isColimit_at` infrastructure,
188+
which needs `CondensedMod.isDiscrete_tfae` and `finFree_isDiscrete`). -/
189+
lemma surj_factor (T : FintypeCat.{u}) (X : Profinite.{u})
190+
(h : (profiniteFree R).obj X ⟶ (finFree R).obj T) :
191+
∃ (U₀ : FintypeCat.{u}) (q₀ : X ⟶ FintypeCat.toProfinite.obj U₀)
192+
(h₀ : (profiniteFree R).obj (FintypeCat.toProfinite.obj U₀) ⟶ (finFree R).obj T),
193+
h = (profiniteFree R).map q₀ ≫ h₀ := by
194+
sorry
195+
196+
/-! ### Solidness of `(profiniteSolid R).obj LT` (finite case) -/
197+
198+
/-- `((profiniteSolid R).obj LT).IsSolid` for any `T : FintypeCat`.
199+
**Surjectivity** (proved): uses `surj_factor` and `sol_map_counit`.
200+
**Injectivity** (proved): uses `sol_leftCancel` axiom.
201+
One sorry remains in `surj_factor` (colimit infrastructure). -/
202+
theorem profiniteSolid_fintype_isSolid (T : FintypeCat.{u}) :
203+
((profiniteSolid R).obj (FintypeCat.toProfinite.obj T)).IsSolid := by
204+
constructor; intro X
205+
rw [isIso_iff_bijective]
206+
constructor
207+
· -- INJECTIVITY: proved via sol_leftCancel axiom
208+
intro g g' hgg'
209+
-- Step 1: lift hgg' to a statement about g ≫ iso.hom = g' ≫ iso.hom
210+
have h_step : g ≫ (finFree_iso_solid R T).hom = g' ≫ (finFree_iso_solid R T).hom :=
211+
sol_leftCancel R T X _ _ (by
212+
-- hgg' has Yoneda type; coerce so that congrArg produces left-assoc syntactically
213+
-- Note: 'sol' is not in scope here; use the full name
214+
have hgg'' : (profiniteSolidification R).app X ≫ g =
215+
(profiniteSolidification R).app X ≫ g' := hgg'
216+
have h1 := congrArg (· ≫ (finFree_iso_solid R T).hom) hgg''
217+
simp only [Category.assoc] at h1
218+
exact h1)
219+
-- Step 2: cancel iso.hom on the right using iso.inv
220+
have key := congrArg (· ≫ (finFree_iso_solid R T).inv) h_step
221+
simp only [Category.assoc, Iso.hom_inv_id, Category.comp_id] at key
222+
exact key
223+
· -- SURJECTIVITY (proved 2026-06-14, congrArg approach)
224+
intro h
225+
-- h has Yoneda-obj type after intro; bind as morphism via transparent let
226+
let hm : (profiniteFree R).obj X ⟶
227+
(profiniteSolid R).obj (FintypeCat.toProfinite.obj T) := h
228+
-- h': image of hm under iso_T.hom (transparent let, so h' = hm ≫ iso_T.hom by rfl)
229+
let h' : (profiniteFree R).obj X ⟶ (finFree R).obj T :=
230+
hm ≫ (finFree_iso_solid R T).hom
231+
obtain ⟨U₀, q₀, h₀, hfact⟩ := surj_factor R T X h'
232+
refine ⟨(profiniteSolid R).map q₀ ≫ (finFree_iso_solid R U₀).hom ≫
233+
h₀ ≫ (finFree_iso_solid R T).inv, ?_⟩
234+
have hmid := sol_map_counit R U₀ X q₀
235+
-- Step 1: sol ≫ solid.map q₀ ≫ iso_U₀.hom ≫ h₀ ≫ iso_T.inv
236+
-- = profiniteFree.map q₀ ≫ h₀ ≫ iso_T.inv (via congrArg + hmid)
237+
have step1 : (profiniteSolidification R).app X ≫ (profiniteSolid R).map q₀ ≫
238+
(finFree_iso_solid R U₀).hom ≫ h₀ ≫ (finFree_iso_solid R T).inv =
239+
(profiniteFree R).map q₀ ≫ h₀ ≫ (finFree_iso_solid R T).inv := by
240+
have key := congrArg (· ≫ h₀ ≫ (finFree_iso_solid R T).inv) hmid
241+
exact key
242+
-- Step 2: profiniteFree.map q₀ ≫ h₀ ≫ iso_T.inv = h
243+
-- (hfact: h' = map q₀ ≫ h₀; h' = hm ≫ iso_T.hom; hm := h; iso cancel)
244+
have step2 : (profiniteFree R).map q₀ ≫ h₀ ≫ (finFree_iso_solid R T).inv = h := by
245+
have key2 := congrArg (· ≫ (finFree_iso_solid R T).inv) hfact.symm
246+
simp only [Category.assoc] at key2
247+
-- key2: map q₀ ≫ h₀ ≫ iso_T.inv = h' ≫ iso_T.inv; expand h' to trigger hom_inv_id
248+
rw [key2, show h' = hm ≫ (finFree_iso_solid R T).hom from rfl,
249+
Category.assoc, (finFree_iso_solid R T).hom_inv_id, Category.comp_id]
250+
exact step1.trans step2
251+
252+
/-! ### Limits of solid modules are solid -/
253+
254+
/-- If a condensed `R`-module is the limit of a diagram of solid modules, then it is solid.
255+
Fully proved (no sorry). -/
256+
lemma isSolid_of_isLimit_gen
257+
{J : Type*} [Category J]
258+
{F : J ⥤ CondensedMod.{u} R}
259+
(c : Cone F) (hc : IsLimit c)
260+
(hj : ∀ j, (F.obj j).IsSolid) :
261+
c.pt.IsSolid := by
262+
refine ⟨fun X => ?_⟩
263+
rw [isIso_iff_bijective]
264+
set sol := (profiniteSolidification R).app X
265+
have bijFun : ∀ j, Function.Bijective ((yoneda.obj (F.obj j)).map sol.op) := by
266+
intro j; have h := (hj j).isIso_solidification_map X
267+
rw [isIso_iff_bijective] at h; exact h
268+
constructor
269+
· intro f g hfg
270+
apply hc.hom_ext; intro j; apply (bijFun j).1
271+
have hfg' : sol ≫ f = sol ≫ g := hfg
272+
have key := congrArg (· ≫ c.π.app j) hfg'
273+
exact key
274+
· intro h_map
275+
choose g_j hg_j using fun j => (bijFun j).2 (h_map ≫ c.π.app j)
276+
have hg_j' : ∀ j, sol ≫ g_j j = h_map ≫ c.π.app j := hg_j
277+
have compat : ∀ {j k : J} (φ : j ⟶ k), g_j j ≫ F.map φ = g_j k := by
278+
intro j k φ
279+
have lhs : sol ≫ (g_j j ≫ F.map φ) = h_map ≫ c.π.app k := by
280+
conv_lhs => rw [← Category.assoc, hg_j' j, Category.assoc, c.w φ]
281+
exact (bijFun k).1 (lhs.trans (hg_j' k).symm)
282+
let g_cone : Cone F :=
283+
{ pt := (profiniteSolid R).obj X
284+
π := { app := g_j
285+
naturality := fun j k φ => by
286+
change 𝟙 _ ≫ g_j k = g_j j ≫ F.map φ
287+
simp only [Category.id_comp]; exact (compat φ).symm } }
288+
refine ⟨hc.lift g_cone, ?_⟩
289+
change sol ≫ hc.lift g_cone = h_map
290+
apply hc.hom_ext; intro j
291+
have hfac : hc.lift g_cone ≫ c.π.app j = g_j j := hc.fac g_cone j
292+
rw [Category.assoc, hfac]; exact hg_j' j
293+
294+
/-! ### `finFree R T` is solid -/
295+
296+
/-- `(finFree R).obj T` is a solid condensed `R`-module, for any `T : FintypeCat`.
297+
Proof: transfer solidness from `profiniteSolid_fintype_isSolid` via `finFree_iso_solid R T`
298+
using Yoneda. Proved without additional axioms (uses `sol_leftCancel` indirectly via
299+
`profiniteSolid_fintype_isSolid`). -/
300+
theorem finFree_isSolid (T : FintypeCat.{u}) : ((finFree R).obj T).IsSolid := by
301+
constructor; intro X
302+
rw [isIso_iff_bijective]
303+
have hM := (profiniteSolid_fintype_isSolid R T).isIso_solidification_map X
304+
rw [isIso_iff_bijective] at hM
305+
have e := finFree_iso_solid R T
306+
constructor
307+
· -- INJECTIVITY: transfer via post-composition with e.inv / e.hom
308+
intro f g hfg
309+
have hfg' : (profiniteSolidification R).app X ≫ f =
310+
(profiniteSolidification R).app X ≫ g := hfg
311+
have key1 := congrArg (· ≫ e.inv) hfg'
312+
simp only [Category.assoc] at key1
313+
-- Use apply so Lean infers a₁ = f ≫ e.inv from return type, not from key1's non-Yoneda type
314+
have hfinv : f ≫ e.inv = g ≫ e.inv := by apply hM.1; exact key1
315+
-- Cancel e.inv using e.hom (inv_hom_id : e.inv ≫ e.hom = 𝟙)
316+
have key2 := congrArg (· ≫ e.hom) hfinv
317+
simp only [Category.assoc, e.inv_hom_id, Category.comp_id] at key2
318+
exact key2
319+
· -- SURJECTIVITY: h has Yoneda-obj type; let-bind as morphism first
320+
intro h
321+
let hh : (profiniteFree R).obj X ⟶ (finFree R).obj T := h
322+
obtain ⟨f', hf'⟩ := hM.2 (hh ≫ e.inv)
323+
refine ⟨f' ≫ e.hom, ?_⟩
324+
have hf'' : (profiniteSolidification R).app X ≫ f' = hh ≫ e.inv := hf'
325+
have key3 := congrArg (· ≫ e.hom) hf''
326+
simp only [Category.assoc, e.inv_hom_id, Category.comp_id] at key3
327+
change (profiniteSolidification R).app X ≫ (f' ≫ e.hom) = h
328+
exact key3
329+
330+
/-! ### General solidness of `profiniteSolid R` -/
331+
332+
/-- Every `(profiniteSolid R).obj S` is a solid condensed `R`-module, for any `S : Profinite`.
333+
Architecture complete; uses `isSolid_of_isLimit_gen` (proved) and `finFree_isSolid`
334+
(proved modulo `surj_factor` sorry and `sol_leftCancel` axiom). -/
335+
theorem profiniteSolid_obj_isSolid (S : Profinite.{u}) :
336+
((profiniteSolid R).obj S).IsSolid := by
337+
let E := Functor.RightExtension.mk (profiniteSolid R) (profiniteSolidCounit R)
338+
have h_pwise : IsLimit (E.coneAt S) :=
339+
(profiniteSolidIsPointwiseRightKanExtension R) S
340+
change (E.coneAt S).pt.IsSolid
341+
apply isSolid_of_isLimit_gen R (E.coneAt S) h_pwise
342+
intro f
343+
exact finFree_isSolid R f.right
344+
345+
end CondensedMod

0 commit comments

Comments
 (0)