English
For every LightDiagram S, the cone point S.cone.pt has a second countable topology.
Русский
Для любого LightDiagram S точка конуса S.cone.pt имеет вторую счетную топологию.
LaTeX
$$$\operatorname{SecondCountableTopology}(S.cone.pt)$$$
Lean4
instance (S : LightDiagram.{u}) : SecondCountableTopology S.cone.pt :=
by
rw [← TopologicalSpace.Clopens.countable_iff_secondCountable]
refine @Countable.of_equiv _ _ ?_ (LocallyConstant.equivClopens (X := S.cone.pt))
refine
@Function.Surjective.countable (Σ (n : ℕ), LocallyConstant ((S.diagram ⋙ FintypeCat.toProfinite).obj ⟨n⟩) (Fin 2)) _
?_ ?_ ?_
· apply @instCountableSigma _ _ _ ?_
intro n
refine @Finite.to_countable _ ?_
refine
@Finite.of_injective _ ((S.diagram ⋙ FintypeCat.toProfinite).obj ⟨n⟩ → (Fin 2)) ?_ _ LocallyConstant.coe_injective
refine @Pi.finite _ _ ?_ _
simp only [Functor.comp_obj]
exact show (Finite (S.diagram.obj _)) from inferInstance
· exact fun a ↦ a.snd.comap (S.cone.π.app ⟨a.fst⟩).hom
· intro a
obtain ⟨n, g, h⟩ := Profinite.exists_locallyConstant S.cone S.isLimit a
exact ⟨⟨unop n, g⟩, h.symm⟩
