fintypeCatAsCofanIsColimit — Mathlib

English

The finite coproduct cocone above is a colimit in Profinite, i.e., it satisfies the universal property of coproducts.

Русский

Этот копро-конус является колимитом в Profinite, то есть удовлетворяет универсальному свойству копроизведения.

LaTeX

$$$\\text{IsColimit}(\\text{fintypeCatAsCofan } X)$$$

Lean4

/-- A finite set is the coproduct of its points in `Profinite`. -/
def fintypeCatAsCofanIsColimit (X : Profinite) [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

Похожие утверждения