Lean4
/-- The counit of the adjunction `lightCondSetToSequential ⊣ sequentialToLightCondSet`
is a homeomorphism.
Note: for now, we only have `ℕ∪{∞}` as a light profinite set at universe level 0, which is why we
can only prove this for `X : TopCat.{0}`.
-/
noncomputable def sequentialAdjunctionHomeo (X : TopCat.{0}) [SequentialSpace X] : X.toLightCondSet.toTopCat ≃ₜ X
where
toEquiv := topCatAdjunctionCounitEquiv X
continuous_toFun := (topCatAdjunctionCounit X).hom.continuous
continuous_invFun := by
apply SeqContinuous.continuous
unfold SeqContinuous
intro f p h
let g := (topCatAdjunctionCounitEquiv X).invFun ∘ (OnePoint.continuousMapMkNat f p h)
change Filter.Tendsto (fun n : ℕ ↦ g n) _ _
erw [← OnePoint.continuous_iff_from_nat]
let x : X.toLightCondSet.val.obj ⟨(ℕ∪{∞})⟩ := OnePoint.continuousMapMkNat f p h
exact continuous_coinducingCoprod X.toLightCondSet x
