has_decomp_connected_components' — Mathlib

English

A variant of the decomposition: there exists ι with a finite structure and an isomorphism ∐ f ≅ X, with each f i connected.

Русский

Вариант разложения: существует ι с конечной структурой и изоморфизм ∐ f ≅ X, причём каждый f i связан.

LaTeX

$$$\exists ι\ (\text{Finite } ι)\ (f:ι \to C)\ (\text{iso}: \bigl(\coprod_{i∈ι} f i\bigr) \cong X),\ \forall i, IsConnected (f i)$$$

Lean4

/-- In a Galois category, every object is the sum of connected objects. -/
theorem has_decomp_connected_components' (X : C) :
    ∃ (ι : Type) (_ : Finite ι) (f : ι → C) (_ : ∐ f ≅ X), ∀ i, IsConnected (f i) :=
  by
  obtain ⟨ι, f, g, hl, hc, hf⟩ := has_decomp_connected_components X
  exact ⟨ι, hf, f, colimit.isoColimitCocone ⟨Cofan.mk X g, hl⟩, hc⟩

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