English
For a finite family of Galois objects X_i, there exists a single g in G that acts on every fiber F(X_i) as t_Xi does.
Русский
Для конечного множества Galois-объектов X_i существует один элемент g ∈ G, действующий на каждой волокне F(X_i) как t_Xi.
LaTeX
$$$\exists g\in G\;\forall i\;\forall x\in F(X_i),\; g\cdot x = t_{X_i}(x)$$$
Lean4
theorem toAut_surjective_isGalois_finite_family (t : Aut F) {ι : Type*} [Finite ι] (X : ι → C) [∀ i, IsGalois (X i)]
(h : ∀ (X : C) [IsGalois X], MulAction.IsPretransitive G (F.obj X)) :
∃ (g : G), ∀ (i : ι) (x : F.obj (X i)), g • x = t.hom.app (X i) x :=
by
let x (i : ι) : F.obj (X i) := (nonempty_fiber_of_isConnected F (X i)).some
let P : C := ∏ᶜ X
letI : Fintype ι := Fintype.ofFinite ι
let is₁ : F.obj P ≅ ∏ᶜ fun i ↦ (F.obj (X i)) := PreservesProduct.iso F X
let is₂ : (∏ᶜ fun i ↦ F.obj (X i) : FintypeCat) ≃ ∀ i, F.obj (X i) :=
Limits.FintypeCat.productEquiv (fun i ↦ (F.obj (X i)))
let px : F.obj P := is₁.inv (is₂.symm x)
have hpx (i : ι) : F.map (Pi.π X i) px = x i :=
by
simp only [px, is₁, is₂, ← piComparison_comp_π, ← PreservesProduct.iso_hom]
simp only [FintypeCat.comp_apply, FintypeCat.inv_hom_id_apply, FintypeCat.productEquiv_symm_comp_π_apply]
obtain ⟨A, f, a, _, hfa⟩ := exists_hom_from_galois_of_fiber F P px
obtain ⟨g, hg⟩ := toAut_surjective_isGalois F G t A
refine ⟨g, fun i y ↦ action_ext_of_isGalois F (x i) ?_ _⟩
rw [← hpx i, ← IsNaturalSMul.naturality, FunctorToFintypeCat.naturality, ← hfa, FunctorToFintypeCat.naturality, ←
IsNaturalSMul.naturality, hg]
