English
For a connected X, there exists an isomorphism X ≅ G ⧸ MulAction.stabilizer x, as G-sets.
Русский
Для связного X существует изоморфизм X ≅ G ⧸ стабилизатор x, как G-множества.
LaTeX
$$$X \\cong G \\oslash_{MulAction.stabilizer\,G\,x} $$$
Lean4
/-- Let `X` be an object of a Galois category with fiber functor `F` and `Y` a sub-`Aut F`-set
of `F.obj X`. Then there exists a sub-object `Z` of `X` and an isomorphism
`Y ≅ F.obj X` as `Aut F`-sets such that the obvious triangle commutes.
-/
theorem exists_lift_of_mono (X : C) (Y : Action FintypeCat.{u} (Aut F)) (i : Y ⟶ (functorToAction F).obj X) [Mono i] :
∃ (Z : C) (f : Z ⟶ X) (u : Y ≅ (functorToAction F).obj Z), Mono f ∧ u.hom ≫ (functorToAction F).map f = i :=
by
obtain ⟨ι, hf, f, t, hc⟩ := has_decomp_connected_components' Y
let i' (j : ι) : f j ⟶ (functorToAction F).obj X := Sigma.ι f j ≫ t.hom ≫ i
choose gZ gf gu _ _ h using fun i ↦ exists_lift_of_mono_of_isConnected F X (f i) (i' i)
let is2 : (functorToAction F).obj (∐ gZ) ≅ ∐ fun i => (functorToAction F).obj (gZ i) :=
PreservesCoproduct.iso (functorToAction F) gZ
let u' : ∐ f ≅ ∐ fun i => (functorToAction F).obj (gZ i) := Sigma.mapIso gu
have heq : (functorToAction F).map (Sigma.desc gf) = (t.symm ≪≫ u' ≪≫ is2.symm).inv ≫ i :=
by
simp only [Iso.trans_inv, Iso.symm_inv, Category.assoc]
rw [← Iso.inv_comp_eq]
refine Sigma.hom_ext _ _ (fun j ↦ ?_)
suffices (functorToAction F).map (gf j) = (gu j).inv ≫ i' j by simpa [is2, u']
simp only [h, Iso.inv_hom_id_assoc]
refine ⟨∐ gZ, Sigma.desc gf, t.symm ≪≫ u' ≪≫ is2.symm, ?_, by simp [heq]⟩
· exact mono_of_mono_map (functorToAction F) (heq ▸ mono_comp _ _)
