has_decomp_connected_components — Mathlib

English

In a Galois category, every object is the sum of connected objects.

Русский

В Галуа-категории каждый объект является суммой связных объектов.

LaTeX

$$$\exists ι\ (f:ι \to C)\ (g: (i:ι) \to f i \to X) \;\text{IsColimit}(\text{Cofan.mk } X g) \land (\forall i, IsConnected (f i)) \land Finite ι$$$

Lean4

/-- In a Galois category, every object is the sum of connected objects. -/
theorem has_decomp_connected_components (X : C) :
    ∃ (ι : Type) (f : ι → C) (g : (i : ι) → f i ⟶ X) (_ : IsColimit (Cofan.mk X g)),
      (∀ i, IsConnected (f i)) ∧ Finite ι :=
  by
  let F := GaloisCategory.getFiberFunctor C
  exact has_decomp_connected_components_aux F (Nat.card <| F.obj X) X rfl

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