feat(ring_theory): define the field/algebra norm (#7636)

This PR defines the field norm `algebra.norm K L : L →* K`, where `L` is a finite field extension of `K`. In fact, it defines this for any `algebra R S` instance, where `R` and `S` are integral domains. (With a default value of `1` if `S` does not have a finite `R`-basis.)

The approach is to basically copy `ring_theory/trace.lean` and replace `trace` with `det` or `norm` as appropriate.

src/ring_theory/norm.lean

@@ -0,0 +1,98 @@
+/-
+Copyright (c) 2021 Anne Baanen. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Anne Baanen
+-/
+
+import linear_algebra.determinant
+import ring_theory.power_basis
+
+/-!
+# Norm for (finite) ring extensions
+
+Suppose we have an `R`-algebra `S` with a finite basis. For each `s : S`,
+the determinant of the linear map given by multiplying by `s` gives information
+about the roots of the minimal polynomial of `s` over `R`.
+
+## Implementation notes
+
+Typically, the norm is defined specifically for finite field extensions.
+The current definition is as general as possible and the assumption that we have
+fields or that the extension is finite is added to the lemmas as needed.
+
+We only define the norm for left multiplication (`algebra.left_mul_matrix`,
+i.e. `algebra.lmul_left`).
+For now, the definitions assume `S` is commutative, so the choice doesn't
+matter anyway.
+
+See also `algebra.trace`, which is defined similarly as the trace of
+`algebra.left_mul_matrix`.
+
+## References
+
+ * https://en.wikipedia.org/wiki/Field_norm
+
+-/
+
+universes u v w
+
+variables {R S T : Type*} [integral_domain R] [integral_domain S] [integral_domain T]
+variables [algebra R S] [algebra R T]
+variables {K L : Type*} [field K] [field L] [algebra K L]
+variables {ι : Type w} [fintype ι]
+
+open finite_dimensional
+open linear_map
+open matrix
+
+open_locale big_operators
+open_locale matrix
+
+namespace algebra
+
+variables (R)
+
+/-- The norm of an element `s` of an `R`-algebra is the determinant of `(*) s`. -/
+noncomputable def norm : S →* R :=
+linear_map.det.comp (lmul R S).to_ring_hom.to_monoid_hom
+
+@[simp] lemma norm_apply (x : S) : norm R x = linear_map.det (lmul R S x) := rfl
+
+lemma norm_eq_one_of_not_exists_basis
+  (h : ¬ ∃ (s : set S) (b : basis s R S), s.finite) (x : S) : norm R x = 1 :=
+by { rw [norm_apply, linear_map.det], split_ifs with h, refl }
+
+variables {R}
+
+-- Can't be a `simp` lemma because it depends on a choice of basis
+lemma norm_eq_matrix_det [decidable_eq ι] (b : basis ι R S) (s : S) :
+  norm R s = matrix.det (algebra.left_mul_matrix b s) :=
+by rw [norm_apply, ← linear_map.det_to_matrix b, to_matrix_lmul_eq]
+
+/-- If `x` is in the base field `K`, then the norm is `x ^ [L : K]`. -/
+lemma norm_algebra_map_of_basis (b : basis ι R S) (x : R) :
+  norm R (algebra_map R S x) = x ^ fintype.card ι :=
+begin
+  haveI := classical.dec_eq ι,
+  rw [norm_apply, ← det_to_matrix b, lmul_algebra_map],
+  convert @det_diagonal _ _ _ _ _ (λ (i : ι), x),
+  { ext i j, rw [to_matrix_lsmul, matrix.diagonal] },
+  { rw [finset.prod_const, finset.card_univ] }
+end
+
+/-- If `x` is in the base field `K`, then the norm is `x ^ [L : K]`.
+
+(If `L` is not finite-dimensional over `K`, then `norm = 1 = x ^ 0 = x ^ (finrank L K)`.)
+-/
+@[simp]
+lemma norm_algebra_map (x : K) : norm K (algebra_map K L x) = x ^ finrank K L :=
+begin
+  by_cases H : ∃ (s : set L) (b : basis s K L), s.finite,
+  { haveI : fintype H.some := H.some_spec.some_spec.some,
+    rw [norm_algebra_map_of_basis H.some_spec.some, finrank_eq_card_basis H.some_spec.some] },
+  { rw [norm_eq_one_of_not_exists_basis K H, finrank_eq_zero_of_not_exists_basis, pow_zero],
+    rintros ⟨s, ⟨b⟩⟩,
+    exact H ⟨↑s, b, s.finite_to_set⟩ },
+end
+
+end algebra