feat(Condensed/Solid): prove profiniteSolidification is iso at finite types

Proves three helper lemmas toward the TODO (hard) in Condensed/Solid.lean:

* profiniteSolidCounit_isIso: The counit of the profinite solidification is
  an isomorphism at every T : FintypeCat. Uses IsPointwiseRightKanExtension.isIso_hom.

* profiniteSolidification_comp_counit: The solidification composed with the counit
  equals the identity at FintypeCat objects. Uses liftOfIsRightKanExtension_fac_app.

* profiniteSolidification_isIso_at_fintype: The solidification map is an isomorphism
  at every object in the image of FintypeCat.toProfinite. Uses isIso_of_comp_hom_eq_id.

* profiniteSolid_isSolid_at_fintype: Partial result: IsSolid holds when the test
  object is in the image of FintypeCat.toProfinite.

* profiniteSolid_obj_isSolid: States the full result (with sorry). The remaining
  step is: limits of solid modules are solid, which follows from the adjunction
  solidification ⊣ inclusionOfSolidModules (not yet in Mathlib).

Imports Mathlib.Topology.Category.Profinite.AsLimit for the limit structure of
profinite spaces that will be needed for the general proof.

Author: thothrde

Mathlib/Condensed/Solid.lean

@@ -1,16 +1,14 @@
 /-
 Copyright (c) 2023 Dagur Asgeirsson. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
-Authors: Dagur Asgeirsson
+Authors: Dagur Asgeirsson, Thomas Riepe
 -/
 module
-
 public import Mathlib.CategoryTheory.Functor.KanExtension.Pointwise
 public import Mathlib.Condensed.Functors
 public import Mathlib.Condensed.Limits
-
+public import Mathlib.Topology.Category.Profinite.AsLimit
 /-!
-
 # Solid modules
 
 This file contains the definition of a solid `R`-module: `CondensedMod.isSolid R`. Solid modules
@@ -21,14 +19,20 @@ groups were introduced in [scholze2019condensed], Definition 5.1.
 * `CondensedMod.IsSolid R`: the predicate on condensed `R`-modules describing the property of
   being solid.
 
-TODO (hard): prove that `((profiniteSolid ℤ).obj S).IsSolid` for `S : Profinite`.
-TODO (slightly easier): prove that `((profiniteSolid 𝔽ₚ).obj S).IsSolid` for `S : Profinite`.
--/
+## Main theorems (new in this PR)
 
-@[expose] public section
+* `CondensedMod.profiniteSolidCounit_isIso`: the counit of the profinite solidification is
+  an isomorphism at every finite type.
+* `CondensedMod.profiniteSolidification_isIso_at_fintype`: the solidification map is an
+  isomorphism at every object in the image of `FintypeCat.toProfinite`.
+* `CondensedMod.profiniteSolid_isSolid_at_fintype`: `((profiniteSolid R).obj S).IsSolid`
+  when tested against objects in the image of `FintypeCat.toProfinite`.
+* `CondensedMod.profiniteSolid_obj_isSolid`: `((profiniteSolid ℤ).obj S).IsSolid`
+  for `S : Profinite`. (TODO: remove sorry)
 
+-/
+@[expose] public section
 universe u
-
 variable (R : Type (u + 1)) [Ring R]
 
 open CategoryTheory Limits Profinite Condensed
@@ -74,7 +78,6 @@ end Condensed
 
 /--
 The predicate on condensed `R`-modules describing the property of being solid.
-
 TODO: This is not the correct definition of solid `R`-modules for a general `R`. The correct one is
 as follows: Use this to define solid modules over a finite type `ℤ`-algebra `R`. In particular this
 gives a definition of solid modules over `ℤ[X]` (polynomials in one variable). Then a solid
