English
There exists a lift of a mono Y → functorToAction F.obj X through some Z with an isomorphism Y ≅ functorToAction F.obj Z, whenever Y is connected.
Русский
Существaет подъём моно-отрезка Y → functorToAction F.obj X через Z, если Y связано, и существует изоморфизм Y ≅ functorToAction F.obj Z.
LaTeX
$$$\\exists Z:\\, C, \\exists f:\\, Z \\to X, \\exists u:\\, Y \\cong (\\mathrm{functorToAction} F).obj Z, \\text{Mono } f \\land i = u.hom \\circ (\\mathrm{functorToAction} F).map f$$$
Lean4
/-- If `X` is a connected `G`-set and `x` is an element of `X`, `X` is isomorphic
to the quotient of `G` by the stabilizer of `x` as `G`-sets. -/
noncomputable def isoQuotientStabilizerOfIsConnected (X : Action FintypeCat G) [IsConnected X] (x : X.V)
[Fintype (G ⧸ (MulAction.stabilizer G x))] : X ≅ G ⧸ₐ MulAction.stabilizer G x :=
haveI : MulAction.IsPretransitive G X.V := Action.pretransitive_of_isConnected G X
let e : X.V ≃ G ⧸ MulAction.stabilizer G x :=
(Equiv.Set.univ X.V).symm.trans <|
(Equiv.setCongr ((MulAction.orbit_eq_univ G x).symm)).trans <| MulAction.orbitEquivQuotientStabilizer G x
Iso.symm <|
Action.mkIso (FintypeCat.equivEquivIso e.symm) <| fun σ : G ↦
by
ext (a : G ⧸ MulAction.stabilizer G x)
obtain ⟨τ, rfl⟩ := Quotient.exists_rep a
exact mul_smul σ τ x
