Definitions/Def_GroupCohomology_LevelSubgroup.lean

Fix a group G together with a homomorphism r \colon G \to (\overline{\mathbb Q} \simeq_{\mathrm{alg}[\mathbb Q]} \overline{\mathbb Q}) into the group of \mathbb Q-algebra automorphisms of a chosen algebraic closure of \mathbb Q, and let F be an intermediate field of \overline{\mathbb Q}/\mathbb Q. The object studied throughout is the subgroup r^{-1}(\mathrm{Gal}(\overline{\mathbb Q}/F)) \le G, written in Lean as the Subgroup.comap of Mathlib's IntermediateField.fixingSubgroup of F along r; it is the set of g \in G whose image r(g) fixes F pointwise.

Four facts about this subgroup are recorded. First, comap_fixingSubgroup_eq_ker: if F is normal over \mathbb Q, then r^{-1}(\mathrm{Gal}(\overline{\mathbb Q}/F)) is exactly the kernel of the composite of r with the restriction homomorphism \mathrm{Aut}_{\mathbb Q}(\overline{\mathbb Q}) \to \mathrm{Aut}_{\mathbb Q}(F) given by AlgEquiv.restrictNormalHom, i.e. the kernel of G \to \mathrm{Gal}(F/\mathbb Q). Second and third, two consequences of this identification are registered as typeclass instances, so that they are available automatically wherever the subgroup occurs: for F normal over \mathbb Q the subgroup is normal in G (normal_comap_fixingSubgroup), and for F in addition finite-dimensional over \mathbb Q it has finite index (finiteIndex_comap_fixingSubgroup), the quotient embedding into the finite group \mathrm{Gal}(F/\mathbb Q). Fourth, comap_fixingSubgroup_antitone records the order reversal in F: if F \le F' then r^{-1}(\mathrm{Gal}(\overline{\mathbb Q}/F')) \le r^{-1}(\mathrm{Gal}(\overline{\mathbb Q}/F)), so the subgroups shrink as the field grows. No topology on G or on the Galois group enters; the fixing subgroups are taken as abstract subgroups and r as an abstract homomorphism.