Transporting finite Galois subextensions between separable closures

Let L/K be embedded in Kˢ by σ, and let E/L be embedded in Kˢ compatibly with σ. The chosen identification separableClosureRingEquiv K L σ : Lˢ ≃+* Kˢ transports this embedding to an L-embedding in Lˢ. If E/L is finite and normal, its image is a finite Galois subextension of Lˢ/L, with an algebra equivalence recording the ambient embedding.

This supplies finite fields and compatible coefficient maps for comparing finite cocycle restriction with restriction on absolute Galois cohomology. In particular, a finite Galois extension of K containing the image of L can be read inside the separable closure of L. No normality of L/K is needed.

A field isomorphism e : K ≃+* L, with K and L in independent universes, transports every intermediate field of Kˢ/K to one of Lˢ/L through the chosen identification e.separableClosureCongr : Lˢ ≃+* Kˢ. Finiteness, degree, normality and the Galois property are preserved, each subextension is identified with its transport by a ring isomorphism semilinear over e, and their automorphism groups are identified compatibly with it. These are the finite coefficient fields, coefficient maps and automorphism maps along which a finite 2-cocycle over K is transported to one over L, for instance when L is the universe lift ULift K.

Main definitions

• AlgHom.liftToSeparableClosure: an embedding of E into Kˢ compatible with σ, read as an L-embedding into Lˢ.
• RingEquiv.intermediateFieldCongr e: the order isomorphism between the intermediate fields of Kˢ/K and of Lˢ/L induced by e : K ≃+* L.
• RingEquiv.intermediateFieldCongrEquiv e E: the ring isomorphism from E to its transport.
• RingEquiv.intermediateFieldAutCongr e E: the induced isomorphism from the automorphism group of the transport of E over L to the automorphism group of E over K.

Main results

• AlgHom.exists_finiteGalois_subextension_equiv: a finite normal extension of L embedded compatibly in Kˢ is isomorphic to a finite Galois subextension of Lˢ/L.
• RingEquiv.finrank_intermediateFieldCongr, RingEquiv.normal_intermediateFieldCongr, RingEquiv.isGalois_intermediateFieldCongr: transport preserves degree, normality and the Galois property.
• RingEquiv.intermediateFieldCongrEquiv_intermediateFieldAutCongr: the ring isomorphism intertwines corresponding automorphisms.

References

• J.-P. Serre, Local Fields, Chapter X, §5.
• J. Neukirch, A. Schmidt, K. Wingberg, Cohomology of Number Fields, 2nd ed., Chapter VI, §1.

noncomputable def AlgHom.liftToSeparableClosure {K : Type u} [Field K] {L : Type v} [Field L] [Algebra K L] {E : Type w} [Field E] [Algebra K E] [Algebra L E] (σ : L →ₐ[K] SeparableClosure K) (ι : E →ₐ[K] SeparableClosure K) (hι : ∀ (x : L), ι ((algebraMap L E) x) = σ x) : E →ₐ[L] SeparableClosure L

Transport a compatible embedding of E into Kˢ to an L-embedding into Lˢ, using the chosen identification of separable closures extending σ.

theorem AlgHom.liftToSeparableClosure_apply {K : Type u} [Field K] {L : Type v} [Field L] [Algebra K L] {E : Type w} [Field E] [Algebra K E] [Algebra L E] (σ : L →ₐ[K] SeparableClosure K) (ι : E →ₐ[K] SeparableClosure K) (hι : ∀ (x : L), ι ((algebraMap L E) x) = σ x) (y : E) : (σ.liftToSeparableClosure ι hι) y = (TauCeti.separableClosureRingEquiv K L σ).symm (ι y)

The transported embedding is the original embedding followed by the inverse identification of separable closures.

@[simp]

theorem AlgHom.separableClosureRingEquiv_liftToSeparableClosure {K : Type u} [Field K] {L : Type v} [Field L] [Algebra K L] {E : Type w} [Field E] [Algebra K E] [Algebra L E] (σ : L →ₐ[K] SeparableClosure K) (ι : E →ₐ[K] SeparableClosure K) (hι : ∀ (x : L), ι ((algebraMap L E) x) = σ x) (y : E) : (TauCeti.separableClosureRingEquiv K L σ) ((σ.liftToSeparableClosure ι hι) y) = ι y

The two ambient embeddings agree through the identification of separable closures.

