Stream: new members

Topic: intermediate_field.map_map

Sebastian Monnet (Dec 23 2021 at 20:48):

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 (Dec 23 2021 at 21:09):

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 (Dec 23 2021 at 21:11):

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.

Last updated: Dec 20 2023 at 11:08 UTC