Fixed fields and fixing subgroups #
Complements to Mathlib's Galois correspondence: its interaction with the complete-lattice
operations, when a fixed field and an intermediate field generate the whole extension, when the
correspondence survives dropping finiteness of M / K for a finite subgroup, and what the
correspondence gives for a cyclic subgroup.
Taking fixed fields always sends joins of automorphism subgroups to intersections of intermediate fields. For a finite Galois extension it also sends subgroup intersections to composita of fixed fields. Both the binary and indexed forms are recorded so that finite generating families and arbitrary families can use these lattice laws without manually passing through the order dual in the Galois correspondence.
For a finite Galois extension M / K, a subgroup H ≤ Gal(M/K) and an intermediate field E,
the fixed field of H and E generate M exactly when H meets the fixers of E trivially.
With no hypothesis on M / K, the fixers of an arbitrary join of intermediate fields are the
automorphisms fixing each of them.
The correspondence is equivariant for conjugation: the fixed field of a conjugate subgroup is the image of the fixed field under the conjugating automorphism.
The correspondence between subgroups and their fixed fields also holds with no hypothesis on
M / K at all, provided the subgroup is finite: Artin's theorem makes M finite Galois over the
fixed field of a finite H, and the fixers of that field are then exactly H. This is how a
subgroup of the automorphism group of an infinite extension is recovered from the field it cuts
out; the fixing subgroup of a subfield of finite degree is finite for the same reason.
The last results specialise the correspondence to a cyclic subgroup: the field fixed by a finite
cyclic group of automorphisms has M cyclic over it, and for ⟨σ⟩ there is a named automorphism
over the fixed field — AlgEquiv.toFixedFieldAlgEquiv σ acts on M as σ does, and generates
once ⟨σ⟩ is finite.
Neither M / K Galois nor M / K finite is needed, and neither is faithfulness of the action:
FixedPoints.toAlgAut_surjective asks only that the group be finite, and cyclicity passes along
its surjection. The fixed-point subfield it produces is the one underlying
IntermediateField.fixedField.
A simple extension K⟮x⟯ is fixed pointwise by exactly those automorphisms that fix x, so
its fixing subgroup is the stabilizer of x; this too needs no hypothesis on M / K at all.
Two facts hold for every intermediate field E algebraic over K, with no separability anywhere
and nothing asked of M / K: its fixing subgroup is closed in the Krull topology, being the
intersection over the finite simple subextensions of their open fixing subgroups; and it is
unchanged by cutting E down to its part inside separableClosure K M, because every element of
E has a q-th power iterate there. The second is why a Galois correspondence over an
inseparable extension can only be indexed by the intermediate fields of the separable closure.
Main results #
Subgroup.fixedField_infandSubgroup.fixedField_supSubgroup.fixedField_iInfandSubgroup.fixedField_iSupSubgroup.fixedField_sup_eq_top_iffSubgroup.fixedField_map_conjIntermediateField.fixingSubgroup_infIntermediateField.fixingSubgroup_iSupIntermediateField.fixingSubgroup_isClosed_of_isAlgebraicIntermediateField.fixingSubgroup_inf_separableClosureIntermediateField.fixingSubgroup_fixedField_of_finiteIntermediateField.finiteDimensional_fixedField,IntermediateField.isGalois_fixedFieldandIntermediateField.finrank_fixedField_eq_natCard: Artin's theorem on the fixed field of a finite subgroup, with no hypothesis onM / KIntermediateField.finite_of_finiteDimensional_fixedFieldIntermediateField.card_fixingSubgroup_leIntermediateField.fixingSubgroup_adjoin_simple, withIntermediateField.mem_fixedField_stabilizer,IntermediateField.fixedField_stabilizer_eq_adjoin_simple,IntermediateField.fixedField_iInf_stabilizer_eq_adjoin_rangeandIntermediateField.adjoin_eq_top_of_fixedField_stabilizer: the stabilizer ofxfixes exactlyK⟮x⟯, in whichxis a primitive elementFixedPoints.isCyclic_algEquivAlgEquiv.toFixedFieldAlgEquiv, withAlgEquiv.zpowers_toFixedFieldAlgEquiv_eq_topandAlgEquiv.card_algEquiv_fixedField_zpowersTauCeti.natCard_algEquiv_dvd_finrank: the automorphism group of a finite extension has order dividing the degree, since that order is the degree over the field fixed by all automorphisms
The degree of a cyclic fixed field times the order of its generator is the total degree.
The fixed field of a common intersection is the compositum of the fixed fields. This is
the indexed Galois-lattice law: an element fixed by every automorphism common to all H i lies in
the field generated by the individual fixed fields.
The fixed field of the subgroups generated by a family is their common fixed field. This
direction, like Subgroup.fixedField_sup, needs no finiteness or Galois hypothesis. At the level
of carriers, this is fixedPoints_subgroup_iSup.
The fixed field of an intersection is the compositum of the fixed fields. For a finite Galois extension, the Galois correspondence reverses binary meets and joins.
The fixed field of generated subgroups is the intersection of their fixed fields. This
direction needs no finiteness or Galois hypothesis: fixing every generator is exactly fixing the
subgroup they generate. At the level of carriers, this is fixedPoints_subgroup_sup.
A trivial meet of subgroups is a full join of fields. M ^ H and E generate M exactly
when H ⊓ Gal(M/E) is trivial.
This is the Galois correspondence read in both directions: fixingSubgroup turns a join of fields
into a meet of subgroups, and fixedField turns the trivial subgroup back into ⊤.
Stated in the Subgroup namespace rather than IntermediateField, so that H — the first
explicit argument, and the one fixedField is applied to — carries the dot notation: a consumer
writes H.fixedField_sup_eq_top_iff E.
The Galois correspondence turns a meet of fields into a join of subgroups. In a finite
Galois extension, the automorphisms fixing E ⊓ E' pointwise form the subgroup generated by those
fixing E and those fixing E'. The dual IntermediateField.fixingSubgroup_sup holds with no
hypothesis on M / K; this direction needs the full correspondence.
The fixing subgroup of a join of fields is the meet of the fixing subgroups. An
automorphism fixes ⨆ i, E i pointwise exactly when it fixes every E i pointwise. This is the
indexed form of Mathlib's IntermediateField.fixingSubgroup_sup, and like it needs no hypothesis
on M / K.
The fixing subgroup of an algebraic intermediate field is closed for the Krull topology:
E is the join of the simple extensions it contains, each of them finite over K, so
E.fixingSubgroup is the intersection of the open subgroups K⟮x⟯.fixingSubgroup.
Mathlib's IntermediateField.fixingSubgroup_isClosed is the case of a finite E / K, where the
subgroup is even open, and InfiniteGalois.fixingSubgroup_isClosed is the case of a Galois
M / K. Algebraicity of E / K alone suffices — nothing is asked of M / K, so E may be an
algebraic subfield of a transcendental extension, and over an algebraic M / K the hypothesis is
supplied by IntermediateField.isAlgebraic_tower_bot. The suffix names that hypothesis, as
MulAction.stabilizer_isOpen_of_isIntegral does.
A fixing subgroup sees only the separable closure. For an intermediate field E algebraic
over K a K-automorphism of M fixing E ⊓ separableClosure K M pointwise already fixes E
pointwise, because every x ∈ E has a power x ^ q ^ n in that intersection, q the exponential
characteristic of K.
So an intermediate field outside the separable closure is invisible to the correspondence between
fixing subgroups and fields: it has the same fixing subgroup as its separable part. Like
IntermediateField.fixingSubgroup_isClosed_of_isAlgebraic this asks nothing of M / K; the power
is produced inside E, where separableClosure K E is what the elements of E are purely
inseparable over.
A finite group of automorphisms is the whole fixing subgroup of its fixed field. Every
K-automorphism of M that fixes M ^ H pointwise already lies in H.
Mathlib's IntermediateField.fixingSubgroup_fixedField is the same conclusion under
[FiniteDimensional K M], which is the stronger hypothesis: a finite-dimensional M / K has a
finite automorphism group, so every subgroup of it is finite. Finiteness of H is what an
infinite extension M / K can still supply.
Artin's theorem: M is finite over the field fixed by a finite group of automorphisms.
Mathlib has this for FixedPoints.subfield H M; the fixed field of the Galois correspondence is
the same subfield, and this is the instance on that form, with no hypothesis on M / K.
Artin's theorem: M is Galois over the field fixed by a finite group of automorphisms,
Mathlib's IsGalois.of_fixed_field on the fixed field of the Galois correspondence.
Artin's theorem, degree form: the degree of M over the field fixed by a finite group of
automorphisms is the order of the group.
Mathlib's IntermediateField.finrank_fixedField_eq_card is the same conclusion under
[FiniteDimensional K M], which a subgroup of the automorphism group of an infinite extension does
not supply.
An intermediate field of finite degree has a finite fixing subgroup, being a copy of the automorphism group of a finite extension.
A group of automorphisms whose fixed field has finite degree is finite. Thus a subgroup of
K-automorphisms cannot be infinite when its fixed field has finite degree in M.
The fixing subgroup of an intermediate field of finite degree is no larger than that degree, the bound on the automorphisms of a finite extension.
The fixing subgroup of a simple extension is the stabilizer of its generator. A
K-automorphism of M is determined on K⟮x⟯ by its value at x, so fixing K⟮x⟯ pointwise is
fixing x; no hypothesis on M / K is needed, and x need not be algebraic.
This is what turns a statement about the action of Gal(M/K) on a set of elements of M into a
statement about the Galois correspondence.
The common stabilizer of a family fixes exactly the field generated by that family. For a
Galois extension, intersecting the point stabilizers of x i cuts out K(Set.range x). This is
the family form of fixedField_stabilizer_eq_adjoin_simple.
The Galois correspondence is conjugation-equivariant. The fixed field of the conjugate
subgroup σ H σ⁻¹ is the image under σ of the fixed field of H.
Stated in the Subgroup namespace, so that H — the first explicit argument, and the one
fixedField is applied to — carries the dot notation.
The fixed subfield of a finite cyclic group action has cyclic Galois group. For a finite
cyclic group G acting on a field F by ring automorphisms, F is cyclic over its subfield of
G-fixed points.
No faithfulness is asked of the action: FixedPoints.toAlgAut_surjective needs only finiteness,
and cyclicity passes along any surjection. A non-faithful action simply presents the Galois group
as a proper quotient of G, which is cyclic all the same.
The automorphism of M over M ^ ⟨σ⟩ given by σ. Acting through ⟨σ⟩ fixes
M ^ ⟨σ⟩ pointwise, so σ is an automorphism over that field; this is that automorphism, and
nothing more. It is σ rebundled over a smaller base, so the name says only that.
Named rather than inlined so that consumers have a term to talk about: a fibre count needs the
relative Frobenius exhibited as a specific power of a specific generator, and IsCyclic supplies
only an anonymous one. Use toFixedFieldAlgEquiv_apply to compute with it. That it generates is
zpowers_toFixedFieldAlgEquiv_eq_top, a separate statement, and it is the only one that needs
⟨σ⟩ to be finite.
Equations
- σ.toFixedFieldAlgEquiv = (MulSemiringAction.toAlgAut (↥(Subgroup.zpowers σ)) (↥(FixedPoints.subfield (↥(Subgroup.zpowers σ)) M)) M) ⟨σ, ⋯⟩
Instances For
The rebundled automorphism acts as σ. This is what makes toFixedFieldAlgEquiv σ
usable: it is a different bundling of the same underlying map, over the fixed field rather than
over K. It says nothing about generation, which needs ⟨σ⟩ finite and is
zpowers_toFixedFieldAlgEquiv_eq_top.
Restricting scalars undoes the rebundling. Read back over K, σ.toFixedFieldAlgEquiv
is σ itself — the elimination rule matching toFixedFieldAlgEquiv_apply, in bundled form, which
is what a tower argument needs when it must produce an equation between automorphisms rather than
between their values.
And, for finite ⟨σ⟩, it generates. The automorphisms of M fixing M ^ ⟨σ⟩ are exactly
the powers of σ.toFixedFieldAlgEquiv.
Together with FixedPoints.isCyclic_algEquiv, applied to the action of ⟨σ⟩ on M, this is the
cyclic picture of M / M ^ ⟨σ⟩ with a named generator; neither statement asks M / K to be
finite or Galois.
The automorphism group of M over M ^ ⟨σ⟩ has order orderOf σ. The automorphisms of
M fixing the field cut out by ⟨σ⟩ number exactly the order of σ.
Only the generated subgroup ⟨σ⟩ need be finite: M / K is asked to be neither finite nor
Galois, so this applies to an automorphism of finite order of an arbitrary extension.
The order of the automorphism group of a finite field extension divides its degree.