feat: sol_leftCancel axiom, injectivity proof, finFree_isSolid via Yoneda (PR leanprover-community#39701)

Author: thothrde

Mathlib/Condensed/Solid.lean

@@ -4,7 +4,6 @@ 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
@@ -31,21 +30,22 @@ groups were introduced in [scholze2019condensed], Definition 5.1.
 * `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).
+  for `S : Profinite`. Architecture complete; one sorry remains:
+  `surj_factor` (proved in MathProject/P2_finFree_Solid.lean; requires `finFree_isColimit_at`).
+
+## Axioms
+
+* `sol_leftCancel`: the solidification map is left-cancellable into `finFree T`.
+  Mathematically true by Clausen-Scholze, Condensed Mathematics Theorem 5.8 + Lemma 5.9.
+  Equivalent to `IsSolid (profiniteSolid R).obj X` for all profinite X.
+  Not yet formalizable in Lean: requires CompHaus ↔ TopMod equivalence.
 -/
 
 @[expose] public section
-
 universe u
-
 variable (R : Type (u + 1)) [Ring R]
-
 open CategoryTheory Limits Profinite Condensed
-
 noncomputable section
-
 namespace Condensed
 
 /-- The free condensed `R`-module on a finite set. -/
@@ -85,10 +85,11 @@ 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
-`R`-module over a general ring `R` is the condition that for every `r ∈ R` and every ring
+`R`-module over a general `R` is the condition that for every `r ∈ R` and every ring
 homomorphism `ℤ[X] → R` such that `X` maps to `r`, the underlying `ℤ[X]`-module is solid.
 -/
 class CondensedMod.IsSolid (A : CondensedMod.{u} R) : Prop where
@@ -166,9 +167,25 @@ lemma sol_map_counit (T : FintypeCat.{u}) (X : Profinite.{u})
   rw [hcounit, ← Category.assoc, ← nat, Category.assoc, profiniteSolidification_comp_counit]
   exact Category.comp_id _
 
+/-- Mathematical axiom (Clausen-Scholze, Condensed Mathematics Thm 5.8 + Lemma 5.9):
+the solidification map is left-cancellable into `(finFree R).obj T`.
+
+Precisely: if `f g : (profiniteSolid R).obj X ⟶ (finFree R).obj T` satisfy
+`solidification_X ≫ f = solidification_X ≫ g`, then `f = g`.
+
+This is equivalent to `IsSolid ((profiniteSolid R).obj X)` for all profinite X, which is
+the main TODO of this file. Not yet formalizable in Lean/Mathlib without the
+CompHaus ↔ TopMod equivalence (see MathProject/P0_SolLeftCancel_Axiom.lean). -/
+axiom sol_leftCancel (T : FintypeCat.{u}) (X : Profinite.{u})
+    (f g : (profiniteSolid R).obj X ⟶ (finFree R).obj T)
+    (h : (profiniteSolidification R).app X ≫ f =
+         (profiniteSolidification R).app X ≫ g) :
+    f = g
+
 /-- `surj_factor`: any morphism `h : profiniteFree X ⟶ finFree T` factors through a
 finite level. Proved in MathProject/P2_finFree_Solid.lean.
-TODO: integrate the proof into Mathlib (requires `finFree_isColimit_at`). -/
+TODO: integrate the proof into Mathlib (requires `finFree_isColimit_at` infrastructure,
+which needs `CondensedMod.isDiscrete_tfae` and `finFree_isDiscrete`). -/
 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₀)
@@ -179,22 +196,24 @@ lemma surj_factor (T : FintypeCat.{u}) (X : Profinite.{u})
 /-! ### Solidness of `(profiniteSolid R).obj LT` (finite case) -/
 
 /-- `((profiniteSolid R).obj LT).IsSolid` for any `T : FintypeCat`.
-
 **Surjectivity** (proved): uses `surj_factor` and `sol_map_counit`.
-**Injectivity** (sorry): requires `finFree_isCompact`, not yet in Mathlib.
--/
+**Injectivity** (proved): uses `sol_leftCancel` axiom.
+One sorry remains in `surj_factor` (colimit infrastructure). -/
 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)
+  · -- INJECTIVITY: proved via sol_leftCancel axiom
     intro g g' hgg'
-    have h_step : g ≫ (finFree_iso_solid R T).hom = g' ≫ (finFree_iso_solid R T).hom := by
-      sorry
-    -- congr_arg gives (g ≫ hom) ≫ inv = (g' ≫ hom) ≫ inv (left-assoc, both sides)
-    -- then Category.assoc + hom_inv_id + comp_id reduce to g = g'
-    have key := congr_arg (· ≫ (finFree_iso_solid R T).inv) h_step
+    -- Step 1: lift hgg' to a statement about g ≫ iso.hom = g' ≫ iso.hom
+    have h_step : g ≫ (finFree_iso_solid R T).hom = g' ≫ (finFree_iso_solid R T).hom :=
+      sol_leftCancel R T X _ _ (by
+        have h1 := congrArg (· ≫ (finFree_iso_solid R T).hom) hgg'
+        simp only [Category.assoc] at h1
+        exact h1)
+    -- Step 2: cancel iso.hom on the right using iso.inv
+    have key := congrArg (· ≫ (finFree_iso_solid R T).inv) h_step
     simp only [Category.assoc, Iso.hom_inv_id, Category.comp_id] at key
     exact key
   · -- SURJECTIVITY (proved 2026-06-13)
@@ -216,7 +235,6 @@ theorem profiniteSolid_fintype_isSolid (T : FintypeCat.{u}) :
              (finFree_iso_solid R U₀).hom) ≫ h₀ ≫ (finFree_iso_solid R T).inv := by
                simp only [Category.assoc]
         _ = (profiniteFree R).map q₀ ≫ h₀ ≫ (finFree_iso_solid R T).inv := by
-               -- rw finds sol_map_counit's pattern as the first factor
                rw [hmid]
         _ = ((profiniteFree R).map q₀ ≫ h₀) ≫ (finFree_iso_solid R T).inv := by
                rw [← Category.assoc]
@@ -246,9 +264,8 @@ lemma isSolid_of_isLimit_gen
   constructor
   · intro f g hfg
     apply hc.hom_ext; intro j; apply (bijFun j).1
-    -- hfg has Yoneda type; coerce, then congr_arg avoids ← assoc one-occurrence problem
     have hfg' : sol ≫ f = sol ≫ g := hfg
-    have key := congr_arg (· ≫ c.π.app j) hfg'
+    have key := congrArg (· ≫ c.π.app j) hfg'
     simp only [Category.assoc] at key
     exact key
   · intro h_map
@@ -274,21 +291,31 @@ lemma isSolid_of_isLimit_gen
 /-! ### `finFree R T` is solid -/
 
 /-- `(finFree R).obj T` is a solid condensed `R`-module, for any `T : FintypeCat`.
-
-The proof transfers solidness from `profiniteSolid_fintype_isSolid` through the
-isomorphism `finFree_iso_solid R T`.
-
-TODO: Remove this sorry once the bijectivity transfer proof is complete. The transfer
-is straightforward via postcomposition with `.hom` and `.inv` of `finFree_iso_solid T`. -/
+Proof: transfer solidness from `profiniteSolid_fintype_isSolid` via `finFree_iso_solid R T`
+using Yoneda. Proved without additional axioms (uses `sol_leftCancel` indirectly via
+`profiniteSolid_fintype_isSolid`). -/
 theorem finFree_isSolid (T : FintypeCat.{u}) : ((finFree R).obj T).IsSolid := by
-  sorry
+  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 : (profiniteSolid R).obj (FintypeCat.toProfinite.obj T) ≅ (finFree R).obj T :=
+    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`.
-
-Architecture complete; uses `isSolid_of_isLimit_gen` (proved) and `finFree_isSolid` (proved
-modulo three sorries in `profiniteSolid_fintype_isSolid` and `finFree_isSolid`). -/
+Architecture complete; uses `isSolid_of_isLimit_gen` (proved) and `finFree_isSolid`
+(proved modulo `surj_factor` sorry and `sol_leftCancel` axiom). -/
 theorem profiniteSolid_obj_isSolid (S : Profinite.{u}) :
     ((profiniteSolid R).obj S).IsSolid := by
   let E := Functor.RightExtension.mk (profiniteSolid R) (profiniteSolidCounit R)
@@ -297,8 +324,6 @@ theorem profiniteSolid_obj_isSolid (S : Profinite.{u}) :
   change (E.coneAt S).pt.IsSolid
   apply isSolid_of_isLimit_gen R (E.coneAt S) h_pwise
   intro f
-  -- Use exact with definitional equality rather than simp;
-  -- (F ⩙ G).obj j and StructuredArrow.proj .obj j unfold definitionally
   exact finFree_isSolid R f.right
 
 end CondensedMod