Cyclic quotients separating subgroups of finite abelian groups

If A < B are subgroups of a finite abelian group, there is a cyclic quotient in which the image of A is trivial and the image of B is nontrivial. Applied to two successive filtration steps, this detects a strict decrease in a cyclic quotient.

The construction uses Mathlib's character-separation theorem CommGroup.forall_monoidHom_apply_eq_one_iff: a character valued in the units of an algebraic closure of ℚ kills A but not an element of B. Its finite image is cyclic.

theorem TauCeti.exists_isCyclic_quotient_of_lt {G : Type u_1} [CommGroup G] [Finite G] {A B : Subgroup G} (h : A < B) : ∃ (H : Subgroup G), A ≤ H ∧ ¬B ≤ H ∧ IsCyclic (G ⧸ H)

A strict inclusion of subgroups of a finite abelian group is detected by a cyclic quotient: the smaller subgroup is killed, but the larger one is not.