@@ -83,4 +86,84 @@ homomorphism `ℤ[X] → R` such that `X` maps to `r`, the underlying `ℤ[X]`-m
 -/
 class CondensedMod.IsSolid (A : CondensedMod.{u} R) : Prop where
   isIso_solidification_map : ∀ X : Profinite.{u}, IsIso ((yoneda.obj A).map
-    ((profiniteSolidification R).app X).op)
+    ((Condensed.profiniteSolidification R).app X).op)
+
+namespace CondensedMod
+
+open CategoryTheory Limits Profinite Condensed Functor
+
+/-! ### Profiniteness of the solidification -/
+
+/-- The counit of the profinite solidification is an isomorphism at every `T : FintypeCat`.
+This uses the fact that `profiniteSolidIsPointwiseRightKanExtension` holds and that
+`FintypeCat.toProfinite` is fully faithful. -/
+lemma profiniteSolidCounit_isIso (T : FintypeCat.{u}) :
+    IsIso ((profiniteSolidCounit R).app T) := by
+  haveI : IsIso (profiniteSolidCounit R) :=
+    (profiniteSolidIsPointwiseRightKanExtension R).isIso_hom
+  infer_instance
+
+/-- The solidification map `profiniteSolidification R` composed with the counit equals the
+identity, at every `T : FintypeCat`. This is the naturality condition from
+`liftOfIsRightKanExtension_fac_app`. -/
+lemma profiniteSolidification_comp_counit (T : FintypeCat.{u}) :
+    (profiniteSolidification R).app (FintypeCat.toProfinite.obj T) ≫
+    (profiniteSolidCounit R).app T = 𝟙 _ := by
+  have h := (profiniteSolid R).liftOfIsRightKanExtension_fac_app
+              (profiniteSolidCounit R) (profiniteFree R) (𝟙 _) T
+  simp only [profiniteSolidification]
+  exact h
+
+/-- The solidification map `profiniteSolidification R` is an isomorphism at every object in
+the image of `FintypeCat.toProfinite`. This follows from `profiniteSolidCounit_isIso` and
+`profiniteSolidification_comp_counit` via `isIso_of_comp_hom_eq_id`. -/
+lemma profiniteSolidification_isIso_at_fintype (T : FintypeCat.{u}) :
+    IsIso ((profiniteSolidification R).app (FintypeCat.toProfinite.obj T)) := by
+  haveI := profiniteSolidCounit_isIso R T
+  exact isIso_of_comp_hom_eq_id ((profiniteSolidCounit R).app T)
+          (profiniteSolidification_comp_counit R T)
+
+/-! ### Solidness of `profiniteSolid R` -/
+
+/-- `((profiniteSolid R).obj S).IsSolid` when the test object `X` is in the image of
+`FintypeCat.toProfinite`. The proof uses that `profiniteSolidification_isIso_at_fintype`
+makes the solidification map itself an isomorphism at finite objects, and then functoriality
+of `yoneda` gives the required isomorphism on hom-sets. -/
+theorem profiniteSolid_isSolid_at_fintype
+    (S : Profinite.{u}) (T : FintypeCat.{u}) :
+    IsIso ((yoneda.obj ((profiniteSolid R).obj S)).map
+           ((profiniteSolidification R).app (FintypeCat.toProfinite.obj T)).op) := by
+  haveI : IsIso ((profiniteSolidification R).app (FintypeCat.toProfinite.obj T)) :=
+    profiniteSolidification_isIso_at_fintype R T
+  infer_instance
+
+/-- TODO: prove that `((profiniteSolid ℤ).obj S).IsSolid` for `S : Profinite`.
+The case when the test object is in the image of `FintypeCat.toProfinite` is already handled
+by `profiniteSolid_isSolid_at_fintype`. The general case requires showing that
+`X : Profinite` can be expressed as a cofiltered limit of its finite discrete quotients
+(which is available via `X.asLimit`) and that the solid module condition is preserved under
+such limits. This in turn follows from the adjunction between the solidification functor
+and the inclusion of solid modules, which has not yet been formalized in Mathlib.
+
+Proof sketch for the general case (using `X.asLimit`):
+- `X ≅ lim_{S : DiscreteQuotient X} (FintypeCat.toProfinite.obj (X.fintypeDiagram.obj S))`
+- `(profiniteSolid R).obj S = limit_{T : StructuredArrow S L} (finFree R).obj T`
+  (from `profiniteSolidIsPointwiseRightKanExtension`)
+- For surjectivity: given `h : freeX → A`, for each finite component `T`:
+  `h ≫ proj_T : freeX → finFree T`, which lifts to `solidX → finFree T`
+  using `profiniteSolid_isSolid_at_fintype` at the finite T.
+  These lifts are compatible (by uniqueness) and yield a lift `solidX → A`.
+- For injectivity: use `IsLimit.hom_ext` for the limit structure of `A`.
+-/
+theorem profiniteSolid_obj_isSolid (S : Profinite.{u}) :
+    ((profiniteSolid R).obj S).IsSolid :=
+  { isIso_solidification_map := fun X => by
+      -- The case X = FintypeCat.toProfinite.obj T is handled:
+      -- haveI := profiniteSolid_isSolid_at_fintype R S T; infer_instance
+      --
+      -- For general X, we use X.asLimit (Profinite/AsLimit.lean):
+      -- X is the limit of its finite discrete quotients X.fintypeDiagram.
+      -- The proof proceeds by showing bijectivity using this limit structure.
+      sorry }
+
+end CondensedMod