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

Closed

thothrde wants to merge 26 commits into

leanprover-community:masterfrom

thothrde:feat/condensed-solid-isSolid-profiniteSolid

Commits on Jun 22, 2026

Commits on Jun 23, 2026

fix(Condensed/Solid): CategoryStruct.id + Sheaf.val accessors
thothrde
committed
fix(Condensed/Solid): use CategoryTheory.id to avoid 𝟙/𝟭 confusion
thothrde
committed
revert(Condensed/Solid): surj_factor back to axiom
thothrde
committed
fix(Condensed/Solid): isIso_iff_bijective explicit arg + constructor syntax
thothrde
committed
fix(Condensed/Solid): correct liftOfIsRightKanExtension arg order
thothrde
committed
fix(Condensed/Solid): restructure proofs to eliminate all type errors
thothrde
committed
fix(Condensed/Solid): three fixes for isIso_iff_bijective API (v6)
thothrde
committed
fix(Condensed/Solid): v7 - targeted fixes for CI lines 104/106/114
thothrde
committed
fix(Condensed/Solid): v8 - L99 exact comp_id + L203 yoneda.mapIso infer_instance
thothrde
committed
fix(Condensed/Solid): v9 - remove Plane-1 char + safer finFree_isSolid
thothrde
committed
fix(Condensed/Solid): v10 - revert sol_map_counit to simp (no exact comp_id)
thothrde
committed
fix(Condensed/Solid): sol_map_counit: replace simp with rw+comp_id (Lean 4.32)
thothrde
committed
fix(Condensed/Solid): add module syntax for Lean 4.32 compatibility
thothrde
committed

Commits on Jun 24, 2026