English
A technical matching lemma associated with lifting quotients by open subgroups; aligns the quotient data with the action structure.
Русский
Технический вспомогательный лемма, связанная с восстановлением квадрата по открытым подгруппам; согласует данные о квартировании с структурой действия.
LaTeX
$$$\\text{(technical matching lemma for open subgroups and quotients)}$$$
Lean4
/-- For every open subgroup `V` of `Aut F`, there exists an `X : C` such that
`F.obj X ≅ Aut F ⧸ V` as `Aut F`-sets. -/
theorem exists_lift_of_quotient_openSubgroup (V : OpenSubgroup (Aut F)) :
∃ (X : C), Nonempty ((functorToAction F).obj X ≅ Aut F ⧸ₐ V.toSubgroup) :=
by
obtain ⟨I, hf, hc, hi⟩ := exists_set_ker_evaluation_subset_of_isOpen F (one_mem V) V.isOpen'
haveI (X : I) : IsConnected X.val := hc X X.property
haveI (X : I) : Nonempty (F.obj X.val) := nonempty_fiber_of_isConnected F X
have hn : Nonempty (F.obj <| (∏ᶜ fun X : I => X)) := nonempty_fiber_pi_of_nonempty_of_finite F _
obtain ⟨A, f, hgal⟩ := exists_hom_from_galois_of_fiber_nonempty F (∏ᶜ fun X : I => X) hn
obtain ⟨a⟩ := nonempty_fiber_of_isConnected F A
let U : OpenSubgroup (Aut F) := ⟨MulAction.stabilizer (Aut F) a, stabilizer_isOpen (Aut F) a⟩
let u := fiberIsoQuotientStabilizer A a
have hUnormal : U.toSubgroup.Normal := stabilizer_normal_of_isGalois F A a
have h1 (σ : Aut F) (σinU : σ ∈ U) : σ.hom.app A = 𝟙 (F.obj A) :=
by
have hi : (Aut F ⧸ₐ MulAction.stabilizer (Aut F) a).ρ σ = 𝟙 _ :=
by
refine FintypeCat.hom_ext _ _ (fun x ↦ ?_)
induction x using Quotient.inductionOn with
| _ τ
change ⟦σ * τ⟧ = ⟦τ⟧
apply Quotient.sound
apply (QuotientGroup.leftRel_apply).mpr
simp only [mul_inv_rev]
exact Subgroup.Normal.conj_mem hUnormal _ (Subgroup.inv_mem U.toSubgroup σinU) _
simp [← cancel_mono u.hom.hom, show σ.hom.app A ≫ u.hom.hom = _ from u.hom.comm σ, hi]
have h2 (σ : Aut F) (σinU : σ ∈ U) : ∀ X : I, σ.hom.app X = 𝟙 (F.obj X) :=
by
intro ⟨X, hX⟩
ext (x : F.obj X)
let p : A ⟶ X := f ≫ Pi.π (fun Z : I => (Z : C)) ⟨X, hX⟩
have : IsConnected X := hc X hX
obtain ⟨a, rfl⟩ := surjective_of_nonempty_fiber_of_isConnected F p x
simp only [FintypeCat.id_apply, FunctorToFintypeCat.naturality, h1 σ σinU]
have hUinV : (U : Set (Aut F)) ≤ V := fun u uinU ↦ hi u (h2 u uinU)
have := V.quotient_finite_of_isOpen' (U.subgroupOf V) V.isOpen (V.subgroupOf_isOpen U U.isOpen)
exact
⟨colimit (quotientDiag V hUnormal u),
⟨preservesColimitIso (functorToAction F) (quotientDiag V hUnormal u) ≪≫
colimit.isoColimitCocone ⟨coconeQuotientDiag hUnormal u hUinV, coconeQuotientDiagIsColimit hUnormal u hUinV⟩⟩⟩