theorem AlgHom.exists_finiteGalois_subextension_equiv {K : Type u} [Field K] {L : Type v} [Field L] [Algebra K L] {E : Type w} [Field E] [Algebra K E] [Algebra L E] [FiniteDimensional L E] [Normal L E] (σ : L →ₐ[K] SeparableClosure K) (ι : E →ₐ[K] SeparableClosure K) (hι : ∀ (x : L), ι ((algebraMap L E) x) = σ x) : ∃ (M : IntermediateField L (SeparableClosure L)), FiniteDimensional L ↥M ∧ IsGalois L ↥M ∧ ∃ (e : E ≃ₐ[L] ↥M), ∀ (y : E), (TauCeti.separableClosureRingEquiv K L σ) ↑(e y) = ι y

A finite normal extension embedded compatibly in Kˢ is isomorphic to a finite Galois subextension of Lˢ/L. The equivalence preserves the specified embedding into Kˢ through the chosen identification of separable closures.

noncomputable def RingEquiv.intermediateFieldCongr {K : Type u} [Field K] {L : Type v} [Field L] (e : K ≃+* L) : IntermediateField K (SeparableClosure K) ≃o IntermediateField L (SeparableClosure L)

A field isomorphism e : K ≃+* L identifies the intermediate fields of Kˢ/K with those of Lˢ/L. The intermediate field E goes to its image under the inverse of the chosen identification e.separableClosureCongr : Lˢ ≃+* Kˢ, which extends e.symm.

@[simp]

theorem RingEquiv.mem_intermediateFieldCongr {K : Type u} [Field K] {L : Type v} [Field L] {e : K ≃+* L} {E : IntermediateField K (SeparableClosure K)} {y : SeparableClosure L} : y ∈ e.intermediateFieldCongr E ↔ e.separableClosureCongr y ∈ E

An element of Lˢ lies in the transported intermediate field exactly when its image in Kˢ under the chosen identification lies in the original one.

@[simp]

theorem RingEquiv.mem_intermediateFieldCongr_symm {K : Type u} [Field K] {L : Type v} [Field L] {e : K ≃+* L} {F : IntermediateField L (SeparableClosure L)} {x : SeparableClosure K} : x ∈ e.intermediateFieldCongr.symm F ↔ e.separableClosureCongr.symm x ∈ F

An element of Kˢ lies in the inverse transport of an intermediate field of Lˢ/L exactly when its image under the inverse identification lies in that intermediate field.

noncomputable def RingEquiv.intermediateFieldCongrEquiv {K : Type u} [Field K] {L : Type v} [Field L] (e : K ≃+* L) (E : IntermediateField K (SeparableClosure K)) : ↥E ≃+* ↥(e.intermediateFieldCongr E)

The ring isomorphism from an intermediate field E of Kˢ/K to its transport, given by the inverse of the chosen identification of separable closures. It is semilinear over e (intermediateFieldCongrEquiv_algebraMap).

@[simp]

theorem RingEquiv.coe_intermediateFieldCongrEquiv {K : Type u} [Field K] {L : Type v} [Field L] (e : K ≃+* L) (E : IntermediateField K (SeparableClosure K)) (x : ↥E) : ↑((e.intermediateFieldCongrEquiv E) x) = e.separableClosureCongr.symm ↑x

The transport of an element of E is its image under the inverse of the chosen identification of separable closures.

@[simp]

theorem RingEquiv.coe_intermediateFieldCongrEquiv_symm {K : Type u} [Field K] {L : Type v} [Field L] (e : K ≃+* L) (E : IntermediateField K (SeparableClosure K)) (y : ↥(e.intermediateFieldCongr E)) : ↑((e.intermediateFieldCongrEquiv E).symm y) = e.separableClosureCongr ↑y

The inverse transport of an element is its image under the chosen identification of separable closures.

@[simp]

theorem RingEquiv.intermediateFieldCongrEquiv_algebraMap {K : Type u} [Field K] {L : Type v} [Field L] (e : K ≃+* L) (E : IntermediateField K (SeparableClosure K)) (x : K) : (e.intermediateFieldCongrEquiv E) ((algebraMap K ↥E) x) = (algebraMap L ↥(e.intermediateFieldCongr E)) (e x)

The transport of an intermediate field is semilinear over e.

@[simp]

