(Joint Center)Library PFsection1

(* (c) Copyright Microsoft Corporation and Inria. All rights reserved. *)
Require Import ssreflect ssrbool ssrfun eqtype ssrnat seq path div choice.
Require Import fintype tuple finfun bigop prime ssralg finset fingroup morphism.
Require Import perm automorphism quotient action zmodp center commutator.
Require Import poly cyclic pgroup nilpotent matrix mxalgebra mxrepresentation.
Require Import vector falgebra fieldext ssrnum algC rat algnum galois.
Require Import classfun character inertia integral_char vcharacter.
Require ssrint.

This file covers Peterfalvi, Section 1: Preliminary results.

Set Implicit Arguments.

Import GroupScope GRing.Theory Num.Theory.
Local Open Scope ring_scope.

Local Notation algCF := [fieldType of algC].

Section Main.

Variable gT : finGroupType.

This is Peterfalvi (1.1).
Lemma odd_eq_conj_irr1 (G : {group gT}) t :
  odd #|G|(('chi[G]_t)^*%CF == 'chi_t) = ('chi_t == 1).

Variables G H : {group gT}.

This is Peterfalvi (1.2).
Lemma not_in_ker_char0 t g : g \in G
  H <| G~~ (H \subset cfker 'chi[G]_t)'C_H[g] = 1%g'chi_t g = 0.

This is Peterfalvi (1.3)(a).
Lemma equiv_restrict_compl A m (Phi : m.-tuple 'CF(H)) (mu : 'CF(G)) d :
    H \subset GA <| Hbasis_of 'CF(H, A) Phi
  ({in A, mu =1 \sum_i d i *: 'chi_i}
    ( j : 'I_m,
        \sum_i '[Phi`_j, 'chi_i] × (d i)^* = '['Ind[G] Phi`_j, mu])).

This is Peterfalvi (1.3)(b).
Lemma equiv_restrict_compl_ortho A m (Phi : m.-tuple 'CF(H)) mu_ :
    H \subset GA <| Hbasis_of 'CF(H, A) Phi
     ( i j, '[mu_ i, mu_ j] = (i == j)%:R) →
     ( j : 'I_m, 'Ind[G] Phi`_j = \sum_i '[Phi`_j, 'chi_i] *: mu_ i) →
   [/\ i, {in A, mu_ i =1 'chi_i}
     & mu, ( i, '[mu, mu_ i] = 0) → {in A, x, mu x = 0}].

Let vchar_isometry_base3 f f' :
  f \in 'Z[irr G, G^#]'[f]_G = 2%:R
  f' \in 'Z[irr G, G^#]'[f']_G = 2%:R
  '[f, f'] = 1 →
    es : _ × bool, let: (i, j, k, epsilon) := es in
     [/\ f = (-1) ^+ epsilon *: ('chi_j - 'chi_i),
          f' = (-1) ^+ epsilon *: ('chi_j - 'chi_k)
        & uniq [:: i; j; k]].

Let vchar_isometry_base4 (eps : bool) i j k n m :
    let f1 := 'chi_j - 'chi_i in
    let f2 := 'chi_k - 'chi_i in
    let f3 := 'chi_n - 'chi_m in
    j != k'[f3, f1]_G = (-1) ^+ eps'[f3, f2] = (-1) ^+ eps
  if eps then n == i else m == i.

This is Peterfalvi (1.4).
Lemma vchar_isometry_base m L (Chi : m.-tuple 'CF(H))
                            (tau : {linear 'CF(H)'CF(G)}) :
    (1 < m)%N{subset Chi irr H}free Chi
    ( chi, chi \in Chichi 1%g = Chi`_0 1%g) →
    ( i : 'I_m, (Chi`_i - Chi`_0) \in 'CF(H, L)) →
    {in 'Z[Chi, L], isometry tau, to 'Z[irr G, G^#]}
    exists2 mu : m.-tuple (Iirr G),
      uniq mu
    & epsilon : bool, i : 'I_m,
      tau (Chi`_i - Chi`_0) = (-1) ^+ epsilon *: ('chi_(mu`_i) - 'chi_(mu`_0)).

This is Peterfalvi (1.5)(a).
Lemma cfResInd_sum_cfclass t : H <| G
  'Res[H] ('Ind[G] 'chi_t)
     = #|'I_G['chi_t] : H|%:R *: \sum_(xi <- ('chi_t ^: G)%CF) xi.

This is Peterfalvi (1.5)(b), main formula.
This is Peterfalvi (1.5)(b), irreducibility remark.
This is Peterfalvi (1.5)(c).
Lemma cfclass_Ind_cases t1 t2 : H <| G
   if 'chi_t2 \in ('chi[H]_t1 ^: G)%CF
   then 'Ind[G] 'chi_t1 = 'Ind[G] 'chi_t2
   else '['Ind[G] 'chi_t1, 'Ind[G] 'chi_t2] = 0.

Useful consequences of (1.5)(c)
Lemma not_cfclass_Ind_ortho i j :
    H <| G → ('chi_i \notin 'chi_j ^: G)%CF
  '['Ind[G, H] 'chi_i, 'Ind[G, H] 'chi_j] = 0.

Lemma cfclass_Ind_irrP i j :
    H <| G
  reflect ('Ind[G, H] 'chi_i = 'Ind[G, H] 'chi_j) ('chi_i \in 'chi_j ^: G)%CF.

Lemma card_imset_Ind_irr (calX : {set Iirr H}) :
    H <| G{in calX, i, 'Ind 'chi_i \in irr G}
    {in calX & G, i y, conjg_Iirr i y \in calX}
  #|calX| = (#|G : H| × #|[set cfIirr ('Ind[G] 'chi_i) | i in calX]|)%N.

This is Peterfalvi (1.5)(d).
Lemma scaled_cfResInd_sum_cfclass t : H <| G
  let chiG := 'Ind[G] 'chi_t in
  (chiG 1%g / '[chiG]) *: 'Res[H] chiG
     = #|G : H|%:R *: (\sum_(xi <- ('chi_t ^: G)%CF) xi 1%g *: xi).

This is Peterfalvi (1.5)(e).
Lemma odd_induced_orthogonal t :
     H <| Godd #|G|t != 0 →
  '['Ind[G, H] 'chi_t, ('Ind[G] 'chi_t)^*] = 0.

This is Peterfalvi (1.6)(a).
Some consequences and related results.
This is a stronger version of Peterfalvi (1.6)(b).
Lemma cfIndMod (K : {group gT}) (phi : 'CF(H / K)) :
    K \subset HH \subset GK <| G
  'Ind[G] (phi %% K)%CF = ('Ind[G / K] phi %% K)%CF.

Lemma cfIndQuo (K : {group gT}) (phi : 'CF(H)) :
    K \subset cfker phiH \subset GK <| G
  'Ind[G / K] (phi / K)%CF = ('Ind[G] phi / K)%CF.

Section IndSumInertia.

Variable s : Iirr H.

Let theta := 'chi_s.
Let T := 'I_G[theta].
Let calA := irr_constt ('Ind[T] theta).
Let calB := irr_constt ('Ind[G] theta).
Let AtoB (t : Iirr T) := Ind_Iirr G t.
Let e_ t := '['Ind theta, 'chi[T]_t].

Hypothesis nsHG: H <| G.

This is Peterfalvi (1.7)(a).
Lemma cfInd_sum_Inertia :
  [/\ {in calA, t, 'Ind 'chi_t \in irr G},
      {in calA, t, 'chi_(AtoB t) = 'Ind 'chi_t},
      {in calA &, injective AtoB},
      AtoB @: calA =i calB
    & 'Ind[G] theta = \sum_(t in calA) e_ t *: 'Ind 'chi_t].

Hypothesis abTbar : abelian (T / H).

This is Peterfalvi (1.7)(b).
Lemma cfInd_central_Inertia :
   exists2 e, [/\ e \in Cnat, e != 0 & {in calA, t, e_ t = e}]
           & [/\ 'Ind[G] theta = e *: \sum_(j in calB) 'chi_j,
                 #|calB|%:R = #|T : H|%:R / e ^+ 2
               & {in calB, i, 'chi_i 1%g = #|G : T|%:R × e × theta 1%g}].

This is Peterfalvi (1.7)(c).
Lemma cfInd_Hall_central_Inertia :
     Hall T H
  [/\ 'Ind[G] theta = \sum_(i in calB) 'chi_i, #|calB| = #|T : H|
    & {in calB, i, 'chi_i 1%g = #|G : T|%:R × theta 1%g}].

End IndSumInertia.

This is Peterfalvi (1.8).
Lemma irr1_bound_quo (B C D : {group gT}) i :
    B <| CB \subset cfker 'chi[G]_i
    B \subset DD \subset CC \subset G → (D / B \subset 'Z(C / B))%g
  'chi_i 1%g #|G : C|%:R × sqrtC #|C : D|%:R.

This is Peterfalvi (1.9)(a).
Lemma extend_coprime_Qn_aut a b (Qa Qb : fieldExtType rat) w_a w_b
          (QaC : {rmorphism QaalgC}) (QbC : {rmorphism QbalgC})
          (mu : {rmorphism algCalgC}) :
    coprime a b
    a.-primitive_root w_a <<1; w_a>>%VS = {:Qa}%VS
    b.-primitive_root w_b <<1; w_b>>%VS = {:Qb}%VS
  {nu : {rmorphism algCalgC} | x, nu (QaC x) = mu (QaC x)
                                 & y, nu (QbC y) = QbC y}.

This intermediate result in the proof of Peterfalvi (1.9)(b) is used in he proof of (3.9)(c).
Lemma dvd_restrict_cfAut a (v : {rmorphism algCalgC}) :
  exists2 u : {rmorphism algCalgC},
     gT0 G0 chi x,
      chi \in 'Z[irr (@gval gT0 G0)]#[x] %| au (chi x) = v (chi x)
  & chi x, chi \in 'Z[irr G]coprime #[x] au (chi x) = chi x.

This is Peterfalvi (1.9)(b). We have strengthened the statement of this lemma so that it can be used rather than reproved for Peterfalvi (3.9). In particular we corrected a quantifier inversion in the original statement: the automorphism is constructed uniformly for all (virtual) characters. We have also removed the spurrious condition that a be a \pi(a) part of #|G| -- the proof works for all a, and indeed the first part holds uniformaly for all groups!
Lemma make_pi_cfAut a k :
    coprime k a
  exists2 u : {rmorphism algCalgC},
     (gT0 : finGroupType) (G0 : {group gT0}) chi x,
      chi \in 'Z[irr G0]#[x] %| acfAut u chi x = chi (x ^+ k)%g
  & chi x, chi \in 'Z[irr G]coprime #[x] acfAut u chi x = chi x.

Section ANT.
Import ssrint.

This section covers Peterfalvi (1.10). We have simplified the statement somewhat by substituting the global ring of algebraic integers for the specific ring Z[eta]. Formally this amounts to strengthening (b) and weakening (a) accordingly, but since actually the Z[eta] is equal to the ring of integers of Q[eta] (cf. Theorem 6.4 in J.S. Milne's course notes on Algebraic Number Theory), the simplified statement is actually equivalent to the textbook one.
Variable (p : nat) (eps : algC).
Hypothesis (pr_eps : p.-primitive_root eps).
Local Notation e := (1 - eps).

This is Peterfalvi (1.10) (a).
Lemma vchar_ker_mod_prim : {in G & G & 'Z[irr G], x y (chi : 'CF(G)),
  #[x] = py \in 'C[x]chi (x × y)%g == chi y %[mod e]}%A.

This is Peterfalvi (1.10)(b); the primality condition is only needed here.
Lemma int_eqAmod_prime_prim n :
  prime pn \in Cint → (n == 0 %[mod e])%A → (p %| n)%C.

End ANT.

End Main.