Prove circle is an instance of CWComplex

Stream: new members

[Hank]

Hello, I am trying to prove that the unit circle in the complex plane is an instance of the CWComplex, but am having some trouble.
For the unit circle, I use the existing definition in Mathlib.Analysis.Complex.Circle, and the for CWComplex, I use the existing class in Mathlib.Topology.CWComplex.Classical.Basic.

Here is my current code:

import Mathlib.Analysis.Complex.Circle
import Mathlib.Topology.CWComplex

set_option autoImplicit false

open Set TopologicalSpace Metric
open scoped Real Topology

/-- The indexing type for the cells of S¹.
We have one 0-cell and one 1-cell.
-/
def S1Cell : ℕ → Type
  | 0 => Fin 1
  | 1 => Fin 1
  | _ => Fin 0

instance : CWComplex (univ : Set Circle) where
    /-- The indexing type of the cells of dimension `n`. -/
  cell (n : ℕ) := sorry
  /-- The characteristic map of the `n`-cell given by the index `i`.
  This map is a bijection when restricting to `ball 0 1`, where we consider `(Fin n → ℝ)`
  endowed with the maximum metric. -/
  map (n : ℕ) (i : cell n) : PartialEquiv (Fin n → ℝ) X := sorry

Already at the line instance : CWComplex (univ : Set Circle) , Lean complains that

function expected at
  CWComplex
term has type
  Type (?u.198 + 1)

To solve this, I typed #check CWComplex, which gave me

CWComplex.{u} : Type (u + 1)

but I don't know how to proceed.

[Hannah Scholz]

Hello,
Glad to see you are interested in CW complexes in Lean! So I don't know which version of Mathlib you are on to get this error. When I open this in the Lean playground I get a complaint that Mathlib.Topology.CWComplex does not exist because as you note in your message the correct file would be Mathlib.Topology.CWComplex.Classical.Basic. And to be able to just write CWComplex instead of Topology.CWComplex I think you need to have open Topology not just open scoped Topology.

I actually have code on the CW structure on spheres in real euclidean space here but it is unfortunatly still far from polished. (This is not to discourage you to try this, just as a reference.)

[Hank]

Hello Hannah,
Yes, it is probably due to different versions. I was writing the code in lean4:v4.17.0-rc1. I created a new project using the recent version lean4:v4.25.0-rc2 and pasted my code there. Then things happened just like what you said.
Also, thank you for sharing your CW complex project! It is very cool!