exists_hom_from_galois_of_connected

English

A variant stating that a connected X admits a morphism from a Galois object.

Русский

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

LaTeX

$$$\exists A\;\exists f:\, A \to X,\ IsGalois A$$$

Lean4

/-- Any connected object admits a hom from a Galois object. -/
theorem exists_hom_from_galois_of_connected (X : C) [IsConnected X] : ∃ (A : C) (_ : A ⟶ X), IsGalois A :=
  exists_hom_from_galois_of_fiber_nonempty F X inferInstance

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