English
Every fiber element x is the evaluation of a morphism from a Galois object.
Русский
Каждый элемент фибера является значением отображения из Галуа-объекта.
LaTeX
$$$\exists A\; f:\, A \to X\; a:\, F.obj A,\ IsGalois A\land F.map f a = x$$$
Lean4
/-- The fiber of any object in a Galois category is represented by a Galois object. -/
theorem exists_galois_representative (X : C) :
∃ (A : C) (a : F.obj A), IsGalois A ∧ Function.Bijective (fun (f : A ⟶ X) ↦ F.map f a) :=
by
obtain ⟨A, u, a, h1, h2, h3⟩ := fiber_in_connected_component F (selfProd F X) (mkSelfProdFib F X)
use A
use a
constructor
· refine (isGalois_iff_pretransitive F A).mpr ⟨fun x y ↦ ?_⟩
obtain ⟨fi1, hfi1⟩ := subobj_selfProd_trans h1 x
obtain ⟨fi2, hfi2⟩ := subobj_selfProd_trans h1 y
use fi1 ≪≫ fi2.symm
change F.map (fi1.hom ≫ fi2.inv) x = y
simp only [map_comp, FintypeCat.comp_apply]
rw [hfi1, ← hfi2]
exact congr_fun (F.mapIso fi2).hom_inv_id y
· refine ⟨evaluation_injective_of_isConnected F A X a, ?_⟩
intro x
use u ≫ Pi.π _ x
exact (selfProdProj_fiber h1) x
