English
For every open subgroup V of Aut F, there exists an object X in C such that F.obj X is isomorphic to Aut F modulo V as Aut F-sets.
Русский
Для каждой открытой подгруппы V в Aut F существует объект X в C такой, что F.obj X изоморфно Aut F / V как Aut F-множества.
LaTeX
$$$\\forall V \\in \\mathrm{OpenSubgroup}(\\mathrm{Aut}\\,F): \\ \\exists X:\\, C, \\ F.obj X \\cong \\mathrm{Aut}\\,F / V$$$
Lean4
/-- If `X` is a finite discrete `G`-set, it can be written as the finite disjoint union
of quotients of the form `G ⧸ Uᵢ` for open subgroups `(Uᵢ)`. Note that this
is simply the decomposition into orbits. -/
theorem has_decomp_quotients (X : Action FintypeCat G) [TopologicalSpace X.V] [DiscreteTopology X.V]
[ContinuousSMul G X.V] :
∃ (ι : Type) (_ : Finite ι) (f : ι → OpenSubgroup (G)), Nonempty ((∐ fun i ↦ G ⧸ₐ (f i).toSubgroup) ≅ X) :=
by
obtain ⟨ι, hf, f, u, hc⟩ := has_decomp_connected_components' X
letI (i : ι) : TopologicalSpace (f i).V := ⊥
haveI (i : ι) : DiscreteTopology (f i).V := ⟨rfl⟩
have (i : ι) : ContinuousSMul G (f i).V :=
ContinuousSMul.mk <| by
let r : f i ⟶ X := Sigma.ι f i ≫ u.hom
let r'' (p : G × (f i).V) : G × X.V := (p.1, r.hom p.2)
let q (p : G × X.V) : X.V := X.ρ p.1 p.2
let q' (p : G × (f i).V) : (f i).V := (f i).ρ p.1 p.2
have heq : q ∘ r'' = r.hom ∘ q' := by
ext (p : G × (f i).V)
exact (congr_fun (r.comm p.1) p.2).symm
have hrinj : Function.Injective r.hom :=
(ConcreteCategory.mono_iff_injective_of_preservesPullback r).mp <| mono_comp _ _
let t₁ : TopologicalSpace (G × (f i).V) := inferInstance
change @Continuous _ _ _ ⊥ q'
have : TopologicalSpace.induced r.hom inferInstance = ⊥ :=
by
rw [← le_bot_iff]
exact fun s _ ↦ ⟨r.hom '' s, ⟨isOpen_discrete (r.hom '' s), Set.preimage_image_eq s hrinj⟩⟩
rw [← this, continuous_induced_rng, ← heq]
exact Continuous.comp continuous_smul (by fun_prop)
have (i : ι) : ∃ (U : OpenSubgroup (G)), (Nonempty ((f i) ≅ G ⧸ₐ U.toSubgroup)) :=
by
obtain ⟨(x : (f i).V)⟩ := nonempty_fiber_of_isConnected (forget₂ _ _) (f i)
let U : OpenSubgroup (G) := ⟨MulAction.stabilizer (G) x, stabilizer_isOpen (G) x⟩
letI : Fintype (G ⧸ MulAction.stabilizer (G) x) := fintypeQuotient U
exact ⟨U, ⟨FintypeCat.isoQuotientStabilizerOfIsConnected (f i) x⟩⟩
choose g ui using this
exact ⟨ι, hf, g, ⟨(Sigma.mapIso (fun i ↦ (ui i).some)).symm ≪≫ u⟩⟩
