Skip to content

Commit 4411562

Browse files
dagurtomasdagurtomas
committed
feat(Condensed): light condensed modules satisfy countable AB4* (leanprover-community#18497)
Given sequences `M N : ℕ → C` of objects with morphisms `f n : M n ⟶ N n` for all `n`, we exhibit `∏ M` as the limit of the tower ``` ⋯ → ∏_{n < m + 1} M n × ∏_{n ≥ m + 1} N n → ∏_{n < m} M n × ∏_{n ≥ m} N n → ⋯ → ∏ N ``` Further, the transition maps in this tower are epimorphisms, in the case when each `f n` is an epimorphism and `C` has finite biproducts. We use this to conclude that light condensed modules over a ring R satisfy a countable version of Grothendieck's AB4* axiom.
1 parent 7fe7d99 commit 4411562

File tree

5 files changed

+303
-6
lines changed

5 files changed

+303
-6
lines changed

‎Mathlib.lean‎

Lines changed: 2 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -1898,6 +1898,7 @@ import Mathlib.CategoryTheory.Limits.Shapes.Pullback.PullbackCone
18981898
import Mathlib.CategoryTheory.Limits.Shapes.Pullback.Square
18991899
import Mathlib.CategoryTheory.Limits.Shapes.Reflexive
19001900
import Mathlib.CategoryTheory.Limits.Shapes.RegularMono
1901+
import Mathlib.CategoryTheory.Limits.Shapes.SequentialProduct
19011902
import Mathlib.CategoryTheory.Limits.Shapes.SingleObj
19021903
import Mathlib.CategoryTheory.Limits.Shapes.SplitCoequalizer
19031904
import Mathlib.CategoryTheory.Limits.Shapes.SplitEqualizer
@@ -2312,6 +2313,7 @@ import Mathlib.Condensed.Epi
23122313
import Mathlib.Condensed.Equivalence
23132314
import Mathlib.Condensed.Explicit
23142315
import Mathlib.Condensed.Functors
2316+
import Mathlib.Condensed.Light.AB
23152317
import Mathlib.Condensed.Light.Basic
23162318
import Mathlib.Condensed.Light.CartesianClosed
23172319
import Mathlib.Condensed.Light.Epi

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

Lines changed: 230 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,230 @@
1+
/-
2+
Copyright (c) 2024 Dagur Asgeirsson. All rights reserved.
3+
Released under Apache 2.0 license as described in the file LICENSE.
4+
Authors: Dagur Asgeirsson
5+
-/
6+
import Mathlib.Algebra.Order.Monoid.Canonical.Defs
7+
import Mathlib.CategoryTheory.Functor.OfSequence
8+
import Mathlib.CategoryTheory.Limits.Shapes.Biproducts
9+
import Mathlib.CategoryTheory.Limits.Shapes.Countable
10+
import Mathlib.CategoryTheory.Limits.Shapes.PiProd
11+
import Mathlib.CategoryTheory.Limits.Shapes.RegularMono
12+
import Mathlib.Order.Interval.Finset.Nat
13+
/-!
14+
15+
# ℕ-indexed products as sequential limits
16+
17+
Given sequences `M N : ℕ → C` of objects with morphisms `f n : M n ⟶ N n` for all `n`, this file
18+
exhibits `∏ M` as the limit of the tower
19+
20+
```
21+
⋯ → ∏_{n < m + 1} M n × ∏_{n ≥ m + 1} N n → ∏_{n < m} M n × ∏_{n ≥ m} N n → ⋯ → ∏ N
22+
```
23+
24+
Further, we prove that the transition maps in this tower are epimorphisms, in the case when each
25+
`f n` is an epimorphism and `C` has finite biproducts.
26+
-/
27+
28+
namespace CategoryTheory.Limits.SequentialProduct
29+
30+
variable {C : Type*} {M N : ℕ → C}
31+
32+
lemma functorObj_eq_pos {n m : ℕ} (h : m < n) :
33+
(fun i ↦ if _ : i < n then M i else N i) m = M m := dif_pos h
34+
35+
lemma functorObj_eq_neg {n m : ℕ} (h : ¬(m < n)) :
36+
(fun i ↦ if _ : i < n then M i else N i) m = N m := dif_neg h
37+
38+
variable [Category C] (f : ∀ n, M n ⟶ N n) [HasProductsOfShape ℕ C]
39+
40+
variable (M N) in
41+
/-- The product of the `m` first objects of `M` and the rest of the rest of `N` -/
42+
noncomputable def functorObj : ℕ → C :=
43+
fun n ↦ ∏ᶜ (fun m ↦ if _ : m < n then M m else N m)
44+
45+
/-- The projection map from `functorObj M N n` to `M m`, when `m < n` -/
46+
noncomputable def functorObjProj_pos (n m : ℕ) (h : m < n) :
47+
functorObj M N n ⟶ M m :=
48+
Pi.π (fun m ↦ if _ : m < n then M m else N m) m ≫ eqToHom (functorObj_eq_pos (by omega))
49+
50+
/-- The projection map from `functorObj M N n` to `N m`, when `m ≥ n` -/
51+
noncomputable def functorObjProj_neg (n m : ℕ) (h : ¬(m < n)) :
52+
functorObj M N n ⟶ N m :=
53+
Pi.π (fun m ↦ if _ : m < n then M m else N m) m ≫ eqToHom (functorObj_eq_neg (by omega))
54+
55+
/-- The transition maps in the sequential limit of products -/
56+
noncomputable def functorMap : ∀ n,
57+
functorObj M N (n + 1) ⟶ functorObj M N n := by
58+
intro n
59+
refine Limits.Pi.map fun m ↦ if h : m < n then eqToHom ?_ else
60+
if h' : m < n + 1 then eqToHom ?_ ≫ f m ≫ eqToHom ?_ else eqToHom ?_
61+
all_goals split_ifs; try rfl; try omega
62+
63+
lemma functorMap_commSq_succ (n : ℕ) :
64+
(Functor.ofOpSequence (functorMap f)).map (homOfLE (by omega : n ≤ n+1)).op ≫ Pi.π _ n ≫
65+
eqToHom (functorObj_eq_neg (by omega : ¬(n < n))) =
66+
(Pi.π (fun i ↦ if _ : i < (n + 1) then M i else N i) n) ≫
67+
eqToHom (functorObj_eq_pos (by omega)) ≫ f n := by
68+
simp [functorMap]
69+
70+
lemma functorMap_commSq_aux {n m k : ℕ} (h : n ≤ m) (hh : ¬(k < m)) :
71+
(Functor.ofOpSequence (functorMap f)).map (homOfLE h).op ≫ Pi.π _ k ≫
72+
eqToHom (functorObj_eq_neg (by omega : ¬(k < n))) =
73+
(Pi.π (fun i ↦ if _ : i < m then M i else N i) k) ≫
74+
eqToHom (functorObj_eq_neg hh) := by
75+
induction' h using Nat.leRec with m h ih
76+
· simp
77+
· specialize ih (by omega)
78+
have : homOfLE (by omega : n ≤ m + 1) =
79+
homOfLE (by omega : n ≤ m) ≫ homOfLE (by omega : m ≤ m + 1) := by simp
80+
rw [this, op_comp, Functor.map_comp]
81+
slice_lhs 2 4 => rw [ih]
82+
simp only [Functor.ofOpSequence_obj, homOfLE_leOfHom, Functor.ofOpSequence_map_homOfLE_succ,
83+
functorMap, dite_eq_ite, limMap_π_assoc, Discrete.functor_obj_eq_as, Discrete.natTrans_app]
84+
split_ifs
85+
simp [dif_neg (by omega : ¬(k < m))]
86+
87+
lemma functorMap_commSq {n m : ℕ} (h : ¬(m < n)) :
88+
(Functor.ofOpSequence (functorMap f)).map (homOfLE (by omega : n ≤ m + 1)).op ≫ Pi.π _ m ≫
89+
eqToHom (functorObj_eq_neg (by omega : ¬(m < n))) =
90+
(Pi.π (fun i ↦ if _ : i < m + 1 then M i else N i) m) ≫
91+
eqToHom (functorObj_eq_pos (by omega)) ≫ f m := by
92+
cases m with
93+
| zero =>
94+
have : n = 0 := by omega
95+
subst this
96+
simp [functorMap]
97+
| succ m =>
98+
rw [← functorMap_commSq_succ f (m + 1)]
99+
simp only [Functor.ofOpSequence_obj, homOfLE_leOfHom, dite_eq_ite,
100+
Functor.ofOpSequence_map_homOfLE_succ, add_le_iff_nonpos_right, nonpos_iff_eq_zero,
101+
one_ne_zero]
102+
have : homOfLE (by omega : n ≤ m + 1 + 1) =
103+
homOfLE (by omega : n ≤ m + 1) ≫ homOfLE (by omega : m + 1 ≤ m + 1 + 1) := by simp
104+
rw [this, op_comp, Functor.map_comp]
105+
simp only [Functor.ofOpSequence_obj, homOfLE_leOfHom, Functor.ofOpSequence_map_homOfLE_succ,
106+
Category.assoc, add_le_iff_nonpos_right, nonpos_iff_eq_zero, one_ne_zero]
107+
congr 1
108+
exact functorMap_commSq_aux f (by omega) (by omega)
109+
110+
/--
111+
The cone over the tower
112+
```
113+
⋯ → ∏_{n < m} M n × ∏_{n ≥ m} N n → ⋯ → ∏ N
114+
```
115+
with cone point `∏ M`. This is a limit cone, see `CategoryTheory.Limits.SequentialProduct.isLimit`.
116+
-/
117+
noncomputable def cone : Cone (Functor.ofOpSequence (functorMap f)) where
118+
pt := ∏ᶜ M
119+
π := by
120+
refine NatTrans.ofOpSequence
121+
(fun n ↦ Limits.Pi.map fun m ↦ if h : m < n then eqToHom (functorObj_eq_pos h).symm else
122+
f m ≫ eqToHom (functorObj_eq_neg h).symm) (fun n ↦ ?_)
123+
apply Limits.Pi.hom_ext
124+
intro m
125+
simp only [Functor.const_obj_obj, Functor.ofOpSequence_obj, homOfLE_leOfHom,
126+
Functor.const_obj_map, Category.id_comp, limMap_π, Discrete.functor_obj_eq_as,
127+
Discrete.natTrans_app, Functor.ofOpSequence_map_homOfLE_succ, functorMap, Category.assoc,
128+
limMap_π_assoc]
129+
split
130+
· simp [dif_pos (by omega : m < n + 1)]
131+
· split
132+
all_goals simp
133+
134+
lemma cone_π_app (n : ℕ) : (cone f).π.app ⟨n⟩ =
135+
Limits.Pi.map fun m ↦ if h : m < n then eqToHom (functorObj_eq_pos h).symm else
136+
f m ≫ eqToHom (functorObj_eq_neg h).symm := rfl
137+
138+
@[reassoc]
139+
lemma cone_π_app_comp_Pi_π_pos (m n : ℕ) (h : n < m) : (cone f).π.app ⟨m⟩ ≫
140+
Pi.π (fun i ↦ if _ : i < m then M i else N i) n =
141+
Pi.π _ n ≫ eqToHom (functorObj_eq_pos h).symm := by
142+
simp only [Functor.const_obj_obj, dite_eq_ite, Functor.ofOpSequence_obj, cone_π_app, limMap_π,
143+
Discrete.functor_obj_eq_as, Discrete.natTrans_app]
144+
rw [dif_pos h]
145+
146+
@[reassoc]
147+
lemma cone_π_app_comp_Pi_π_neg (m n : ℕ) (h : ¬(n < m)) : (cone f).π.app ⟨m⟩ ≫ Pi.π _ n =
148+
Pi.π _ n ≫ f n ≫ eqToHom (functorObj_eq_neg h).symm := by
149+
simp only [Functor.const_obj_obj, dite_eq_ite, Functor.ofOpSequence_obj, cone_π_app, limMap_π,
150+
Discrete.functor_obj_eq_as, Discrete.natTrans_app]
151+
rw [dif_neg h]
152+
153+
/--
154+
The cone over the tower
155+
```
156+
⋯ → ∏_{n < m} M n × ∏_{n ≥ m} N n → ⋯ → ∏ N
157+
```
158+
with cone point `∏ M` is indeed a limit cone.
159+
-/
160+
noncomputable def isLimit : IsLimit (cone f) where
161+
lift s := Pi.lift fun m ↦
162+
s.π.app ⟨m + 1⟩ ≫ Pi.π (fun i ↦ if _ : i < m + 1 then M i else N i) m ≫
163+
eqToHom (dif_pos (by omega : m < m + 1))
164+
fac s := by
165+
intro ⟨n⟩
166+
apply Pi.hom_ext
167+
intro m
168+
by_cases h : m < n
169+
· simp only [le_refl, Category.assoc, cone_π_app_comp_Pi_π_pos f _ _ h]
170+
simp only [dite_eq_ite, Functor.ofOpSequence_obj, le_refl, limit.lift_π_assoc, Fan.mk_pt,
171+
Discrete.functor_obj_eq_as, Fan.mk_π_app, Category.assoc, eqToHom_trans]
172+
have hh : m + 1 ≤ n := by omega
173+
rw [← s.w (homOfLE hh).op]
174+
simp only [Functor.const_obj_obj, Functor.ofOpSequence_obj, homOfLE_leOfHom, le_refl,
175+
Category.assoc]
176+
congr
177+
induction' hh using Nat.leRec with n hh ih
178+
· simp
179+
· have : homOfLE (Nat.le_succ_of_le hh) = homOfLE hh ≫ homOfLE (Nat.le_succ n) := by simp
180+
rw [this, op_comp, Functor.map_comp]
181+
simp only [Functor.ofOpSequence_obj, Nat.succ_eq_add_one, homOfLE_leOfHom,
182+
Functor.ofOpSequence_map_homOfLE_succ, le_refl, Category.assoc]
183+
have h₁ : (if _ : m < m + 1 then M m else N m) = if _ : m < n then M m else N m := by
184+
rw [dif_pos (by omega), dif_pos (by omega)]
185+
have h₂ : (if _ : m < n then M m else N m) = if _ : m < n + 1 then M m else N m := by
186+
rw [dif_pos h, dif_pos (by omega)]
187+
rw [← eqToHom_trans h₁ h₂]
188+
slice_lhs 2 4 => rw [ih (by omega)]
189+
simp only [functorMap, dite_eq_ite, Pi.π, limMap_π_assoc, Discrete.functor_obj_eq_as,
190+
Discrete.natTrans_app]
191+
split_ifs
192+
rw [dif_pos (by omega)]
193+
simp
194+
· simp only [le_refl, Category.assoc]
195+
rw [cone_π_app_comp_Pi_π_neg f _ _ h]
196+
simp only [dite_eq_ite, Functor.ofOpSequence_obj, le_refl, limit.lift_π_assoc, Fan.mk_pt,
197+
Discrete.functor_obj_eq_as, Fan.mk_π_app, Category.assoc]
198+
slice_lhs 2 4 => erw [← functorMap_commSq f h]
199+
simp
200+
uniq s m h := by
201+
apply Pi.hom_ext
202+
intro n
203+
simp only [Functor.ofOpSequence_obj, le_refl, dite_eq_ite, limit.lift_π, Fan.mk_pt,
204+
Fan.mk_π_app, ← h ⟨n + 1⟩, Category.assoc]
205+
slice_rhs 2 3 => erw [cone_π_app_comp_Pi_π_pos f (n + 1) _ (by omega)]
206+
simp
207+
208+
section
209+
210+
variable [HasZeroMorphisms C] [HasFiniteBiproducts C] [HasCountableProducts C] [∀ n, Epi (f n)]
211+
212+
attribute [local instance] hasBinaryBiproducts_of_finite_biproducts
213+
214+
lemma functorMap_epi (n : ℕ) : Epi (functorMap f n) := by
215+
rw [functorMap, Pi.map_eq_prod_map (P := fun m : ℕ ↦ m < n + 1)]
216+
apply ( config := { allowSynthFailures := true } ) epi_comp
217+
apply ( config := { allowSynthFailures := true } ) epi_comp
218+
apply ( config := { allowSynthFailures := true } ) prod.map_epi
219+
· apply ( config := { allowSynthFailures := true } ) Pi.map_epi
220+
intro ⟨_, _⟩
221+
split
222+
all_goals infer_instance
223+
· apply ( config := { allowSynthFailures := true } ) IsIso.epi_of_iso
224+
apply ( config := { allowSynthFailures := true } ) Pi.map_isIso
225+
intro ⟨_, _⟩
226+
split
227+
all_goals infer_instance
228+
end
229+
230+
end CategoryTheory.Limits.SequentialProduct

‎Mathlib/Condensed/Light/AB.lean‎

Lines changed: 30 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,30 @@
1+
/-
2+
Copyright (c) 2024 Dagur Asgeirsson. All rights reserved.
3+
Released under Apache 2.0 license as described in the file LICENSE.
4+
Authors: Dagur Asgeirsson
5+
-/
6+
import Mathlib.CategoryTheory.Abelian.GrothendieckAxioms
7+
import Mathlib.Condensed.Light.Epi
8+
import Mathlib.Condensed.Light.Limits
9+
/-!
10+
11+
# Grothendieck's AB axioms for light condensed modules
12+
13+
The category of light condensed `R`-modules over a ring satisfies the countable version of
14+
Grothendieck's AB4* axiom
15+
-/
16+
universe u
17+
18+
open CategoryTheory Limits
19+
20+
namespace LightCondensed
21+
22+
variable {R : Type u} [Ring R]
23+
24+
attribute [local instance] Abelian.hasFiniteBiproducts
25+
26+
noncomputable instance : CountableAB4Star (LightCondMod.{u} R) :=
27+
have := hasExactLimitsOfShape_of_preservesEpi (LightCondMod R) (Discrete ℕ)
28+
CountableAB4Star.of_hasExactLimitsOfShape_nat _
29+
30+
end LightCondensed

‎Mathlib/Condensed/Light/Epi.lean‎

Lines changed: 36 additions & 3 deletions
Original file line numberDiff line numberDiff line change
@@ -3,17 +3,18 @@ Copyright (c) 2024 Dagur Asgeirsson. All rights reserved.
33
Released under Apache 2.0 license as described in the file LICENSE.
44
Authors: Dagur Asgeirsson
55
-/
6-
import Mathlib.CategoryTheory.ConcreteCategory.EpiMono
7-
import Mathlib.CategoryTheory.Sites.EpiMono
6+
import Mathlib.CategoryTheory.Limits.Shapes.SequentialProduct
87
import Mathlib.CategoryTheory.Sites.Coherent.SequentialLimit
9-
import Mathlib.Condensed.Light.Module
8+
import Mathlib.Condensed.Light.Limits
109
/-!
1110
1211
# Epimorphisms of light condensed objects
1312
1413
This file characterises epimorphisms in light condensed sets and modules as the locally surjective
1514
morphisms. Here, the condition of locally surjective is phrased in terms of continuous surjections
1615
of light profinite sets.
16+
17+
Further, we prove that the functor `lim : Discrete ℕ ⥤ LightCondMod R` preserves epimorphisms.
1718
-/
1819

1920
universe v u w u' v'
@@ -93,3 +94,35 @@ lemma epi_π_app_zero_of_epi : Epi (c.π.app ⟨0⟩) := by
9394
· exact fun _ ↦ (forget R).map_epi _
9495

9596
end LightCondensed
97+
98+
open CategoryTheory.Limits.SequentialProduct
99+
100+
namespace LightCondensed
101+
102+
variable (n : ℕ)
103+
104+
attribute [local instance] functorMap_epi Abelian.hasFiniteBiproducts
105+
106+
variable {R : Type u} [Ring R] {M N : ℕ → LightCondMod.{u} R} (f : ∀ n, M n ⟶ N n) [∀ n, Epi (f n)]
107+
108+
instance : Epi (Limits.Pi.map f) := by
109+
have : Limits.Pi.map f = (cone f).π.app ⟨0⟩ := rfl
110+
rw [this]
111+
exact epi_π_app_zero_of_epi R (isLimit f) (fun n ↦ by simp; infer_instance)
112+
113+
instance : (lim (J := Discrete ℕ) (C := LightCondMod R)).PreservesEpimorphisms where
114+
preserves f _ := by
115+
have : lim.map f = (Pi.isoLimit _).inv ≫ Limits.Pi.map (f.app ⟨·⟩) ≫ (Pi.isoLimit _).hom := by
116+
apply limit.hom_ext
117+
intro ⟨n⟩
118+
simp only [lim_obj, lim_map, limMap, IsLimit.map, limit.isLimit_lift, limit.lift_π,
119+
Cones.postcompose_obj_pt, limit.cone_x, Cones.postcompose_obj_π, NatTrans.comp_app,
120+
Functor.const_obj_obj, limit.cone_π, Pi.isoLimit, Limits.Pi.map, Category.assoc,
121+
limit.conePointUniqueUpToIso_hom_comp, Pi.cone_pt, Pi.cone_π, Discrete.natTrans_app,
122+
Discrete.functor_obj_eq_as]
123+
erw [IsLimit.conePointUniqueUpToIso_inv_comp_assoc]
124+
rfl
125+
rw [this]
126+
infer_instance
127+
128+
end LightCondensed

‎Mathlib/Condensed/Light/Limits.lean‎

Lines changed: 5 additions & 3 deletions
Original file line numberDiff line numberDiff line change
@@ -23,8 +23,10 @@ instance : HasFiniteLimits LightCondSet.{u} := hasFiniteLimits_of_hasLimitsOfSiz
2323

2424
variable (R : Type u) [Ring R]
2525

26-
instance : HasLimitsOfSize.{u, u} (LightCondMod.{u} R) := by
27-
change HasLimitsOfSize (Sheaf _ _)
28-
infer_instance
26+
instance : HasLimitsOfSize.{u, u} (LightCondMod.{u} R) :=
27+
inferInstanceAs (HasLimitsOfSize (Sheaf _ _))
28+
29+
instance : HasLimitsOfSize.{0, 0} (LightCondMod.{u} R) :=
30+
inferInstanceAs (HasLimitsOfSize (Sheaf _ _))
2931

3032
instance : HasFiniteLimits (LightCondMod.{u} R) := hasFiniteLimits_of_hasLimitsOfSize _

0 commit comments

Comments
 (0)