Library mathcomp.solvable.finmodule

This file regroups constructions and results that are based on the most primitive version of representation theory -- viewing an abelian group as the additive group of a (finite) Z-module. This includes the Gaschutz splitting and transitivity theorem, from which we will later derive the Schur-Zassenhaus theorem and the elementary abelian special case of Maschke's theorem, the coprime abelian centraliser/commutator trivial intersection theorem, which is used to show that p-groups under coprime action factor into special groups, and the construction of the transfer homomorphism and its expansion relative to a cycle, from which we derive the Higman Focal Subgroup and the Burnside Normal Complement theorems. The definitions and lemmas for the finite Z-module induced by an abelian are packaged in an auxiliary FiniteModule submodule: they should not be needed much outside this file, which contains all the results that exploit this construction. FiniteModule defines the Z[N(A) ]-module associated with a finite abelian abelian group A, given a proof (abelA : abelian A) : fmod_of abelA == the type of elements of the module (similar to but distinct from [subg A]). fmod abelA x == the injection of x into fmod_of abelA if x \in A, else 0 fmval u == the projection of u : fmod_of abelA onto A u ^@ x == the action of x \in 'N(A) on u : fmod_of abelA The transfer morphism is be constructed from a morphism f : H >-> rT, and a group G, along with the two assumptions sHG : H \subset G and abfH : abelian (f @* H): transfer sGH abfH == the function gT -> FiniteModule.fmod_of abfH that implements the transfer morphism induced by f on G. The Lemma transfer_indep states that the transfer morphism can be expanded using any transversal of the partition HG := rcosets H G of G. Further, for any g \in G, HG :* < [g]> is also a partition of G (Lemma rcosets_cycle_partition), and for any transversal X of HG :* < [g]> the function r mapping x : gT to rcosets (H :* x) < [g]> is (constructively) a bijection from X to the < [g]>-orbit partition of HG, and Lemma transfer_pcycle_def gives a simplified expansion of the transfer morphism.

Still allow ring notations, but give priority to groups now.

This is the TI part of B & G, Proposition 1.6(d). We go with B & G rather than Aschbacher and will derive 1.6(e) from (d), rather than the converse, because the derivation of 24.6 from 24.3 in Aschbacher requires a separate reduction to p-groups to yield 1.6(d), making it altogether longer than the direct Gaschutz-style proof. This Lemma is used in maximal.v for the proof of Aschbacher 24.7.

This is Aschbacher (37.2).

This is Aschbacher (37.1).