refactor(Condensed): redefine condensed abelian groups as condensed `…

…ℤ`-modules (#12510)

Mathlib.lean

@@ -1670,8 +1670,6 @@ import Mathlib.Computability.RegularExpressions
 import Mathlib.Computability.TMComputable
 import Mathlib.Computability.TMToPartrec
 import Mathlib.Computability.TuringMachine
-import Mathlib.Condensed.Abelian
-import Mathlib.Condensed.Adjunctions
 import Mathlib.Condensed.Basic
 import Mathlib.Condensed.Discrete
 import Mathlib.Condensed.Equivalence

Mathlib/Condensed/Explicit.lean

@@ -5,7 +5,7 @@ Authors: Dagur Asgeirsson, Riccardo Brasca, Filippo A. E. Nuccio
 -/
 import Mathlib.CategoryTheory.Sites.Coherent.ExtensiveSheaves
 import Mathlib.CategoryTheory.Sites.Coherent.RegularSheaves
-import Mathlib.Condensed.Abelian
+import Mathlib.Condensed.Module
 import Mathlib.Condensed.Equivalence
 /-!
 
@@ -186,21 +186,23 @@ noncomputable instance (Y : Sheaf (coherentTopology Stonean.{u}) (Type (u+1))) :
 
 end CondensedSet
 
-namespace CondensedAb
+namespace CondensedMod
 
-/-- A `CondensedAb` version of `Condensed.ofSheafStonean`. -/
-noncomputable abbrev ofSheafStonean (F : Stonean.{u}ᵒᵖ ⥤ AddCommGroupCat.{u+1})
-    [PreservesFiniteProducts F] : CondensedAb :=
+variable (R : Type (u+1)) [Ring R]
+
+/-- A `CondensedMod` version of `Condensed.ofSheafStonean`. -/
+noncomputable abbrev ofSheafStonean (F : Stonean.{u}ᵒᵖ ⥤ ModuleCat.{u+1} R)
+    [PreservesFiniteProducts F] : CondensedMod R :=
   Condensed.ofSheafStonean (forget _) F
 
-/-- A `CondensedAb` version of `Condensed.ofSheafProfinite`. -/
-noncomputable abbrev ofSheafProfinite (F : Profinite.{u}ᵒᵖ ⥤ AddCommGroupCat.{u+1})
-    [PreservesFiniteProducts F] (hF : EqualizerCondition (F ⋙ forget _)) : CondensedAb :=
+/-- A `CondensedMod` version of `Condensed.ofSheafProfinite`. -/
+noncomputable abbrev ofSheafProfinite (F : Profinite.{u}ᵒᵖ ⥤ ModuleCat.{u+1} R)
+    [PreservesFiniteProducts F] (hF : EqualizerCondition (F ⋙ forget _)) : CondensedMod R :=
   Condensed.ofSheafProfinite (forget _) F hF
 
-/-- A `CondensedAb` version of `Condensed.ofSheafCompHaus`. -/
-noncomputable abbrev ofSheafCompHaus (F : CompHaus.{u}ᵒᵖ ⥤ AddCommGroupCat.{u+1})
-    [PreservesFiniteProducts F] (hF : EqualizerCondition (F ⋙ forget _)) : CondensedAb :=
+/-- A `CondensedMod` version of `Condensed.ofSheafCompHaus`. -/
+noncomputable abbrev ofSheafCompHaus (F : CompHaus.{u}ᵒᵖ ⥤ ModuleCat.{u+1} R)
+    [PreservesFiniteProducts F] (hF : EqualizerCondition (F ⋙ forget _)) : CondensedMod R :=
   Condensed.ofSheafCompHaus (forget _) F hF
 
-end CondensedAb
+end CondensedMod

Mathlib/Condensed/Limits.lean

@@ -3,7 +3,7 @@ Copyright (c) 2023 Dagur Asgeirsson. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Dagur Asgeirsson
 -/
-import Mathlib.Condensed.Abelian
+import Mathlib.Condensed.Module
 
 /-!
 
@@ -22,8 +22,10 @@ instance : HasLimits CondensedSet.{u} := by
 
 instance : HasLimitsOfSize.{u} CondensedSet.{u} := hasLimitsOfSizeShrink.{u, u+1, u+1, u} _
 
-instance : HasLimits CondensedAb.{u} := by
+variable (R : Type (u+1)) [Ring R]
+
+instance : HasLimits (CondensedMod.{u} R) := by
   change HasLimits (Sheaf _ _)
   infer_instance
 
-instance : HasLimitsOfSize.{u} CondensedAb.{u} := hasLimitsOfSizeShrink.{u, u+1, u+1, u} _
+instance : HasLimitsOfSize.{u} (CondensedMod.{u} R) := hasLimitsOfSizeShrink.{u, u+1, u+1, u} _

Mathlib/Condensed/Module.lean

@@ -6,23 +6,65 @@ Authors: Dagur Asgeirsson
 import Mathlib.Algebra.Category.ModuleCat.Abelian
 import Mathlib.Algebra.Category.ModuleCat.Colimits
 import Mathlib.Algebra.Category.ModuleCat.FilteredColimits
+import Mathlib.Algebra.Category.ModuleCat.Adjunctions
 import Mathlib.CategoryTheory.Sites.Abelian
+import Mathlib.CategoryTheory.Sites.Adjunction
 import Mathlib.CategoryTheory.Sites.LeftExact
 import Mathlib.Condensed.Basic
 /-!
 
-Condensed modules form an abelian category.
+# Condensed `R`-modules
 
+This files defines condensed modules over a ring `R`.
+
+## Main results
+
+* Condensed `R`-modules form an abelian category.
+
+* The forgetful functor from condensed `R`-modules to condensed sets has a left adjoint, sending a
+  condensed set to the corresponding *free* condensed `R`-module.
 -/
 
 universe u
 
 open CategoryTheory
 
+variable (R : Type (u+1)) [Ring R]
+
 /--
 The category of condensed `R`-modules, defined as sheaves of `R`-modules over
 `CompHaus` with respect to the coherent Grothendieck topology.
 -/
-abbrev CondensedMod (R : Type (u+1)) [Ring R] := Condensed.{u} (ModuleCat.{u+1} R)
+abbrev CondensedMod := Condensed.{u} (ModuleCat.{u+1} R)
+
+noncomputable instance : Abelian (CondensedMod.{u} R) := sheafIsAbelian
+
+/-- The forgetful functor from condensed `R`-modules to condensed sets. -/
+def Condensed.forget : CondensedMod R ⥤ CondensedSet := sheafCompose _ (CategoryTheory.forget _)
+
+/--
+The left adjoint to the forgetful functor. The *free condensed `R`-module* on a condensed set.
+-/
+noncomputable
+def Condensed.free : CondensedSet ⥤ CondensedMod R :=
+  Sheaf.composeAndSheafify _ (ModuleCat.free R)
+
+/-- The condensed version of the free-forgetful adjunction. -/
+noncomputable
+def Condensed.freeForgetAdjunction : free R ⊣ forget R := Sheaf.adjunction _ (ModuleCat.adj R)
+
+/--
+The category of condensed abelian groups is defined as condensed `ℤ`-modules.
+-/
+abbrev CondensedAb := CondensedMod.{u} (ULift ℤ)
+
+noncomputable example : Abelian CondensedAb.{u} := inferInstance
+
+/-- The forgetful functor from condensed abelian groups to condensed sets. -/
+abbrev Condensed.abForget : CondensedAb ⥤ CondensedSet := forget _
+
+/-- The free condensed abelian group on a condensed set. -/
+noncomputable abbrev Condensed.freeAb : CondensedSet ⥤ CondensedAb := free _
 
-noncomputable instance (R : Type (u+1)) [Ring R] : Abelian (CondensedMod.{u} R) := sheafIsAbelian
+/-- The free-forgetful adjunction for condensed abelian groups. -/
+noncomputable abbrev Condensed.setAbAdjunction : freeAb ⊣ abForget := freeForgetAdjunction _

Mathlib/Condensed/Solid.lean

@@ -4,52 +4,54 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Dagur Asgeirsson
 -/
 import Mathlib.CategoryTheory.Limits.KanExtension
-import Mathlib.Condensed.Adjunctions
 import Mathlib.Condensed.Functors
 import Mathlib.Condensed.Limits
 
 /-!
 
-# Solid abelian groups
+# Solid modules
 
-This file contains the definition of a solid abelian group: `CondensedAb.isSolid`. Solid abelian
+This file contains the definition of a solid `R`-module: `CondensedMod.isSolid R`. Solid modules
 groups were introduced in [scholze2019condensed], Definition 5.1.
 
 ## Main definition
 
-* `CondensedAb.IsSolid`: the predicate on condensed abelian groups describing the property of being
-  solid.
+* `CondensedMod.IsSolid R`: the predicate on condensed abelian groups describing the property of
+  being solid.
 
-TODO (hard): prove that `(profiniteSolid.obj S).IsSolid` for `S : Profinite`.
+TODO (hard): prove that `((profiniteSolid ℤ).obj S).IsSolid` for `S : Profinite`.
+TODO (slightly easier): prove that `((profiniteSolid 𝔽ₚ).obj S).IsSolid` for `S : Profinite`.
 -/
 
 universe u
 
+variable (R : Type (u+1)) [Ring R]
+
 open CategoryTheory Limits Profinite Condensed
 
 noncomputable section
 
 namespace Condensed
 
 /-- The free condensed abelian group on a finite set. -/
-abbrev finFree : FintypeCat.{u} ⥤ CondensedAb.{u} :=
-  FintypeCat.toProfinite ⋙ profiniteToCondensed ⋙ freeAb.{u}
+abbrev finFree : FintypeCat.{u} ⥤ CondensedMod.{u} R :=
+  FintypeCat.toProfinite ⋙ profiniteToCondensed ⋙ free R
 
 /-- The free condensed abelian group on a profinite space. -/
-abbrev profiniteFree : Profinite.{u} ⥤ CondensedAb.{u} :=
-  profiniteToCondensed ⋙ freeAb.{u}
+abbrev profiniteFree : Profinite.{u} ⥤ CondensedMod.{u} R :=
+  profiniteToCondensed ⋙ free R
 
-/-- The functor sending a profinite space `S` to the condensed abelian group `ℤ[S]^\solid`. -/
-def profiniteSolid : Profinite.{u} ⥤ CondensedAb.{u} :=
-  Ran.loc FintypeCat.toProfinite finFree
+/-- The functor sending a profinite space `S` to the condensed abelian group `R[S]^\solid`. -/
+def profiniteSolid : Profinite.{u} ⥤ CondensedMod.{u} R :=
+  Ran.loc FintypeCat.toProfinite (finFree R)
 
-/-- The natural transformation `ℤ[S] ⟶ ℤ[S]^\solid`. -/
-def profiniteSolidification : profiniteFree ⟶ profiniteSolid :=
-  (Ran.equiv FintypeCat.toProfinite finFree profiniteFree).symm (NatTrans.id _)
+/-- The natural transformation `R[S] ⟶ R[S]^\solid`. -/
+def profiniteSolidification : profiniteFree R ⟶ profiniteSolid.{u} R :=
+  (Ran.equiv FintypeCat.toProfinite (finFree R) (profiniteFree R)).symm (NatTrans.id _)
 
 end Condensed
 
 /-- The predicate on condensed abelian groups describing the property of being solid. -/
-class CondensedAb.IsSolid (A : CondensedAb.{u}) : Prop where
+class CondensedMod.IsSolid (A : CondensedMod.{u} R) : Prop where
   isIso_solidification_map : ∀ X : Profinite.{u}, IsIso ((yoneda.obj A).map
-    (profiniteSolidification.app X).op)
+    ((profiniteSolidification R).app X).op)