From 80ac9b4a7b409c2f52eadd7ab2a71605dc411367 Mon Sep 17 00:00:00 2001 From: Riccardo Brasca Date: Fri, 23 Jun 2023 11:48:41 +0200 Subject: [PATCH 01/11] feat: port NumberTheory.Cyclotomic.Rat From bfeeebf122af6f74231bb6edc349fcb3cb6bb726 Mon Sep 17 00:00:00 2001 From: Riccardo Brasca Date: Fri, 23 Jun 2023 11:48:41 +0200 Subject: [PATCH 02/11] Initial file copy from mathport --- Mathlib/NumberTheory/Cyclotomic/Rat.lean | 278 +++++++++++++++++++++++ 1 file changed, 278 insertions(+) create mode 100644 Mathlib/NumberTheory/Cyclotomic/Rat.lean diff --git a/Mathlib/NumberTheory/Cyclotomic/Rat.lean b/Mathlib/NumberTheory/Cyclotomic/Rat.lean new file mode 100644 index 0000000000000..6d91c9a352534 --- /dev/null +++ b/Mathlib/NumberTheory/Cyclotomic/Rat.lean @@ -0,0 +1,278 @@ +/- +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 Mathbin.NumberTheory.Cyclotomic.Discriminant +import Mathbin.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 +* `is_cyclotomic_extension.rat.is_integral_closure_adjoin_singleton_of_prime_pow`: if `K` is a + `p ^ k`-th cyclotomic extension of `ℚ`, then `(adjoin ℤ {ζ})` is the integral closure of + `ℤ` in `K`. +* `is_cyclotomic_extension.rat.cyclotomic_ring_is_integral_closure_of_prime_pow`: the integral + closure of `ℤ` inside `cyclotomic_field (p ^ k) ℚ` is `cyclotomic_ring (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] + +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 `is_cyclotomic_extension.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 `is_cyclotomic_extension {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 `is_cyclotomic_extension.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ζ.is_integral (p ^ k).Pos)) _) + let B := hζ.sub_one_power_basis ℚ + have hint : IsIntegral ℤ B.gen := isIntegral_sub (hζ.is_integral (p ^ k).Pos) isIntegral_one + have H := discr_mul_is_integral_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 + rw [← smul_assoc, ← smul_mul_assoc, Units.inv_eq_val_inv, coe_coe, zsmul_eq_mul, ← Int.cast_mul, + Units.inv_mul, Int.cast_one, one_mul, + show (p : ℚ) ^ n • x = ((p : ℕ) : ℤ) ^ n • x by simp [smul_def]] 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 _ _ + refine' + adjoin_le _ + (mem_adjoin_of_smul_prime_pow_smul_of_minpoly_is_eiseinstein_at + (Nat.prime_iff_prime_int.1 hp.out) hint h 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 is_integral_closure_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 `cyclotomic_field (p ^ k) ℚ` is +`cyclotomic_ring (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⟩, _⟩⟩ + · have := (is_integral_closure_adjoin_singleton_of_prime_pow hζ).isIntegral_iff + obtain ⟨y, rfl⟩ := this.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 cyclotomic_ring_is_integral_closure_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 IsPrimitiveRoot.adjoinEquivRingOfIntegers + [hcycl : 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 IsCyclotomicExtension.ringOfIntegers + +/-- The integral `power_basis` of `𝓞 K` given by a primitive root of unity, where `K` is a `p ^ k` +cyclotomic extension of `ℚ`. -/ +noncomputable def integralPowerBasis [hcycl : IsCyclotomicExtension {p ^ k} ℚ K] + (hζ : IsPrimitiveRoot ζ ↑(p ^ k)) : PowerBasis ℤ (𝓞 K) := + (minpoly.Algebra.adjoin.powerBasis' (hζ.IsIntegral (p ^ k).Pos)).map hζ.adjoinEquivRingOfIntegers +#align is_primitive_root.integral_power_basis IsPrimitiveRoot.integralPowerBasis + +@[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 simpa [integral_power_basis] +#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 [integral_power_basis, ← cyclotomic_eq_minpoly hζ, nat_degree_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 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 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 `power_basis` 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 [@integral_power_basis_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 `power_basis` 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) := + minpoly.PowerBasis.ofGenMemAdjoin' hζ.integralPowerBasis + (isIntegral_of_mem_ringOfIntegers <| + Subalgebra.sub_mem _ (hζ.IsIntegral (p ^ k).Pos) (Subalgebra.one_mem _)) + (by + simp only [integral_power_basis_gen] + convert + Subalgebra.add_mem _ (self_mem_adjoin_singleton ℤ (⟨ζ - 1, _⟩ : 𝓞 K)) (Subalgebra.one_mem _) + simp) +#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 [sub_one_integral_power_basis] +#align is_primitive_root.sub_one_integral_power_basis_gen IsPrimitiveRoot.subOneIntegralPowerBasis_gen + +/-- The integral `power_basis` 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 + From 576c1be7e3741c05c4458d29d4fd4b9c76ce41f6 Mon Sep 17 00:00:00 2001 From: Riccardo Brasca Date: Fri, 23 Jun 2023 11:48:41 +0200 Subject: [PATCH 03/11] automated fixes Mathbin -> Mathlib fix certain import statements move "by" to end of line add import to Mathlib.lean --- Mathlib.lean | 1 + Mathlib/NumberTheory/Cyclotomic/Rat.lean | 31 +++++++++--------------- 2 files changed, 12 insertions(+), 20 deletions(-) diff --git a/Mathlib.lean b/Mathlib.lean index aa7f55391abdd..0031530245e3f 100644 --- a/Mathlib.lean +++ b/Mathlib.lean @@ -2297,6 +2297,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 index 6d91c9a352534..acef69bbd6b76 100644 --- a/Mathlib/NumberTheory/Cyclotomic/Rat.lean +++ b/Mathlib/NumberTheory/Cyclotomic/Rat.lean @@ -8,8 +8,8 @@ Authors: Riccardo Brasca ! Please do not edit these lines, except to modify the commit id ! if you have ported upstream changes. -/ -import Mathbin.NumberTheory.Cyclotomic.Discriminant -import Mathbin.RingTheory.Polynomial.Eisenstein.IsIntegral +import Mathlib.NumberTheory.Cyclotomic.Discriminant +import Mathlib.RingTheory.Polynomial.Eisenstein.IsIntegral /-! # Ring of integers of `p ^ n`-th cyclotomic fields @@ -39,15 +39,13 @@ namespace IsCyclotomicExtension.Rat 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 + (-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 + 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' @@ -57,8 +55,7 @@ theorem discr_odd_prime' [IsCyclotomicExtension {p} ℚ K] (hζ : IsPrimitiveRoo result. See also `is_cyclotomic_extension.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 + (-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' @@ -68,8 +65,7 @@ theorem discr_prime_pow' [IsCyclotomicExtension {p ^ k} ℚ K] (hζ : IsPrimitiv enough and less cumbersome to use than `is_cyclotomic_extension.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 + ∃ (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' @@ -77,8 +73,7 @@ theorem discr_prime_pow_eq_unit_mul_pow' [IsCyclotomicExtension {p ^ k} ℚ K] /-- 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 + (hζ : IsPrimitiveRoot ζ ↑(p ^ k)) : IsIntegralClosure (adjoin ℤ ({ζ} : Set K)) ℤ K := by refine' ⟨Subtype.val_injective, fun x => ⟨fun h => ⟨⟨x, _⟩, rfl⟩, _⟩⟩ swap · rintro ⟨y, rfl⟩ @@ -105,8 +100,7 @@ theorem isIntegralClosure_adjoin_singleton_of_prime_pow [hcycl : IsCyclotomicExt 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 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₁ @@ -125,8 +119,7 @@ theorem isIntegralClosure_adjoin_singleton_of_prime_pow [hcycl : IsCyclotomicExt #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 + (hζ : IsPrimitiveRoot ζ ↑p) : IsIntegralClosure (adjoin ℤ ({ζ} : Set K)) ℤ K := by rw [← pow_one p] at hζ hcycl exact is_integral_closure_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 @@ -134,8 +127,7 @@ theorem isIntegralClosure_adjoin_singleton_of_prime [hcycl : IsCyclotomicExtensi /-- The integral closure of `ℤ` inside `cyclotomic_field (p ^ k) ℚ` is `cyclotomic_ring (p ^ k) ℤ ℚ`. -/ theorem cyclotomicRing_isIntegralClosure_of_prime_pow : - IsIntegralClosure (CyclotomicRing (p ^ k) ℤ ℚ) ℤ (CyclotomicField (p ^ k) ℚ) := - by + 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⟩, _⟩⟩ @@ -149,8 +141,7 @@ theorem cyclotomicRing_isIntegralClosure_of_prime_pow : #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 + IsIntegralClosure (CyclotomicRing p ℤ ℚ) ℤ (CyclotomicField p ℚ) := by rw [← pow_one p] exact cyclotomic_ring_is_integral_closure_of_prime_pow #align is_cyclotomic_extension.rat.cyclotomic_ring_is_integral_closure_of_prime IsCyclotomicExtension.Rat.cyclotomicRing_isIntegralClosure_of_prime From 72f887cc0d5bdb888dd93e17ed78c2e66b07fbc0 Mon Sep 17 00:00:00 2001 From: Riccardo Brasca Date: Fri, 23 Jun 2023 12:52:04 +0200 Subject: [PATCH 04/11] good progress --- Mathlib/NumberTheory/Cyclotomic/Rat.lean | 94 +++++++++++++----------- 1 file changed, 51 insertions(+), 43 deletions(-) diff --git a/Mathlib/NumberTheory/Cyclotomic/Rat.lean b/Mathlib/NumberTheory/Cyclotomic/Rat.lean index acef69bbd6b76..92a1397036e82 100644 --- a/Mathlib/NumberTheory/Cyclotomic/Rat.lean +++ b/Mathlib/NumberTheory/Cyclotomic/Rat.lean @@ -33,6 +33,8 @@ 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`. -/ @@ -40,7 +42,7 @@ 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] + 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' @@ -56,7 +58,7 @@ result. See also `is_cyclotomic_extension.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)] + 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' @@ -67,61 +69,64 @@ 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) + 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⟩, _⟩⟩ + 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ζ.is_integral (p ^ k).Pos)) _) - let B := hζ.sub_one_power_basis ℚ - have hint : IsIntegral ℤ B.gen := isIntegral_sub (hζ.is_integral (p ^ k).Pos) isIntegral_one - have H := discr_mul_is_integral_mem_adjoin ℚ hint h + (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 + rw [hun] at H replace H := Subalgebra.smul_mem _ H u.inv - rw [← smul_assoc, ← smul_mul_assoc, Units.inv_eq_val_inv, coe_coe, zsmul_eq_mul, ← Int.cast_mul, - Units.inv_mul, Int.cast_one, one_mul, - show (p : ℚ) ^ n • x = ((p : ℕ) : ℤ) ^ n • x by simp [smul_def]] at H +-- 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 + 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₁ + 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₂ + 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 _ _ + 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 - (Nat.prime_iff_prime_int.1 hp.out) hint h H hmin) + (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 is_integral_closure_adjoin_singleton_of_prime_pow hζ + 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 `cyclotomic_field (p ^ k) ℚ` is @@ -130,9 +135,10 @@ 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⟩, _⟩⟩ - · have := (is_integral_closure_adjoin_singleton_of_prime_pow hζ).isIntegral_iff - obtain ⟨y, rfl⟩ := this.1 h + 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 @@ -143,7 +149,7 @@ theorem cyclotomicRing_isIntegralClosure_of_prime_pow : theorem cyclotomicRing_isIntegralClosure_of_prime : IsIntegralClosure (CyclotomicRing p ℤ ℚ) ℤ (CyclotomicField p ℚ) := by rw [← pow_one p] - exact cyclotomic_ring_is_integral_closure_of_prime_pow + 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 @@ -156,9 +162,9 @@ 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 IsPrimitiveRoot.adjoinEquivRingOfIntegers - [hcycl : IsCyclotomicExtension {p ^ k} ℚ K] (hζ : IsPrimitiveRoot ζ ↑(p ^ k)) : +@[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) @@ -169,38 +175,41 @@ instance IsCyclotomicExtension.ringOfIntegers [IsCyclotomicExtension {p ^ 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 IsCyclotomicExtension.ringOfIntegers +#align is_cyclotomic_extension.ring_of_integers IsPrimitiveRoot.IsCyclotomicExtension.ringOfIntegers /-- The integral `power_basis` of `𝓞 K` given by a primitive root of unity, where `K` is a `p ^ k` cyclotomic extension of `ℚ`. -/ -noncomputable def integralPowerBasis [hcycl : IsCyclotomicExtension {p ^ k} ℚ K] +noncomputable def integralPowerBasis [IsCyclotomicExtension {p ^ k} ℚ K] (hζ : IsPrimitiveRoot ζ ↑(p ^ k)) : PowerBasis ℤ (𝓞 K) := - (minpoly.Algebra.adjoin.powerBasis' (hζ.IsIntegral (p ^ k).Pos)).map hζ.adjoinEquivRingOfIntegers + (minpoly.Algebra.adjoin.powerBasis' (hζ.isIntegral (p ^ k).pos)).map hζ.adjoinEquivRingOfIntegers #align is_primitive_root.integral_power_basis IsPrimitiveRoot.integralPowerBasis @[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 simpa [integral_power_basis] + hζ.integralPowerBasis.gen = ⟨ζ, hζ.isIntegral (p ^ k).pos⟩ := + Subtype.ext <| show algebraMap (𝓞 K) K hζ.integralPowerBasis.gen = _ by + simp only [integralPowerBasis, PowerBasis.map_gen, minpoly.Algebra.adjoin.powerBasis'_gen, adjoin_equiv_ring_of_integers_apply, + is_integral_closure.algebra_map_lift, subtype.coe_mk] #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 [integral_power_basis, ← cyclotomic_eq_minpoly hζ, nat_degree_cyclotomic] + 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 IsPrimitiveRoot.adjoinEquivRingOfIntegers' [hcycl : IsCyclotomicExtension {p} ℚ K] - (hζ : IsPrimitiveRoot ζ p) : adjoin ℤ ({ζ} : Set K) ≃ₐ[ℤ] 𝓞 K := +@[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 IsCyclotomicExtension.ring_of_integers' [IsCyclotomicExtension {p} ℚ K] : +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' @@ -215,7 +224,7 @@ noncomputable def integralPowerBasis' [hcycl : IsCyclotomicExtension {p} ℚ K] @[simp] theorem integralPowerBasis'_gen [hcycl : IsCyclotomicExtension {p} ℚ K] (hζ : IsPrimitiveRoot ζ p) : - hζ.integralPowerBasis'.gen = ⟨ζ, hζ.IsIntegral p.Pos⟩ := + 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 @@ -232,7 +241,7 @@ noncomputable def subOneIntegralPowerBasis [IsCyclotomicExtension {p ^ k} ℚ K] (hζ : IsPrimitiveRoot ζ ↑(p ^ k)) : PowerBasis ℤ (𝓞 K) := minpoly.PowerBasis.ofGenMemAdjoin' hζ.integralPowerBasis (isIntegral_of_mem_ringOfIntegers <| - Subalgebra.sub_mem _ (hζ.IsIntegral (p ^ k).Pos) (Subalgebra.one_mem _)) + Subalgebra.sub_mem _ (hζ.isIntegral (p ^ k).pos) (Subalgebra.one_mem _)) (by simp only [integral_power_basis_gen] convert @@ -244,7 +253,7 @@ noncomputable def subOneIntegralPowerBasis [IsCyclotomicExtension {p ^ k} ℚ K] 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 _)⟩ := + ⟨ζ - 1, Subalgebra.sub_mem _ (hζ.isIntegral (p ^ k).pos) (Subalgebra.one_mem _)⟩ := by simp [sub_one_integral_power_basis] #align is_primitive_root.sub_one_integral_power_basis_gen IsPrimitiveRoot.subOneIntegralPowerBasis_gen @@ -259,11 +268,10 @@ noncomputable def subOneIntegralPowerBasis' [hcycl : IsCyclotomicExtension {p} theorem subOneIntegralPowerBasis'_gen [hcycl : IsCyclotomicExtension {p} ℚ K] (hζ : IsPrimitiveRoot ζ p) : hζ.subOneIntegralPowerBasis'.gen = - ⟨ζ - 1, Subalgebra.sub_mem _ (hζ.IsIntegral p.Pos) (Subalgebra.one_mem _)⟩ := + ⟨ζ - 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 - From c5a18e4587c86e67ed6c46a254c5efb15e5a6e73 Mon Sep 17 00:00:00 2001 From: Riccardo Brasca Date: Fri, 23 Jun 2023 12:54:04 +0200 Subject: [PATCH 05/11] chore: use `_root_.` as in mathlib3 --- Mathlib/FieldTheory/Minpoly/IsIntegrallyClosed.lean | 8 ++++---- 1 file changed, 4 insertions(+), 4 deletions(-) diff --git a/Mathlib/FieldTheory/Minpoly/IsIntegrallyClosed.lean b/Mathlib/FieldTheory/Minpoly/IsIntegrallyClosed.lean index 0da1d5c998a1d..c8b8df50e555d 100644 --- a/Mathlib/FieldTheory/Minpoly/IsIntegrallyClosed.lean +++ b/Mathlib/FieldTheory/Minpoly/IsIntegrallyClosed.lean @@ -180,19 +180,19 @@ def equivAdjoin (hx : IsIntegral R x) : AdjoinRoot (minpoly R x) ≃ₐ[R] adjoi /-- The `PowerBasis` of `adjoin R {x}` given by `x`. See `Algebra.adjoin.powerBasis` for a version over a field. -/ @[simps!] -def Algebra.adjoin.powerBasis' (hx : IsIntegral R x) : +def _root_.Algebra.adjoin.powerBasis' (hx : IsIntegral R x) : PowerBasis R (Algebra.adjoin R ({x} : Set S)) := PowerBasis.map (AdjoinRoot.powerBasis' (minpoly.monic hx)) (minpoly.equivAdjoin hx) -#align algebra.adjoin.power_basis' minpoly.Algebra.adjoin.powerBasis' +#align algebra.adjoin.power_basis' Algebra.adjoin.powerBasis' /-- The power basis given by `x` if `B.gen ∈ adjoin R {x}`. -/ @[simps!] -noncomputable def PowerBasis.ofGenMemAdjoin' (B : PowerBasis R S) (hint : IsIntegral R x) +noncomputable def _root_.PowerBasis.ofGenMemAdjoin' (B : PowerBasis R S) (hint : IsIntegral R x) (hx : B.gen ∈ adjoin R ({x} : Set S)) : PowerBasis R S := (Algebra.adjoin.powerBasis' hint).map <| (Subalgebra.equivOfEq _ _ <| PowerBasis.adjoin_eq_top_of_gen_mem_adjoin hx).trans Subalgebra.topEquiv -#align power_basis.of_gen_mem_adjoin' minpoly.PowerBasis.ofGenMemAdjoin' +#align power_basis.of_gen_mem_adjoin' PowerBasis.ofGenMemAdjoin' end AdjoinRoot From 8d7169b1b75817d659aff1d8f25739ce4ca8ce90 Mon Sep 17 00:00:00 2001 From: Riccardo Brasca Date: Fri, 23 Jun 2023 13:03:29 +0200 Subject: [PATCH 06/11] better --- Mathlib/NumberTheory/Cyclotomic/Rat.lean | 6 +++--- 1 file changed, 3 insertions(+), 3 deletions(-) diff --git a/Mathlib/NumberTheory/Cyclotomic/Rat.lean b/Mathlib/NumberTheory/Cyclotomic/Rat.lean index 92a1397036e82..16d8a8c41c583 100644 --- a/Mathlib/NumberTheory/Cyclotomic/Rat.lean +++ b/Mathlib/NumberTheory/Cyclotomic/Rat.lean @@ -181,7 +181,7 @@ instance IsCyclotomicExtension.ringOfIntegers [IsCyclotomicExtension {p ^ k} ℚ cyclotomic extension of `ℚ`. -/ noncomputable def integralPowerBasis [IsCyclotomicExtension {p ^ k} ℚ K] (hζ : IsPrimitiveRoot ζ ↑(p ^ k)) : PowerBasis ℤ (𝓞 K) := - (minpoly.Algebra.adjoin.powerBasis' (hζ.isIntegral (p ^ k).pos)).map hζ.adjoinEquivRingOfIntegers + (Algebra.adjoin.powerBasis' (hζ.isIntegral (p ^ k).pos)).map hζ.adjoinEquivRingOfIntegers #align is_primitive_root.integral_power_basis IsPrimitiveRoot.integralPowerBasis @[simp] @@ -189,8 +189,8 @@ 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) K hζ.integralPowerBasis.gen = _ by - simp only [integralPowerBasis, PowerBasis.map_gen, minpoly.Algebra.adjoin.powerBasis'_gen, adjoin_equiv_ring_of_integers_apply, - is_integral_closure.algebra_map_lift, subtype.coe_mk] + simp only [integralPowerBasis, PowerBasis.map_gen, Algebra.adjoin.powerBasis'_gen, adjoinEquivRingOfIntegers_apply, + IsIntegralClosure.algebraMap_lift, Subtype.coe_mk] #align is_primitive_root.integral_power_basis_gen IsPrimitiveRoot.integralPowerBasis_gen @[simp] From bd78f26e3c7e54c3ca0bda715b8b34ed85d0311e Mon Sep 17 00:00:00 2001 From: Riccardo Brasca Date: Fri, 23 Jun 2023 17:14:17 +0200 Subject: [PATCH 07/11] better --- .../Minpoly/IsIntegrallyClosed.lean | 26 +++++++++++++++++-- 1 file changed, 24 insertions(+), 2 deletions(-) diff --git a/Mathlib/FieldTheory/Minpoly/IsIntegrallyClosed.lean b/Mathlib/FieldTheory/Minpoly/IsIntegrallyClosed.lean index c8b8df50e555d..dda1a6eba6378 100644 --- a/Mathlib/FieldTheory/Minpoly/IsIntegrallyClosed.lean +++ b/Mathlib/FieldTheory/Minpoly/IsIntegrallyClosed.lean @@ -179,14 +179,24 @@ def equivAdjoin (hx : IsIntegral R x) : AdjoinRoot (minpoly R x) ≃ₐ[R] adjoi /-- The `PowerBasis` of `adjoin R {x}` given by `x`. See `Algebra.adjoin.powerBasis` for a version over a field. -/ -@[simps!] def _root_.Algebra.adjoin.powerBasis' (hx : IsIntegral R x) : PowerBasis R (Algebra.adjoin R ({x} : Set S)) := PowerBasis.map (AdjoinRoot.powerBasis' (minpoly.monic hx)) (minpoly.equivAdjoin hx) #align algebra.adjoin.power_basis' Algebra.adjoin.powerBasis' +@[simp] +theorem _root_.Algebra.adjoin.powerBasis'_dim (hx : IsIntegral R x) : + (Algebra.adjoin.powerBasis' hx).dim = (minpoly R x).natDegree := rfl +#align algebra.adjoin.power_basis'_dim Algebra.adjoin.powerBasis'_dim + +@[simp] +theorem _root_.Algebra.adjoin.powerBasis'_gen (hx : IsIntegral R x) : + (adjoin.powerBasis' hx).gen = ⟨x, SetLike.mem_coe.1 <| subset_adjoin <| mem_singleton x⟩ := by + rw [Algebra.adjoin.powerBasis', PowerBasis.map_gen, AdjoinRoot.powerBasis'_gen, equivAdjoin, + AlgEquiv.ofBijective_apply, Minpoly.toAdjoin, liftHom_root] +#align algebra.adjoin.power_basis'_gen Algebra.adjoin.powerBasis'_gen + /-- The power basis given by `x` if `B.gen ∈ adjoin R {x}`. -/ -@[simps!] noncomputable def _root_.PowerBasis.ofGenMemAdjoin' (B : PowerBasis R S) (hint : IsIntegral R x) (hx : B.gen ∈ adjoin R ({x} : Set S)) : PowerBasis R S := (Algebra.adjoin.powerBasis' hint).map <| @@ -194,6 +204,18 @@ noncomputable def _root_.PowerBasis.ofGenMemAdjoin' (B : PowerBasis R S) (hint : Subalgebra.topEquiv #align power_basis.of_gen_mem_adjoin' PowerBasis.ofGenMemAdjoin' +@[simp] +theorem _root_.PowerBasis.ofGenMemAdjoin'_dim (B : PowerBasis R S) (hint : IsIntegral R x) + (hx : B.gen ∈ adjoin R ({x} : Set S)) : + (B.ofGenMemAdjoin' hint hx).dim = (minpoly R x).natDegree := rfl +#align power_basis.of_gen_mem_adjoin'_dim PowerBasis.ofGenMemAdjoin'_dim + +@[simp] +theorem _root_.PowerBasis.ofGenMemAdjoin'_gen (B : PowerBasis R S) (hint : IsIntegral R x) + (hx : B.gen ∈ adjoin R ({x} : Set S)) : + (B.ofGenMemAdjoin' hint hx).gen = x := by + simp [PowerBasis.ofGenMemAdjoin'] +#align power_basis.of_gen_mem_adjoin'_gen PowerBasis.ofGenMemAdjoin'_gen end AdjoinRoot From 97813e7b5cc94ac8bd7051b815cdda90c158cf36 Mon Sep 17 00:00:00 2001 From: Riccardo Brasca Date: Fri, 23 Jun 2023 17:14:41 +0200 Subject: [PATCH 08/11] progress --- Mathlib/NumberTheory/Cyclotomic/Rat.lean | 11 +++++------ 1 file changed, 5 insertions(+), 6 deletions(-) diff --git a/Mathlib/NumberTheory/Cyclotomic/Rat.lean b/Mathlib/NumberTheory/Cyclotomic/Rat.lean index 16d8a8c41c583..2b81df97b5324 100644 --- a/Mathlib/NumberTheory/Cyclotomic/Rat.lean +++ b/Mathlib/NumberTheory/Cyclotomic/Rat.lean @@ -189,8 +189,7 @@ 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) K hζ.integralPowerBasis.gen = _ by - simp only [integralPowerBasis, PowerBasis.map_gen, Algebra.adjoin.powerBasis'_gen, adjoinEquivRingOfIntegers_apply, - IsIntegralClosure.algebraMap_lift, Subtype.coe_mk] + sorry #align is_primitive_root.integral_power_basis_gen IsPrimitiveRoot.integralPowerBasis_gen @[simp] @@ -231,7 +230,7 @@ theorem integralPowerBasis'_gen [hcycl : IsCyclotomicExtension {p} ℚ K] (hζ : @[simp] theorem power_basis_int'_dim [hcycl : IsCyclotomicExtension {p} ℚ K] (hζ : IsPrimitiveRoot ζ p) : hζ.integralPowerBasis'.dim = φ p := by - erw [@integral_power_basis_dim p 1 K _ _ _ _ (by convert hcycl; rw [pow_one]) (by rwa [pow_one]), + 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 @@ -239,11 +238,11 @@ 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) := - minpoly.PowerBasis.ofGenMemAdjoin' hζ.integralPowerBasis + PowerBasis.ofGenMemAdjoin' hζ.integralPowerBasis (isIntegral_of_mem_ringOfIntegers <| Subalgebra.sub_mem _ (hζ.isIntegral (p ^ k).pos) (Subalgebra.one_mem _)) (by - simp only [integral_power_basis_gen] + simp only [integralPowerBasis_gen] convert Subalgebra.add_mem _ (self_mem_adjoin_singleton ℤ (⟨ζ - 1, _⟩ : 𝓞 K)) (Subalgebra.one_mem _) simp) @@ -254,7 +253,7 @@ 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 [sub_one_integral_power_basis] + by simp [subOneIntegralPowerBasis] #align is_primitive_root.sub_one_integral_power_basis_gen IsPrimitiveRoot.subOneIntegralPowerBasis_gen /-- The integral `power_basis` of `𝓞 K` given by `ζ - 1`, where `K` is a `p`-th cyclotomic From 3d45a19afbf8c8a7215a9cc654af027c89c45d29 Mon Sep 17 00:00:00 2001 From: Riccardo Brasca Date: Fri, 23 Jun 2023 17:15:23 +0200 Subject: [PATCH 09/11] better statements --- .../Minpoly/IsIntegrallyClosed.lean | 36 +++++++++++++++---- 1 file changed, 29 insertions(+), 7 deletions(-) diff --git a/Mathlib/FieldTheory/Minpoly/IsIntegrallyClosed.lean b/Mathlib/FieldTheory/Minpoly/IsIntegrallyClosed.lean index 0da1d5c998a1d..dda1a6eba6378 100644 --- a/Mathlib/FieldTheory/Minpoly/IsIntegrallyClosed.lean +++ b/Mathlib/FieldTheory/Minpoly/IsIntegrallyClosed.lean @@ -179,21 +179,43 @@ def equivAdjoin (hx : IsIntegral R x) : AdjoinRoot (minpoly R x) ≃ₐ[R] adjoi /-- The `PowerBasis` of `adjoin R {x}` given by `x`. See `Algebra.adjoin.powerBasis` for a version over a field. -/ -@[simps!] -def Algebra.adjoin.powerBasis' (hx : IsIntegral R x) : +def _root_.Algebra.adjoin.powerBasis' (hx : IsIntegral R x) : PowerBasis R (Algebra.adjoin R ({x} : Set S)) := PowerBasis.map (AdjoinRoot.powerBasis' (minpoly.monic hx)) (minpoly.equivAdjoin hx) -#align algebra.adjoin.power_basis' minpoly.Algebra.adjoin.powerBasis' +#align algebra.adjoin.power_basis' Algebra.adjoin.powerBasis' + +@[simp] +theorem _root_.Algebra.adjoin.powerBasis'_dim (hx : IsIntegral R x) : + (Algebra.adjoin.powerBasis' hx).dim = (minpoly R x).natDegree := rfl +#align algebra.adjoin.power_basis'_dim Algebra.adjoin.powerBasis'_dim + +@[simp] +theorem _root_.Algebra.adjoin.powerBasis'_gen (hx : IsIntegral R x) : + (adjoin.powerBasis' hx).gen = ⟨x, SetLike.mem_coe.1 <| subset_adjoin <| mem_singleton x⟩ := by + rw [Algebra.adjoin.powerBasis', PowerBasis.map_gen, AdjoinRoot.powerBasis'_gen, equivAdjoin, + AlgEquiv.ofBijective_apply, Minpoly.toAdjoin, liftHom_root] +#align algebra.adjoin.power_basis'_gen Algebra.adjoin.powerBasis'_gen /-- The power basis given by `x` if `B.gen ∈ adjoin R {x}`. -/ -@[simps!] -noncomputable def PowerBasis.ofGenMemAdjoin' (B : PowerBasis R S) (hint : IsIntegral R x) +noncomputable def _root_.PowerBasis.ofGenMemAdjoin' (B : PowerBasis R S) (hint : IsIntegral R x) (hx : B.gen ∈ adjoin R ({x} : Set S)) : PowerBasis R S := (Algebra.adjoin.powerBasis' hint).map <| (Subalgebra.equivOfEq _ _ <| PowerBasis.adjoin_eq_top_of_gen_mem_adjoin hx).trans Subalgebra.topEquiv -#align power_basis.of_gen_mem_adjoin' minpoly.PowerBasis.ofGenMemAdjoin' - +#align power_basis.of_gen_mem_adjoin' PowerBasis.ofGenMemAdjoin' + +@[simp] +theorem _root_.PowerBasis.ofGenMemAdjoin'_dim (B : PowerBasis R S) (hint : IsIntegral R x) + (hx : B.gen ∈ adjoin R ({x} : Set S)) : + (B.ofGenMemAdjoin' hint hx).dim = (minpoly R x).natDegree := rfl +#align power_basis.of_gen_mem_adjoin'_dim PowerBasis.ofGenMemAdjoin'_dim + +@[simp] +theorem _root_.PowerBasis.ofGenMemAdjoin'_gen (B : PowerBasis R S) (hint : IsIntegral R x) + (hx : B.gen ∈ adjoin R ({x} : Set S)) : + (B.ofGenMemAdjoin' hint hx).gen = x := by + simp [PowerBasis.ofGenMemAdjoin'] +#align power_basis.of_gen_mem_adjoin'_gen PowerBasis.ofGenMemAdjoin'_gen end AdjoinRoot From b154f5e15c98d140e56739fc16a40fa34143732c Mon Sep 17 00:00:00 2001 From: Riccardo Brasca Date: Fri, 23 Jun 2023 17:38:17 +0200 Subject: [PATCH 10/11] ths should compile --- Mathlib/NumberTheory/Cyclotomic/Rat.lean | 16 +++++++++++----- 1 file changed, 11 insertions(+), 5 deletions(-) diff --git a/Mathlib/NumberTheory/Cyclotomic/Rat.lean b/Mathlib/NumberTheory/Cyclotomic/Rat.lean index 2b81df97b5324..164955fdbe7cd 100644 --- a/Mathlib/NumberTheory/Cyclotomic/Rat.lean +++ b/Mathlib/NumberTheory/Cyclotomic/Rat.lean @@ -184,12 +184,15 @@ noncomputable def integralPowerBasis [IsCyclotomicExtension {p ^ k} ℚ 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) K hζ.integralPowerBasis.gen = _ by - sorry + 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] @@ -243,9 +246,12 @@ noncomputable def subOneIntegralPowerBasis [IsCyclotomicExtension {p ^ k} ℚ K] 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 _) - simp) + 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] From 6e638c5f409b09e88ffde0dd8cc4f9b59706ecbe Mon Sep 17 00:00:00 2001 From: Riccardo Brasca Date: Fri, 23 Jun 2023 17:43:58 +0200 Subject: [PATCH 11/11] names --- Mathlib/NumberTheory/Cyclotomic/Rat.lean | 24 ++++++++++++------------ 1 file changed, 12 insertions(+), 12 deletions(-) diff --git a/Mathlib/NumberTheory/Cyclotomic/Rat.lean b/Mathlib/NumberTheory/Cyclotomic/Rat.lean index 164955fdbe7cd..549b083b0386e 100644 --- a/Mathlib/NumberTheory/Cyclotomic/Rat.lean +++ b/Mathlib/NumberTheory/Cyclotomic/Rat.lean @@ -17,11 +17,11 @@ We gather results about cyclotomic extensions of `ℚ`. In particular, we comput integers of a `p ^ n`-th cyclotomic extension of `ℚ`. ## Main results -* `is_cyclotomic_extension.rat.is_integral_closure_adjoin_singleton_of_prime_pow`: if `K` is a +* `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`. -* `is_cyclotomic_extension.rat.cyclotomic_ring_is_integral_closure_of_prime_pow`: the integral - closure of `ℤ` inside `cyclotomic_field (p ^ k) ℚ` is `cyclotomic_ring (p ^ k) ℤ ℚ`. +* `IsCyclotomicExtension.Rat.cyclotomicRing_isIntegralClosure_of_prime_pow`: the integral + closure of `ℤ` inside `CyclotomicField (p ^ k) ℚ` is `CyclotomicRing (p ^ k) ℤ ℚ`. -/ @@ -54,7 +54,7 @@ theorem discr_odd_prime' [IsCyclotomicExtension {p} ℚ K] (hζ : IsPrimitiveRoo /-- 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 `is_cyclotomic_extension.rat.discr_prime_pow_eq_unit_mul_pow'`. -/ +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 @@ -62,9 +62,9 @@ theorem discr_prime_pow' [IsCyclotomicExtension {p ^ k} ℚ K] (hζ : IsPrimitiv 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 `is_cyclotomic_extension {p ^ k} K L`, then there are `u : ℤˣ` and +/-- 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 `is_cyclotomic_extension.rat.discr_prime_pow'`. -/ +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 @@ -129,8 +129,8 @@ theorem isIntegralClosure_adjoin_singleton_of_prime [hcycl : IsCyclotomicExtensi 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 `cyclotomic_field (p ^ k) ℚ` is -`cyclotomic_ring (p ^ k) ℤ ℚ`. -/ +/-- 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 @@ -177,7 +177,7 @@ instance IsCyclotomicExtension.ringOfIntegers [IsCyclotomicExtension {p ^ k} ℚ IsCyclotomicExtension.equiv _ ℤ _ (zeta_spec (p ^ k) ℚ K).adjoinEquivRingOfIntegers #align is_cyclotomic_extension.ring_of_integers IsPrimitiveRoot.IsCyclotomicExtension.ringOfIntegers -/-- The integral `power_basis` of `𝓞 K` given by a primitive root of unity, where `K` is a `p ^ k` +/-- 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) := @@ -217,7 +217,7 @@ instance _root_.IsCyclotomicExtension.ring_of_integers' [IsCyclotomicExtension { IsCyclotomicExtension.equiv _ ℤ _ (zeta_spec p ℚ K).adjoinEquivRingOfIntegers' #align is_cyclotomic_extension.ring_of_integers' IsCyclotomicExtension.ring_of_integers' -/-- The integral `power_basis` of `𝓞 K` given by a primitive root of unity, where `K` is a `p`-th +/-- 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) := @@ -237,7 +237,7 @@ theorem power_basis_int'_dim [hcycl : IsCyclotomicExtension {p} ℚ K] (hζ : Is pow_one] #align is_primitive_root.power_basis_int'_dim IsPrimitiveRoot.power_basis_int'_dim -/-- The integral `power_basis` of `𝓞 K` given by `ζ - 1`, where `K` is a `p ^ k` cyclotomic +/-- 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) := @@ -262,7 +262,7 @@ theorem subOneIntegralPowerBasis_gen [IsCyclotomicExtension {p ^ k} ℚ K] by simp [subOneIntegralPowerBasis] #align is_primitive_root.sub_one_integral_power_basis_gen IsPrimitiveRoot.subOneIntegralPowerBasis_gen -/-- The integral `power_basis` of `𝓞 K` given by `ζ - 1`, where `K` is a `p`-th cyclotomic +/-- 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) :=