From fc92b786b5872260a7ce7bcee99e264c38d08715 Mon Sep 17 00:00:00 2001 From: Riccardo Brasca Date: Sat, 24 Jun 2023 07:10:49 +0000 Subject: [PATCH] feat: port NumberTheory.Cyclotomic.Rat (#5417) --- Mathlib.lean | 1 + Mathlib/NumberTheory/Cyclotomic/Rat.lean | 282 +++++++++++++++++++++++ 2 files changed, 283 insertions(+) create mode 100644 Mathlib/NumberTheory/Cyclotomic/Rat.lean diff --git a/Mathlib.lean b/Mathlib.lean index 4aed8375feed34..fe70591cfd6fac 100644 --- a/Mathlib.lean +++ b/Mathlib.lean @@ -2304,6 +2304,7 @@ import Mathlib.NumberTheory.ClassNumber.AdmissibleCardPowDegree import Mathlib.NumberTheory.Cyclotomic.Basic import Mathlib.NumberTheory.Cyclotomic.Discriminant import Mathlib.NumberTheory.Cyclotomic.PrimitiveRoots +import Mathlib.NumberTheory.Cyclotomic.Rat import Mathlib.NumberTheory.Dioph import Mathlib.NumberTheory.DiophantineApproximation import Mathlib.NumberTheory.Divisors diff --git a/Mathlib/NumberTheory/Cyclotomic/Rat.lean b/Mathlib/NumberTheory/Cyclotomic/Rat.lean new file mode 100644 index 00000000000000..549b083b0386ef --- /dev/null +++ b/Mathlib/NumberTheory/Cyclotomic/Rat.lean @@ -0,0 +1,282 @@ +/- +Copyright (c) 2022 Riccardo Brasca. All rights reserved. +Released under Apache 2.0 license as described in the file LICENSE. +Authors: Riccardo Brasca + +! This file was ported from Lean 3 source module number_theory.cyclotomic.rat +! leanprover-community/mathlib commit b353176c24d96c23f0ce1cc63efc3f55019702d9 +! Please do not edit these lines, except to modify the commit id +! if you have ported upstream changes. +-/ +import Mathlib.NumberTheory.Cyclotomic.Discriminant +import Mathlib.RingTheory.Polynomial.Eisenstein.IsIntegral + +/-! +# Ring of integers of `p ^ n`-th cyclotomic fields +We gather results about cyclotomic extensions of `ℚ`. In particular, we compute the ring of +integers of a `p ^ n`-th cyclotomic extension of `ℚ`. + +## Main results +* `IsCyclotomicExtension.Rat.isIntegralClosure_adjoin_singleton_of_prime_pow`: if `K` is a + `p ^ k`-th cyclotomic extension of `ℚ`, then `(adjoin ℤ {ζ})` is the integral closure of + `ℤ` in `K`. +* `IsCyclotomicExtension.Rat.cyclotomicRing_isIntegralClosure_of_prime_pow`: the integral + closure of `ℤ` inside `CyclotomicField (p ^ k) ℚ` is `CyclotomicRing (p ^ k) ℤ ℚ`. +-/ + + +universe u + +open Algebra IsCyclotomicExtension Polynomial NumberField + +open scoped Cyclotomic NumberField Nat + +variable {p : ℕ+} {k : ℕ} {K : Type u} [Field K] [CharZero K] {ζ : K} [hp : Fact (p : ℕ).Prime] + +local macro_rules | `($x ^ $y) => `(HPow.hPow $x $y) -- Porting note: See issue #2220 + +namespace IsCyclotomicExtension.Rat + +/-- The discriminant of the power basis given by `ζ - 1`. -/ +theorem discr_prime_pow_ne_two' [IsCyclotomicExtension {p ^ (k + 1)} ℚ K] + (hζ : IsPrimitiveRoot ζ ↑(p ^ (k + 1))) (hk : p ^ (k + 1) ≠ 2) : + discr ℚ (hζ.subOnePowerBasis ℚ).basis = + (-1) ^ ((p ^ (k + 1) : ℕ).totient / 2) * p ^ ((p : ℕ) ^ k * ((p - 1) * (k + 1) - 1)) := by + rw [← discr_prime_pow_ne_two hζ (cyclotomic.irreducible_rat (p ^ (k + 1)).pos) hk] + exact hζ.discr_zeta_eq_discr_zeta_sub_one.symm +#align is_cyclotomic_extension.rat.discr_prime_pow_ne_two' IsCyclotomicExtension.Rat.discr_prime_pow_ne_two' + +theorem discr_odd_prime' [IsCyclotomicExtension {p} ℚ K] (hζ : IsPrimitiveRoot ζ p) (hodd : p ≠ 2) : + discr ℚ (hζ.subOnePowerBasis ℚ).basis = (-1) ^ (((p : ℕ) - 1) / 2) * p ^ ((p : ℕ) - 2) := by + rw [← discr_odd_prime hζ (cyclotomic.irreducible_rat hp.out.pos) hodd] + exact hζ.discr_zeta_eq_discr_zeta_sub_one.symm +#align is_cyclotomic_extension.rat.discr_odd_prime' IsCyclotomicExtension.Rat.discr_odd_prime' + +/-- The discriminant of the power basis given by `ζ - 1`. Beware that in the cases `p ^ k = 1` and +`p ^ k = 2` the formula uses `1 / 2 = 0` and `0 - 1 = 0`. It is useful only to have a uniform +result. See also `IsCyclotomicExtension.Rat.discr_prime_pow_eq_unit_mul_pow'`. -/ +theorem discr_prime_pow' [IsCyclotomicExtension {p ^ k} ℚ K] (hζ : IsPrimitiveRoot ζ ↑(p ^ k)) : + discr ℚ (hζ.subOnePowerBasis ℚ).basis = + (-1) ^ ((p ^ k : ℕ).totient / 2) * p ^ ((p : ℕ) ^ (k - 1) * ((p - 1) * k - 1)) := by + rw [← discr_prime_pow hζ (cyclotomic.irreducible_rat (p ^ k).pos)] + exact hζ.discr_zeta_eq_discr_zeta_sub_one.symm +#align is_cyclotomic_extension.rat.discr_prime_pow' IsCyclotomicExtension.Rat.discr_prime_pow' + +/-- If `p` is a prime and `IsCyclotomicExtension {p ^ k} K L`, then there are `u : ℤˣ` and +`n : ℕ` such that the discriminant of the power basis given by `ζ - 1` is `u * p ^ n`. Often this is +enough and less cumbersome to use than `IsCyclotomicExtension.Rat.discr_prime_pow'`. -/ +theorem discr_prime_pow_eq_unit_mul_pow' [IsCyclotomicExtension {p ^ k} ℚ K] + (hζ : IsPrimitiveRoot ζ ↑(p ^ k)) : + ∃ (u : ℤˣ) (n : ℕ), discr ℚ (hζ.subOnePowerBasis ℚ).basis = u * p ^ n := by + rw [hζ.discr_zeta_eq_discr_zeta_sub_one.symm] + exact discr_prime_pow_eq_unit_mul_pow hζ (cyclotomic.irreducible_rat (p ^ k).pos) +#align is_cyclotomic_extension.rat.discr_prime_pow_eq_unit_mul_pow' IsCyclotomicExtension.Rat.discr_prime_pow_eq_unit_mul_pow' + +/-- If `K` is a `p ^ k`-th cyclotomic extension of `ℚ`, then `(adjoin ℤ {ζ})` is the +integral closure of `ℤ` in `K`. -/ +theorem isIntegralClosure_adjoin_singleton_of_prime_pow [hcycl : IsCyclotomicExtension {p ^ k} ℚ K] + (hζ : IsPrimitiveRoot ζ ↑(p ^ k)) : IsIntegralClosure (adjoin ℤ ({ζ} : Set K)) ℤ K := by + refine' ⟨Subtype.val_injective, @fun x => ⟨fun h => ⟨⟨x, _⟩, rfl⟩, _⟩⟩ + swap + · rintro ⟨y, rfl⟩ + exact + IsIntegral.algebraMap + (le_integralClosure_iff_isIntegral.1 + (adjoin_le_integralClosure (hζ.isIntegral (p ^ k).pos)) _) + let B := hζ.subOnePowerBasis ℚ + have hint : IsIntegral ℤ B.gen := isIntegral_sub (hζ.isIntegral (p ^ k).pos) isIntegral_one +-- Porting note: the following `haveI` was not needed because the locale `cyclotomic` set it +-- as instances. + letI := IsCyclotomicExtension.finiteDimensional {p ^ k} ℚ K + have H := discr_mul_isIntegral_mem_adjoin ℚ hint h + obtain ⟨u, n, hun⟩ := discr_prime_pow_eq_unit_mul_pow' hζ + rw [hun] at H + replace H := Subalgebra.smul_mem _ H u.inv +-- Porting note: the proof is slightly different because of coercions. + rw [← smul_assoc, ← smul_mul_assoc, Units.inv_eq_val_inv, zsmul_eq_mul, ← Int.cast_mul, + Units.inv_mul, Int.cast_one, one_mul, PNat.pow_coe, Nat.cast_pow, smul_def, map_pow] at H + cases k + · haveI : IsCyclotomicExtension {1} ℚ K := by simpa using hcycl + have : x ∈ (⊥ : Subalgebra ℚ K) := by + rw [singleton_one ℚ K] + exact mem_top + obtain ⟨y, rfl⟩ := mem_bot.1 this + replace h := (isIntegral_algebraMap_iff (algebraMap ℚ K).injective).1 h + obtain ⟨z, hz⟩ := IsIntegrallyClosed.isIntegral_iff.1 h + rw [← hz, ← IsScalarTower.algebraMap_apply] + exact Subalgebra.algebraMap_mem _ _ + · have hmin : (minpoly ℤ B.gen).IsEisensteinAt (Submodule.span ℤ {((p : ℕ) : ℤ)}) := by + have h₁ := minpoly.isIntegrallyClosed_eq_field_fractions' ℚ hint + have h₂ := hζ.minpoly_sub_one_eq_cyclotomic_comp (cyclotomic.irreducible_rat (p ^ _).pos) + rw [IsPrimitiveRoot.subOnePowerBasis_gen] at h₁ + rw [h₁, ← map_cyclotomic_int, show Int.castRingHom ℚ = algebraMap ℤ ℚ by rfl, + show X + 1 = map (algebraMap ℤ ℚ) (X + 1) by simp, ← map_comp] at h₂ + haveI : CharZero ℚ := StrictOrderedSemiring.to_charZero + rw [IsPrimitiveRoot.subOnePowerBasis_gen, + map_injective (algebraMap ℤ ℚ) (algebraMap ℤ ℚ).injective_int h₂] + exact cyclotomic_prime_pow_comp_x_add_one_isEisensteinAt p _ + refine' + adjoin_le _ + (mem_adjoin_of_smul_prime_pow_smul_of_minpoly_is_eiseinstein_at (n := n) + (Nat.prime_iff_prime_int.1 hp.out) hint h (by simpa using H) hmin) + simp only [Set.singleton_subset_iff, SetLike.mem_coe] + exact Subalgebra.sub_mem _ (self_mem_adjoin_singleton ℤ _) (Subalgebra.one_mem _) +#align is_cyclotomic_extension.rat.is_integral_closure_adjoin_singleton_of_prime_pow IsCyclotomicExtension.Rat.isIntegralClosure_adjoin_singleton_of_prime_pow + +theorem isIntegralClosure_adjoin_singleton_of_prime [hcycl : IsCyclotomicExtension {p} ℚ K] + (hζ : IsPrimitiveRoot ζ ↑p) : IsIntegralClosure (adjoin ℤ ({ζ} : Set K)) ℤ K := by + rw [← pow_one p] at hζ hcycl + exact isIntegralClosure_adjoin_singleton_of_prime_pow hζ +#align is_cyclotomic_extension.rat.is_integral_closure_adjoin_singleton_of_prime IsCyclotomicExtension.Rat.isIntegralClosure_adjoin_singleton_of_prime + +/-- The integral closure of `ℤ` inside `CyclotomicField (p ^ k) ℚ` is +`CyclotomicRing (p ^ k) ℤ ℚ`. -/ +theorem cyclotomicRing_isIntegralClosure_of_prime_pow : + IsIntegralClosure (CyclotomicRing (p ^ k) ℤ ℚ) ℤ (CyclotomicField (p ^ k) ℚ) := by + haveI : CharZero ℚ := StrictOrderedSemiring.to_charZero + have hζ := zeta_spec (p ^ k) ℚ (CyclotomicField (p ^ k) ℚ) + refine' ⟨IsFractionRing.injective _ _, @fun x => ⟨fun h => ⟨⟨x, _⟩, rfl⟩, _⟩⟩ +-- Porting note: having `.isIntegral_iff` inside the definition of `this` causes an error. + · have := (isIntegralClosure_adjoin_singleton_of_prime_pow hζ) + obtain ⟨y, rfl⟩ := this.isIntegral_iff.1 h + refine' adjoin_mono _ y.2 + simp only [PNat.pow_coe, Set.singleton_subset_iff, Set.mem_setOf_eq] + exact hζ.pow_eq_one + · rintro ⟨y, rfl⟩ + exact IsIntegral.algebraMap ((IsCyclotomicExtension.integral {p ^ k} ℤ _) _) +#align is_cyclotomic_extension.rat.cyclotomic_ring_is_integral_closure_of_prime_pow IsCyclotomicExtension.Rat.cyclotomicRing_isIntegralClosure_of_prime_pow + +theorem cyclotomicRing_isIntegralClosure_of_prime : + IsIntegralClosure (CyclotomicRing p ℤ ℚ) ℤ (CyclotomicField p ℚ) := by + rw [← pow_one p] + exact cyclotomicRing_isIntegralClosure_of_prime_pow +#align is_cyclotomic_extension.rat.cyclotomic_ring_is_integral_closure_of_prime IsCyclotomicExtension.Rat.cyclotomicRing_isIntegralClosure_of_prime + +end IsCyclotomicExtension.Rat + +section PowerBasis + +open IsCyclotomicExtension.Rat + +namespace IsPrimitiveRoot + +/-- The algebra isomorphism `adjoin ℤ {ζ} ≃ₐ[ℤ] (𝓞 K)`, where `ζ` is a primitive `p ^ k`-th root of +unity and `K` is a `p ^ k`-th cyclotomic extension of `ℚ`. -/ +@[simps!] +noncomputable def _root_.IsPrimitiveRoot.adjoinEquivRingOfIntegers + [IsCyclotomicExtension {p ^ k} ℚ K] (hζ : IsPrimitiveRoot ζ ↑(p ^ k)) : + adjoin ℤ ({ζ} : Set K) ≃ₐ[ℤ] 𝓞 K := + let _ := isIntegralClosure_adjoin_singleton_of_prime_pow hζ + IsIntegralClosure.equiv ℤ (adjoin ℤ ({ζ} : Set K)) K (𝓞 K) +#align is_primitive_root.adjoin_equiv_ring_of_integers IsPrimitiveRoot.adjoinEquivRingOfIntegers + +/-- The ring of integers of a `p ^ k`-th cyclotomic extension of `ℚ` is a cyclotomic extension. -/ +instance IsCyclotomicExtension.ringOfIntegers [IsCyclotomicExtension {p ^ k} ℚ K] : + IsCyclotomicExtension {p ^ k} ℤ (𝓞 K) := + let _ := (zeta_spec (p ^ k) ℚ K).adjoin_isCyclotomicExtension ℤ + IsCyclotomicExtension.equiv _ ℤ _ (zeta_spec (p ^ k) ℚ K).adjoinEquivRingOfIntegers +#align is_cyclotomic_extension.ring_of_integers IsPrimitiveRoot.IsCyclotomicExtension.ringOfIntegers + +/-- The integral `PowerBasis` of `𝓞 K` given by a primitive root of unity, where `K` is a `p ^ k` +cyclotomic extension of `ℚ`. -/ +noncomputable def integralPowerBasis [IsCyclotomicExtension {p ^ k} ℚ K] + (hζ : IsPrimitiveRoot ζ ↑(p ^ k)) : PowerBasis ℤ (𝓞 K) := + (Algebra.adjoin.powerBasis' (hζ.isIntegral (p ^ k).pos)).map hζ.adjoinEquivRingOfIntegers +#align is_primitive_root.integral_power_basis IsPrimitiveRoot.integralPowerBasis + +--Porting note: the proof changed because `simp` unfolds too much. +@[simp] +theorem integralPowerBasis_gen [hcycl : IsCyclotomicExtension {p ^ k} ℚ K] + (hζ : IsPrimitiveRoot ζ ↑(p ^ k)) : + hζ.integralPowerBasis.gen = ⟨ζ, hζ.isIntegral (p ^ k).pos⟩ := + Subtype.ext <| show algebraMap _ K hζ.integralPowerBasis.gen = _ by + rw [integralPowerBasis, PowerBasis.map_gen, adjoin.powerBasis'_gen] + simp only [adjoinEquivRingOfIntegers_apply, IsIntegralClosure.algebraMap_lift] + rfl +#align is_primitive_root.integral_power_basis_gen IsPrimitiveRoot.integralPowerBasis_gen + +@[simp] +theorem integralPowerBasis_dim [hcycl : IsCyclotomicExtension {p ^ k} ℚ K] + (hζ : IsPrimitiveRoot ζ ↑(p ^ k)) : hζ.integralPowerBasis.dim = φ (p ^ k) := by + simp [integralPowerBasis, ← cyclotomic_eq_minpoly hζ, natDegree_cyclotomic] +#align is_primitive_root.integral_power_basis_dim IsPrimitiveRoot.integralPowerBasis_dim + +/-- The algebra isomorphism `adjoin ℤ {ζ} ≃ₐ[ℤ] (𝓞 K)`, where `ζ` is a primitive `p`-th root of +unity and `K` is a `p`-th cyclotomic extension of `ℚ`. -/ +@[simps!] +noncomputable def _root_.IsPrimitiveRoot.adjoinEquivRingOfIntegers' + [hcycl : IsCyclotomicExtension {p} ℚ K] (hζ : IsPrimitiveRoot ζ p) : + adjoin ℤ ({ζ} : Set K) ≃ₐ[ℤ] 𝓞 K := + @adjoinEquivRingOfIntegers p 1 K _ _ _ _ (by convert hcycl; rw [pow_one]) (by rwa [pow_one]) +#align is_primitive_root.adjoin_equiv_ring_of_integers' IsPrimitiveRoot.adjoinEquivRingOfIntegers' + +/-- The ring of integers of a `p`-th cyclotomic extension of `ℚ` is a cyclotomic extension. -/ +instance _root_.IsCyclotomicExtension.ring_of_integers' [IsCyclotomicExtension {p} ℚ K] : + IsCyclotomicExtension {p} ℤ (𝓞 K) := + let _ := (zeta_spec p ℚ K).adjoin_isCyclotomicExtension ℤ + IsCyclotomicExtension.equiv _ ℤ _ (zeta_spec p ℚ K).adjoinEquivRingOfIntegers' +#align is_cyclotomic_extension.ring_of_integers' IsCyclotomicExtension.ring_of_integers' + +/-- The integral `PowerBasis` of `𝓞 K` given by a primitive root of unity, where `K` is a `p`-th +cyclotomic extension of `ℚ`. -/ +noncomputable def integralPowerBasis' [hcycl : IsCyclotomicExtension {p} ℚ K] + (hζ : IsPrimitiveRoot ζ p) : PowerBasis ℤ (𝓞 K) := + @integralPowerBasis p 1 K _ _ _ _ (by convert hcycl; rw [pow_one]) (by rwa [pow_one]) +#align is_primitive_root.integral_power_basis' IsPrimitiveRoot.integralPowerBasis' + +@[simp] +theorem integralPowerBasis'_gen [hcycl : IsCyclotomicExtension {p} ℚ K] (hζ : IsPrimitiveRoot ζ p) : + hζ.integralPowerBasis'.gen = ⟨ζ, hζ.isIntegral p.pos⟩ := + @integralPowerBasis_gen p 1 K _ _ _ _ (by convert hcycl; rw [pow_one]) (by rwa [pow_one]) +#align is_primitive_root.integral_power_basis'_gen IsPrimitiveRoot.integralPowerBasis'_gen + +@[simp] +theorem power_basis_int'_dim [hcycl : IsCyclotomicExtension {p} ℚ K] (hζ : IsPrimitiveRoot ζ p) : + hζ.integralPowerBasis'.dim = φ p := by + erw [@integralPowerBasis_dim p 1 K _ _ _ _ (by convert hcycl; rw [pow_one]) (by rwa [pow_one]), + pow_one] +#align is_primitive_root.power_basis_int'_dim IsPrimitiveRoot.power_basis_int'_dim + +/-- The integral `PowerBasis` of `𝓞 K` given by `ζ - 1`, where `K` is a `p ^ k` cyclotomic +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 _)) + (by + simp only [integralPowerBasis_gen] + convert Subalgebra.add_mem _ (self_mem_adjoin_singleton ℤ (⟨ζ - 1, _⟩ : 𝓞 K)) + (Subalgebra.one_mem _) +-- Porting note: `simp` was able to finish the proof. + simp only [Subsemiring.coe_add, Subalgebra.coe_toSubsemiring, + OneMemClass.coe_one, sub_add_cancel] + exact Subalgebra.sub_mem _ (hζ.isIntegral (by simp)) (Subalgebra.one_mem _)) +#align is_primitive_root.sub_one_integral_power_basis IsPrimitiveRoot.subOneIntegralPowerBasis + +@[simp] +theorem subOneIntegralPowerBasis_gen [IsCyclotomicExtension {p ^ k} ℚ K] + (hζ : IsPrimitiveRoot ζ ↑(p ^ k)) : + hζ.subOneIntegralPowerBasis.gen = + ⟨ζ - 1, Subalgebra.sub_mem _ (hζ.isIntegral (p ^ k).pos) (Subalgebra.one_mem _)⟩ := + by simp [subOneIntegralPowerBasis] +#align is_primitive_root.sub_one_integral_power_basis_gen IsPrimitiveRoot.subOneIntegralPowerBasis_gen + +/-- The integral `PowerBasis` of `𝓞 K` given by `ζ - 1`, where `K` is a `p`-th cyclotomic +extension of `ℚ`. -/ +noncomputable def subOneIntegralPowerBasis' [hcycl : IsCyclotomicExtension {p} ℚ K] + (hζ : IsPrimitiveRoot ζ p) : PowerBasis ℤ (𝓞 K) := + @subOneIntegralPowerBasis p 1 K _ _ _ _ (by convert hcycl; rw [pow_one]) (by rwa [pow_one]) +#align is_primitive_root.sub_one_integral_power_basis' IsPrimitiveRoot.subOneIntegralPowerBasis' + +@[simp] +theorem subOneIntegralPowerBasis'_gen [hcycl : IsCyclotomicExtension {p} ℚ K] + (hζ : IsPrimitiveRoot ζ p) : + hζ.subOneIntegralPowerBasis'.gen = + ⟨ζ - 1, Subalgebra.sub_mem _ (hζ.isIntegral p.pos) (Subalgebra.one_mem _)⟩ := + @subOneIntegralPowerBasis_gen p 1 K _ _ _ _ (by convert hcycl; rw [pow_one]) (by rwa [pow_one]) +#align is_primitive_root.sub_one_integral_power_basis'_gen IsPrimitiveRoot.subOneIntegralPowerBasis'_gen + +end IsPrimitiveRoot + +end PowerBasis