From de183ff9862375be655303343aa60b50f9cc96be Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Xavier-Fran=C3=A7ois=20Roblot?= <46200072+xroblot@users.noreply.github.com> Date: Thu, 6 Jul 2023 22:06:14 +0200 Subject: [PATCH 01/12] 1st commit --- Mathlib/GroupTheory/Torsion.lean | 4 +- Mathlib/NumberTheory/NumberField/Units.lean | 60 +++++++++++++++++++++ 2 files changed, 63 insertions(+), 1 deletion(-) diff --git a/Mathlib/GroupTheory/Torsion.lean b/Mathlib/GroupTheory/Torsion.lean index 49a729a7d3eef..86e6fcdc99b75 100644 --- a/Mathlib/GroupTheory/Torsion.lean +++ b/Mathlib/GroupTheory/Torsion.lean @@ -326,6 +326,9 @@ theorem torsion_eq_torsion_submonoid : CommMonoid.torsion G = (torsion G).toSubm #align comm_group.torsion_eq_torsion_submonoid CommGroup.torsion_eq_torsion_submonoid #align add_comm_group.add_torsion_eq_add_torsion_submonoid AddCommGroup.add_torsion_eq_add_torsion_submonoid +@[to_additive] +theorem mem_torsion (g : G) : g ∈ torsion G ↔ IsOfFinOrder g := Iff.rfl + variable (p : β„•) [hp : Fact p.Prime] /-- The `p`-primary component is the subgroup of elements with order prime-power of `p`. -/ @@ -441,4 +444,3 @@ theorem IsTorsionFree.quotient_torsion : IsTorsionFree <| G β§Έ torsion G := fun #align add_is_torsion_free.quotient_torsion AddIsTorsionFree.quotient_torsion end CommGroup - diff --git a/Mathlib/NumberTheory/NumberField/Units.lean b/Mathlib/NumberTheory/NumberField/Units.lean index 32a20af73d41e..55054ea7c7d6a 100644 --- a/Mathlib/NumberTheory/NumberField/Units.lean +++ b/Mathlib/NumberTheory/NumberField/Units.lean @@ -8,7 +8,10 @@ Authors: Xavier Roblot ! Please do not edit these lines, except to modify the commit id ! if you have ported upstream changes. -/ +import Mathlib.GroupTheory.Torsion +import Mathlib.NumberTheory.NumberField.Embeddings import Mathlib.NumberTheory.NumberField.Norm +import Mathlib.RingTheory.RootsOfUnity.Basic /-! # Units of a number field @@ -54,3 +57,60 @@ theorem isUnit_iff_norm [NumberField K] (x : π“ž K) : #align is_unit_iff_norm isUnit_iff_norm end IsUnit + +namespace NumberField.units + +section coe + +/-- The `MonoidHom` from the group of units `(π“ž K)Λ£` to the field `K`. -/ +def coe_to_field : (π“ž K)Λ£ β†’* K := (Units.coeHom K).comp (map (algebraMap (π“ž K) K)) + +theorem coe_to_field_injective : Function.Injective (coe_to_field K) := + fun _ _ h => Units.eq_iff.mp (SetCoe.ext h) + +/-- There is a natural coercion from `(π“ž K)Λ£` to `(π“ž K)` and then from `(π“ž K)` to `K` but it is +useful to also have a direct one from `(π“ž K)Λ£` to `K`. -/ +instance : Coe (π“ž K)Λ£ K := ⟨coe_to_field K⟩ + +@[ext] +theorem ext {x y : (π“ž K)Λ£} (h : (x : K) = y) : x = y := (coe_to_field_injective K).eq_iff.mp h + +end coe + +open NumberField.InfinitePlace + +section torsion + +/-- The torsion subgroup of the group of units. -/ +def torsion : Subgroup (π“ž K)Λ£ := CommGroup.torsion (π“ž K)Λ£ + +theorem mem_torsion {x : (π“ž K)Λ£} [NumberField K] : + x ∈ torsion K ↔ βˆ€ w : InfinitePlace K, w x = 1 := by + rw [eq_iff_eq (x : K) 1, torsion, CommGroup.mem_torsion, isOfFinOrder_iff_pow_eq_one] + refine ⟨fun ⟨n, h_pos, h_eq⟩ Ο† => ?_, fun h => ?_⟩ + Β· refine norm_map_one_of_pow_eq_one Ο†.toMonoidHom (k := ⟨n, h_pos⟩) ?_ + rw [PNat.mk_coe, ← map_pow, h_eq, map_one] + Β· obtain ⟨n, hn, hx⟩ := Embeddings.pow_eq_one_of_norm_eq_one K β„‚ x.val.prop h + exact ⟨n, hn, by ext; rwa [map_pow, map_one]⟩ +end torsion + +instance : Nonempty (torsion K) := ⟨1⟩ + +/-- The torsion subgroup is finite. -/ +instance [NumberField K] : Fintype (torsion K) := by + refine @Fintype.ofFinite _ (Set.finite_coe_iff.mpr ?_) + refine Set.Finite.of_finite_image ?_ ((coe_to_field_injective K).injOn _) + refine (Embeddings.finite_of_norm_le K β„‚ 1).subset + (fun a ⟨u, ⟨h_tors, h_ua⟩⟩ => ⟨?_, fun Ο† => ?_⟩) + Β· rw [← h_ua] + exact u.val.prop + Β· rw [← h_ua] + exact le_of_eq ((eq_iff_eq _ 1).mp ((mem_torsion K).mp h_tors) Ο†) + +/-- The torsion subgroup is cylic. -/ +instance [NumberField K] : IsCyclic (torsion K) := subgroup_units_cyclic _ + +/-- The order of the torsion subgroup as positive integer. -/ +def torsion_order [NumberField K] : β„•+ := ⟨Fintype.card (torsion K), Fintype.card_pos⟩ + +end NumberField.units From 993f95a36e36bf7c2cbd442174432e8665bd60c7 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Xavier-Fran=C3=A7ois=20Roblot?= <46200072+xroblot@users.noreply.github.com> Date: Sat, 8 Jul 2023 11:27:18 +0200 Subject: [PATCH 02/12] add results about rootsOfUnity --- Mathlib/NumberTheory/NumberField/Units.lean | 25 +++++++++++++++++++++ 1 file changed, 25 insertions(+) diff --git a/Mathlib/NumberTheory/NumberField/Units.lean b/Mathlib/NumberTheory/NumberField/Units.lean index 55054ea7c7d6a..44b1151684e22 100644 --- a/Mathlib/NumberTheory/NumberField/Units.lean +++ b/Mathlib/NumberTheory/NumberField/Units.lean @@ -113,4 +113,29 @@ instance [NumberField K] : IsCyclic (torsion K) := subgroup_units_cyclic _ /-- The order of the torsion subgroup as positive integer. -/ def torsion_order [NumberField K] : β„•+ := ⟨Fintype.card (torsion K), Fintype.card_pos⟩ +/-- If `k` does not divide `torsion_order` then there are no nontrivial roots of unity of + order dividing `k`. -/ +theorem rootsOfUnity_eq_one [NumberField K] {k : β„•+} (hc : Nat.coprime k (torsion_order K)) : + ΞΆ ∈ rootsOfUnity k (π“ž K) ↔ ΞΆ = 1 := by + rw [mem_rootsOfUnity] + refine ⟨fun h => ?_, fun h => by rw [h, one_pow]⟩ + refine orderOf_eq_one_iff.mp (Nat.eq_one_of_dvd_coprimes hc ?_ ?_) + Β· exact orderOf_dvd_of_pow_eq_one h + Β· have hΞΆ : ΞΆ ∈ torsion K := by + rw [torsion, CommGroup.mem_torsion, isOfFinOrder_iff_pow_eq_one] + exact ⟨k, k.prop, h⟩ + rw [orderOf_submonoid (⟨΢, h΢⟩ : torsion K)] + exact orderOf_dvd_card_univ + +/-- The group of roots of unity of order dividing `torsion_order` is equal to the torsion +group. -/ +theorem rootsOfUnity_eq_torsion [NumberField K] : + rootsOfUnity (torsion_order K) (π“ž K) = torsion K := by + ext ΞΆ + rw [torsion, mem_rootsOfUnity] + refine ⟨fun h => ?_, fun h => ?_⟩ + Β· rw [CommGroup.mem_torsion, isOfFinOrder_iff_pow_eq_one] + exact βŸ¨β†‘(torsion_order K), (torsion_order K).prop, h⟩ + Β· exact Subtype.ext_iff.mp (@pow_card_eq_one (torsion K) ⟨΢, h⟩ _ _) + end NumberField.units From 4a13f8666738d3aa06671cd26413a6620c04dd02 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Xavier-Fran=C3=A7ois=20Roblot?= <46200072+xroblot@users.noreply.github.com> Date: Wed, 19 Jul 2023 08:45:48 +0900 Subject: [PATCH 03/12] Update --- Mathlib/NumberTheory/NumberField/Units.lean | 15 +++++++++++++-- 1 file changed, 13 insertions(+), 2 deletions(-) diff --git a/Mathlib/NumberTheory/NumberField/Units.lean b/Mathlib/NumberTheory/NumberField/Units.lean index 44b1151684e22..bb7da44c68656 100644 --- a/Mathlib/NumberTheory/NumberField/Units.lean +++ b/Mathlib/NumberTheory/NumberField/Units.lean @@ -65,16 +65,27 @@ section coe /-- The `MonoidHom` from the group of units `(π“ž K)Λ£` to the field `K`. -/ def coe_to_field : (π“ž K)Λ£ β†’* K := (Units.coeHom K).comp (map (algebraMap (π“ž K) K)) +variable {K} + +@[coe] def to_field (x : (π“ž K)Λ£) : K := coe_to_field K x + +variable (K) + theorem coe_to_field_injective : Function.Injective (coe_to_field K) := fun _ _ h => Units.eq_iff.mp (SetCoe.ext h) /-- There is a natural coercion from `(π“ž K)Λ£` to `(π“ž K)` and then from `(π“ž K)` to `K` but it is useful to also have a direct one from `(π“ž K)Λ£` to `K`. -/ -instance : Coe (π“ž K)Λ£ K := ⟨coe_to_field K⟩ +instance : Coe (π“ž K)Λ£ K := ⟨to_field⟩ @[ext] theorem ext {x y : (π“ž K)Λ£} (h : (x : K) = y) : x = y := (coe_to_field_injective K).eq_iff.mp h +theorem map_pow (x : (π“ž K)Λ£) (n : β„•) : (x ^ n : K) = (x : K) ^ n := + _root_.map_pow (coe_to_field K) x n + +theorem map_one : ((1 : (π“ž K)Λ£) : K) = 1 := rfl + end coe open NumberField.InfinitePlace @@ -136,6 +147,6 @@ theorem rootsOfUnity_eq_torsion [NumberField K] : refine ⟨fun h => ?_, fun h => ?_⟩ Β· rw [CommGroup.mem_torsion, isOfFinOrder_iff_pow_eq_one] exact βŸ¨β†‘(torsion_order K), (torsion_order K).prop, h⟩ - Β· exact Subtype.ext_iff.mp (@pow_card_eq_one (torsion K) ⟨΢, h⟩ _ _) + Β· exact Subtype.ext_iff.mp (@pow_card_eq_one (torsion K) _ ⟨΢, h⟩ _) end NumberField.units From 929e27ec8b8f2e16db5f3015f7e4621f2244daaf Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Xavier-Fran=C3=A7ois=20Roblot?= <46200072+xroblot@users.noreply.github.com> Date: Wed, 19 Jul 2023 15:51:34 +0900 Subject: [PATCH 04/12] backport --- Mathlib/NumberTheory/NumberField/Units.lean | 14 +++++++++++--- 1 file changed, 11 insertions(+), 3 deletions(-) diff --git a/Mathlib/NumberTheory/NumberField/Units.lean b/Mathlib/NumberTheory/NumberField/Units.lean index bb7da44c68656..292e87c63702a 100644 --- a/Mathlib/NumberTheory/NumberField/Units.lean +++ b/Mathlib/NumberTheory/NumberField/Units.lean @@ -50,7 +50,7 @@ attribute [local instance] NumberField.ringOfIntegersAlgebra variable {K} -theorem isUnit_iff_norm [NumberField K] (x : π“ž K) : +theorem isUnit_iff_norm [NumberField K] {x : π“ž K} : IsUnit x ↔ |(RingOfIntegers.norm β„š x : β„š)| = 1 := by convert (RingOfIntegers.isUnit_norm β„š (F := K)).symm rw [← abs_one, abs_eq_abs, ← Rat.RingOfIntegers.isUnit_iff] @@ -58,7 +58,7 @@ theorem isUnit_iff_norm [NumberField K] (x : π“ž K) : end IsUnit -namespace NumberField.units +namespace NumberField.Units section coe @@ -67,6 +67,7 @@ def coe_to_field : (π“ž K)Λ£ β†’* K := (Units.coeHom K).comp (map (algebraMap ( variable {K} +/-- The coercion of `x : (π“ž K)Λ£` into `K`. -/ @[coe] def to_field (x : (π“ž K)Λ£) : K := coe_to_field K x variable (K) @@ -81,11 +82,17 @@ instance : Coe (π“ž K)Λ£ K := ⟨to_field⟩ @[ext] theorem ext {x y : (π“ž K)Λ£} (h : (x : K) = y) : x = y := (coe_to_field_injective K).eq_iff.mp h +@[simp] theorem map_pow (x : (π“ž K)Λ£) (n : β„•) : (x ^ n : K) = (x : K) ^ n := _root_.map_pow (coe_to_field K) x n +@[simp] theorem map_one : ((1 : (π“ž K)Λ£) : K) = 1 := rfl +@[simp] +theorem ne_zero (x : (π“ž K)Λ£) : (x : K) β‰  0 := + Subtype.coe_injective.ne_iff.mpr (_root_.Units.ne_zero x) + end coe open NumberField.InfinitePlace @@ -103,7 +110,6 @@ theorem mem_torsion {x : (π“ž K)Λ£} [NumberField K] : rw [PNat.mk_coe, ← map_pow, h_eq, map_one] Β· obtain ⟨n, hn, hx⟩ := Embeddings.pow_eq_one_of_norm_eq_one K β„‚ x.val.prop h exact ⟨n, hn, by ext; rwa [map_pow, map_one]⟩ -end torsion instance : Nonempty (torsion K) := ⟨1⟩ @@ -149,4 +155,6 @@ theorem rootsOfUnity_eq_torsion [NumberField K] : exact βŸ¨β†‘(torsion_order K), (torsion_order K).prop, h⟩ Β· exact Subtype.ext_iff.mp (@pow_card_eq_one (torsion K) _ ⟨΢, h⟩ _) +end torsion + end NumberField.units From 57192afac26cb9fb1b729686b617474f4ae07222 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Xavier-Fran=C3=A7ois=20Roblot?= <46200072+xroblot@users.noreply.github.com> Date: Wed, 19 Jul 2023 16:33:39 +0900 Subject: [PATCH 05/12] Fix end --- Mathlib/NumberTheory/NumberField/Units.lean | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/Mathlib/NumberTheory/NumberField/Units.lean b/Mathlib/NumberTheory/NumberField/Units.lean index 292e87c63702a..ab3887d2015aa 100644 --- a/Mathlib/NumberTheory/NumberField/Units.lean +++ b/Mathlib/NumberTheory/NumberField/Units.lean @@ -157,4 +157,4 @@ theorem rootsOfUnity_eq_torsion [NumberField K] : end torsion -end NumberField.units +end NumberField.Units From 8aa9980c0d66608b2a535b3b785fc69fcf385514 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Xavier-Fran=C3=A7ois=20Roblot?= <46200072+xroblot@users.noreply.github.com> Date: Wed, 19 Jul 2023 18:44:14 +0900 Subject: [PATCH 06/12] Add doc --- Mathlib/NumberTheory/NumberField/Units.lean | 3 ++- 1 file changed, 2 insertions(+), 1 deletion(-) diff --git a/Mathlib/NumberTheory/NumberField/Units.lean b/Mathlib/NumberTheory/NumberField/Units.lean index ab3887d2015aa..85724eb59158f 100644 --- a/Mathlib/NumberTheory/NumberField/Units.lean +++ b/Mathlib/NumberTheory/NumberField/Units.lean @@ -19,7 +19,8 @@ We prove results about the group `(π“ž K)Λ£` of units of the ring of integers ` field `K`. ## Main results -* `isUnit_iff_norm`: an algebraic integer `x : π“ž K` is a unit if and only if `|norm β„š x| = 1` +* `isUnit_iff_norm`: an algebraic integer `x : π“ž K` is a unit if and only if `|norm β„š x| = 1`. +* `mem_torsion`: a unit `x : (π“ž K)Λ£` is torsion iff `w x = 1` for all infinite places of `K`. ## Tags number field, units From 2238c4fe908547ab81a1d97ce89e04c485299949 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Xavier-Fran=C3=A7ois=20Roblot?= <46200072+xroblot@users.noreply.github.com> Date: Sun, 30 Jul 2023 08:31:17 +0900 Subject: [PATCH 07/12] Add map_zpow --- Mathlib/NumberTheory/NumberField/Units.lean | 4 ++++ 1 file changed, 4 insertions(+) diff --git a/Mathlib/NumberTheory/NumberField/Units.lean b/Mathlib/NumberTheory/NumberField/Units.lean index 85724eb59158f..66e6d972a176e 100644 --- a/Mathlib/NumberTheory/NumberField/Units.lean +++ b/Mathlib/NumberTheory/NumberField/Units.lean @@ -87,6 +87,10 @@ theorem ext {x y : (π“ž K)Λ£} (h : (x : K) = y) : x = y := (coe_to_field_inject theorem map_pow (x : (π“ž K)Λ£) (n : β„•) : (x ^ n : K) = (x : K) ^ n := _root_.map_pow (coe_to_field K) x n +@[simp] +theorem map_zpow (x : (π“ž K)Λ£) (n : β„€) : (x ^ n : K) = (x : K) ^ n := + _root_.map_zpow (coe_to_field K) x n + @[simp] theorem map_one : ((1 : (π“ž K)Λ£) : K) = 1 := rfl From 6c5a344f77230f3961ea49995b7b25f242b14569 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Xavier-Fran=C3=A7ois=20Roblot?= <46200072+xroblot@users.noreply.github.com> Date: Sun, 30 Jul 2023 08:33:11 +0900 Subject: [PATCH 08/12] Add coe_coe --- Mathlib/NumberTheory/NumberField/Units.lean | 3 +++ 1 file changed, 3 insertions(+) diff --git a/Mathlib/NumberTheory/NumberField/Units.lean b/Mathlib/NumberTheory/NumberField/Units.lean index 66e6d972a176e..8f2fe078d27b6 100644 --- a/Mathlib/NumberTheory/NumberField/Units.lean +++ b/Mathlib/NumberTheory/NumberField/Units.lean @@ -83,6 +83,9 @@ instance : Coe (π“ž K)Λ£ K := ⟨to_field⟩ @[ext] theorem ext {x y : (π“ž K)Λ£} (h : (x : K) = y) : x = y := (coe_to_field_injective K).eq_iff.mp h +@[simp] +theorem coe_coe (x : (π“ž K)Λ£) : ((x : π“ž K) : K) = (x : K) := rfl + @[simp] theorem map_pow (x : (π“ž K)Λ£) (n : β„•) : (x ^ n : K) = (x : K) ^ n := _root_.map_pow (coe_to_field K) x n From 4dbe2df92d3c7cc0a926b16eb5a092a58bdae84b Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Xavier-Fran=C3=A7ois=20Roblot?= <46200072+xroblot@users.noreply.github.com> Date: Wed, 2 Aug 2023 10:50:27 +0900 Subject: [PATCH 09/12] Review --- Mathlib/NumberTheory/NumberField/Units.lean | 3 ++- 1 file changed, 2 insertions(+), 1 deletion(-) diff --git a/Mathlib/NumberTheory/NumberField/Units.lean b/Mathlib/NumberTheory/NumberField/Units.lean index 8f2fe078d27b6..44176a404b560 100644 --- a/Mathlib/NumberTheory/NumberField/Units.lean +++ b/Mathlib/NumberTheory/NumberField/Units.lean @@ -119,7 +119,8 @@ theorem mem_torsion {x : (π“ž K)Λ£} [NumberField K] : Β· obtain ⟨n, hn, hx⟩ := Embeddings.pow_eq_one_of_norm_eq_one K β„‚ x.val.prop h exact ⟨n, hn, by ext; rwa [map_pow, map_one]⟩ -instance : Nonempty (torsion K) := ⟨1⟩ +/-- Shortcut instance because Lean tends to time out before finding the general instance. -/ +instance : Nonempty (torsion K) := One.nonempty /-- The torsion subgroup is finite. -/ instance [NumberField K] : Fintype (torsion K) := by From abfa77e58077f8daee2403e5f644f1c2a598a840 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Xavier-Fran=C3=A7ois=20Roblot?= <46200072+xroblot@users.noreply.github.com> Date: Wed, 2 Aug 2023 17:08:06 +0900 Subject: [PATCH 10/12] Remove coercion --- Mathlib/NumberTheory/NumberField/Units.lean | 45 ++++++--------------- 1 file changed, 12 insertions(+), 33 deletions(-) diff --git a/Mathlib/NumberTheory/NumberField/Units.lean b/Mathlib/NumberTheory/NumberField/Units.lean index 44176a404b560..488a7fa89d151 100644 --- a/Mathlib/NumberTheory/NumberField/Units.lean +++ b/Mathlib/NumberTheory/NumberField/Units.lean @@ -63,42 +63,21 @@ namespace NumberField.Units section coe -/-- The `MonoidHom` from the group of units `(π“ž K)Λ£` to the field `K`. -/ -def coe_to_field : (π“ž K)Λ£ β†’* K := (Units.coeHom K).comp (map (algebraMap (π“ž K) K)) +theorem coe_injective : Function.Injective ((↑) : (π“ž K)Λ£ β†’ K) := + fun _ _ h => by rwa [SetLike.coe_eq_coe, Units.eq_iff] at h variable {K} -/-- The coercion of `x : (π“ž K)Λ£` into `K`. -/ -@[coe] def to_field (x : (π“ž K)Λ£) : K := coe_to_field K x +theorem coe_pow (x : (π“ž K)Λ£) (n : β„•) : (x ^ n : K) = (x : K) ^ n := by + rw [← SubmonoidClass.coe_pow, ← val_pow_eq_pow_val] -variable (K) +theorem coe_zpow (x : (π“ž K)Λ£) (n : β„€) : (x ^ n : K) = (x : K) ^ n := by + change ((Units.coeHom K).comp (map (algebraMap (π“ž K) K))) (x ^ n) = _ + exact _root_.map_zpow _ x n -theorem coe_to_field_injective : Function.Injective (coe_to_field K) := - fun _ _ h => Units.eq_iff.mp (SetCoe.ext h) +theorem coe_one : ((1 : (π“ž K)Λ£) : K) = (1 : K) := rfl -/-- There is a natural coercion from `(π“ž K)Λ£` to `(π“ž K)` and then from `(π“ž K)` to `K` but it is -useful to also have a direct one from `(π“ž K)Λ£` to `K`. -/ -instance : Coe (π“ž K)Λ£ K := ⟨to_field⟩ - -@[ext] -theorem ext {x y : (π“ž K)Λ£} (h : (x : K) = y) : x = y := (coe_to_field_injective K).eq_iff.mp h - -@[simp] -theorem coe_coe (x : (π“ž K)Λ£) : ((x : π“ž K) : K) = (x : K) := rfl - -@[simp] -theorem map_pow (x : (π“ž K)Λ£) (n : β„•) : (x ^ n : K) = (x : K) ^ n := - _root_.map_pow (coe_to_field K) x n - -@[simp] -theorem map_zpow (x : (π“ž K)Λ£) (n : β„€) : (x ^ n : K) = (x : K) ^ n := - _root_.map_zpow (coe_to_field K) x n - -@[simp] -theorem map_one : ((1 : (π“ž K)Λ£) : K) = 1 := rfl - -@[simp] -theorem ne_zero (x : (π“ž K)Λ£) : (x : K) β‰  0 := +theorem coe_ne_zero (x : (π“ž K)Λ£) : (x : K) β‰  0 := Subtype.coe_injective.ne_iff.mpr (_root_.Units.ne_zero x) end coe @@ -115,9 +94,9 @@ theorem mem_torsion {x : (π“ž K)Λ£} [NumberField K] : rw [eq_iff_eq (x : K) 1, torsion, CommGroup.mem_torsion, isOfFinOrder_iff_pow_eq_one] refine ⟨fun ⟨n, h_pos, h_eq⟩ Ο† => ?_, fun h => ?_⟩ Β· refine norm_map_one_of_pow_eq_one Ο†.toMonoidHom (k := ⟨n, h_pos⟩) ?_ - rw [PNat.mk_coe, ← map_pow, h_eq, map_one] + rw [PNat.mk_coe, ← coe_pow, h_eq, coe_one] Β· obtain ⟨n, hn, hx⟩ := Embeddings.pow_eq_one_of_norm_eq_one K β„‚ x.val.prop h - exact ⟨n, hn, by ext; rwa [map_pow, map_one]⟩ + exact ⟨n, hn, by ext; rw [coe_pow, hx, coe_one]⟩ /-- Shortcut instance because Lean tends to time out before finding the general instance. -/ instance : Nonempty (torsion K) := One.nonempty @@ -125,7 +104,7 @@ instance : Nonempty (torsion K) := One.nonempty /-- The torsion subgroup is finite. -/ instance [NumberField K] : Fintype (torsion K) := by refine @Fintype.ofFinite _ (Set.finite_coe_iff.mpr ?_) - refine Set.Finite.of_finite_image ?_ ((coe_to_field_injective K).injOn _) + refine Set.Finite.of_finite_image ?_ ((coe_injective K).injOn _) refine (Embeddings.finite_of_norm_le K β„‚ 1).subset (fun a ⟨u, ⟨h_tors, h_ua⟩⟩ => ⟨?_, fun Ο† => ?_⟩) Β· rw [← h_ua] From e8e322bd51844e6cedf343b06788971cc33ca7b8 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Xavier-Fran=C3=A7ois=20Roblot?= <46200072+xroblot@users.noreply.github.com> Date: Wed, 2 Aug 2023 17:10:14 +0900 Subject: [PATCH 11/12] Clean up --- Mathlib/NumberTheory/NumberField/Units.lean | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/Mathlib/NumberTheory/NumberField/Units.lean b/Mathlib/NumberTheory/NumberField/Units.lean index 488a7fa89d151..692934e52c23c 100644 --- a/Mathlib/NumberTheory/NumberField/Units.lean +++ b/Mathlib/NumberTheory/NumberField/Units.lean @@ -73,7 +73,7 @@ theorem coe_pow (x : (π“ž K)Λ£) (n : β„•) : (x ^ n : K) = (x : K) ^ n := by theorem coe_zpow (x : (π“ž K)Λ£) (n : β„€) : (x ^ n : K) = (x : K) ^ n := by change ((Units.coeHom K).comp (map (algebraMap (π“ž K) K))) (x ^ n) = _ - exact _root_.map_zpow _ x n + exact map_zpow _ x n theorem coe_one : ((1 : (π“ž K)Λ£) : K) = (1 : K) := rfl From 3d5e3349f1dfdbb67903944c9fc7bc2a0c8d333d Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Xavier-Fran=C3=A7ois=20Roblot?= <46200072+xroblot@users.noreply.github.com> Date: Thu, 3 Aug 2023 08:27:12 +0900 Subject: [PATCH 12/12] Add coe_mul and coe_neg_one --- Mathlib/NumberTheory/NumberField/Units.lean | 4 ++++ 1 file changed, 4 insertions(+) diff --git a/Mathlib/NumberTheory/NumberField/Units.lean b/Mathlib/NumberTheory/NumberField/Units.lean index 4c199e36e474c..dfcd0baead598 100644 --- a/Mathlib/NumberTheory/NumberField/Units.lean +++ b/Mathlib/NumberTheory/NumberField/Units.lean @@ -65,6 +65,8 @@ theorem coe_injective : Function.Injective ((↑) : (π“ž K)Λ£ β†’ K) := variable {K} +theorem coe_mul (x y : (π“ž K)Λ£) : ((x * y : (π“ž K)Λ£) : K) = (x : K) * (y : K) := rfl + theorem coe_pow (x : (π“ž K)Λ£) (n : β„•) : (x ^ n : K) = (x : K) ^ n := by rw [← SubmonoidClass.coe_pow, ← val_pow_eq_pow_val] @@ -74,6 +76,8 @@ theorem coe_zpow (x : (π“ž K)Λ£) (n : β„€) : (x ^ n : K) = (x : K) ^ n := by theorem coe_one : ((1 : (π“ž K)Λ£) : K) = (1 : K) := rfl +theorem coe_neg_one : ((-1 : (π“ž K)Λ£) : K) = (-1 : K) := rfl + theorem coe_ne_zero (x : (π“ž K)Λ£) : (x : K) β‰  0 := Subtype.coe_injective.ne_iff.mpr (_root_.Units.ne_zero x)