From 154a87cdc796f476922d458f987f6f4d1709ed8c Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Dagur=20T=C3=B3mas=20=C3=81sgeirsson?= Date: Wed, 1 May 2024 09:30:34 +0000 Subject: [PATCH] =?UTF-8?q?refactor(Condensed):=20redefine=20condensed=20a?= =?UTF-8?q?belian=20groups=20as=20condensed=20`=E2=84=A4`-modules=20(#1251?= =?UTF-8?q?0)?= MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit --- Mathlib.lean | 2 -- Mathlib/Condensed/Abelian.lean | 27 ----------------- Mathlib/Condensed/Adjunctions.lean | 36 ---------------------- Mathlib/Condensed/Explicit.lean | 26 ++++++++-------- Mathlib/Condensed/Limits.lean | 8 +++-- Mathlib/Condensed/Module.lean | 48 ++++++++++++++++++++++++++++-- Mathlib/Condensed/Solid.lean | 38 ++++++++++++----------- 7 files changed, 84 insertions(+), 101 deletions(-) delete mode 100644 Mathlib/Condensed/Abelian.lean delete mode 100644 Mathlib/Condensed/Adjunctions.lean diff --git a/Mathlib.lean b/Mathlib.lean index 72a762ac51e13..a30fcebd21423 100644 --- a/Mathlib.lean +++ b/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 diff --git a/Mathlib/Condensed/Abelian.lean b/Mathlib/Condensed/Abelian.lean deleted file mode 100644 index 80d5b2112e7ba..0000000000000 --- a/Mathlib/Condensed/Abelian.lean +++ /dev/null @@ -1,27 +0,0 @@ -/- -Copyright (c) 2023 Adam Topaz. All rights reserved. -Released under Apache 2.0 license as described in the file LICENSE. -Authors: Adam Topaz --/ -import Mathlib.Algebra.Category.GroupCat.Abelian -import Mathlib.CategoryTheory.Sites.Abelian -import Mathlib.CategoryTheory.Sites.LeftExact -import Mathlib.Condensed.Basic - -/-! - -Condensed abelian groups form an abelian category. - --/ - -universe u - -open CategoryTheory - -/-- -The category of condensed abelian groups, defined as sheaves of abelian groups over -`CompHaus` with respect to the coherent Grothendieck topology. --/ -abbrev CondensedAb := Condensed.{u} AddCommGroupCat.{u+1} - -noncomputable instance CondensedAb.abelian : Abelian CondensedAb.{u} := sheafIsAbelian diff --git a/Mathlib/Condensed/Adjunctions.lean b/Mathlib/Condensed/Adjunctions.lean deleted file mode 100644 index 353c93d5ad0b5..0000000000000 --- a/Mathlib/Condensed/Adjunctions.lean +++ /dev/null @@ -1,36 +0,0 @@ -/- -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.Algebra.Category.GroupCat.Adjunctions -import Mathlib.CategoryTheory.Sites.Adjunction -import Mathlib.Condensed.Abelian - -/-! -# Adjunctions regarding categories of condensed objects - -This file shows that the forgetful functor from condensed abelian groups to condensed sets has a -left adjoint, called the free condensed abelian group on a condensed set. - -TODO (Dagur): -* Add free condensed modules over more general rings. --/ - -universe u - -open CategoryTheory - -/-- The forgetful functor from condensed abelian groups to condensed sets. -/ -def Condensed.abForget : CondensedAb ⥤ CondensedSet := sheafCompose _ (forget AddCommGroupCat) - -/-- -The left adjoint to the forgetful functor. The *free condensed abelian group* on a condensed set. --/ -noncomputable -def Condensed.freeAb : CondensedSet ⥤ CondensedAb := - Sheaf.composeAndSheafify _ AddCommGroupCat.free - -/-- The condensed version of the free-forgetful adjunction. -/ -noncomputable -def Condensed.setAbAdjunction : freeAb ⊣ abForget := Sheaf.adjunction _ AddCommGroupCat.adj diff --git a/Mathlib/Condensed/Explicit.lean b/Mathlib/Condensed/Explicit.lean index d99970a194677..501de361cae20 100644 --- a/Mathlib/Condensed/Explicit.lean +++ b/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 diff --git a/Mathlib/Condensed/Limits.lean b/Mathlib/Condensed/Limits.lean index e42040a90e65d..75002e62eb947 100644 --- a/Mathlib/Condensed/Limits.lean +++ b/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} _ diff --git a/Mathlib/Condensed/Module.lean b/Mathlib/Condensed/Module.lean index 6a1e555642ed7..6e40b41005b72 100644 --- a/Mathlib/Condensed/Module.lean +++ b/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 _ diff --git a/Mathlib/Condensed/Solid.lean b/Mathlib/Condensed/Solid.lean index 59ae0eb6533ec..5252b64cf912d 100644 --- a/Mathlib/Condensed/Solid.lean +++ b/Mathlib/Condensed/Solid.lean @@ -4,27 +4,29 @@ 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 @@ -32,24 +34,24 @@ 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)