instFiniteAutOfIsConnected — Mathlib

English

There exists a Galois object A with a fiber element a ∈ F.obj A such that the fiber admits a bijection with the morphisms to X.

Русский

Существует Галуа-объект A с элементом волокна a ∈ F.obj A, для которого волокно сопоставимо по биекции отображениям в X.

LaTeX

$$$\exists A\; \exists a:\, F.obj A,\ IsGalois A \land \\text{Bijective}(\lambda f: A ⟶ X, F.map f a))$$$

Lean4

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

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