Groups: Gassmann equivalence (and arithmetically equivalent fields)

[CBirkbeck]

Goal

Define Gassmann equivalence of two subgroups H₁, H₂ ≤ G: |C ∩ H₁| = |C ∩ H₂| for every conjugacy class C of G; equivalently ℚ[H₁\\G] ≅ ℚ[H₂\\G] as ℚ[G]-modules. This is the group-theoretic source of arithmetically equivalent number fields (same Dedekind zeta).

What already exists

• mathlib: ConjClasses, Subgroup, permutation/MonoidAlgebra representations, MulAction. Number-field side: Dedekind zeta (NumberField.DedekindZeta).

What's missing

• GassmannEquiv H₁ H₂ : Prop (the conjugacy-class-intersection condition) and the equivalence with isomorphism of the rational permutation modules; the link to arithmetically equivalent fields (nf.arithmetically_equivalent): same Galois group G, Gassmann-equivalent point-stabilisers ⇒ equal zeta functions.

Test cases

• The classic order-32 (or GL(3,2) index-7) Gassmann triple giving non-isomorphic arithmetically equivalent fields.

LMFDB targets

• group.gassmann_equivalence
• nf.arithmetically_equivalent
• group.conjugacy_class

New area, not yet in the Verso blueprint — links go to the LMFDB knowls.