Conjugate intermediate fields

The automorphism group of an extension acts on its intermediate fields by mapping their elements. The conjugates of a field form its orbit under this action.

Main definitions

• TauCeti.instMulActionIntermediateField: automorphisms act by mapping intermediate fields.
• IntermediateField.conjugateFields: the orbit of an intermediate field.

Main results

• AlgEquiv.smul_intermediateField_def: the action is IntermediateField.map.
• IntermediateField.mem_conjugateFields_iff: orbit membership is an automorphism image.

@[instance_reducible]

instance TauCeti.instMulActionIntermediateField {K : Type u_1} {L : Type u_2} [Field K] [Field L] [Algebra K L] : MulAction (L ≃ₐ[K] L) (IntermediateField K L)

The action of the automorphism group of L / K on its intermediate fields.

Equations

• TauCeti.instMulActionIntermediateField = { smul := fun (σ : L ≃ₐ[K] L) (E : IntermediateField K L) => IntermediateField.map (↑σ) E, mul_smul := ⋯, one_smul := ⋯ }

@[simp]

theorem AlgEquiv.smul_intermediateField_def {K : Type u_1} {L : Type u_2} [Field K] [Field L] [Algebra K L] (σ : L ≃ₐ[K] L) (E : IntermediateField K L) : σ • E = IntermediateField.map (↑σ) E

Conjugating an intermediate field means mapping it along the automorphism.

def IntermediateField.conjugateFields {K : Type u_1} {L : Type u_2} [Field K] [Field L] [Algebra K L] (E : IntermediateField K L) : Set (IntermediateField K L)

The set of images of E under automorphisms of the ambient extension.

Equations

• E.conjugateFields = MulAction.orbit (L ≃ₐ[K] L) E

@[simp]

theorem IntermediateField.mem_conjugateFields_iff {K : Type u_1} {L : Type u_2} [Field K] [Field L] [Algebra K L] {E E' : IntermediateField K L} : E' ∈ E.conjugateFields ↔ ∃ (σ : L ≃ₐ[K] L), map (↑σ) E = E'

Membership in conjugateFields E means being the image of E under an automorphism.