instFiniteHomOfIsConnected — Mathlib

English

For a connected object A, the set of morphisms A ⟶ X is finite.

Русский

Для связного A множество морфизмов A ⟶ X является конечным.

LaTeX

$$$\operatorname{Finite}(A \to X)$$$

Lean4

/-- In a `GaloisCategory` the set of morphisms out of a connected object is finite. -/
instance (A X : C) [IsConnected A] : Finite (A ⟶ X) :=
  by
  let F := GaloisCategory.getFiberFunctor C
  obtain ⟨a⟩ := nonempty_fiber_of_isConnected F A
  apply Finite.of_injective (fun f ↦ F.map f a)
  exact evaluation_injective_of_isConnected F A X a

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