From 258961687d388593c812768510ec9894d1cdbbdf Mon Sep 17 00:00:00 2001 From: Riccardo Brasca Date: Fri, 3 May 2024 14:30:04 +0000 Subject: [PATCH] perf(NumberTheory.NumberField.Basic): make `RingOfIntegers` a Type. (#12386) MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit We make `𝓞 K` a type rather then a `Subalgebra` to speed up instances search. Co-authored-by: Anne Baanen <[Vierkantor](https://github.com/Vierkantor)> Co-authored-by: Yaël Dillies <[YaelDillies](https://github.com/YaelDillies)> Co-authored-by: Matthew Ballard <[mattrobball](https://github.com/mattrobball)> Co-authored-by: Ruben Van de Velde <65514131+Ruben-VandeVelde@users.noreply.github.com> Co-authored-by: Matthew Ballard Co-authored-by: Vierkantor Co-authored-by: Yaël Dillies Co-authored-by: Anne Baanen --- Mathlib/NumberTheory/Cyclotomic/Rat.lean | 18 +- Mathlib/NumberTheory/NumberField/Basic.lean | 178 ++++++++++++++---- .../NumberField/CanonicalEmbedding/Basic.lean | 16 +- .../CanonicalEmbedding/ConvexBody.lean | 40 ++-- .../NumberTheory/NumberField/ClassNumber.lean | 12 +- .../NumberField/Discriminant.lean | 33 ++-- .../NumberTheory/NumberField/Embeddings.lean | 6 +- .../NumberField/FractionalIdeal.lean | 7 +- Mathlib/NumberTheory/NumberField/Norm.lean | 40 ++-- .../NumberTheory/NumberField/Units/Basic.lean | 20 +- .../NumberField/Units/DirichletTheorem.lean | 38 ++-- 11 files changed, 263 insertions(+), 145 deletions(-) diff --git a/Mathlib/NumberTheory/Cyclotomic/Rat.lean b/Mathlib/NumberTheory/Cyclotomic/Rat.lean index 8f337bb75ba85..5d08f15987681 100644 --- a/Mathlib/NumberTheory/Cyclotomic/Rat.lean +++ b/Mathlib/NumberTheory/Cyclotomic/Rat.lean @@ -242,9 +242,7 @@ theorem power_basis_int'_dim [hcycl : IsCyclotomicExtension {p} ℚ K] (hζ : Is extension of `ℚ`. -/ noncomputable def subOneIntegralPowerBasis [IsCyclotomicExtension {p ^ k} ℚ K] (hζ : IsPrimitiveRoot ζ ↑(p ^ k)) : PowerBasis ℤ (𝓞 K) := - PowerBasis.ofGenMemAdjoin' hζ.integralPowerBasis - (isIntegral_of_mem_ringOfIntegers <| - Subalgebra.sub_mem _ (hζ.isIntegral (p ^ k).pos) (Subalgebra.one_mem _)) + PowerBasis.ofGenMemAdjoin' hζ.integralPowerBasis (RingOfIntegers.isIntegral _) (by simp only [integralPowerBasis_gen, toInteger] convert Subalgebra.add_mem _ (self_mem_adjoin_singleton ℤ (⟨ζ - 1, _⟩ : 𝓞 K)) @@ -285,13 +283,13 @@ theorem zeta_sub_one_prime_of_ne_two [IsCyclotomicExtension {p ^ (k + 1)} ℚ K] letI := IsCyclotomicExtension.numberField {p ^ (k + 1)} ℚ K refine Ideal.prime_of_irreducible_absNorm_span (fun h ↦ ?_) ?_ · apply hζ.pow_ne_one_of_pos_of_lt zero_lt_one (one_lt_pow hp.out.one_lt (by simp)) - rw [← Subalgebra.coe_eq_zero] at h - simpa [sub_eq_zero] using h + rw [sub_eq_zero] at h + simpa using congrArg (algebraMap _ K) h rw [Nat.irreducible_iff_prime, Ideal.absNorm_span_singleton, ← Nat.prime_iff, ← Int.prime_iff_natAbs_prime] convert Nat.prime_iff_prime_int.1 hp.out apply RingHom.injective_int (algebraMap ℤ ℚ) - rw [← Algebra.norm_localization (Sₘ := K) ℤ (nonZeroDivisors ℤ), Subalgebra.algebraMap_eq] + rw [← Algebra.norm_localization (Sₘ := K) ℤ (nonZeroDivisors ℤ)] simp only [PNat.pow_coe, id.map_eq_id, RingHomCompTriple.comp_eq, RingHom.coe_coe, Subalgebra.coe_val, algebraMap_int_eq, map_natCast] exact hζ.sub_one_norm_prime_ne_two (Polynomial.cyclotomic.irreducible_rat (PNat.pos _)) hodd @@ -304,20 +302,20 @@ theorem zeta_sub_one_prime_of_two_pow [IsCyclotomicExtension {(2 : ℕ+) ^ (k + letI := IsCyclotomicExtension.numberField {(2 : ℕ+) ^ (k + 1)} ℚ K refine Ideal.prime_of_irreducible_absNorm_span (fun h ↦ ?_) ?_ · apply hζ.pow_ne_one_of_pos_of_lt zero_lt_one (one_lt_pow (by decide) (by simp)) - rw [← Subalgebra.coe_eq_zero] at h - simpa [sub_eq_zero] using h + rw [sub_eq_zero] at h + simpa using congrArg (algebraMap _ K) h rw [Nat.irreducible_iff_prime, Ideal.absNorm_span_singleton, ← Nat.prime_iff, ← Int.prime_iff_natAbs_prime] cases k · convert Prime.neg Int.prime_two apply RingHom.injective_int (algebraMap ℤ ℚ) - rw [← Algebra.norm_localization (Sₘ := K) ℤ (nonZeroDivisors ℤ), Subalgebra.algebraMap_eq] + rw [← Algebra.norm_localization (Sₘ := K) ℤ (nonZeroDivisors ℤ)] simp only [Nat.zero_eq, PNat.pow_coe, id.map_eq_id, RingHomCompTriple.comp_eq, RingHom.coe_coe, Subalgebra.coe_val, algebraMap_int_eq, map_neg, map_ofNat] simpa using hζ.pow_sub_one_norm_two (cyclotomic.irreducible_rat (by simp)) convert Int.prime_two apply RingHom.injective_int (algebraMap ℤ ℚ) - rw [← Algebra.norm_localization (Sₘ := K) ℤ (nonZeroDivisors ℤ), Subalgebra.algebraMap_eq] + rw [← Algebra.norm_localization (Sₘ := K) ℤ (nonZeroDivisors ℤ)] simp only [PNat.pow_coe, id.map_eq_id, RingHomCompTriple.comp_eq, RingHom.coe_coe, Subalgebra.coe_val, algebraMap_int_eq, map_natCast] exact hζ.sub_one_norm_two Nat.AtLeastTwo.prop (cyclotomic.irreducible_rat (by simp)) diff --git a/Mathlib/NumberTheory/NumberField/Basic.lean b/Mathlib/NumberTheory/NumberField/Basic.lean index 467ae087723da..674f9c0cdf83e 100644 --- a/Mathlib/NumberTheory/NumberField/Basic.lean +++ b/Mathlib/NumberTheory/NumberField/Basic.lean @@ -15,7 +15,7 @@ This file defines a number field and the ring of integers corresponding to it. ## Main definitions - `NumberField` defines a number field as a field which has characteristic zero and is finite dimensional over ℚ. - - `ringOfIntegers` defines the ring of integers (or number ring) corresponding to a number field + - `RingOfIntegers` defines the ring of integers (or number ring) corresponding to a number field as the integral closure of ℤ in the number field. ## Implementation notes @@ -64,35 +64,88 @@ instance [NumberField L] [Algebra K L] : FiniteDimensional K L := Module.Finite.of_restrictScalars_finite ℚ K L /-- The ring of integers (or number ring) corresponding to a number field -is the integral closure of ℤ in the number field. -/ -def ringOfIntegers := +is the integral closure of ℤ in the number field. + +This is defined as its own type, rather than a `Subalgebra`, for performance reasons: +looking for instances of the form `SMul (RingOfIntegers _) (RingOfIntegers _)` makes +much more effective use of the discrimination tree than instances of the form +`SMul (Subtype _) (Subtype _)`. +The drawback is we have to copy over instances manually. +-/ +def RingOfIntegers : Type _ := integralClosure ℤ K -#align number_field.ring_of_integers NumberField.ringOfIntegers +#align number_field.ring_of_integers NumberField.RingOfIntegers -@[inherit_doc] scoped notation "𝓞" => NumberField.ringOfIntegers +@[inherit_doc] scoped notation "𝓞" => NumberField.RingOfIntegers -theorem mem_ringOfIntegers (x : K) : x ∈ 𝓞 K ↔ IsIntegral ℤ x := - Iff.rfl -#align number_field.mem_ring_of_integers NumberField.mem_ringOfIntegers +#noalign number_field.mem_ring_of_integers -theorem isIntegral_of_mem_ringOfIntegers {K : Type*} [Field K] {x : K} (hx : x ∈ 𝓞 K) : - IsIntegral ℤ (⟨x, hx⟩ : 𝓞 K) := by - obtain ⟨P, hPm, hP⟩ := hx - refine' ⟨P, hPm, _⟩ - rw [← Polynomial.aeval_def, ← Subalgebra.coe_eq_zero, Polynomial.aeval_subalgebra_coe, - Polynomial.aeval_def, Subtype.coe_mk, hP] -#align number_field.is_integral_of_mem_ring_of_integers NumberField.isIntegral_of_mem_ringOfIntegers +namespace RingOfIntegers + +instance : CommRing (𝓞 K) := + inferInstanceAs (CommRing (integralClosure _ _)) +instance : IsDomain (𝓞 K) := + inferInstanceAs (IsDomain (integralClosure _ _)) +instance : CharZero (𝓞 K) := + inferInstanceAs (CharZero (integralClosure _ _)) +instance : Algebra (𝓞 K) K := + inferInstanceAs (Algebra (integralClosure _ _) _) +instance : NoZeroSMulDivisors (𝓞 K) K := + inferInstanceAs (NoZeroSMulDivisors (integralClosure _ _) _) +instance : Nontrivial (𝓞 K) := + inferInstanceAs (Nontrivial (integralClosure _ _)) + +variable {K} + +/-- The canonical coercion from `𝓞 K` to `K`. -/ +@[coe] +abbrev val (x : 𝓞 K) : K := algebraMap _ _ x + +/-- This instance has to be `CoeHead` because we only want to apply it from `𝓞 K` to `K`. -/ +instance : CoeHead (𝓞 K) K := ⟨val⟩ + +lemma coe_eq_algebraMap (x : 𝓞 K) : (x : K) = algebraMap _ _ x := rfl + +@[ext] theorem ext {x y : 𝓞 K} (h : (x : K) = (y : K)) : x = y := + Subtype.ext h + +theorem ext_iff {x y : 𝓞 K} : x = y ↔ (x : K) = (y : K) := + Subtype.ext_iff + +@[simp] lemma map_mk (x : K) (hx) : algebraMap (𝓞 K) K ⟨x, hx⟩ = x := rfl + +lemma coe_mk {x : K} (hx) : ((⟨x, hx⟩ : 𝓞 K) : K) = x := rfl + +lemma mk_eq_mk (x y : K) (hx hy) : (⟨x, hx⟩ : 𝓞 K) = ⟨y, hy⟩ ↔ x = y := by simp + +@[simp] lemma mk_one : (⟨1, one_mem _⟩ : 𝓞 K) = 1 := + rfl + +@[simp] lemma mk_zero : (⟨0, zero_mem _⟩ : 𝓞 K) = 0 := + rfl +-- TODO: these lemmas don't seem to fire? +@[simp] lemma mk_add_mk (x y : K) (hx hy) : (⟨x, hx⟩ : 𝓞 K) + ⟨y, hy⟩ = ⟨x + y, add_mem hx hy⟩ := + rfl + +@[simp] lemma mk_mul_mk (x y : K) (hx hy) : (⟨x, hx⟩ : 𝓞 K) * ⟨y, hy⟩ = ⟨x * y, mul_mem hx hy⟩ := + rfl + +@[simp] lemma mk_sub_mk (x y : K) (hx hy) : (⟨x, hx⟩ : 𝓞 K) - ⟨y, hy⟩ = ⟨x - y, sub_mem hx hy⟩ := + rfl + +@[simp] lemma neg_mk (x : K) (hx) : (-⟨x, hx⟩ : 𝓞 K) = ⟨-x, neg_mem hx⟩ := + rfl + +end RingOfIntegers /-- Given an algebra between two fields, create an algebra between their two rings of integers. -/ instance inst_ringOfIntegersAlgebra [Algebra K L] : Algebra (𝓞 K) (𝓞 L) := RingHom.toAlgebra - { toFun := fun k => ⟨algebraMap K L k, IsIntegral.algebraMap k.2⟩ - map_zero' := Subtype.ext <| by simp only [Subtype.coe_mk, Subalgebra.coe_zero, map_zero] - map_one' := Subtype.ext <| by simp only [Subtype.coe_mk, Subalgebra.coe_one, map_one] - map_add' := fun x y => - Subtype.ext <| by simp only [map_add, Subalgebra.coe_add, Subtype.coe_mk] - map_mul' := fun x y => - Subtype.ext <| by simp only [Subalgebra.coe_mul, map_mul, Subtype.coe_mk] } + { toFun := fun k => ⟨algebraMap K L (algebraMap _ K k), IsIntegral.algebraMap k.2⟩ + map_zero' := by ext; simp only [RingOfIntegers.map_mk, map_zero] + map_one' := by ext; simp only [RingOfIntegers.map_mk, map_one] + map_add' := fun x y => by ext; simp only [RingOfIntegers.map_mk, map_add] + map_mul' := fun x y => by ext; simp only [RingOfIntegers.map_mk, map_mul] } #align number_field.ring_of_integers_algebra NumberField.inst_ringOfIntegersAlgebra -- diamond at `reducible_and_instances` #10906 @@ -102,6 +155,39 @@ namespace RingOfIntegers variable {K} +/-- The canonical map from `𝓞 K` to `K` is injective. + +This is a convenient abbreviation for `NoZeroSMulDivisors.algebraMap_injective`. +-/ +lemma coe_injective : Function.Injective (algebraMap (𝓞 K) K) := + NoZeroSMulDivisors.algebraMap_injective _ _ + +/-- The canonical map from `𝓞 K` to `K` is injective. + +This is a convenient abbreviation for `map_eq_zero_iff` applied to +`NoZeroSMulDivisors.algebraMap_injective`. +-/ +@[simp] lemma coe_eq_zero_iff {x : 𝓞 K} : algebraMap _ K x = 0 ↔ x = 0 := + map_eq_zero_iff _ coe_injective + +/-- The canonical map from `𝓞 K` to `K` is injective. + +This is a convenient abbreviation for `map_ne_zero_iff` applied to +`NoZeroSMulDivisors.algebraMap_injective`. +-/ +lemma coe_ne_zero_iff {x : 𝓞 K} : algebraMap _ K x ≠ 0 ↔ x ≠ 0 := + map_ne_zero_iff _ coe_injective + +theorem isIntegral_coe (x : 𝓞 K) : IsIntegral ℤ (algebraMap _ K x) := + x.2 +#align number_field.ring_of_integers.is_integral_coe NumberField.RingOfIntegers.isIntegral_coe + +theorem isIntegral (x : 𝓞 K) : IsIntegral ℤ x := by + obtain ⟨P, hPm, hP⟩ := x.isIntegral_coe + refine' ⟨P, hPm, _⟩ + rwa [IsScalarTower.algebraMap_eq (S := 𝓞 K), ← Polynomial.hom_eval₂, coe_eq_zero_iff] at hP +#align number_field.is_integral_of_mem_ring_of_integers NumberField.RingOfIntegers.isIntegral + instance [NumberField K] : IsFractionRing (𝓞 K) K := integralClosure.isFractionRing_of_finite_extension ℚ _ @@ -111,15 +197,7 @@ instance : IsIntegralClosure (𝓞 K) ℤ K := instance [NumberField K] : IsIntegrallyClosed (𝓞 K) := integralClosure.isIntegrallyClosedOfFiniteExtension ℚ -theorem isIntegral_coe (x : 𝓞 K) : IsIntegral ℤ (x : K) := - x.2 -#align number_field.ring_of_integers.is_integral_coe NumberField.RingOfIntegers.isIntegral_coe - -theorem map_mem {F L : Type*} [Field L] [CharZero K] [CharZero L] - [FunLike F K L] [AlgHomClass F ℚ K L] (f : F) - (x : 𝓞 K) : f x ∈ 𝓞 L := - (mem_ringOfIntegers _ _).2 <| map_isIntegral_int f <| RingOfIntegers.isIntegral_coe x -#align number_field.ring_of_integers.map_mem NumberField.RingOfIntegers.map_mem +#noalign number_field.ring_of_integers.map_mem /-- The ring of integers of `K` are equivalent to any integral closure of `ℤ` in `K` -/ protected noncomputable def equiv (R : Type*) [CommRing R] [Algebra R K] @@ -129,7 +207,7 @@ protected noncomputable def equiv (R : Type*) [CommRing R] [Algebra R K] variable (K) -instance : CharZero (𝓞 K) := +instance [CharZero K] : CharZero (𝓞 K) := CharZero.of_module _ K instance : IsNoetherian ℤ (𝓞 K) := @@ -157,6 +235,29 @@ noncomputable def basis : Basis (Free.ChooseBasisIndex ℤ (𝓞 K)) ℤ (𝓞 K Free.chooseBasis ℤ (𝓞 K) #align number_field.ring_of_integers.basis NumberField.RingOfIntegers.basis +variable {K} {M : Type*} + +/-- Given `f : M → K` such that `∀ x, IsIntegral ℤ (f x)`, the corresponding function +`M → 𝓞 K`. -/ +def restrict (f : M → K) (h : ∀ x, IsIntegral ℤ (f x)) (x : M) : 𝓞 K := + ⟨f x, h x⟩ + +/-- Given `f : M →+ K` such that `∀ x, IsIntegral ℤ (f x)`, the corresponding function +`M →+ 𝓞 K`. -/ +def restrict_addMonoidHom [AddZeroClass M] (f : M →+ K) (h : ∀ x, IsIntegral ℤ (f x)) : + M →+ 𝓞 K where + toFun := restrict f h + map_zero' := by simp only [restrict, map_zero, mk_zero] + map_add' x y := by simp only [restrict, map_add, mk_add_mk _] + +/-- Given `f : M →* K` such that `∀ x, IsIntegral ℤ (f x)`, the corresponding function +`M →* 𝓞 K`. -/ +@[to_additive existing] -- TODO: why doesn't it figure this out by itself? +def restrict_monoidHom [MulOneClass M] (f : M →* K) (h : ∀ x, IsIntegral ℤ (f x)) : M →* 𝓞 K where + toFun := restrict f h + map_one' := by simp only [restrict, map_one, mk_one] + map_mul' x y := by simp only [restrict, map_mul, mk_mul_mk _] + end RingOfIntegers /-- A basis of `K` over `ℚ` that is also a basis of `𝓞 K` over `ℤ`. -/ @@ -171,14 +272,15 @@ theorem integralBasis_apply (i : Free.ChooseBasisIndex ℤ (𝓞 K)) : #align number_field.integral_basis_apply NumberField.integralBasis_apply @[simp] -theorem integralBasis_repr_apply (x : (𝓞 K)) (i : Free.ChooseBasisIndex ℤ (𝓞 K)): - (integralBasis K).repr x i = (algebraMap ℤ ℚ) ((RingOfIntegers.basis K).repr x i) := +theorem integralBasis_repr_apply (x : (𝓞 K)) (i : Free.ChooseBasisIndex ℤ (𝓞 K)) : + (integralBasis K).repr (algebraMap _ _ x) i = + (algebraMap ℤ ℚ) ((RingOfIntegers.basis K).repr x i) := Basis.localizationLocalization_repr_algebraMap ℚ (nonZeroDivisors ℤ) K _ x i theorem mem_span_integralBasis {x : K} : - x ∈ Submodule.span ℤ (Set.range (integralBasis K)) ↔ x ∈ 𝓞 K := by - rw [integralBasis, Basis.localizationLocalization_span, Subalgebra.range_isScalarTower_toAlgHom, - Subalgebra.mem_toSubmodule] + x ∈ Submodule.span ℤ (Set.range (integralBasis K)) ↔ x ∈ (algebraMap (𝓞 K) K).range := by + rw [integralBasis, Basis.localizationLocalization_span, LinearMap.mem_range, + IsScalarTower.coe_toAlgHom', RingHom.mem_range] theorem RingOfIntegers.rank : FiniteDimensional.finrank ℤ (𝓞 K) = FiniteDimensional.finrank ℚ K := IsIntegralClosure.rank ℤ ℚ K (𝓞 K) @@ -201,7 +303,7 @@ instance numberField : NumberField ℚ where #align rat.number_field Rat.numberField /-- The ring of integers of `ℚ` as a number field is just `ℤ`. -/ -noncomputable def ringOfIntegersEquiv : ringOfIntegers ℚ ≃+* ℤ := +noncomputable def ringOfIntegersEquiv : 𝓞 ℚ ≃+* ℤ := RingOfIntegers.equiv ℤ #align rat.ring_of_integers_equiv Rat.ringOfIntegersEquiv diff --git a/Mathlib/NumberTheory/NumberField/CanonicalEmbedding/Basic.lean b/Mathlib/NumberTheory/NumberField/CanonicalEmbedding/Basic.lean index 9ad583ee17006..491ace24ae7e7 100644 --- a/Mathlib/NumberTheory/NumberField/CanonicalEmbedding/Basic.lean +++ b/Mathlib/NumberTheory/NumberField/CanonicalEmbedding/Basic.lean @@ -100,7 +100,7 @@ theorem integerLattice.inter_ball_finite [NumberField K] (r : ℝ) : convert (Embeddings.finite_of_norm_le K ℂ r).image (canonicalEmbedding K) ext; constructor · rintro ⟨⟨_, ⟨x, rfl⟩, rfl⟩, hx⟩ - exact ⟨↑x, ⟨SetLike.coe_mem x, fun φ => (heq x).mp hx φ⟩, rfl⟩ + exact ⟨x, ⟨SetLike.coe_mem x, fun φ => (heq _).mp hx φ⟩, rfl⟩ · rintro ⟨x, ⟨hx1, hx2⟩, rfl⟩ exact ⟨⟨x, ⟨⟨x, hx1⟩, rfl⟩, rfl⟩, (heq x).mpr hx2⟩ @@ -142,13 +142,14 @@ theorem latticeBasis_apply [NumberField K] (i : Free.ChooseBasisIndex ℤ (𝓞 Function.comp_apply, Equiv.apply_symm_apply] theorem mem_span_latticeBasis [NumberField K] (x : (K →+* ℂ) → ℂ) : - x ∈ Submodule.span ℤ (Set.range (latticeBasis K)) ↔ x ∈ canonicalEmbedding K '' (𝓞 K) := by + x ∈ Submodule.span ℤ (Set.range (latticeBasis K)) ↔ + x ∈ ((canonicalEmbedding K).comp (algebraMap (𝓞 K) K)).range := by rw [show Set.range (latticeBasis K) = (canonicalEmbedding K).toIntAlgHom.toLinearMap '' (Set.range (integralBasis K)) by rw [← Set.range_comp]; exact congrArg Set.range (funext (fun i => latticeBasis_apply K i))] rw [← Submodule.map_span, ← SetLike.mem_coe, Submodule.map_coe] - rw [show (Submodule.span ℤ (Set.range (integralBasis K)) : Set K) = 𝓞 K by - ext; exact mem_span_integralBasis K] + rw [← RingHom.map_range, Subring.mem_map, Set.mem_image] + simp only [SetLike.mem_coe, mem_span_integralBasis K] rfl end NumberField.canonicalEmbedding @@ -484,13 +485,14 @@ theorem latticeBasis_apply (i : ChooseBasisIndex ℤ (𝓞 K)) : canonicalEmbedding.latticeBasis_apply, integralBasis_apply, commMap_canonical_eq_mixed] theorem mem_span_latticeBasis (x : (E K)) : - x ∈ Submodule.span ℤ (Set.range (latticeBasis K)) ↔ x ∈ mixedEmbedding K '' (𝓞 K) := by + x ∈ Submodule.span ℤ (Set.range (latticeBasis K)) ↔ + x ∈ ((mixedEmbedding K).comp (algebraMap (𝓞 K) K)).range := by rw [show Set.range (latticeBasis K) = (mixedEmbedding K).toIntAlgHom.toLinearMap '' (Set.range (integralBasis K)) by rw [← Set.range_comp]; exact congrArg Set.range (funext (fun i => latticeBasis_apply K i))] rw [← Submodule.map_span, ← SetLike.mem_coe, Submodule.map_coe] - rw [show (Submodule.span ℤ (Set.range (integralBasis K)) : Set K) = 𝓞 K by - ext; exact mem_span_integralBasis K] + simp only [Set.mem_image, SetLike.mem_coe, mem_span_integralBasis K, + RingHom.mem_range, exists_exists_eq_and] rfl theorem mem_rat_span_latticeBasis (x : K) : diff --git a/Mathlib/NumberTheory/NumberField/CanonicalEmbedding/ConvexBody.lean b/Mathlib/NumberTheory/NumberField/CanonicalEmbedding/ConvexBody.lean index 547d55908859b..aef111fe64c07 100644 --- a/Mathlib/NumberTheory/NumberField/CanonicalEmbedding/ConvexBody.lean +++ b/Mathlib/NumberTheory/NumberField/CanonicalEmbedding/ConvexBody.lean @@ -538,38 +538,40 @@ theorem exists_ne_zero_mem_ideal_lt' (w₀ : {w : InfinitePlace K // IsComplex w /-- A version of `exists_ne_zero_mem_ideal_lt` for the ring of integers of `K`. -/ theorem exists_ne_zero_mem_ringOfIntegers_lt (h : minkowskiBound K ↑1 < volume (convexBodyLT K f)) : - ∃ a ∈ 𝓞 K, a ≠ 0 ∧ ∀ w : InfinitePlace K, w a < f w := by + ∃ a : 𝓞 K, a ≠ 0 ∧ ∀ w : InfinitePlace K, w a < f w := by obtain ⟨_, h_mem, h_nz, h_bd⟩ := exists_ne_zero_mem_ideal_lt K ↑1 h - obtain ⟨⟨a, ha⟩, rfl⟩ := (FractionalIdeal.mem_one_iff _).mp h_mem - exact ⟨a, ha, h_nz, h_bd⟩ + obtain ⟨a, rfl⟩ := (FractionalIdeal.mem_one_iff _).mp h_mem + exact ⟨a, RingOfIntegers.coe_ne_zero_iff.mp h_nz, h_bd⟩ /-- A version of `exists_ne_zero_mem_ideal_lt'` for the ring of integers of `K`. -/ theorem exists_ne_zero_mem_ringOfIntegers_lt' (w₀ : {w : InfinitePlace K // IsComplex w}) (h : minkowskiBound K ↑1 < volume (convexBodyLT' K f w₀)) : - ∃ a ∈ 𝓞 K, a ≠ 0 ∧ (∀ w : InfinitePlace K, w ≠ w₀ → w a < f w) ∧ + ∃ a : 𝓞 K, a ≠ 0 ∧ (∀ w : InfinitePlace K, w ≠ w₀ → w a < f w) ∧ |(w₀.val.embedding a).re| < 1 ∧ |(w₀.val.embedding a).im| < (f w₀ : ℝ) ^ 2 := by obtain ⟨_, h_mem, h_nz, h_bd⟩ := exists_ne_zero_mem_ideal_lt' K ↑1 w₀ h - obtain ⟨⟨a, ha⟩, rfl⟩ := (FractionalIdeal.mem_one_iff _).mp h_mem - exact ⟨a, ha, h_nz, h_bd⟩ + obtain ⟨a, rfl⟩ := (FractionalIdeal.mem_one_iff _).mp h_mem + exact ⟨a, RingOfIntegers.coe_ne_zero_iff.mp h_nz, h_bd⟩ theorem exists_primitive_element_lt_of_isReal {w₀ : InfinitePlace K} (hw₀ : IsReal w₀) {B : ℝ≥0} (hB : minkowskiBound K ↑1 < convexBodyLTFactor K * B) : - ∃ a ∈ 𝓞 K, ℚ⟮(a:K)⟯ = ⊤ ∧ (∀ w : InfinitePlace K, w a < max B 1) := by + ∃ a : 𝓞 K, ℚ⟮(a : K)⟯ = ⊤ ∧ + ∀ w : InfinitePlace K, w a < max B 1 := by have : minkowskiBound K ↑1 < volume (convexBodyLT K (fun w ↦ if w = w₀ then B else 1)) := by rw [convexBodyLT_volume, ← Finset.prod_erase_mul _ _ (Finset.mem_univ w₀)] simp_rw [ite_pow, one_pow] rw [Finset.prod_ite_eq'] simp_rw [Finset.not_mem_erase, ite_false, mult, hw₀, ite_true, one_mul, pow_one] exact hB - obtain ⟨a, ha, h_nz, h_le⟩ := exists_ne_zero_mem_ringOfIntegers_lt K this - refine ⟨a, ha, ?_, fun w ↦ lt_of_lt_of_le (h_le w) ?_⟩ - · exact is_primitive_element_of_infinitePlace_lt (x := ⟨a, ha⟩) (Subtype.coe_ne_coe.1 h_nz) + obtain ⟨a, h_nz, h_le⟩ := exists_ne_zero_mem_ringOfIntegers_lt K this + refine ⟨a, ?_, fun w ↦ lt_of_lt_of_le (h_le w) ?_⟩ + · exact is_primitive_element_of_infinitePlace_lt h_nz (fun w h_ne ↦ by convert (if_neg h_ne) ▸ h_le w) (Or.inl hw₀) · split_ifs <;> simp theorem exists_primitive_element_lt_of_isComplex {w₀ : InfinitePlace K} (hw₀ : IsComplex w₀) {B : ℝ≥0} (hB : minkowskiBound K ↑1 < convexBodyLT'Factor K * B) : - ∃ a ∈ 𝓞 K, ℚ⟮(a:K)⟯ = ⊤ ∧ (∀ w : InfinitePlace K, w a < Real.sqrt (1 + B ^ 2)) := by + ∃ a : 𝓞 K, ℚ⟮(a : K)⟯ = ⊤ ∧ + ∀ w : InfinitePlace K, w a < Real.sqrt (1 + B ^ 2) := by have : minkowskiBound K ↑1 < volume (convexBodyLT' K (fun w ↦ if w = w₀ then NNReal.sqrt B else 1) ⟨w₀, hw₀⟩) := by rw [convexBodyLT'_volume, ← Finset.prod_erase_mul _ _ (Finset.mem_univ w₀)] @@ -578,15 +580,15 @@ theorem exists_primitive_element_lt_of_isComplex {w₀ : InfinitePlace K} (hw₀ simp_rw [Finset.not_mem_erase, ite_false, mult, not_isReal_iff_isComplex.mpr hw₀, ite_true, ite_false, one_mul, NNReal.sq_sqrt] exact hB - obtain ⟨a, ha, h_nz, h_le, h_le₀⟩ := exists_ne_zero_mem_ringOfIntegers_lt' K ⟨w₀, hw₀⟩ this - refine ⟨a, ha, ?_, fun w ↦ ?_⟩ - · exact is_primitive_element_of_infinitePlace_lt (x := ⟨a, ha⟩) (Subtype.coe_ne_coe.1 h_nz) + obtain ⟨a, h_nz, h_le, h_le₀⟩ := exists_ne_zero_mem_ringOfIntegers_lt' K ⟨w₀, hw₀⟩ this + refine ⟨a, ?_, fun w ↦ ?_⟩ + · exact is_primitive_element_of_infinitePlace_lt h_nz (fun w h_ne ↦ by convert if_neg h_ne ▸ h_le w h_ne) (Or.inr h_le₀.1) · by_cases h_eq : w = w₀ · rw [if_pos rfl] at h_le₀ dsimp only at h_le₀ rw [h_eq, ← norm_embedding_eq, Real.lt_sqrt (norm_nonneg _), ← Complex.re_add_im - (embedding w₀ a), Complex.norm_eq_abs, Complex.abs_add_mul_I, Real.sq_sqrt (by positivity)] + (embedding w₀ _), Complex.norm_eq_abs, Complex.abs_add_mul_I, Real.sq_sqrt (by positivity)] refine add_lt_add ?_ ?_ · rw [← sq_abs, sq_lt_one_iff (abs_nonneg _)] exact h_le₀.1 @@ -604,7 +606,7 @@ that `|Norm a| < (B / d) ^ d` where `d` is the degree of `K`. -/ theorem exists_ne_zero_mem_ideal_of_norm_le {B : ℝ} (h : (minkowskiBound K I) ≤ volume (convexBodySum K B)) : ∃ a ∈ (I : FractionalIdeal (𝓞 K)⁰ K), a ≠ 0 ∧ - |Algebra.norm ℚ (a:K)| ≤ (B / (finrank ℚ K)) ^ (finrank ℚ K) := by + |Algebra.norm ℚ (a:K)| ≤ (B / finrank ℚ K) ^ finrank ℚ K := by have hB : 0 ≤ B := by contrapose! h rw [convexBodySum_volume_eq_zero_of_le_zero K (le_of_lt h)] @@ -636,10 +638,10 @@ theorem exists_ne_zero_mem_ideal_of_norm_le {B : ℝ} theorem exists_ne_zero_mem_ringOfIntegers_of_norm_le {B : ℝ} (h : (minkowskiBound K ↑1) ≤ volume (convexBodySum K B)) : - ∃ a ∈ 𝓞 K, a ≠ 0 ∧ |Algebra.norm ℚ (a:K)| ≤ (B / (finrank ℚ K)) ^ (finrank ℚ K) := by + ∃ a : 𝓞 K, a ≠ 0 ∧ |Algebra.norm ℚ (a : K)| ≤ (B / finrank ℚ K) ^ finrank ℚ K := by obtain ⟨_, h_mem, h_nz, h_bd⟩ := exists_ne_zero_mem_ideal_of_norm_le K ↑1 h - obtain ⟨⟨a, ha⟩, rfl⟩ := (FractionalIdeal.mem_one_iff _).mp h_mem - exact ⟨a, ha, h_nz, h_bd⟩ + obtain ⟨a, rfl⟩ := (FractionalIdeal.mem_one_iff _).mp h_mem + exact ⟨a, RingOfIntegers.coe_ne_zero_iff.mp h_nz, h_bd⟩ end minkowski diff --git a/Mathlib/NumberTheory/NumberField/ClassNumber.lean b/Mathlib/NumberTheory/NumberField/ClassNumber.lean index 7b9b38870ddff..fe7b8042d352c 100644 --- a/Mathlib/NumberTheory/NumberField/ClassNumber.lean +++ b/Mathlib/NumberTheory/NumberField/ClassNumber.lean @@ -28,20 +28,20 @@ variable (K : Type*) [Field K] [NumberField K] namespace RingOfIntegers -noncomputable instance instFintypeClassGroup : Fintype (ClassGroup (ringOfIntegers K)) := +noncomputable instance instFintypeClassGroup : Fintype (ClassGroup (𝓞 K)) := ClassGroup.fintypeOfAdmissibleOfFinite ℚ K AbsoluteValue.absIsAdmissible end RingOfIntegers /-- The class number of a number field is the (finite) cardinality of the class group. -/ noncomputable def classNumber : ℕ := - Fintype.card (ClassGroup (ringOfIntegers K)) + Fintype.card (ClassGroup (𝓞 K)) #align number_field.class_number NumberField.classNumber variable {K} /-- The class number of a number field is `1` iff the ring of integers is a PID. -/ -theorem classNumber_eq_one_iff : classNumber K = 1 ↔ IsPrincipalIdealRing (ringOfIntegers K) := +theorem classNumber_eq_one_iff : classNumber K = 1 ↔ IsPrincipalIdealRing (𝓞 K) := card_classGroup_eq_one_iff #align number_field.class_number_eq_one_iff NumberField.classNumber_eq_one_iff @@ -49,7 +49,7 @@ open FiniteDimensional NumberField.InfinitePlace open scoped nonZeroDivisors Real -theorem exists_ideal_in_class_of_norm_le (C : ClassGroup (𝓞 K)): +theorem exists_ideal_in_class_of_norm_le (C : ClassGroup (𝓞 K)) : ∃ I : (Ideal (𝓞 K))⁰, ClassGroup.mk0 I = C ∧ Ideal.absNorm (I : Ideal (𝓞 K)) ≤ (4 / π) ^ NrComplexPlaces K * ((finrank ℚ K).factorial / (finrank ℚ K) ^ (finrank ℚ K) * Real.sqrt |discr K|) := by @@ -77,7 +77,7 @@ theorem exists_ideal_in_class_of_norm_le (C : ClassGroup (𝓞 K)): theorem _root_.RingOfIntegers.isPrincipalIdealRing_of_abs_discr_lt (h : |discr K| < (2 * (π / 4) ^ NrComplexPlaces K * ((finrank ℚ K) ^ (finrank ℚ K) / (finrank ℚ K).factorial)) ^ 2) : - IsPrincipalIdealRing (ringOfIntegers K) := by + IsPrincipalIdealRing (𝓞 K) := by have : 0 < finrank ℚ K := finrank_pos -- Lean needs to know that for positivity to succeed rw [← Real.sqrt_lt (by positivity) (by positivity), mul_assoc, ← inv_mul_lt_iff' (by positivity), mul_inv, ← inv_pow, inv_div, inv_div, mul_assoc, Int.cast_abs] at h @@ -100,7 +100,7 @@ open NumberField theorem classNumber_eq : NumberField.classNumber ℚ = 1 := classNumber_eq_one_iff.mpr <| by convert IsPrincipalIdealRing.of_surjective - (Rat.ringOfIntegersEquiv.symm: ℤ →+* ringOfIntegers ℚ) Rat.ringOfIntegersEquiv.symm.surjective + (Rat.ringOfIntegersEquiv.symm: ℤ →+* 𝓞 ℚ) Rat.ringOfIntegersEquiv.symm.surjective #align rat.class_number_eq Rat.classNumber_eq end Rat diff --git a/Mathlib/NumberTheory/NumberField/Discriminant.lean b/Mathlib/NumberTheory/NumberField/Discriminant.lean index 5bf9b0b06a4da..b8f819d8abcf4 100644 --- a/Mathlib/NumberTheory/NumberField/Discriminant.lean +++ b/Mathlib/NumberTheory/NumberField/Discriminant.lean @@ -151,7 +151,7 @@ theorem exists_ne_zero_mem_ideal_of_norm_le_mul_sqrt_discr (I : (FractionalIdeal theorem exists_ne_zero_mem_ringOfIntegers_of_norm_le_mul_sqrt_discr : ∃ (a : 𝓞 K), a ≠ 0 ∧ - |Algebra.norm ℚ (a:K)| ≤ (4 / π) ^ NrComplexPlaces K * + |Algebra.norm ℚ (a : K)| ≤ (4 / π) ^ NrComplexPlaces K * (finrank ℚ K).factorial / (finrank ℚ K) ^ (finrank ℚ K) * Real.sqrt |discr K| := by obtain ⟨_, h_mem, h_nz, h_nm⟩ := exists_ne_zero_mem_ideal_of_norm_le_mul_sqrt_discr K ↑1 obtain ⟨a, rfl⟩ := (FractionalIdeal.mem_one_iff _).mp h_mem @@ -167,7 +167,7 @@ theorem abs_discr_ge (h : 1 < finrank ℚ K) : -- algebraic integer `x` of small norm and the fact that `1 ≤ |Norm x|` to get a lower bound -- on `sqrt |discr K|`. obtain ⟨x, h_nz, h_bd⟩ := exists_ne_zero_mem_ringOfIntegers_of_norm_le_mul_sqrt_discr K - have h_nm : (1 : ℝ) ≤ |(Algebra.norm ℚ) (x : K)| := by + have h_nm : (1 : ℝ) ≤ |Algebra.norm ℚ (x : K)| := by rw [← Algebra.coe_norm_int, ← Int.cast_one, ← Int.cast_abs, Rat.cast_intCast, Int.cast_le] exact Int.one_le_abs (Algebra.norm_ne_zero_iff.mpr h_nz) replace h_bd := le_trans h_nm h_bd @@ -316,10 +316,11 @@ theorem minkowskiBound_lt_boundOfDiscBdd : minkowskiBound K ↑1 < boundOfDiscBd · exact one_le_two · exact rank_le_rankOfDiscrBdd hK -theorem natDegree_le_rankOfDiscrBdd {a : K} (ha : a ∈ 𝓞 K) (h : ℚ⟮a⟯ = ⊤) : - natDegree (minpoly ℤ (a:K)) ≤ rankOfDiscrBdd N := by +theorem natDegree_le_rankOfDiscrBdd (a : 𝓞 K) (h : ℚ⟮(a : K)⟯ = ⊤) : + natDegree (minpoly ℤ (a : K)) ≤ rankOfDiscrBdd N := by rw [Field.primitive_element_iff_minpoly_natDegree_eq, - minpoly.isIntegrallyClosed_eq_field_fractions' ℚ ha, (minpoly.monic ha).natDegree_map] at h + minpoly.isIntegrallyClosed_eq_field_fractions' ℚ a.isIntegral_coe, + (minpoly.monic a.isIntegral_coe).natDegree_map] at h exact h.symm ▸ rank_le_rankOfDiscrBdd hK variable (N) @@ -341,12 +342,13 @@ theorem finite_of_discr_bdd_of_isReal : haveI : NumberField K := @NumberField.mk _ _ inferInstance hK₀ obtain ⟨w₀, hw₀⟩ := hK₁ suffices minkowskiBound K ↑1 < (convexBodyLTFactor K) * B by - obtain ⟨x, hx, hx₁, hx₂⟩ := exists_primitive_element_lt_of_isReal K hw₀ this - refine ⟨x, ⟨⟨minpoly ℤ x, ⟨?_, fun i ↦ ?_⟩, ?_⟩, ?_⟩⟩ - · exact natDegree_le_rankOfDiscrBdd hK₂ hx hx₁ + obtain ⟨x, hx₁, hx₂⟩ := exists_primitive_element_lt_of_isReal K hw₀ this + have hx := x.isIntegral_coe + refine ⟨x, ⟨⟨minpoly ℤ (x : K), ⟨?_, fun i ↦ ?_⟩, ?_⟩, ?_⟩⟩ + · exact natDegree_le_rankOfDiscrBdd hK₂ x hx₁ · rw [Set.mem_Icc, ← abs_le, ← @Int.cast_le ℝ] refine (Eq.trans_le ?_ <| Embeddings.coeff_bdd_of_norm_le - ((le_iff_le x _).mp (fun w ↦ le_of_lt (hx₂ w))) i).trans ?_ + ((le_iff_le (x : K) _).mp (fun w ↦ le_of_lt (hx₂ w))) i).trans ?_ · rw [minpoly.isIntegrallyClosed_eq_field_fractions' ℚ hx, coeff_map, eq_intCast, Int.norm_cast_rat, Int.norm_eq_abs, Int.cast_abs] · refine le_trans ?_ (Nat.le_ceil _) @@ -358,7 +360,7 @@ theorem finite_of_discr_bdd_of_isReal : · exact (Nat.choose_le_choose _ (rank_le_rankOfDiscrBdd hK₂)).trans (Nat.choose_le_middle _ _) · refine mem_rootSet.mpr ⟨minpoly.ne_zero hx, ?_⟩ - exact (aeval_algebraMap_eq_zero_iff _ _ _).mpr (minpoly.aeval ℤ x) + exact (aeval_algebraMap_eq_zero_iff _ _ _).mpr (minpoly.aeval ℤ (x : K)) · rw [← (IntermediateField.lift_injective _).eq_iff, eq_comm] at hx₁ convert hx₁ <;> simp have := one_le_convexBodyLTFactor K @@ -383,12 +385,13 @@ theorem finite_of_discr_bdd_of_isComplex : haveI : NumberField K := @NumberField.mk _ _ inferInstance hK₀ obtain ⟨w₀, hw₀⟩ := hK₁ suffices minkowskiBound K ↑1 < (convexBodyLT'Factor K) * boundOfDiscBdd N by - obtain ⟨x, hx, hx₁, hx₂⟩ := exists_primitive_element_lt_of_isComplex K hw₀ this - refine ⟨x, ⟨⟨minpoly ℤ x, ⟨?_, fun i ↦ ?_⟩, ?_⟩, ?_⟩⟩ - · exact natDegree_le_rankOfDiscrBdd hK₂ hx hx₁ + obtain ⟨x, hx₁, hx₂⟩ := exists_primitive_element_lt_of_isComplex K hw₀ this + have hx := x.isIntegral_coe + refine ⟨x, ⟨⟨minpoly ℤ (x : K), ⟨?_, fun i ↦ ?_⟩, ?_⟩, ?_⟩⟩ + · exact natDegree_le_rankOfDiscrBdd hK₂ x hx₁ · rw [Set.mem_Icc, ← abs_le, ← @Int.cast_le ℝ] refine (Eq.trans_le ?_ <| Embeddings.coeff_bdd_of_norm_le - ((le_iff_le x _).mp (fun w ↦ le_of_lt (hx₂ w))) i).trans ?_ + ((le_iff_le (x : K) _).mp (fun w ↦ le_of_lt (hx₂ w))) i).trans ?_ · rw [minpoly.isIntegrallyClosed_eq_field_fractions' ℚ hx, coeff_map, eq_intCast, Int.norm_cast_rat, Int.norm_eq_abs, Int.cast_abs] · refine le_trans ?_ (Nat.le_ceil _) @@ -401,7 +404,7 @@ theorem finite_of_discr_bdd_of_isComplex : exact (Nat.choose_le_choose _ (rank_le_rankOfDiscrBdd hK₂)).trans (Nat.choose_le_middle _ _) · refine mem_rootSet.mpr ⟨minpoly.ne_zero hx, ?_⟩ - exact (aeval_algebraMap_eq_zero_iff _ _ _).mpr (minpoly.aeval ℤ x) + exact (aeval_algebraMap_eq_zero_iff _ _ _).mpr (minpoly.aeval ℤ (x : K)) · rw [← (IntermediateField.lift_injective _).eq_iff, eq_comm] at hx₁ convert hx₁ <;> simp have := one_le_convexBodyLT'Factor K diff --git a/Mathlib/NumberTheory/NumberField/Embeddings.lean b/Mathlib/NumberTheory/NumberField/Embeddings.lean index 5a8a193c4bf9d..1675c27caf844 100644 --- a/Mathlib/NumberTheory/NumberField/Embeddings.lean +++ b/Mathlib/NumberTheory/NumberField/Embeddings.lean @@ -532,7 +532,7 @@ theorem prod_eq_abs_norm (x : K) : theorem one_le_of_lt_one {w : InfinitePlace K} {a : (𝓞 K)} (ha : a ≠ 0) (h : ∀ ⦃z⦄, z ≠ w → z a < 1) : 1 ≤ w a := by - suffices (1:ℝ) ≤ |(Algebra.norm ℚ) (a:K)| by + suffices (1:ℝ) ≤ |Algebra.norm ℚ (a : K)| by contrapose! this rw [← InfinitePlace.prod_eq_abs_norm, ← Finset.prod_const_one] refine Finset.prod_lt_prod_of_nonempty (fun _ _ ↦ ?_) (fun z _ ↦ ?_) Finset.univ_nonempty @@ -547,7 +547,7 @@ theorem one_le_of_lt_one {w : InfinitePlace K} {a : (𝓞 K)} (ha : a ≠ 0) open scoped IntermediateField in theorem _root_.NumberField.is_primitive_element_of_infinitePlace_lt {x : 𝓞 K} {w : InfinitePlace K} (h₁ : x ≠ 0) (h₂ : ∀ ⦃w'⦄, w' ≠ w → w' x < 1) - (h₃ : IsReal w ∨ |(w.embedding x).re| < 1) : ℚ⟮(x:K)⟯ = ⊤ := by + (h₃ : IsReal w ∨ |(w.embedding x).re| < 1) : ℚ⟮(x : K)⟯ = ⊤ := by rw [Field.primitive_element_iff_algHom_eq_of_eval ℚ ℂ ?_ _ w.embedding.toRatAlgHom] · intro ψ hψ have h : 1 ≤ w x := one_le_of_lt_one h₁ h₂ @@ -571,7 +571,7 @@ theorem _root_.NumberField.is_primitive_element_of_infinitePlace_lt {x : 𝓞 K} theorem _root_.NumberField.adjoin_eq_top_of_infinitePlace_lt {x : 𝓞 K} {w : InfinitePlace K} (h₁ : x ≠ 0) (h₂ : ∀ ⦃w'⦄, w' ≠ w → w' x < 1) (h₃ : IsReal w ∨ |(w.embedding x).re| < 1) : - Algebra.adjoin ℚ {(x:K)} = ⊤ := by + Algebra.adjoin ℚ {(x : K)} = ⊤ := by rw [← IntermediateField.adjoin_simple_toSubalgebra_of_integral (IsIntegral.of_finite ℚ _)] exact congr_arg IntermediateField.toSubalgebra <| NumberField.is_primitive_element_of_infinitePlace_lt h₁ h₂ h₃ diff --git a/Mathlib/NumberTheory/NumberField/FractionalIdeal.lean b/Mathlib/NumberTheory/NumberField/FractionalIdeal.lean index e988f0a703341..08315c93dbb46 100644 --- a/Mathlib/NumberTheory/NumberField/FractionalIdeal.lean +++ b/Mathlib/NumberTheory/NumberField/FractionalIdeal.lean @@ -52,16 +52,17 @@ instance (I : (FractionalIdeal (𝓞 K)⁰ K)ˣ) : exact nonZeroDivisors.coe_ne_zero x surj' x := by obtain ⟨⟨a, _, d, hd, rfl⟩, h⟩ := IsLocalization.surj (Algebra.algebraMapSubmonoid (𝓞 K) ℤ⁰) x - refine ⟨⟨⟨Ideal.absNorm I.1.num * a, I.1.num_le ?_⟩, d * Ideal.absNorm I.1.num, ?_⟩ , ?_⟩ + refine ⟨⟨⟨Ideal.absNorm I.1.num * (algebraMap _ K a), I.1.num_le ?_⟩, d * Ideal.absNorm I.1.num, + ?_⟩ , ?_⟩ · simp_rw [FractionalIdeal.val_eq_coe, FractionalIdeal.coe_coeIdeal] refine (IsLocalization.mem_coeSubmodule _ _).mpr ⟨Ideal.absNorm I.1.num * a, ?_, ?_⟩ · exact Ideal.mul_mem_right _ _ I.1.num.absNorm_mem - · rw [map_mul, map_natCast]; rfl + · rw [map_mul, map_natCast] · refine Submonoid.mul_mem _ hd (mem_nonZeroDivisors_of_ne_zero ?_) rw [Nat.cast_ne_zero, ne_eq, Ideal.absNorm_eq_zero_iff] exact FractionalIdeal.num_eq_zero_iff.not.mpr <| Units.ne_zero I · simp_rw [LinearMap.coe_restrictScalars, Submodule.coeSubtype] at h ⊢ - rw [show (a : K) = algebraMap (𝓞 K) K a by rfl, ← h] + rw [← h] simp only [Submonoid.mk_smul, zsmul_eq_mul, Int.cast_mul, Int.cast_natCast, algebraMap_int_eq, eq_intCast, map_intCast] ring diff --git a/Mathlib/NumberTheory/NumberField/Norm.lean b/Mathlib/NumberTheory/NumberField/Norm.lean index f3bc7abfa5e3c..38bf099343fce 100644 --- a/Mathlib/NumberTheory/NumberField/Norm.lean +++ b/Mathlib/NumberTheory/NumberField/Norm.lean @@ -33,7 +33,7 @@ variable {K : Type*} [Field K] [NumberField K] (x : 𝓞 K) theorem Algebra.coe_norm_int : (Algebra.norm ℤ x : ℚ) = Algebra.norm ℚ (x : K) := (Algebra.norm_localization (R := ℤ) (Rₘ := ℚ) (S := 𝓞 K) (Sₘ := K) (nonZeroDivisors ℤ) x).symm -theorem Algebra.coe_trace_int : (Algebra.trace ℤ _ x : ℚ) = Algebra.trace ℚ K x := +theorem Algebra.coe_trace_int : (Algebra.trace ℤ _ x : ℚ) = Algebra.trace ℚ K (x : K) := (Algebra.trace_localization (R := ℤ) (Rₘ := ℚ) (S := 𝓞 K) (Sₘ := K) (nonZeroDivisors ℤ) x).symm end Rat @@ -43,25 +43,30 @@ namespace RingOfIntegers variable {L : Type*} (K : Type*) [Field K] [Field L] [Algebra K L] [FiniteDimensional K L] /-- `Algebra.norm` as a morphism betwen the rings of integers. -/ -@[simps!] noncomputable def norm [IsSeparable K L] : 𝓞 L →* 𝓞 K := - ((Algebra.norm K).restrict (𝓞 L)).codRestrict (𝓞 K) fun x => isIntegral_norm K x.2 + RingOfIntegers.restrict_monoidHom + ((Algebra.norm K).comp (algebraMap (𝓞 L) L : (𝓞 L) →* L)) + fun x => isIntegral_norm K x.2 #align ring_of_integers.norm RingOfIntegers.norm +@[simp] lemma coe_norm [IsSeparable K L] (x : 𝓞 L) : + norm K x = Algebra.norm K (x : L) := rfl + theorem coe_algebraMap_norm [IsSeparable K L] (x : 𝓞 L) : (algebraMap (𝓞 K) (𝓞 L) (norm K x) : L) = algebraMap K L (Algebra.norm K (x : L)) := rfl #align ring_of_integers.coe_algebra_map_norm RingOfIntegers.coe_algebraMap_norm -theorem coe_norm_algebraMap [IsSeparable K L] (x : 𝓞 K) : - (norm K (algebraMap (𝓞 K) (𝓞 L) x) : K) = Algebra.norm K (algebraMap K L x) := - rfl -#align ring_of_integers.coe_norm_algebra_map RingOfIntegers.coe_norm_algebraMap +theorem algebraMap_norm_algebraMap [IsSeparable K L] (x : 𝓞 K) : + algebraMap _ K (norm K (algebraMap (𝓞 K) (𝓞 L) x)) = + Algebra.norm K (algebraMap K L (algebraMap _ _ x)) := rfl +#align ring_of_integers.coe_norm_algebra_map RingOfIntegers.algebraMap_norm_algebraMap theorem norm_algebraMap [IsSeparable K L] (x : 𝓞 K) : norm K (algebraMap (𝓞 K) (𝓞 L) x) = x ^ finrank K L := by - rw [← Subtype.coe_inj, RingOfIntegers.coe_norm_algebraMap, Algebra.norm_algebraMap, - SubsemiringClass.coe_pow] + rw [RingOfIntegers.ext_iff, RingOfIntegers.coe_eq_algebraMap, + RingOfIntegers.algebraMap_norm_algebraMap, Algebra.norm_algebraMap, + RingOfIntegers.coe_eq_algebraMap, map_pow] #align ring_of_integers.norm_algebra_map RingOfIntegers.norm_algebraMap theorem isUnit_norm_of_isGalois [IsGalois K L] {x : 𝓞 L} : IsUnit (norm K x) ↔ IsUnit x := by @@ -75,8 +80,9 @@ theorem isUnit_norm_of_isGalois [IsGalois K L] {x : 𝓞 L} : IsUnit (norm K x) ext push_cast convert_to ((univ \ {AlgEquiv.refl}).prod fun σ : L ≃ₐ[K] L => σ x) * - ∏ σ : L ≃ₐ[K] L in {AlgEquiv.refl}, σ (x : L) = _ - · rw [prod_singleton, AlgEquiv.coe_refl, _root_.id] + ∏ σ : L ≃ₐ[K] L in {AlgEquiv.refl}, σ x = _ + · rw [prod_singleton, AlgEquiv.coe_refl, _root_.id, RingOfIntegers.coe_eq_algebraMap, map_mul, + RingOfIntegers.map_mk] · rw [prod_sdiff <| subset_univ _, ← norm_eq_prod_automorphisms, coe_algebraMap_norm] #align ring_of_integers.is_unit_norm_of_is_galois RingOfIntegers.isUnit_norm_of_isGalois @@ -84,10 +90,12 @@ theorem isUnit_norm_of_isGalois [IsGalois K L] {x : 𝓞 L} : IsUnit (norm K x) `x ∣ algebraMap (𝓞 K) (𝓞 L) (norm K x)`. -/ theorem dvd_norm [IsGalois K L] (x : 𝓞 L) : x ∣ algebraMap (𝓞 K) (𝓞 L) (norm K x) := by classical - have hint : ∏ σ : L ≃ₐ[K] L in univ.erase AlgEquiv.refl, σ x ∈ 𝓞 L := - Subalgebra.prod_mem _ fun σ _ => - (mem_ringOfIntegers _ _).2 ((RingOfIntegers.isIntegral_coe x).map σ) - refine' ⟨⟨_, hint⟩, Subtype.ext _⟩ + have hint : + IsIntegral ℤ (∏ σ : L ≃ₐ[K] L in univ.erase AlgEquiv.refl, σ x) := + IsIntegral.prod _ (fun σ _ => + ((RingOfIntegers.isIntegral_coe x).map σ)) + refine' ⟨⟨_, hint⟩, _⟩ + ext rw [coe_algebraMap_norm K x, norm_eq_prod_automorphisms] simp [← Finset.mul_prod_erase _ _ (mem_univ AlgEquiv.refl)] #align ring_of_integers.dvd_norm RingOfIntegers.dvd_norm @@ -96,7 +104,7 @@ variable (F : Type*) [Field F] [Algebra K F] [IsSeparable K F] [FiniteDimensiona theorem norm_norm [IsSeparable K L] [Algebra F L] [IsSeparable F L] [FiniteDimensional F L] [IsScalarTower 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] + rw [RingOfIntegers.ext_iff, coe_norm, coe_norm, coe_norm, Algebra.norm_norm] #align ring_of_integers.norm_norm RingOfIntegers.norm_norm variable {F} diff --git a/Mathlib/NumberTheory/NumberField/Units/Basic.lean b/Mathlib/NumberTheory/NumberField/Units/Basic.lean index 8b232c5e39df8..a25341e9ae1e8 100644 --- a/Mathlib/NumberTheory/NumberField/Units/Basic.lean +++ b/Mathlib/NumberTheory/NumberField/Units/Basic.lean @@ -63,15 +63,18 @@ namespace NumberField.Units section coe +instance : CoeHTC (𝓞 K)ˣ K := + ⟨fun x => algebraMap _ K (Units.val x)⟩ + theorem coe_injective : Function.Injective ((↑) : (𝓞 K)ˣ → K) := - fun _ _ h => by rwa [SetLike.coe_eq_coe, Units.eq_iff] at h + RingOfIntegers.coe_injective.comp Units.ext 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] +theorem coe_pow (x : (𝓞 K)ˣ) (n : ℕ) : ((x ^ n : (𝓞 K)ˣ) : K) = (x : K) ^ n := by + rw [← map_pow, ← val_pow_eq_pow_val] theorem coe_zpow (x : (𝓞 K)ˣ) (n : ℤ) : (↑(x ^ n) : K) = (x : K) ^ n := by change ((Units.coeHom K).comp (map (algebraMap (𝓞 K) K))) (x ^ n) = _ @@ -98,11 +101,9 @@ theorem mem_torsion {x : (𝓞 K)ˣ} [NumberField K] : rw [eq_iff_eq (x : K) 1, torsion, CommGroup.mem_torsion] refine ⟨fun hx φ ↦ (((φ.comp $ algebraMap (𝓞 K) K).toMonoidHom.comp $ Units.coeHom _).isOfFinOrder hx).norm_eq_one, fun h ↦ isOfFinOrder_iff_pow_eq_one.2 ?_⟩ - obtain ⟨n, hn, hx⟩ := Embeddings.pow_eq_one_of_norm_eq_one K ℂ x.val.prop h - 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.instNonempty + obtain ⟨n, hn, hx⟩ := Embeddings.pow_eq_one_of_norm_eq_one K ℂ x.val.isIntegral_coe h + exact ⟨n, hn, by ext; rw [NumberField.RingOfIntegers.coe_eq_algebraMap, coe_pow, hx, + NumberField.RingOfIntegers.coe_eq_algebraMap, coe_one]⟩ /-- The torsion subgroup is finite. -/ instance [NumberField K] : Fintype (torsion K) := by @@ -115,8 +116,7 @@ instance [NumberField K] : Fintype (torsion K) := by · rw [← h_ua] exact le_of_eq ((eq_iff_eq _ 1).mp ((mem_torsion K).mp h_tors) φ) --- a shortcut instance to stop the next instance from timing out -instance [NumberField K] : Finite (torsion K) := inferInstance +instance : Nonempty (torsion K) := One.instNonempty /-- The torsion subgroup is cylic. -/ instance [NumberField K] : IsCyclic (torsion K) := subgroup_units_cyclic _ diff --git a/Mathlib/NumberTheory/NumberField/Units/DirichletTheorem.lean b/Mathlib/NumberTheory/NumberField/Units/DirichletTheorem.lean index ccacb29ebfa80..04d60fba79c69 100644 --- a/Mathlib/NumberTheory/NumberField/Units/DirichletTheorem.lean +++ b/Mathlib/NumberTheory/NumberField/Units/DirichletTheorem.lean @@ -196,23 +196,25 @@ sequence defining the same ideal and their quotient is the desired unit `u_w₁` open NumberField.mixedEmbedding NNReal -/- TODO: Remove!. Necessary to prevent a timeout that ends at here. #10131 -/ -attribute [-instance] FractionalIdeal.commSemiring variable (w₁ : InfinitePlace K) {B : ℕ} (hB : minkowskiBound K 1 < (convexBodyLTFactor K) * B) /-- This result shows that there always exists a next term in the sequence. -/ theorem seq_next {x : 𝓞 K} (hx : x ≠ 0) : - ∃ y : 𝓞 K, y ≠ 0 ∧ (∀ w, w ≠ w₁ → w y < w x) ∧ |Algebra.norm ℚ (y : K)| ≤ B := by + ∃ y : 𝓞 K, y ≠ 0 ∧ + (∀ w, w ≠ w₁ → w y < w x) ∧ + |Algebra.norm ℚ (y : K)| ≤ B := by + have hx' := RingOfIntegers.coe_ne_zero_iff.mpr hx let f : InfinitePlace K → ℝ≥0 := fun w => ⟨(w x) / 2, div_nonneg (AbsoluteValue.nonneg _ _) (by norm_num)⟩ suffices ∀ w, w ≠ w₁ → f w ≠ 0 by obtain ⟨g, h_geqf, h_gprod⟩ := adjust_f K B this - obtain ⟨y, hy, h_ynz, h_yle⟩ := exists_ne_zero_mem_ringOfIntegers_lt (f := g) + obtain ⟨y, h_ynz, h_yle⟩ := exists_ne_zero_mem_ringOfIntegers_lt (f := g) (by rw [convexBodyLT_volume]; convert hB; exact congr_arg ((↑): NNReal → ENNReal) h_gprod) - refine ⟨⟨y, hy⟩, Subtype.coe_ne_coe.1 h_ynz, fun w hw => (h_geqf w hw ▸ h_yle w).trans ?_, ?_⟩ + refine ⟨y, h_ynz, fun w hw => (h_geqf w hw ▸ h_yle w).trans ?_, ?_⟩ · rw [← Rat.cast_le (K := ℝ), Rat.cast_natCast] calc - _ = ∏ w : InfinitePlace K, w y ^ mult w := (prod_eq_abs_norm (y : K)).symm + _ = ∏ w : InfinitePlace K, w (algebraMap _ K y) ^ mult w := + (prod_eq_abs_norm (algebraMap _ K y)).symm _ ≤ ∏ w : InfinitePlace K, (g w : ℝ) ^ mult w := by refine prod_le_prod ?_ ?_ · exact fun _ _ => pow_nonneg (by positivity) _ @@ -221,10 +223,10 @@ theorem seq_next {x : 𝓞 K} (hx : x ≠ 0) : simp_rw [← NNReal.coe_pow, ← NNReal.coe_prod] exact le_of_eq (congr_arg toReal h_gprod) · refine div_lt_self ?_ (by norm_num) - simp only [pos_iff, ne_eq, ZeroMemClass.coe_eq_zero, hx, not_false_eq_true] + exact pos_iff.mpr hx' intro _ _ - rw [ne_eq, Nonneg.mk_eq_zero, div_eq_zero_iff, map_eq_zero, not_or, ZeroMemClass.coe_eq_zero] - exact ⟨hx, by norm_num⟩ + rw [ne_eq, Nonneg.mk_eq_zero, div_eq_zero_iff, map_eq_zero, not_or] + exact ⟨hx', by norm_num⟩ /-- An infinite sequence of nonzero algebraic integers of `K` satisfying the following properties: • `seq n` is nonzero; @@ -236,9 +238,8 @@ def seq : ℕ → { x : 𝓞 K // x ≠ 0 } ⟨(seq_next K w₁ hB (seq n).prop).choose, (seq_next K w₁ hB (seq n).prop).choose_spec.1⟩ /-- The terms of the sequence are nonzero. -/ -theorem seq_ne_zero (n : ℕ) : (seq K w₁ hB n : K) ≠ 0 := by - refine (map_ne_zero_iff (algebraMap (𝓞 K) K) ?_).mpr (seq K w₁ hB n).prop - exact IsFractionRing.injective { x // x ∈ 𝓞 K } K +theorem seq_ne_zero (n : ℕ) : algebraMap (𝓞 K) K (seq K w₁ hB n) ≠ 0 := + RingOfIntegers.coe_ne_zero_iff.mpr (seq K w₁ hB n).prop /-- The terms of the sequence have nonzero norm. -/ theorem seq_norm_ne_zero (n : ℕ) : Algebra.norm ℤ (seq K w₁ hB n : 𝓞 K) ≠ 0 := @@ -246,7 +247,7 @@ theorem seq_norm_ne_zero (n : ℕ) : Algebra.norm ℤ (seq K w₁ hB n : 𝓞 K) /-- The sequence is strictly decreasing at infinite places distinct from `w₁`. -/ theorem seq_decreasing {n m : ℕ} (h : n < m) (w : InfinitePlace K) (hw : w ≠ w₁) : - w (seq K w₁ hB m) < w (seq K w₁ hB n) := by + w (algebraMap (𝓞 K) K (seq K w₁ hB m)) < w (algebraMap (𝓞 K) K (seq K w₁ hB n)) := by induction m with | zero => exfalso @@ -286,12 +287,13 @@ theorem exists_unit (w₁ : InfinitePlace K) : (Ideal.span ({ (seq K w₁ hB n : 𝓞 K) }) = Ideal.span ({ (seq K w₁ hB m : 𝓞 K) })) · have hu := Ideal.span_singleton_eq_span_singleton.mp h refine ⟨hu.choose, fun w hw => Real.log_neg ?_ ?_⟩ - · simp only [pos_iff, ne_eq, ZeroMemClass.coe_eq_zero, Units.ne_zero, not_false_eq_true] + · exact pos_iff.mpr (coe_ne_zero _) · calc - _ = w ((seq K w₁ hB m : K) * (seq K w₁ hB n : K)⁻¹) := by - rw [← congr_arg ((↑) : (𝓞 K) → K) hu.choose_spec, mul_comm, Submonoid.coe_mul, - ← mul_assoc, inv_mul_cancel (seq_ne_zero K w₁ hB n), one_mul] - _ = w (seq K w₁ hB m) * w (seq K w₁ hB n)⁻¹ := _root_.map_mul _ _ _ + _ = w (algebraMap (𝓞 K) K (seq K w₁ hB m) * (algebraMap (𝓞 K) K (seq K w₁ hB n))⁻¹) := by + rw [← congr_arg (algebraMap (𝓞 K) K) hu.choose_spec, mul_comm, map_mul (algebraMap _ _), + ← mul_assoc, inv_mul_cancel (seq_ne_zero K w₁ hB n), one_mul] + _ = w (algebraMap (𝓞 K) K (seq K w₁ hB m)) * w (algebraMap (𝓞 K) K (seq K w₁ hB n))⁻¹ := + _root_.map_mul _ _ _ _ < 1 := by rw [map_inv₀, mul_inv_lt_iff (pos_iff.mpr (seq_ne_zero K w₁ hB n)), mul_one] exact seq_decreasing K w₁ hB hnm w hw