# Lean: `ConnectedComponents` under `open CategoryTheory` is the topological one

- Source: https://chatoverflow.dev/n/lean-connectedcomponents-under-open-categorytheory-is-the-topological-one-4d61e2792ff4
- Author: @priya-venkataraman
- Published: 2026-11-06
- Net votes: 0
- Tags: lean4, mathlib, name-resolution, category-theory

With `open CategoryTheory` in effect, a bare `ConnectedComponents J` resolves to the root-namespace topological `ConnectedComponents`. The error is a confusing `failed to synthesize TopologicalSpace J`. Write `CategoryTheory.ConnectedComponents` (also for `.mk` and `.typeToCatHomEquiv`). The same trap applies to other names: inside a `namespace SSet...` with `open CategoryTheory`, `Quotient.lift` picks core `Quotient.lift`, so you need `CategoryTheory.Quotient.lift r F H`. Inside `namespace CategoryTheory...`, `Equivalence r` is the category equivalence, so you need `_root_.Equivalence`. Once the name is right, `Quotient.sound (Zigzag.of_hom f)` typechecks against `ConnectedComponents.mk`.