move stuff

LeanCondensed/Projects/InternallyProjective.lean

@@ -3,29 +3,18 @@ Copyright (c) 2024 Dagur Asgeirsson. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Dagur Asgeirsson
 -/
-import Mathlib.Algebra.Category.ModuleCat.Monoidal.Basic
 import Mathlib.CategoryTheory.Closed.Monoidal
-import Mathlib.CategoryTheory.Monoidal.FunctorCategory
-import Mathlib.CategoryTheory.Preadditive.Injective
-import Mathlib.CategoryTheory.Preadditive.Projective
-import Mathlib.Condensed.Light.Functors
-import Mathlib.Condensed.Light.Module
-import Mathlib.Topology.Category.LightProfinite.Sequence
-import LeanCondensed.Mathlib.Condensed.Light.Limits
-import LeanCondensed.LightCondensed.Yoneda
 /-!
 
-# Project: prove that `ℤ[ℕ∪{∞}]` is internally projective in light condensed abelian groups
+# Project: prove that `ℤ[ℕ∪{∞}]` is internally projective in light condensed abelian groups
 
 -/
 
 noncomputable section
 
 universe u
 
-open CategoryTheory LightProfinite MonoidalCategory OnePoint Limits LightCondensed
-
-attribute [local instance] ConcreteCategory.instFunLike
+open CategoryTheory MonoidalCategory Limits
 
 section InternallyProjective
 
@@ -35,83 +24,3 @@ class InternallyProjective (P : C) : Prop where
   preserves_epi : (ihom P).PreservesEpimorphisms
 
 end InternallyProjective
