feat(ring_theory/trace): Add trace_eq_sum_automorphisms, `norm_eq_p…

…rod_automorphisms`, `normal.alg_hom_equiv_aut` (#14523)




Co-authored-by: Iván Sadofschi Costa <isadofschi@users.noreply.github.com>

src/field_theory/normal.lean

@@ -263,6 +263,26 @@ alg_equiv.ext (λ _, (algebra_map E K₃).injective
 def alg_equiv.restrict_normal_hom [normal F E] : (K₁ ≃ₐ[F] K₁) →* (E ≃ₐ[F] E) :=
 monoid_hom.mk' (λ χ, χ.restrict_normal E) (λ ω χ, (χ.restrict_normal_trans ω E))
 
+variables (F K₁ E)
+
+/-- If `K₁/E/F` is a tower of fields with `E/F` normal then `normal.alg_hom_equiv_aut` is an
+ equivalence. -/
+@[simps] def normal.alg_hom_equiv_aut [normal F E] : (E →ₐ[F] K₁) ≃ (E ≃ₐ[F] E) :=
+{ to_fun := λ σ, alg_hom.restrict_normal' σ E,
+  inv_fun := λ σ, (is_scalar_tower.to_alg_hom F E K₁).comp σ.to_alg_hom,
+  left_inv := λ σ, begin
+    ext,
+    simp[alg_hom.restrict_normal'],
+  end,
+  right_inv := λ σ, begin
+    ext,
+    simp only [alg_hom.restrict_normal', alg_equiv.to_alg_hom_eq_coe, alg_equiv.coe_of_bijective],
+    apply no_zero_smul_divisors.algebra_map_injective E K₁,
+    rw alg_hom.restrict_normal_commutes,
+    simp,
+  end }
+
+
 end restrict
 
 section lift

src/ring_theory/norm.lean

@@ -6,9 +6,11 @@ Authors: Anne Baanen
 
 import field_theory.primitive_element
 import linear_algebra.determinant
+import linear_algebra.finite_dimensional
 import linear_algebra.matrix.charpoly.minpoly
 import linear_algebra.matrix.to_linear_equiv
 import field_theory.is_alg_closed.algebraic_closure
+import field_theory.galois
 
 /-!
 # Norm for (finite) ring extensions
@@ -283,6 +285,20 @@ begin
     exact is_separable.separable K _ }
 end
 
+lemma norm_eq_prod_automorphisms [finite_dimensional K L] [is_galois K L] {x : L}:
+  algebra_map K L (norm K x) = ∏ (σ : L ≃ₐ[K] L), σ x :=
+begin
+  apply no_zero_smul_divisors.algebra_map_injective L (algebraic_closure L),
+  rw map_prod (algebra_map L (algebraic_closure L)),
+  rw ← fintype.prod_equiv (normal.alg_hom_equiv_aut K (algebraic_closure L) L),
+  { rw ← norm_eq_prod_embeddings,
+    simp only [algebra_map_eq_smul_one, smul_one_smul] },
+  { intro σ,
+    simp only [normal.alg_hom_equiv_aut, alg_hom.restrict_normal', equiv.coe_fn_mk,
+               alg_equiv.coe_of_bijective, alg_hom.restrict_normal_commutes, id.map_eq_id,
+               ring_hom.id_apply] },
+end
+
 lemma is_integral_norm [algebra S L] [algebra S K] [is_scalar_tower S K L]
   [is_separable K L] [finite_dimensional K L] {x : L} (hx : _root_.is_integral S x) :
   _root_.is_integral S (norm K x) :=

src/ring_theory/trace.lean

@@ -7,10 +7,12 @@ Authors: Anne Baanen
 import linear_algebra.matrix.bilinear_form
 import linear_algebra.matrix.charpoly.minpoly
 import linear_algebra.determinant
+import linear_algebra.finite_dimensional
 import linear_algebra.vandermonde
 import linear_algebra.trace
 import field_theory.is_alg_closed.algebraic_closure
 import field_theory.primitive_element
+import field_theory.galois
 import ring_theory.power_basis
 
 /-!
@@ -356,6 +358,21 @@ begin
     exact is_separable.separable K _ }
 end
 
+lemma trace_eq_sum_automorphisms (x : L) [finite_dimensional K L] [is_galois K L] :
+  algebra_map K L (algebra.trace K L x) = ∑ (σ : L ≃ₐ[K] L), σ x :=
+begin
+  apply no_zero_smul_divisors.algebra_map_injective L (algebraic_closure L),
+  rw map_sum (algebra_map L (algebraic_closure L)),
+  rw ← fintype.sum_equiv (normal.alg_hom_equiv_aut K (algebraic_closure L) L),
+  { rw ←trace_eq_sum_embeddings (algebraic_closure L),
+    { simp only [algebra_map_eq_smul_one, smul_one_smul] },
+    { exact is_galois.to_is_separable } },
+  { intro σ,
+    simp only [normal.alg_hom_equiv_aut, alg_hom.restrict_normal', equiv.coe_fn_mk,
+               alg_equiv.coe_of_bijective, alg_hom.restrict_normal_commutes, id.map_eq_id,
+               ring_hom.id_apply] },
+end
+
 end eq_sum_embeddings
 
 section det_ne_zero