Frobenius group determinant

DefinitionGroup matrix#✓fully proved

For a finite group \(G\), the group matrix of Dedekind and Frobenius is the \(G \times G\) matrix over the polynomial ring \(\mathbb{C}[x_g : g \in G]\) whose entry at \((g, h)\) is the variable \(x_{gh}\).

noncomputable def groupMatrix (G : Type*) [Group G] [Fintype G] [DecidableEq G] :
    Matrix G G (MvPolynomial G ℂ) :=
  fun g h => MvPolynomial.X (g * h)

Used by 1

Used byGroup determinant

DefinitionGroup determinant#✓fully proved

For a finite group \(G\), the group determinant \(\Theta(G)\) is the determinant of the group matrix of \(G\), the \(G \times G\) matrix over \(\mathbb{C}[x_g : g \in G]\) whose entry at \((g, h)\) is the variable \(x_{gh}\); it is a polynomial in these variables.

noncomputable def groupDeterminant (G : Type*) [Group G] [Fintype G] [DecidableEq G] :
    MvPolynomial G ℂ :=
  (groupMatrix G).det

Uses 1 · Used by 1

Statement usesGroup matrix

Used byFrobenius determinant theorem

TheoremFrobenius determinant theorem#●ready to prove

Let \(G\) be a finite group and let \(r\) be the number of conjugacy classes of \(G\). Then there exist polynomials \(p_1, \dots, p_r\) in \(\mathbb{C}[x_g : g \in G]\) such that each \(p_j\) is irreducible, \(p_i\) and \(p_j\) are not associated for \(i \neq j\), and the group determinant of \(G\) equals \(\prod_{j=1}^{r} p_j^{\deg p_j}\), where \(\deg p_j\) is the total degree of \(p_j\).

public theorem_wanted frobenius_group_determinant
    (G : Type*) [Group G] [Fintype G] [DecidableEq G] :
    ∃ (r : ℕ) (p : Fin r → MvPolynomial G ℂ),
      r = Nat.card (ConjClasses G) ∧
      (∀ j, Irreducible (p j)) ∧
      (∀ i j, i ≠ j → ¬ Associated (p i) (p j)) ∧
      groupDeterminant G = ∏ j, (p j) ^ (p j).totalDegree

Sources

• Knill, Some fundamental theorems in mathematics, §171. Problem frobenius_group_determinant of the lean-eval benchmark.

Uses 1

Statement usesGroup determinant

2 fully proved1 ready to prove

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.