feat(number_theory/number_field/units): add is_unit_iff_norm (#18866)

xroblot · xroblot · commit 00f91228655e · 2023-05-05T05:51:17.000Z
This PR creates the file `number_theory/number_field/units.lean` and proves the result : 
```lean
lemma is_unit_iff_norm [number_field K] (x : 𝓞 K) :
  is_unit x ↔ abs (ring_of_integers.norm ℚ x : ℚ) = 1 
```
diff --git a/src/algebra/group_power/order.lean b/src/algebra/group_power/order.lean
@@ -457,6 +457,11 @@ lemma pow_abs (a : R) (n : ℕ) : |a| ^ n = |a ^ n| :=
 lemma abs_neg_one_pow (n : ℕ) : |(-1 : R) ^ n| = 1 :=
 by rw [←pow_abs, abs_neg, abs_one, one_pow]
 
+lemma abs_pow_eq_one (a : R) {n : ℕ} (h : 0 < n) :
+  |a ^ n| = 1 ↔ |a| = 1 :=
+by { convert pow_left_inj (abs_nonneg a) zero_le_one h,
+  exacts [(pow_abs _ _).symm, (one_pow _).symm] }
+
 theorem pow_bit0_nonneg (a : R) (n : ℕ) : 0 ≤ a ^ bit0 n :=
 by { rw pow_bit0, exact mul_self_nonneg _ }
 
diff --git a/src/algebra/ring/equiv.lean b/src/algebra/ring/equiv.lean
@@ -392,6 +392,9 @@ variables [non_assoc_ring R] [non_assoc_ring S] (f : R ≃+* S) (x y : R)
 
 @[simp] lemma map_neg_one : f (-1) = -1 := f.map_one ▸ f.map_neg 1
 
+lemma map_eq_neg_one_iff {x : R} : f x = -1 ↔ x = -1 :=
+by rw [← neg_eq_iff_eq_neg, ← neg_eq_iff_eq_neg, ← map_neg, ring_equiv.map_eq_one_iff]
+
 end ring
 
 section non_unital_semiring_hom
diff --git a/src/field_theory/galois.lean b/src/field_theory/galois.lean
@@ -424,6 +424,16 @@ end is_galois
 
 end galois_equivalent_definitions
 
+section normal_closure
+
+variables (k K F : Type*) [field k] [field K] [field F] [algebra k K] [algebra k F]
+  [algebra K F] [is_scalar_tower k K F] [is_galois k F]
+
+instance is_galois.normal_closure : is_galois k (normal_closure k K F) :=
+{ to_is_separable := is_separable_tower_bot_of_is_separable k _ F }
+
+end normal_closure
+
 section is_alg_closure
 
 @[priority 100]
diff --git a/src/field_theory/is_alg_closed/algebraic_closure.lean b/src/field_theory/is_alg_closed/algebraic_closure.lean
@@ -4,6 +4,7 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Kenny Lau
 -/
 import algebra.direct_limit
+import algebra.char_p.algebra
 import field_theory.is_alg_closed.basic
 
 /-!
diff --git a/src/field_theory/is_alg_closed/basic.lean b/src/field_theory/is_alg_closed/basic.lean
@@ -411,6 +411,10 @@ variables [algebra R S] [algebra R L] [is_scalar_tower R S L]
 variables [algebra K J] [algebra J L] [is_alg_closure J L] [algebra K L]
   [is_scalar_tower K J L]
 
+/-- If `J` is an algebraic extension of `K` and `L` is an algebraic closure of `J`, then it is
+  also an algebraic closure of `K`. -/
+lemma of_algebraic (hKJ : algebra.is_algebraic K J) : is_alg_closure K L :=
+⟨is_alg_closure.alg_closed J, algebra.is_algebraic_trans hKJ is_alg_closure.algebraic⟩
 
 /-- A (random) isomorphism between an algebraic closure of `R` and an algebraic closure of
   an algebraic extension of `R` -/
diff --git a/src/field_theory/normal.lean b/src/field_theory/normal.lean
@@ -435,6 +435,9 @@ begin
   apply intermediate_field.finite_dimensional_supr_of_finite,
 end
 
+instance is_scalar_tower : is_scalar_tower F (normal_closure F K L) L :=
+is_scalar_tower.subalgebra' F L L _
+
 end normal_closure
 
 end normal_closure
diff --git a/src/number_theory/number_field/norm.lean b/src/number_theory/number_field/norm.lean
@@ -22,7 +22,7 @@ rings of integers.
 
 open_locale number_field big_operators
 
-open finset number_field algebra
+open finset number_field algebra finite_dimensional
 
 namespace ring_of_integers
 
@@ -37,7 +37,15 @@ local attribute [instance] number_field.ring_of_integers_algebra
 lemma coe_algebra_map_norm [is_separable K L] (x : 𝓞 L) :
   (algebra_map (𝓞 K) (𝓞 L) (norm K x) : L) = algebra_map K L (algebra.norm K (x : L)) := rfl
 
-lemma is_unit_norm [is_galois K L] {x : 𝓞 L} :
+lemma coe_norm_algebra_map [is_separable K L] (x : 𝓞 K) :
+  (norm K (algebra_map (𝓞 K) (𝓞 L) x) : K) = algebra.norm K (algebra_map K L x) := rfl
+
+lemma norm_algebra_map [is_separable K L] (x : 𝓞 K) :
+  norm K (algebra_map (𝓞 K) (𝓞 L) x) = x ^ finrank K L :=
+by rw [← subtype.coe_inj, ring_of_integers.coe_norm_algebra_map, algebra.norm_algebra_map,
+  subsemiring_class.coe_pow]
+
+lemma is_unit_norm_of_is_galois [is_galois K L] {x : 𝓞 L} :
   is_unit (norm K x) ↔ is_unit x :=
 begin
   classical,
@@ -68,4 +76,32 @@ begin
   simp [← finset.mul_prod_erase _ _ (mem_univ alg_equiv.refl)]
 end
 
+variables (F : Type*) [field F] [algebra K F] [is_separable K F] [finite_dimensional K F]
+
+lemma norm_norm [is_separable K L] [algebra F L] [is_separable F L] [finite_dimensional F L]
+  [is_scalar_tower K F L] (x : 𝓞 L) : norm K (norm F x) = norm K x :=
+by rw [← subtype.coe_inj, norm_apply_coe, norm_apply_coe, norm_apply_coe, algebra.norm_norm]
+
+variable {F}
+
+lemma is_unit_norm [char_zero K] {x : 𝓞 F} :
+  is_unit (norm K x) ↔ is_unit x :=
+begin
+  letI : algebra K (algebraic_closure K) := algebraic_closure.algebra K,
+  let L := normal_closure K F (algebraic_closure F),
+  haveI : finite_dimensional F L := finite_dimensional.right K F L,
+  haveI : is_alg_closure K (algebraic_closure F) :=
+    is_alg_closure.of_algebraic K F (algebraic_closure F) (algebra.is_algebraic_of_finite K F),
+  haveI : is_galois F L := is_galois.tower_top_of_is_galois K F L,
+  calc
+    is_unit (norm K x) ↔ is_unit ((norm K) x ^ finrank F L) :
+        (is_unit_pow_iff (pos_iff_ne_zero.mp finrank_pos)).symm
+      ... ↔ is_unit (norm K (algebra_map (𝓞 F) (𝓞 L) x)) :
+        by rw [← norm_norm K F (algebra_map (𝓞 F) (𝓞 L) x), norm_algebra_map F _, map_pow]
+      ... ↔ is_unit (algebra_map (𝓞 F) (𝓞 L) x) : is_unit_norm_of_is_galois K
+      ... ↔ is_unit (norm F (algebra_map (𝓞 F) (𝓞 L) x)) : (is_unit_norm_of_is_galois F).symm
+      ... ↔ is_unit (x ^ finrank F L) : (congr_arg is_unit (norm_algebra_map F _)).to_iff
+      ... ↔ is_unit x : is_unit_pow_iff (pos_iff_ne_zero.mp finrank_pos),
+end
+
 end ring_of_integers
diff --git a/src/number_theory/number_field/units.lean b/src/number_theory/number_field/units.lean
@@ -0,0 +1,50 @@
+/-
+Copyright (c) 2023 Xavier Roblot. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Xavier Roblot
+-/
+import number_theory.number_field.norm
+
+/-!
+# Units of a number field
+We prove results about the group `(𝓞 K)ˣ` of units of the ring of integers `𝓞 K` of a number
+field `K`.
+
+## Main results
+* `number_field.is_unit_iff_norm`: an algebraic integer `x : 𝓞 K` is a unit if and only if
+`|norm ℚ x| = 1`
+
+## Tags
+number field, units
+ -/
+
+open_locale number_field
+
+noncomputable theory
+
+open number_field units
+
+section rat
+
+lemma rat.ring_of_integers.is_unit_iff {x : 𝓞 ℚ} :
+  is_unit x ↔ ((x : ℚ) = 1) ∨ ((x : ℚ) = -1) :=
+by simp_rw [(is_unit_map_iff (rat.ring_of_integers_equiv : 𝓞 ℚ →+* ℤ) x).symm, int.is_unit_iff,
+  ring_equiv.coe_to_ring_hom, ring_equiv.map_eq_one_iff, ring_equiv.map_eq_neg_one_iff,
+  ← subtype.coe_injective.eq_iff, add_subgroup_class.coe_neg, algebra_map.coe_one]
+
+end rat
+
+variables (K : Type*) [field K]
+
+section is_unit
+
+local attribute [instance] number_field.ring_of_integers_algebra
+
+variable {K}
+
+lemma is_unit_iff_norm [number_field K] (x : 𝓞 K) :
+  is_unit x ↔ |(ring_of_integers.norm ℚ x : ℚ)| = 1 :=
+by { convert (ring_of_integers.is_unit_norm ℚ).symm,
+  rw [← abs_one, abs_eq_abs, ← rat.ring_of_integers.is_unit_iff], }
+
+end is_unit
