feat(number_theory/cyclotomic/rat): add integral_power_basis (#15570)

We add `integral_power_basis` and some variants, defining integral power basis of `𝓞 K`.

From flt-regular

src/number_theory/cyclotomic/rat.lean

@@ -9,7 +9,8 @@ import ring_theory.polynomial.eisenstein
 
 /-!
 # Ring of integers of `p ^ n`-th cyclotomic fields
-We compute the ring of integers of a `p ^ n`-th cyclotomic extension of `ℚ`.
+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_adjoing_singleton_of_prime_pow`: if `K` is a
@@ -21,16 +22,16 @@ We compute the ring of integers of a `p ^ n`-th cyclotomic extension of `ℚ`.
 
 universes u
 
-open algebra is_cyclotomic_extension polynomial
+open algebra is_cyclotomic_extension polynomial number_field
 
-open_locale cyclotomic
-
-namespace is_cyclotomic_extension.rat
+open_locale cyclotomic number_field nat
 
 variables {p : ℕ+} {k : ℕ} {K : Type u} [field K] [char_zero K] {ζ : K} [hp : fact (p : ℕ).prime]
 
 include hp
 
+namespace is_cyclotomic_extension.rat
+
 /-- The discriminant of the power basis given by `ζ - 1`. -/
 lemma discr_prime_pow_ne_two' [is_cyclotomic_extension {p ^ (k + 1)} ℚ K]
   (hζ : is_primitive_root ζ ↑(p ^ (k + 1))) (hk : p ^ (k + 1) ≠ 2) :
@@ -166,3 +167,90 @@ begin
 end
 
 end is_cyclotomic_extension.rat
+
+section power_basis
+
+open is_cyclotomic_extension.rat
+
+namespace is_primitive_root
+
+/-- 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_.is_primitive_root.adjoin_equiv_ring_of_integers
+  [hcycl : is_cyclotomic_extension {p ^ k} ℚ K] (hζ : is_primitive_root ζ ↑(p ^ k)) :
+  adjoin ℤ ({ζ} : set K) ≃ₐ[ℤ] (𝓞 K) :=
+let _ := is_integral_closure_adjoing_singleton_of_prime_pow hζ in
+  by exactI (is_integral_closure.equiv ℤ (adjoin ℤ ({ζ} : set K)) K (𝓞 K))
+
+/-- The integral `power_basis` of `𝓞 K` given by a primitive root of unity, where `K` is a `p ^ k`
+cyclotomic extension of `ℚ`. -/
+noncomputable def integral_power_basis [hcycl : is_cyclotomic_extension {p ^ k} ℚ K]
+  (hζ : is_primitive_root ζ ↑(p ^ k)) : power_basis ℤ (𝓞 K) :=
+(adjoin.power_basis' (hζ.is_integral (p ^ k).pos)).map hζ.adjoin_equiv_ring_of_integers
+
+@[simp] lemma integral_power_basis_gen [hcycl : is_cyclotomic_extension {p ^ k} ℚ K]
+  (hζ : is_primitive_root ζ ↑(p ^ k)) :
+  hζ.integral_power_basis.gen = ⟨ζ, hζ.is_integral (p ^ k).pos⟩ :=
+subtype.ext $ show algebra_map _ K hζ.integral_power_basis.gen = _, by simpa [integral_power_basis]
+
+@[simp] lemma integral_power_basis_dim [hcycl : is_cyclotomic_extension {p ^ k} ℚ K]
+  (hζ : is_primitive_root ζ ↑(p ^ k)) : hζ.integral_power_basis.dim = φ (p ^ k) :=
+by simp [integral_power_basis, ←cyclotomic_eq_minpoly hζ, nat_degree_cyclotomic]
+
+/-- 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_.is_primitive_root.adjoin_equiv_ring_of_integers'
+  [hcycl : is_cyclotomic_extension {p} ℚ K] (hζ : is_primitive_root ζ p) :
+  adjoin ℤ ({ζ} : set K) ≃ₐ[ℤ] (𝓞 K) :=
+@adjoin_equiv_ring_of_integers p 1 K _ _ _ _ (by { convert hcycl, rw pow_one }) (by rwa pow_one)
+
+/-- The integral `power_basis` of `𝓞 K` given by a primitive root of unity, where `K` is a `p`-th
+cyclotomic extension of `ℚ`. -/
+noncomputable def integral_power_basis' [hcycl : is_cyclotomic_extension {p} ℚ K]
+  (hζ : is_primitive_root ζ p) : power_basis ℤ (𝓞 K) :=
+@integral_power_basis p 1 K _ _ _ _ (by { convert hcycl, rw pow_one }) (by rwa pow_one)
+
+@[simp] lemma integral_power_basis'_gen [hcycl : is_cyclotomic_extension {p} ℚ K]
+  (hζ : is_primitive_root ζ p) : hζ.integral_power_basis'.gen = ⟨ζ, hζ.is_integral p.pos⟩ :=
+@integral_power_basis_gen p 1 K _ _ _ _ (by { convert hcycl, rw pow_one }) (by rwa pow_one)
+
+@[simp] lemma power_basis_int'_dim [hcycl : is_cyclotomic_extension {p} ℚ K]
+  (hζ : is_primitive_root ζ p) : hζ.integral_power_basis'.dim = φ p :=
+by erw [@integral_power_basis_dim p 1 K _ _ _ _ (by { convert hcycl, rw pow_one })
+  (by rwa pow_one), pow_one]
+
+/-- The integral `power_basis` of `𝓞 K` given by `ζ - 1`, where `K` is a `p ^ k` cyclotomic
+extension of `ℚ`. -/
+noncomputable def sub_one_integral_power_basis [is_cyclotomic_extension {p ^ k} ℚ K]
+  (hζ : is_primitive_root ζ ↑(p ^ k)) : power_basis ℤ (𝓞 K) :=
+power_basis.of_gen_mem_adjoin' hζ.integral_power_basis (is_integral_of_mem_ring_of_integers $
+  subalgebra.sub_mem _ (hζ.is_integral (p ^ k).pos) (subalgebra.one_mem _))
+begin
+  simp only [integral_power_basis_gen],
+  convert subalgebra.add_mem _
+    (self_mem_adjoin_singleton ℤ (⟨ζ - 1, _⟩ : 𝓞 K))
+    (subalgebra.one_mem _),
+  simp
+end
+
+@[simp] lemma sub_one_integral_power_basis_gen [is_cyclotomic_extension {p ^ k} ℚ K]
+  (hζ : is_primitive_root ζ ↑(p ^ k)) :
+  hζ.sub_one_integral_power_basis.gen =
+  ⟨ζ - 1, subalgebra.sub_mem _ (hζ.is_integral (p ^ k).pos) (subalgebra.one_mem _)⟩ :=
+by simp [sub_one_integral_power_basis]
+
+/-- The integral `power_basis` of `𝓞 K` given by `ζ - 1`, where `K` is a `p`-th cyclotomic
+extension of `ℚ`. -/
+noncomputable def sub_one_integral_power_basis' [hcycl : is_cyclotomic_extension {p} ℚ K]
+  (hζ : is_primitive_root ζ p) : power_basis ℤ (𝓞 K) :=
+@sub_one_integral_power_basis p 1 K _ _ _ _ (by { convert hcycl, rw pow_one }) (by rwa pow_one)
+
+@[simp] lemma sub_one_integral_power_basis'_gen [hcycl : is_cyclotomic_extension {p} ℚ K]
+  (hζ : is_primitive_root ζ p) :
+  hζ.sub_one_integral_power_basis'.gen =
+  ⟨ζ - 1, subalgebra.sub_mem _ (hζ.is_integral p.pos) (subalgebra.one_mem _)⟩ :=
+@sub_one_integral_power_basis_gen p 1 K _ _ _ _ (by { convert hcycl, rw pow_one }) (by rwa pow_one)
+
+end is_primitive_root
+
+end power_basis

src/number_theory/number_field.lean

@@ -70,6 +70,15 @@ localized "notation `𝓞` := number_field.ring_of_integers" in number_field
 
 lemma mem_ring_of_integers (x : K) : x ∈ 𝓞 K ↔ is_integral ℤ x := iff.rfl
 
+lemma is_integral_of_mem_ring_of_integers {K : Type*} [field K] {x : K} (hx : x ∈ 𝓞 K) :
+  is_integral ℤ (⟨x, hx⟩ : 𝓞 K) :=
+begin
+  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]
+end
+
 /-- Given an algebra between two fields, create an algebra between their two rings of integers.
 
 For now, this is not an instance by default as it creates an equal-but-not-defeq diamond with