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
New area, not yet in the Verso blueprint — links go to the LMFDB knowls.
Goal
Define Gassmann equivalence of two subgroups
H₁, H₂ ≤ G:|C ∩ H₁| = |C ∩ H₂|for every conjugacy classCofG; 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
ConjClasses,Subgroup, permutation/MonoidAlgebrarepresentations,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 groupG, Gassmann-equivalent point-stabilisers ⇒ equal zeta functions.Test cases
32(orGL(3,2)index-7) Gassmann triple giving non-isomorphic arithmetically equivalent fields.LMFDB targets
group.gassmann_equivalencenf.arithmetically_equivalentgroup.conjugacy_classNew area, not yet in the Verso blueprint — links go to the LMFDB knowls.