intermediate_field.map_map

Stream: new members

[Sebastian Monnet]

I need the following analogue of subalgebra.map_map and subfield.map_map.

import field_theory.galois

lemma intermediate_field_map_map {K L1 L2 L3 : Type*} [field K] [field L1] [algebra K L1]
[field L2] [algebra K L2] [field L3] [algebra K L3]
(E : intermediate_field K L1) (f : L1 →ₐ[K] L2) (g : L2 →ₐ[K] L3) :
(E.map f).map g = E.map (g.comp f) :=
begin
  sorry,
end

I think this should be called intermediate_field.map_map, but that doesn't exist. Can anyone think of a good way to do it?

[Kevin Buzzard]

lemma intermediate_field.map_map {K L1 L2 L3 : Type*} [field K] [field L1] [algebra K L1]
[field L2] [algebra K L2] [field L3] [algebra K L3]
(E : intermediate_field K L1) (f : L1 →ₐ[K] L2) (g : L2 →ₐ[K] L3) :
(E.map f).map g = E.map (g.comp f) :=
set_like.coe_injective $ set.image_image _ _ _

Looks like I've done something clever but in fact I did something pretty dumb -- just literally copied the proof of subalgebra.map_map.

[Kevin Buzzard]

And yes I agree it should be in mathlib and should be called intermediate_field.map_map, you could make the PR and see what the maintainers think :-) PS I know what you're thinking about and you're doing it the right way -- isolating little basic principles like this with one line proofs and filling in holes in the intermediate_field API is the mathlib-preferred way to do it.