theorem RingEquiv.intermediateFieldCongrEquiv_symm_algebraMap {K : Type u} [Field K] {L : Type v} [Field L] (e : K ≃+* L) (E : IntermediateField K (SeparableClosure K)) (y : L) : (e.intermediateFieldCongrEquiv E).symm ((algebraMap L ↥(e.intermediateFieldCongr E)) y) = (algebraMap K ↥E) (e.symm y)

The inverse transport of an intermediate field is semilinear over e.symm.

theorem RingEquiv.algebraMap_comp_intermediateFieldCongrEquiv {K : Type u} [Field K] {L : Type v} [Field L] (e : K ≃+* L) (E : IntermediateField K (SeparableClosure K)) : (algebraMap L ↥(e.intermediateFieldCongr E)).comp ↑e = (↑(e.intermediateFieldCongrEquiv E)).comp (algebraMap K ↥E)

The semilinearity of intermediateFieldCongrEquiv over e, as an equation of ring homomorphisms; this is the compatibility consumed by Mathlib's *_of_equiv_equiv transfers.

@[simp]

theorem RingEquiv.finrank_intermediateFieldCongr {K : Type u} [Field K] {L : Type v} [Field L] (e : K ≃+* L) (E : IntermediateField K (SeparableClosure K)) : Module.finrank L ↥(e.intermediateFieldCongr E) = Module.finrank K ↥E

Transport preserves degree.

instance RingEquiv.finiteDimensional_intermediateFieldCongr {K : Type u} [Field K] {L : Type v} [Field L] (e : K ≃+* L) (E : IntermediateField K (SeparableClosure K)) [FiniteDimensional K ↥E] : FiniteDimensional L ↥(e.intermediateFieldCongr E)

instance RingEquiv.normal_intermediateFieldCongr {K : Type u} [Field K] {L : Type v} [Field L] (e : K ≃+* L) (E : IntermediateField K (SeparableClosure K)) [Normal K ↥E] : Normal L ↥(e.intermediateFieldCongr E)

instance RingEquiv.isGalois_intermediateFieldCongr {K : Type u} [Field K] {L : Type v} [Field L] (e : K ≃+* L) (E : IntermediateField K (SeparableClosure K)) [IsGalois K ↥E] : IsGalois L ↥(e.intermediateFieldCongr E)

noncomputable def RingEquiv.intermediateFieldAutCongr {K : Type u} [Field K] {L : Type v} [Field L] (e : K ≃+* L) (E : IntermediateField K (SeparableClosure K)) : Gal(↥(e.intermediateFieldCongr E)/L) ≃* Gal(↥E/K)

The automorphism groups of an intermediate field E of Kˢ/K and of its transport are identified by conjugation with intermediateFieldCongrEquiv. Like absoluteGaloisGroupCongr, the identification is contravariant in e.

@[simp]

theorem RingEquiv.intermediateFieldAutCongr_apply {K : Type u} [Field K] {L : Type v} [Field L] (e : K ≃+* L) (E : IntermediateField K (SeparableClosure K)) (g : Gal(↥(e.intermediateFieldCongr E)/L)) (x : ↥E) : ((e.intermediateFieldAutCongr E) g) x = (e.intermediateFieldCongrEquiv E).symm (g ((e.intermediateFieldCongrEquiv E) x))

The automorphism of E corresponding to an automorphism g of its transport is conjugation of g by intermediateFieldCongrEquiv.

theorem RingEquiv.intermediateFieldCongrEquiv_intermediateFieldAutCongr {K : Type u} [Field K] {L : Type v} [Field L] (e : K ≃+* L) (E : IntermediateField K (SeparableClosure K)) (g : Gal(↥(e.intermediateFieldCongr E)/L)) (x : ↥E) : (e.intermediateFieldCongrEquiv E) (((e.intermediateFieldAutCongr E) g) x) = g ((e.intermediateFieldCongrEquiv E) x)

The automorphism identification is compatible with the transport of elements: intermediateFieldCongrEquiv intertwines an automorphism of the transport with the corresponding automorphism of E.

@[simp]

theorem RingEquiv.intermediateFieldAutCongr_symm_apply {K : Type u} [Field K] {L : Type v} [Field L] (e : K ≃+* L) (E : IntermediateField K (SeparableClosure K)) (g : Gal(↥E/K)) (y : ↥(e.intermediateFieldCongr E)) : ((e.intermediateFieldAutCongr E).symm g) y = (e.intermediateFieldCongrEquiv E) (g ((e.intermediateFieldCongrEquiv E).symm y))

The inverse automorphism identification is conjugation by intermediateFieldCongrEquiv.