Splits a Ramification group to union of difference set.

Stream: new members

[Junjie Bai]

I got a series of Ramification groups, say $G_i$, and I want to split $G_(-1)$, the Galois group, as some difference set like $G_i/G_(I + 1)$, till $G_n$ for some n, Is there any theorem can do this?

[Kevin Buzzard]

You can ask for the sup of the j such that x \in G j, is that what you're looking for?

[Junjie Bai]

I'm so sorry that I didn't state my question clearly, let me be more clear. I got a group $G$, and a filtration of normal group $G_i$, I want to prove that $G = \cup_{i \le n} G_i \cup G_{n+1}$, here is my statement, I want to know how can I prove this?

theorem G_split (n : ℤ)  (h : (PairwiseDisjoint (↑(Finset.Icc (-1) (n - 1))) (G_diff K L))) : (⊤ : Finset (L ≃ₐv[K] L)) = (disjiUnion (Finset.Icc (-1) (n - 1)) (G_diff K L) h) ∪ (G(L/K)_[n] : Set (L ≃ₐv[K] L)).toFinset := by sorry

[Kevin Buzzard]

Can you make a #mwe ?