Conjugate intermediate fields

The automorphism group of an extension acts on its intermediate fields by mapping their elements. For a Galois extension, the Galois correspondence intertwines this action with conjugation of fixing subgroups. Consequently the conjugates of an intermediate field correspond bijectively to the conjugates of its fixing subgroup, and their number is the index of the subgroup's normalizer.

This distinguishes two quotients attached to an intermediate field E. Its embeddings into the ambient Galois extension are indexed by the cosets of E.fixingSubgroup, whereas the distinct images of those embeddings are indexed by the cosets of E.fixingSubgroup.normalizer. The latter quotient can be strictly smaller.

Main definitions

• IntermediateField.conjugateFieldsEquivConjugateSubgroups: the Galois-correspondence bijection between those two sets.
• IntermediateField.quotientNormalizerEquivConjugateFields: normalizer cosets index the conjugate fields.

Main results

• IntermediateField.stabilizer_eq_normalizer_fixingSubgroup: the field stabilizer is the normalizer of its fixing subgroup.
• IntermediateField.ncard_conjugateFields: the number of fields is the normalizer index.

@[simp]

theorem IntermediateField.stabilizer_eq_normalizer_fixingSubgroup {K : Type u_1} {L : Type u_2} [Field K] [Field L] [Algebra K L] [IsGalois K L] (E : IntermediateField K L) : MulAction.stabilizer Gal(L/K) E = Subgroup.normalizer ↑E.fixingSubgroup

The stabilizer of an intermediate field under ambient automorphisms is the normalizer of its fixing subgroup.

noncomputable def IntermediateField.conjugateFieldsEquivConjugateSubgroups {K : Type u_1} {L : Type u_2} [Field K] [Field L] [Algebra K L] [IsGalois K L] (E : IntermediateField K L) : ↑E.conjugateFields ≃ ↑(MulAction.orbit (ConjAct Gal(L/K)) E.fixingSubgroup)

The Galois correspondence restricts to a bijection from conjugates of an intermediate field to conjugates of its fixing subgroup.

Equations

• One or more equations did not get rendered due to their size.

@[simp]

theorem IntermediateField.conjugateFieldsEquivConjugateSubgroups_apply {K : Type u_1} {L : Type u_2} [Field K] [Field L] [Algebra K L] [IsGalois K L] (E : IntermediateField K L) (E' : ↑E.conjugateFields) : ↑(E.conjugateFieldsEquivConjugateSubgroups E') = (↑E').fixingSubgroup

The forward Galois correspondence sends a conjugate field to its fixing subgroup.

@[simp]

theorem IntermediateField.conjugateFieldsEquivConjugateSubgroups_symm_apply {K : Type u_1} {L : Type u_2} [Field K] [Field L] [Algebra K L] [IsGalois K L] (E : IntermediateField K L) (H : ↑(MulAction.orbit (ConjAct Gal(L/K)) E.fixingSubgroup)) : ↑(E.conjugateFieldsEquivConjugateSubgroups.symm H) = fixedField ↑H

The inverse Galois correspondence sends a conjugate subgroup to its fixed field.

noncomputable def IntermediateField.quotientNormalizerEquivConjugateFields {K : Type u_1} {L : Type u_2} [Field K] [Field L] [Algebra K L] [IsGalois K L] (E : IntermediateField K L) : Gal(L/K) ⧸ Subgroup.normalizer ↑E.fixingSubgroup ≃ ↑E.conjugateFields

The normalizer cosets index the conjugate images of an intermediate field.

Equations

• E.quotientNormalizerEquivConjugateFields = (Subgroup.quotientEquivOfEq ⋯).trans ((MulAction.orbitEquivQuotientStabilizer Gal(L/K) E).symm.trans (Equiv.subtypeEquivRight ⋯))

@[simp]

theorem IntermediateField.quotientNormalizerEquivConjugateFields_mk {K : Type u_1} {L : Type u_2} [Field K] [Field L] [Algebra K L] [IsGalois K L] (E : IntermediateField K L) (σ : Gal(L/K)) : ↑(E.quotientNormalizerEquivConjugateFields ↑σ) = σ • E

A normalizer coset represented by σ gives the field σ • E.

@[simp]

theorem IntermediateField.quotientNormalizerEquivConjugateFields_smul {K : Type u_1} {L : Type u_2} [Field K] [Field L] [Algebra K L] [IsGalois K L] (E : IntermediateField K L) (σ : Gal(L/K)) (q : Gal(L/K) ⧸ Subgroup.normalizer ↑E.fixingSubgroup) : ↑(E.quotientNormalizerEquivConjugateFields (σ • q)) = σ • ↑(E.quotientNormalizerEquivConjugateFields q)

The normalizer-coset parametrization respects the ambient Galois action.

@[simp]

theorem IntermediateField.ncard_conjugateFields {K : Type u_1} {L : Type u_2} [Field K] [Field L] [Algebra K L] [IsGalois K L] (E : IntermediateField K L) : E.conjugateFields.ncard = (Subgroup.normalizer ↑E.fixingSubgroup).index

The number of distinct conjugates of an intermediate field is the index of the normalizer of its fixing subgroup.