feat(Condensed/Solid): complete proof architecture for profiniteSolid_obj_isSolid

New theorems and lemmas:
- finFree_iso_solid: iso between profiniteSolid LT and finFree T
- sol_map_counit: solidification commutes with finite-level maps
- finFree_iso_solid_inv_eq_sol, iso_counit_sol: supporting lemmas
- isSolid_of_isLimit_gen: limits of solid modules are solid (fully proved)
- surj_factor: factorization lemma (sorry; proved in development branch)
- profiniteSolid_fintype_isSolid: IsSolid for finite types (surjectivity proved,
  injectivity sorry pending finFree_isCompact)
- finFree_isSolid: finFree T is solid (proved given profiniteSolid_fintype_isSolid)
- profiniteSolid_obj_isSolid: complete proof architecture (2 specific sorries remain)

Co-authored-by: Thomas Riepe <thomas.riepe@gmail.com>

Author: thothrde

Mathlib/Condensed/Solid.lean

@@ -4,6 +4,7 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Dagur Asgeirsson, Thomas Riepe
 -/
 module
+
 public import Mathlib.CategoryTheory.Functor.KanExtension.Pointwise
 public import Mathlib.Condensed.Functors
 public import Mathlib.Condensed.Limits
@@ -14,7 +15,7 @@ public import Mathlib.Topology.Category.Profinite.AsLimit
 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
+## Main definitions
 
 * `CondensedMod.IsSolid R`: the predicate on condensed `R`-modules describing the property of
   being solid.
@@ -27,12 +28,18 @@ groups were introduced in [scholze2019condensed], Definition 5.1.
   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)
-
+* `CondensedMod.isSolid_of_isLimit_gen`: if a condensed `R`-module is the limit of solid
+  modules, then it is solid (fully proved).
+* `CondensedMod.profiniteSolid_obj_isSolid`: `((profiniteSolid R).obj S).IsSolid`
+  for `S : Profinite`. Architecture complete; two intermediate sorries remain:
+  (1) `surj_factor` (proved in MathProject/P2_finFree_Solid.lean; colimit argument);
+  (2) `h_step` in injectivity (requires `finFree_isCompact`, not yet in Mathlib).
 -/
+
 @[expose] public section
+
 universe u
+
 variable (R : Type (u + 1)) [Ring R]
 
 open CategoryTheory Limits Profinite Condensed
@@ -49,7 +56,7 @@ abbrev finFree : FintypeCat.{u} ⥤ CondensedMod.{u} R :=
 abbrev profiniteFree : Profinite.{u} ⥤ CondensedMod.{u} R :=
   profiniteToCondensed ⋙ free R
 
-/-- The functor sending a profinite space `S` to the condensed `R`-module `R[S]^\solid`. -/
+/-- The functor sending a profinite space `S` to the condensed `R`-module `R[S]^solid`. -/
 def profiniteSolid : Profinite.{u} ⥤ CondensedMod.{u} R :=
   Functor.rightKanExtension FintypeCat.toProfinite (finFree R)
 
@@ -70,7 +77,7 @@ def profiniteSolidIsPointwiseRightKanExtension :
     (Functor.RightExtension.mk _ (profiniteSolidCounit R)).IsPointwiseRightKanExtension :=
   Functor.isPointwiseRightKanExtensionOfIsRightKanExtension _ _
 
-/-- The natural transformation `R[S] ⟶ R[S]^\solid`. -/
+/-- The natural transformation `R[S] ⟶ R[S]^solid`. -/
 def profiniteSolidification : profiniteFree R ⟶ profiniteSolid.{u} R :=
   (profiniteSolid R).liftOfIsRightKanExtension (profiniteSolidCounit R) _ (𝟙 _)
 
@@ -123,7 +130,7 @@ lemma profiniteSolidification_isIso_at_fintype (T : FintypeCat.{u}) :
   exact isIso_of_comp_hom_eq_id ((profiniteSolidCounit R).app T)
           (profiniteSolidification_comp_counit R T)
 
-/-! ### Solidness of `profiniteSolid R` -/
+/-! ### Solidness of `profiniteSolid R` at finite test objects -/
 
 /-- `((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`
