English
If Aut F maps surjectively onto automorphisms of all Galois objects, then G acts pretransitively on fibers over any Galois X.
Русский
Если отображение Aut F сюръективно на автоморфизмы всех Galois объектов, то G действует прeтранситивно на волокнах над каждого Galois X.
LaTeX
$$$\text{Surjective}(toAut\,F\,G)\Rightarrow\forall X\,[IsGalois(X)]:\ MulAction.IsPretransitive G (F(X))$$$
Lean4
/-- If `G` is a compact, topological group that acts continuously and naturally on the
fibers of `F`, `toAut F G` is surjective if and only if it acts transitively on the fibers
of all Galois objects. This is the `if` direction. For the `only if` see
`isPretransitive_of_surjective`. -/
theorem toAut_surjective_of_isPretransitive [TopologicalSpace G] [IsTopologicalGroup G] [CompactSpace G]
[∀ (X : C), ContinuousSMul G (F.obj X)] (h : ∀ (X : C) [IsGalois X], MulAction.IsPretransitive G (F.obj X)) :
Function.Surjective (toAut F G) := by
intro t
choose gi hgi using (fun X : PointedGaloisObject F ↦ toAut_surjective_isGalois F G t X)
let cl (X : PointedGaloisObject F) : Set G := gi X • MulAction.stabilizer G X.pt
let c : Set G := ⋂ i, cl i
have hne : c.Nonempty := by
rw [← Set.univ_inter c]
apply CompactSpace.isCompact_univ.inter_iInter_nonempty
· intro X
apply IsClosed.leftCoset
exact Subgroup.isClosed_of_isOpen _ (stabilizer_isOpen G X.pt)
· intro s
rw [Set.univ_inter]
obtain ⟨gs, hgs⟩ := toAut_surjective_isGalois_finite_family F G t (fun X : s ↦ X.val.obj) h
use gs
simp only [Set.mem_iInter]
intro X hXmem
rw [mem_leftCoset_iff, SetLike.mem_coe, MulAction.mem_stabilizer_iff, mul_smul, hgs ⟨X, hXmem⟩, ← hgi X,
inv_smul_smul]
obtain ⟨g, hg⟩ := hne
refine ⟨g, Iso.ext <| natTrans_ext_of_isGalois _ <| fun X _ ↦ ?_⟩
ext x
simp only [toAut_hom_app_apply]
have : g ∈ (gi ⟨X, x, inferInstance⟩ • MulAction.stabilizer G x : Set G) :=
by
simp only [Set.mem_iInter, c] at hg
exact hg _
obtain ⟨s, (hsmem : s • x = x), (rfl : gi ⟨X, x, inferInstance⟩ • s = _)⟩ := this
rw [smul_eq_mul, mul_smul, hsmem]
exact hgi ⟨X, x, inferInstance⟩ x
