Embeddings into a normal extension, and the action on them

For fields L and M over a base F, the group M ≃ₐ[F] M acts on the embeddings L →ₐ[F] M by postcomposition (TauCeti/Algebra/GroupAction/AlgHom.lean). This file records the facts that make that action a dictionary for the subfields of L.

Stabilizers. The automorphisms fixing an embedding φ are exactly those fixing its image φ(L) pointwise. Together with transitivity this identifies the coset space of Gal(M / φ(L)) with the set of all embeddings, the coset of g corresponding to g ∘ φ.

Transitivity. When M / F is normal, any two embeddings lie in the same orbit, because an isomorphism between two embedded images extends to M. This asserts nothing about existence: if no embedding L →ₐ[F] M exists the statement holds vacuously.

Faithfulness. When the embedded images generate M — that is, when IntermediateField.normalClosure F L M = ⊤ — an automorphism fixing every embedding is the identity, so the action has trivial kernel.

Counting. When L / F is finite and separable, M / F is normal, and at least one embedding L →ₐ[F] M exists, there are exactly [L : F] of them. All three hypotheses are needed: without separability the count drops, and without normality the minimal polynomials need not split in M.

Main results

• AlgHom.liftNormal_equivFieldRange_apply: lifting the isomorphism between two embedded images carries one embedding to the other. This isolates the field-range bookkeeping.
• AlgEquiv.isPretransitiveAlgHom: over a normal M / F, any two embeddings lie in one orbit.
• TauCeti.FieldTheory.stabilizer_algHom_eq_fixingSubgroup: the stabilizer of an embedding φ is the subgroup fixing φ(L).
• AlgHom.fixingSubgroup_fieldRange_conj: the fixing subgroups of two embedded images are conjugate in a normal ambient extension.
• TauCeti.FieldTheory.fixingSubgroupQuotientEquivAlgHom: over a normal M / F, the cosets of that subgroup are the embeddings of L into M.
• TauCeti.FieldTheory.eq_one_of_forall_smul_eq: if the embedded images generate M, an automorphism fixing every embedding is the identity.
• TauCeti.FieldTheory.faithfulSMul_of_normalClosure_eq_top: equivalently, the action is faithful. Injectivity of the permutation representation is then Mathlib's smul_left_injective'.
• AlgHom.card_of_normal: for L / F finite separable and M / F normal admitting an embedding of L, there are exactly [L : F] embeddings.

References

• J. Neukirch, Algebraic Number Theory, Chapter I, §2 and §9.

@[simp]

theorem AlgHom.liftNormal_equivFieldRange_apply {F : Type u_1} {L : Type u_2} {M : Type u_3} [Field F] [Field L] [Field M] [Algebra F L] [Algebra F M] [Normal F M] (φ ψ : L →ₐ[F] M) (x : L) : ((φ.equivFieldRange.symm.trans ψ.equivFieldRange).liftNormal M) (φ x) = ψ x

Lifting the isomorphism between two embedded images carries one embedding to the other.

This isolates the field-range and coercion bookkeeping: φ x is transported into φ.fieldRange, the isomorphism φ.fieldRange ≃ ψ.fieldRange is applied there, and liftNormal_commutes brings the result back to M. Keeping it separate lets isPretransitiveAlgHom state only the mathematical step.

instance AlgEquiv.isPretransitiveAlgHom {F : Type u_1} {L : Type u_2} {M : Type u_3} [Field F] [Field L] [Field M] [Algebra F L] [Algebra F M] [Normal F M] : MulAction.IsPretransitive Gal(M/F) (L →ₐ[F] M)

Any two embeddings into a normal extension are conjugate, so they lie in the same orbit. No embedding is asserted to exist: when L →ₐ[F] M is empty this holds vacuously.

theorem TauCeti.FieldTheory.eq_one_of_forall_smul_eq {F : Type u_1} {L : Type u_2} {M : Type u_3} [Field F] [Field L] [Field M] [Algebra F L] [Algebra F M] (hgen : IntermediateField.normalClosure F L M = ⊤) {σ : Gal(M/F)} (h : ∀ (φ : L →ₐ[F] M), σ • φ = φ) : σ = 1

