English
Let X be a finite set in LightProfinite. Then X is the coproduct of its points in LightCondensed; equivalently, the cocone built from the inclusions of each point into X exhibits X as a coproduct.
Русский
Пусть X — конечное множество в LightProfinite. Тогда X является копродуктом своих точек в LightCondensed; эквивалентно, конийный конус, построенный из включений каждой точки в X, представляет X как копродукт.
LaTeX
$$$\operatorname{IsColimit}(\text{fintypeCatAsCofan}(X))$$$
Lean4
/-- A finite set is the coproduct of its points in `LightProfinite`. -/
def fintypeCatAsCofanIsColimit (X : LightProfinite) [Finite X] : IsColimit (fintypeCatAsCofan X) :=
by
refine
mkCofanColimit _ (fun t ↦ TopCat.ofHom ⟨fun x ↦ t.inj x PUnit.unit, ?_⟩) ?_
(fun _ _ h ↦ by ext x; exact CategoryTheory.congr_fun (h x) _)
· apply continuous_of_discreteTopology (α := X)
· aesop