@@ -137,33 +144,216 @@ theorem profiniteSolid_isSolid_at_fintype
     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`.
+/-! ### Infrastructure for the general solidness proof -/
+
+/-- The isomorphism `(profiniteSolid R).obj LT ≅ (finFree R).obj T`, for `T : FintypeCat`.
+This is the counit of the right Kan extension, which is an isomorphism by
+`profiniteSolidCounit_isIso`. -/
+noncomputable def finFree_iso_solid (T : FintypeCat.{u}) :
+    (profiniteSolid R).obj (FintypeCat.toProfinite.obj T) ≅ (finFree R).obj T :=
+  @asIso _ _ _ _ ((profiniteSolidCounit R).app T) (profiniteSolidCounit_isIso R T)
+
+/-- Key commutation: the solidification composed with the solid map and the counit iso
+equals the free map. This is the fundamental compatibility between solidification and
+the Kan extension structure. -/
+lemma sol_map_counit (T : FintypeCat.{u}) (X : Profinite.{u})
+    (ψ : X ⟶ FintypeCat.toProfinite.obj T) :
+    (profiniteSolidification R).app X ≫
+    (profiniteSolid R).map ψ ≫
+    (finFree_iso_solid R T).hom = (profiniteFree R).map ψ := by
+  have nat := (profiniteSolidification R).naturality ψ
+  have hcounit : (finFree_iso_solid R T).hom = (profiniteSolidCounit R).app T := rfl
+  rw [hcounit, ← Category.assoc, ← nat, Category.assoc, profiniteSolidification_comp_counit]
+  exact Category.comp_id _
+
+/-- The inverse of `finFree_iso_solid` equals the solidification map. -/
+lemma finFree_iso_solid_inv_eq_sol (T : FintypeCat.{u}) :
+    (finFree_iso_solid R T).inv =
+    (profiniteSolidification R).app (FintypeCat.toProfinite.obj T) := by
+  haveI : IsIso ((profiniteSolidCounit R).app T) := profiniteSolidCounit_isIso R T
+  haveI : IsIso ((profiniteSolidification R).app (FintypeCat.toProfinite.obj T)) :=
+    profiniteSolidification_isIso_at_fintype R T
+  have h_inv : (finFree_iso_solid R T).hom ≫
+      (profiniteSolidification R).app (FintypeCat.toProfinite.obj T) = 𝟙 _ := by
+    simp only [finFree_iso_solid, asIso_hom]
+    rw [show (profiniteSolidCounit R).app T ≫
+        (profiniteSolidification R).app (FintypeCat.toProfinite.obj T) =
+        𝟙 ((finFree R).obj T) from by
+      rw [← profiniteSolidification_comp_counit R T]; simp [Category.assoc]]
+  exact IsIso.eq_inv_of_hom_inv_id h_inv
+
+/-- The counit iso composed with the solidification equals the identity. -/
+lemma iso_counit_sol (T : FintypeCat.{u}) :
+    (finFree_iso_solid R T).hom ≫
+    (profiniteSolidification R).app (FintypeCat.toProfinite.obj T) =
+    𝟙 ((profiniteSolid R).obj (FintypeCat.toProfinite.obj T)) := by
+  rw [← finFree_iso_solid_inv_eq_sol R T]
+  exact (finFree_iso_solid R T).hom_inv_id
+
+/-- `surj_factor`: any morphism `h : profiniteFree X ⟶ finFree T` factors through a
+finite level, i.e., there exist `U₀ : FintypeCat`, `q₀ : X ⟶ LU₀`, and
+`h₀ : profiniteFree LU₀ ⟶ finFree T` such that `h = profiniteFree.map q₀ ≫ h₀`.
+
+Proof: The value `(finFree T)(X)` is the colimit of `(finFree T)(LU)` over the
+cofiltered diagram of finite discrete quotients of X (by `finFree_isColimit_at`).
+The adjunction `freeForgetAdjunction` identifies `h` with an element of `(finFree T)(X)`,
+which by the colimit structure comes from some finite stage `U₀`.
+
+This lemma is proved in MathProject/P2_finFree_Solid.lean.
+TODO: integrate the proof into Mathlib.
+-/
+lemma surj_factor (T : FintypeCat.{u}) (X : Profinite.{u})
+    (h : (profiniteFree R).obj X ⟶ (finFree R).obj T) :
+    ∃ (U₀ : FintypeCat.{u}) (q₀ : X ⟶ FintypeCat.toProfinite.obj U₀)
+      (h₀ : (profiniteFree R).obj (FintypeCat.toProfinite.obj U₀) ⟶ (finFree R).obj T),
+      h = (profiniteFree R).map q₀ ≫ h₀ := by
+  sorry
+
+/-! ### Solidness of `(profiniteSolid R).obj LT` (finite case) -/
+
+/-- `((profiniteSolid R).obj LT).IsSolid` for any `T : FintypeCat`.
+
+The proof establishes bijectivity of the solidification map for any test object `X`.
+
+**Surjectivity** (proved 2026-06-13, using `surj_factor` and `sol_map_counit`):
+Given `h : profiniteFree X ⟶ profiniteSolid LT`, translate via `finFree_iso_solid`,
+apply `surj_factor` to factor through a finite level, then use `sol_map_counit`.
+
+**Injectivity** (one sorry): requires `finFree_isCompact`, not yet in Mathlib.
+Mathematically: `finFree T ≅ ⊕_{t∈T} R_cond` where `R_cond` is compact (by Yoneda),
+and finite direct sums of compact objects are compact in `CondensedMod R`.
+-/
+theorem profiniteSolid_fintype_isSolid (T : FintypeCat.{u}) :
+    ((profiniteSolid R).obj (FintypeCat.toProfinite.obj T)).IsSolid := by
+  constructor; intro X
+  rw [isIso_iff_bijective]
+  constructor
+  · -- INJECTIVITY: sorry (requires finFree_isCompact)
+    intro g g' hgg'
+    have hcoinv := iso_counit_sol R T
+    have h_step : g ≫ (finFree_iso_solid R T).hom = g' ≫ (finFree_iso_solid R T).hom := by
+      sorry
+    calc g = g ≫ 𝟙 _ := (Category.comp_id _).symm
+      _ = g ≫ (finFree_iso_solid R T).hom ≫
+              (profiniteSolidification R).app (FintypeCat.toProfinite.obj T) := by rw [hcoinv]
+      _ = g' ≫ (finFree_iso_solid R T).hom ≫
+              (profiniteSolidification R).app (FintypeCat.toProfinite.obj T) := by
+              simp only [← Category.assoc, h_step]
+      _ = g' ≫ 𝟙 _ := by rw [← hcoinv]
+      _ = g' := Category.comp_id _
+  · -- SURJECTIVITY (proved 2026-06-13, see also SurjProof_FINAL.lean)
+    intro h
+    let h' : (profiniteFree R).obj X ⟶ (finFree R).obj T :=
+      h ≫ (finFree_iso_solid R T).hom
+    obtain ⟨U₀, q₀, h₀, hfact⟩ := surj_factor R T X h'
+    refine ⟨(profiniteSolid R).map q₀ ≫ (finFree_iso_solid R U₀).hom ≫
+            h₀ ≫ (finFree_iso_solid R T).inv, ?_⟩
+    have hmid := sol_map_counit R U₀ X q₀
+    have eq1 : (profiniteSolidification R).app X ≫ (profiniteSolid R).map q₀ ≫
+        (finFree_iso_solid R U₀).hom ≫ h₀ ≫ (finFree_iso_solid R T).inv = h := by
+      rw [show (profiniteSolidification R).app X ≫ (profiniteSolid R).map q₀ ≫
+          (finFree_iso_solid R U₀).hom ≫ h₀ ≫ (finFree_iso_solid R T).inv =
+          ((profiniteSolidification R).app X ≫ (profiniteSolid R).map q₀ ≫
+          (finFree_iso_solid R U₀).hom) ≫ h₀ ≫ (finFree_iso_solid R T).inv
+          from by simp [Category.assoc],
+          hmid, ← Category.assoc, ← hfact]
+      simp only [h', Category.assoc, Iso.hom_inv_id, Category.comp_id]
+    rw [show (profiniteSolidification R).app X ≫
+        ((profiniteSolid R).map q₀ ≫ (finFree_iso_solid R U₀).hom ≫
+         h₀ ≫ (finFree_iso_solid R T).inv) =
+        (profiniteSolidification R).app X ≫ (profiniteSolid R).map q₀ ≫
+        (finFree_iso_solid R U₀).hom ≫ h₀ ≫ (finFree_iso_solid R T).inv
+        from by simp [Category.assoc]]
+    exact eq1
+
+/-! ### Limits of solid modules are solid -/
+
+/-- If a condensed `R`-module is the limit of a diagram of solid modules, then it is solid.
+
+**Proof** (fully proved, no sorry): For any test object `X`, we show bijectivity of the
+solidification map on Hom-sets by using bijectivity at each component of the diagram
+together with the limit property (`IsLimit.hom_ext` for injectivity, `IsLimit.lift`
+for surjectivity). -/
+lemma isSolid_of_isLimit_gen
+    {J : Type*} [Category J]
+    {F : J ⥤ CondensedMod.{u} R}
+    (c : Cone F) (hc : IsLimit c)
+    (hj : ∀ j, (F.obj j).IsSolid) :
+    c.pt.IsSolid := by
+  refine ⟨fun X => ?_⟩
+  rw [isIso_iff_bijective]
+  set sol := (profiniteSolidification R).app X
+  have bijFun : ∀ j, Function.Bijective ((yoneda.obj (F.obj j)).map sol.op) := by
+    intro j; have h := (hj j).isIso_solidification_map X
+    rw [isIso_iff_bijective] at h; exact h
+  constructor
+  · intro f g hfg
+    apply hc.hom_ext; intro j; apply (bijFun j).1
+    show sol ≫ f ≫ c.π.app j = sol ≫ g ≫ c.π.app j
+    simp only [← Category.assoc, hfg]
+  · intro h_map
+    choose g_j hg_j using fun j => (bijFun j).2 (h_map ≫ c.π.app j)
+    have hg_j' : ∀ j, sol ≫ g_j j = h_map ≫ c.π.app j := hg_j
+    have compat : ∀ {j k : J} (φ : j ⟶ k), g_j j ≫ F.map φ = g_j k := by
+      intro j k φ
+      have lhs : sol ≫ (g_j j ≫ F.map φ) = h_map ≫ c.π.app k := by
+        conv_lhs => rw [← Category.assoc, hg_j' j, Category.assoc, c.w φ]
+      exact (bijFun k).1 (lhs.trans (hg_j' k).symm)
+    let g_cone : Cone F :=
+      { pt := (profiniteSolid R).obj X
+        π  := { app        := g_j
+                naturality := fun j k φ => by
+                  change 𝟙 _ ≫ g_j k = g_j j ≫ F.map φ
+                  simp only [Category.id_comp]; exact (compat φ).symm } }
+    refine ⟨hc.lift g_cone, ?_⟩
+    show sol ≫ hc.lift g_cone = h_map
+    apply hc.hom_ext; intro j
+    have hfac : hc.lift g_cone ≫ c.π.app j = g_j j := hc.fac g_cone j
+    rw [Category.assoc, hfac]; exact hg_j' j
+
+/-! ### `finFree R T` is solid -/
+
+/-- `(finFree R).obj T` is a solid condensed `R`-module, for any `T : FintypeCat`.
+
+The proof uses the isomorphism `finFree_iso_solid R T : profiniteSolid LT ≅ finFree T`
+to transfer solidness from `profiniteSolid_fintype_isSolid`. -/
+theorem finFree_isSolid (T : FintypeCat.{u}) : ((finFree R).obj T).IsSolid := by
+  constructor; intro X
+  have hS : IsIso ((yoneda.obj ((profiniteSolid R).obj
+      (FintypeCat.toProfinite.obj T))).map ((profiniteSolidification R).app X).op) :=
+    (profiniteSolid_fintype_isSolid R T).isIso_solidification_map X
+  have e := finFree_iso_solid R T
+  rw [show (yoneda.obj ((finFree R).obj T)).map ((profiniteSolidification R).app X).op =
+    (yoneda.mapIso e).inv.app (op ((profiniteSolid R).obj X)) ≫
+    (yoneda.obj ((profiniteSolid R).obj (FintypeCat.toProfinite.obj T))).map
+      ((profiniteSolidification R).app X).op ≫
+    (yoneda.mapIso e).hom.app (op ((profiniteFree R).obj X)) from ?_]
+  · exact IsIso.comp_isIso
+  · ext g; simp
+
+/-! ### General solidness of `profiniteSolid R` -/
+
+/-- Every `(profiniteSolid R).obj S` is a solid condensed `R`-module, for any `S : Profinite`.
+
+**Proof architecture** (complete, two remaining sorries are in auxiliary lemmas):
+1. `profiniteSolidIsPointwiseRightKanExtension` gives `(profiniteSolid R).obj S` as the
+   limit of `finFree R` over `StructuredArrow S FintypeCat.toProfinite`.
+2. `isSolid_of_isLimit_gen` (proved) reduces to showing each component is solid.
+3. `finFree_isSolid` (proved modulo `profiniteSolid_fintype_isSolid`) handles each component.
+
+Remaining sorries (in `profiniteSolid_fintype_isSolid`):
+- `surj_factor`: proved in MathProject/P2_finFree_Solid.lean; TODO: integrate.
+- Injectivity `h_step`: requires `finFree_isCompact` (not yet in Mathlib).
 -/
 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 }
+    ((profiniteSolid R).obj S).IsSolid := by
+  let E := Functor.RightExtension.mk (profiniteSolid R) (profiniteSolidCounit R)
+  have h_pwise : IsLimit (E.coneAt S) :=
+    (profiniteSolidIsPointwiseRightKanExtension R) S
+  change (E.coneAt S).pt.IsSolid
+  apply isSolid_of_isLimit_gen R (E.coneAt S) h_pwise
+  intro f
+  simp only [comp_obj, StructuredArrow.proj_obj]
+  exact finFree_isSolid R f.right
 
 end CondensedMod