An automorphism fixing every embedding is the identity, provided the embedded images of L generate M.

theorem TauCeti.FieldTheory.faithfulSMul_of_normalClosure_eq_top {F : Type u_1} {L : Type u_2} {M : Type u_3} [Field F] [Field L] [Field M] [Algebra F L] [Algebra F M] (hgen : IntermediateField.normalClosure F L M = ⊤) : FaithfulSMul Gal(M/F) (L →ₐ[F] M)

The action on embeddings is faithful when the embedded images generate M.

With this instance in scope, injectivity of the permutation representation is Mathlib's smul_left_injective'; no separate statement is needed.

theorem TauCeti.FieldTheory.stabilizer_algHom_eq_fixingSubgroup {F : Type u_1} {L : Type u_2} {M : Type u_3} [Field F] [Field L] [Field M] [Algebra F L] [Algebra F M] (φ : L →ₐ[F] M) : MulAction.stabilizer Gal(M/F) φ = φ.fieldRange.fixingSubgroup

The stabilizer of an embedding is the subgroup fixing its image: an automorphism of M fixes φ under postcomposition exactly when it fixes φ(L) pointwise. No hypothesis on M / F is needed.

theorem AlgHom.fixingSubgroup_fieldRange_conj {F : Type u_1} {L : Type u_2} {M : Type u_3} [Field F] [Field L] [Field M] [Algebra F L] [Algebra F M] [Normal F M] (φ ψ : L →ₐ[F] M) : ∃ (g : Gal(M/F)), ψ.fieldRange.fixingSubgroup = Subgroup.map (MulEquiv.toMonoidHom (MulAut.conj g)) φ.fieldRange.fixingSubgroup

The fixing subgroups of the images of two embeddings into a normal extension are conjugate. No finiteness assumption on the embedded extension is needed.

noncomputable def TauCeti.FieldTheory.fixingSubgroupQuotientEquivAlgHom {F : Type u_1} {L : Type u_2} {M : Type u_3} [Field F] [Field L] [Field M] [Algebra F L] [Algebra F M] [Normal F M] (φ : L →ₐ[F] M) : Gal(M/F) ⧸ φ.fieldRange.fixingSubgroup ≃ (L →ₐ[F] M)

The cosets of Gal(M / φ(L)) are the embeddings of L into M for a normal M / F, the coset of g corresponding to g ∘ φ.

Equations

• TauCeti.FieldTheory.fixingSubgroupQuotientEquivAlgHom φ = (Subgroup.quotientEquivOfEq ⋯).trans (TauCeti.quotientStabilizerEquiv Gal(M/F) φ)

@[simp]

theorem TauCeti.FieldTheory.fixingSubgroupQuotientEquivAlgHom_mk {F : Type u_1} {L : Type u_2} {M : Type u_3} [Field F] [Field L] [Field M] [Algebra F L] [Algebra F M] [Normal F M] (φ : L →ₐ[F] M) (g : Gal(M/F)) : (fixingSubgroupQuotientEquivAlgHom φ) ↑g = (↑g).comp φ

fixingSubgroupQuotientEquivAlgHom sends the coset of g to g ∘ φ.

@[simp]

theorem AlgHom.card_of_normal {F : Type u_1} {L : Type u_2} {M : Type u_3} [Field F] [Field L] [Field M] [Algebra F L] [Algebra F M] [FiniteDimensional F L] [Algebra.IsSeparable F L] [Normal F M] [Nonempty (L →ₐ[F] M)] : Fintype.card (L →ₐ[F] M) = Module.finrank F L

The number of embeddings is the degree. For L / F finite and separable and M / F normal, the existence of an embedding L →ₐ[F] M forces there to be exactly [L : F] of them: every minimal polynomial over F of an element of L splits in M.