Finite intermediate fields under inverse images

The inverse image of a finite intermediate field under an algebra map is finite-dimensional. This lets finite subextensions be transported between ambient extensions, for example when comparing their Krull topologies.

instance IntermediateField.finiteDimensional_comap {F : Type u_1} {E : Type u_2} {L : Type u_3} [Field F] [Field E] [Field L] [Algebra F E] [Algebra F L] (M : IntermediateField F E) [FiniteDimensional F ↥M] (g : L →ₐ[F] E) : FiniteDimensional F ↥(comap g M)

The preimage of a finite intermediate field M of E/F under an F-algebra map g into E is finite over F: it is F-isomorphic to its image under g, which is contained in M.