Intermediate fields along an algebra equivalence

An F-algebra equivalence e : K ≃ₐ[F] L identifies the intermediate fields of K / F with those of L / F: pushing forward along e and pulling back along e are mutually inverse and both monotone. Mathlib has the two maps, IntermediateField.map and IntermediateField.comap, and the round trips IntermediateField.comap_map and IntermediateField.map_comap_eq_self_of_surjective, but not the resulting order isomorphism, nor the membership rule for comap that Subalgebra.mem_comap states one level down.

Having it as a single OrderIso is what lets the intermediate fields of an abstract field K be transported to those of the subfield φ(K) of an ambient field along φ.equivFieldRange, and then composed with the Galois correspondence; that composition is the embedding form of the subfield dictionary in TauCeti/FieldTheory/Galois/SubfieldDictionary.lean.

Main results

• IntermediateField.mem_comap: x ∈ S.comap f ↔ f x ∈ S.
• IntermediateField.orderIsoMapComap: the order isomorphism IntermediateField F K ≃o IntermediateField F L induced by e : K ≃ₐ[F] L, with IntermediateField.orderIsoMapComap_apply and IntermediateField.orderIsoMapComap_symm_apply giving its two directions as map and comap.

The name follows Mathlib's Submodule.orderIsoMapComap, the same construction for submodules.

@[simp]

theorem IntermediateField.mem_comap {F : Type u_1} {K : Type u_2} {L : Type u_3} [Field F] [Field K] [Field L] [Algebra F K] [Algebra F L] {f : K →ₐ[F] L} {S : IntermediateField F L} {x : K} : x ∈ comap f S ↔ f x ∈ S

Membership in a preimage: x lies in S.comap f exactly when f x lies in S.

def IntermediateField.orderIsoMapComap {F : Type u_1} {K : Type u_2} {L : Type u_3} [Field F] [Field K] [Field L] [Algebra F K] [Algebra F L] (e : K ≃ₐ[F] L) : IntermediateField F K ≃o IntermediateField F L

An algebra equivalence identifies the intermediate fields of its source and target: the order isomorphism sending E to its image E.map e, with inverse the preimage S.comap e.

Equations

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

@[simp]

theorem IntermediateField.orderIsoMapComap_apply {F : Type u_1} {K : Type u_2} {L : Type u_3} [Field F] [Field K] [Field L] [Algebra F K] [Algebra F L] (e : K ≃ₐ[F] L) (E : IntermediateField F K) : (orderIsoMapComap e) E = map (↑e) E

@[simp]

theorem IntermediateField.orderIsoMapComap_symm_apply {F : Type u_1} {K : Type u_2} {L : Type u_3} [Field F] [Field K] [Field L] [Algebra F K] [Algebra F L] (e : K ≃ₐ[F] L) (S : IntermediateField F L) : (orderIsoMapComap e).symm S = comap (↑e) S