Finite decreasing filtrations of groups

An antitone sequence of subgroups whose first term is finite eventually stabilizes at its intersection. In particular, it is eventually trivial whenever its intersection is trivial. This elementary observation is useful for ramification filtrations.

Main results

• TauCeti.Subgroup.exists_forall_eq_iInf_of_antitone: a decreasing filtration with finite first term eventually equals its intersection.
• TauCeti.Subgroup.exists_forall_eq_bot_of_antitone_iInf_eq_bot: a decreasing filtration with finite first term and trivial intersection is eventually trivial.

theorem TauCeti.Subgroup.exists_forall_eq_iInf_of_antitone {G : Type u_1} [Group G] (f : ℕ → Subgroup G) (hf : Antitone f) [Finite ↥(f 0)] : ∃ (N : ℕ), ∀ (i : ℕ), N ≤ i → f i = ⨅ (j : ℕ), f j

An antitone sequence of subgroups with finite first term eventually equals its intersection.

theorem TauCeti.Subgroup.exists_forall_eq_bot_of_antitone_iInf_eq_bot {G : Type u_1} [Group G] (f : ℕ → Subgroup G) (hf : Antitone f) [Finite ↥(f 0)] (hInf : ⨅ (i : ℕ), f i = ⊥) : ∃ (N : ℕ), ∀ (i : ℕ), N ≤ i → f i = ⊥

An antitone sequence of subgroups with finite first term and trivial intersection is eventually the trivial subgroup.