feat(field_theory.intermediate_field): add intermediate_field.map_map (…

…#11020)




Co-authored-by: Johan Commelin <johan@commelin.net>

src/data/polynomial/eval.lean

@@ -596,7 +596,7 @@ ring_hom.ext $ λ x, map_id
 
 @[simp] lemma map_ring_hom_comp [semiring T] (f : S →+* T) (g : R →+* S) :
   (map_ring_hom f).comp (map_ring_hom g) = map_ring_hom (f.comp g) :=
-ring_hom.ext $ map_map g f
+ring_hom.ext $ polynomial.map_map g f
 
 lemma map_list_prod (L : list (polynomial R)) : L.prod.map f = (L.map $ map f).prod :=
 eq.symm $ list.prod_hom _ (map_ring_hom f).to_monoid_hom

src/field_theory/intermediate_field.lean

@@ -266,6 +266,12 @@ def map (f : L →ₐ[K] L') : intermediate_field K L' :=
   neg_mem' := λ x hx, (S.to_subalgebra.map f).neg_mem hx,
   .. S.to_subalgebra.map f}
 
+lemma map_map {K L₁ L₂ L₃ : Type*} [field K] [field L₁] [algebra K L₁]
+  [field L₂] [algebra K L₂] [field L₃] [algebra K L₃]
+  (E : intermediate_field K L₁) (f : L₁ →ₐ[K] L₂) (g : L₂ →ₐ[K] L₃) :
+  (E.map f).map g = E.map (g.comp f) :=
+set_like.coe_injective $ set.image_image _ _ _
+
 /-- The embedding from an intermediate field of `L / K` to `L`. -/
 def val : S →ₐ[K] L :=
 S.to_subalgebra.val

src/field_theory/primitive_element.lean

@@ -159,7 +159,7 @@ begin
   transitivity euclidean_domain.gcd (_ : polynomial E) (_ : polynomial E),
   { dsimp only [p],
     convert (gcd_map (algebra_map F⟮γ⟯ E)).symm },
-  { simpa [map_comp, map_map, ←is_scalar_tower.algebra_map_eq, h] },
+  { simpa [map_comp, polynomial.map_map, ←is_scalar_tower.algebra_map_eq, h] },
 end
 
 end primitive_element_inf