-
-section MonoidalClosed
-
-variable (R : Type u) [CommRing R] -- might need some more assumptions
-
-/- This is the monoidal structure on localized categories. -/
-instance : MonoidalCategory (LightCondMod.{u} R) := sorry
-
-instance : MonoidalPreadditive (LightCondMod.{u} R) := sorry
-
-instance : SymmetricCategory (LightCondMod.{u} R) := sorry
-
-/- Constructed using Day's reflection theorem. -/
-instance : MonoidalClosed (LightCondMod.{u} R) := sorry
-
-variable (A : LightCondMod R) (S : LightProfinite)
-
-def ihom_points (A B : LightCondMod.{u} R) (S : LightProfinite) :
-    ((ihom A).obj B).val.obj ⟨S⟩ ≃ ((A ⊗ ((free R).obj S.toCondensed)) ⟶ B) := sorry
--- We should have an `R`-module structure on `M ⟶ N` for condensed `R`-modules `M`, `N`,
--- then this could be made an `≅`.
--- But it's probably not needed in this proof.
--- This equivalence follows from the adjunction.
--- This probably needs some naturality lemmas
-
-def tensorFreeIso (X Y : LightCondSet.{u}) :
-    (free R).obj X ⊗ (free R).obj Y ≅ (free R).obj (X ⨯ Y) := sorry
-
-def tensorFreeIso' (S T : LightProfinite) :
-    (free R).obj S.toCondensed ⊗ (free R).obj T.toCondensed ≅
-      (free R).obj (S ⨯ T).toCondensed := tensorFreeIso R S.toCondensed T.toCondensed ≪≫
-        (free R).mapIso (Limits.PreservesLimitPair.iso lightProfiniteToLightCondSet _ _).symm
-
-instance (A : LightCondMod R) : PreservesColimits (tensorRight A) := sorry
-
-def tensorCokerIso {A B C : LightCondMod R} (f : A ⟶ B) : cokernel f ⊗ C ≅ cokernel (f ▷ C) :=
-  preservesColimitIso (tensorRight C) _ ≪≫
-    HasColimit.isoOfNatIso (parallelPair.ext (Iso.refl _) (Iso.refl _) rfl (by simp))
-
-end MonoidalClosed
-
-namespace LightProfinite
-
-instance (S : LightProfinite.{u}) : Injective S := sorry
-
-end LightProfinite
-
-namespace LightCondensed
-
-variable (R : Type _) [CommRing R] -- might need some more assumptions
-
-lemma internallyProjective_iff_tensor_condition (P : LightCondMod R) : InternallyProjective P ↔
-    ∀ {A B : LightCondMod R} (e : A ⟶ B) [Epi e],
-      (∀ (S : LightProfinite) (g : P ⊗ (free R).obj S.toCondensed ⟶ B), ∃ (S' : LightProfinite)
-        (π : S' ⟶ S) (_ : Function.Surjective π) (g' : P ⊗ (free R).obj S'.toCondensed ⟶ A),
-          (P ◁ ((lightProfiniteToLightCondSet ⋙ free R).map π)) ≫ g = g' ≫ e) := sorry
--- It's the ← direction that's important in this proof
--- The proof of this should be completely formal, using the characterisation of epimorphisms in
--- light condensed abelian groups as locally surjective maps
--- (see the file `Epi/LightCondensed.lean`), and `ihom_points` above (together with some ).
-
-def P_map :
-    (free R).obj (LightProfinite.of PUnit.{1}).toCondensed ⟶ (free R).obj (ℕ∪{∞}).toCondensed :=
-  (lightProfiniteToLightCondSet ⋙ free R).map (⟨fun _ ↦ ∞, continuous_const⟩)
-
-def P : LightCondMod R := cokernel (P_map R)
-
-def P_proj : (free R).obj (ℕ∪{∞}).toCondensed ⟶ P R := cokernel.π _
-
-def P_homMk (A : LightCondMod R) (f : (free R).obj (ℕ∪{∞}).toCondensed ⟶ A)
-    (hf : P_map R ≫ f = 0) : P R ⟶ A := cokernel.desc _ f hf
-
-instance : InternallyProjective (P R) := by
-  rw [internallyProjective_iff_tensor_condition]
-  intro A B e he S g
-  sorry
-
-instance : InternallyProjective ((free R).obj (ℕ∪{∞}).toCondensed) := sorry
-
-end LightCondensed

LeanCondensed/Projects/LightSolid.lean

@@ -3,30 +3,69 @@ Copyright (c) 2024 Dagur Asgeirsson. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Dagur Asgeirsson
 -/
+import Mathlib.CategoryTheory.Preadditive.Injective
 import Mathlib.Condensed.Discrete.Basic
+import Mathlib.Topology.Category.LightProfinite.Sequence
+import LeanCondensed.Mathlib.Condensed.Light.Limits
 import LeanCondensed.Projects.InternallyProjective
 /-!
 
 # Project: light solid abelian groups
 
-* Define the condensed abelian group / module called `P`. This is `ℤ[ℕ∪{∞}]/(∞)`, the light
-  condensed abelian group "classifying null sequences".
-
-* Define `shift : P ⟶ P`.
-
-* Define the property of a light condensed abelian group `A` of being solid as the fact that the
-  natural map of internal homs from `P` to `A` induced by `1 - shift` is an iso.
-
 -/
 noncomputable section
 
 universe u
 
-open CategoryTheory LightProfinite OnePoint Limits MonoidalClosed
+open CategoryTheory LightProfinite OnePoint Limits LightCondensed MonoidalCategory MonoidalClosed
 
-namespace LightCondensed
+attribute [local instance] ConcreteCategory.instFunLike
+
+section MonoidalClosed
+
+variable (R : Type u) [CommRing R] -- might need some more assumptions
+
+/- This is the monoidal structure on localized categories. -/
+instance : MonoidalCategory (LightCondMod.{u} R) := sorry
+
+instance : MonoidalPreadditive (LightCondMod.{u} R) := sorry
+
+instance : SymmetricCategory (LightCondMod.{u} R) := sorry
+
+/- Constructed using Day's reflection theorem. -/
+instance : MonoidalClosed (LightCondMod.{u} R) := sorry
+
+variable (A : LightCondMod R) (S : LightProfinite)
+
+def ihom_points (A B : LightCondMod.{u} R) (S : LightProfinite) :
+    ((ihom A).obj B).val.obj ⟨S⟩ ≃ ((A ⊗ ((free R).obj S.toCondensed)) ⟶ B) := sorry
+-- We should have an `R`-module structure on `M ⟶ N` for condensed `R`-modules `M`, `N`,
+-- then this could be made an `≅`.
+-- But it's probably not needed in this proof.
+-- This equivalence follows from the adjunction.
+-- This probably needs some naturality lemmas
+
+def tensorFreeIso (X Y : LightCondSet.{u}) :
+    (free R).obj X ⊗ (free R).obj Y ≅ (free R).obj (X ⨯ Y) := sorry
+
+def tensorFreeIso' (S T : LightProfinite) :
+    (free R).obj S.toCondensed ⊗ (free R).obj T.toCondensed ≅
+      (free R).obj (S ⨯ T).toCondensed := tensorFreeIso R S.toCondensed T.toCondensed ≪≫
+        (free R).mapIso (Limits.PreservesLimitPair.iso lightProfiniteToLightCondSet _ _).symm
+
+instance (A : LightCondMod R) : PreservesColimits (tensorRight A) := sorry
+
+def tensorCokerIso {A B C : LightCondMod R} (f : A ⟶ B) : cokernel f ⊗ C ≅ cokernel (f ▷ C) :=
+  preservesColimitIso (tensorRight C) _ ≪≫
+    HasColimit.isoOfNatIso (parallelPair.ext (Iso.refl _) (Iso.refl _) rfl (by simp))
 
-def _root_.LightProfinite.shift : ℕ∪{∞} ⟶ ℕ∪{∞} where
+end MonoidalClosed
+
+namespace LightProfinite
+
+instance (S : LightProfinite.{u}) : Injective S := sorry
+
+def shift : ℕ∪{∞} ⟶ ℕ∪{∞} where
   toFun
     | ∞ => ∞
     | OnePoint.some n => (n + 1 : ℕ)
@@ -37,6 +76,40 @@ def _root_.LightProfinite.shift : ℕ∪{∞} ⟶ ℕ∪{∞} where
     refine ⟨sSup (Option.some ⁻¹' U)ᶜ + 1, fun n hn ↦ by
       simpa using not_mem_of_csSup_lt (Nat.succ_le_iff.mp hn) (Set.Finite.bddAbove hU)⟩
 
+end LightProfinite
+
+namespace LightCondensed
+
+variable (R : Type _) [CommRing R] -- might need some more assumptions
+
+lemma internallyProjective_iff_tensor_condition (P : LightCondMod R) : InternallyProjective P ↔
+    ∀ {A B : LightCondMod R} (e : A ⟶ B) [Epi e],
+      (∀ (S : LightProfinite) (g : P ⊗ (free R).obj S.toCondensed ⟶ B), ∃ (S' : LightProfinite)
+        (π : S' ⟶ S) (_ : Function.Surjective π) (g' : P ⊗ (free R).obj S'.toCondensed ⟶ A),
+          (P ◁ ((lightProfiniteToLightCondSet ⋙ free R).map π)) ≫ g = g' ≫ e) := sorry
+-- It's the ← direction that's important in this proof
+-- The proof of this should be completely formal, using the characterisation of epimorphisms in
+-- light condensed abelian groups as locally surjective maps
+-- (see the file `Epi/LightCondensed.lean`), and `ihom_points` above (together with some ).
+
+def P_map :
+    (free R).obj (LightProfinite.of PUnit.{1}).toCondensed ⟶ (free R).obj (ℕ∪{∞}).toCondensed :=
+  (lightProfiniteToLightCondSet ⋙ free R).map (⟨fun _ ↦ ∞, continuous_const⟩)
+
+def P : LightCondMod R := cokernel (P_map R)
+
+def P_proj : (free R).obj (ℕ∪{∞}).toCondensed ⟶ P R := cokernel.π _
+
+def P_homMk (A : LightCondMod R) (f : (free R).obj (ℕ∪{∞}).toCondensed ⟶ A)
+    (hf : P_map R ≫ f = 0) : P R ⟶ A := cokernel.desc _ f hf
+
+instance : InternallyProjective (P R) := by
+  rw [internallyProjective_iff_tensor_condition]
+  intro A B e he S g
+  sorry
+
+instance : InternallyProjective ((free R).obj (ℕ∪{∞}).toCondensed) := sorry
+
 variable (R : Type) [CommRing R]
 
 example : Abelian (LightCondMod R) := by infer_instance
@@ -55,13 +128,12 @@ abbrev induced_from_one_minus_shift (A : LightCondMod R) :
     ((ihom (P R)).obj A) ⟶ ((ihom (P R)).obj A) :=
   (pre (one_minus_shift R)).app A
 
-variable {R}
+variable {R : Type} [CommRing R]
 
 class IsSolid (A : LightCondMod R) : Prop where
   one_minus_shift_induces_iso : IsIso ((pre (one_minus_shift R)).app A)
 
-variable (R) in
-structure Solid where
+structure Solid (R : Type) [CommRing R] where
   toLightCondMod : LightCondMod R
   [isSolid : IsSolid toLightCondMod]
 
@@ -76,20 +148,18 @@ instance : IsSolid ((discrete (ModuleCat R)).obj (ModuleCat.of R R)) := sorry
 
 instance : Inhabited (Solid R) := ⟨Solid.of ((discrete (ModuleCat R)).obj (ModuleCat.of R R))⟩
 
-variable (R) in
 @[simps!]
-def solidToCondensed : Solid R ⥤ LightCondMod R :=
+def solidToCondensed (R : Type) [CommRing R] : Solid R ⥤ LightCondMod R :=
   inducedFunctor _
 
-variable (R) in
-def solidification : LightCondMod R ⥤ Solid R := sorry
+def solidification  (R : Type) [CommRing R] : LightCondMod R ⥤ Solid R := sorry
 
 def _root_.LightCondMod.solidify (A : LightCondMod R) : Solid R := (solidification R).obj A
 
 def val (A : Solid R) : LightCondMod R := A.toLightCondMod -- maybe unnecessary, `A.1` is fine.
 
-variable (R) in
-def solidificationAdjunction : solidification R ⊣ solidToCondensed R := sorry
+def solidificationAdjunction (R : Type) [CommRing R] : solidification R ⊣ solidToCondensed R :=
+  sorry
 
 instance : (solidification R).IsLeftAdjoint := (solidificationAdjunction R).isLeftAdjoint