Skip to content

Commit 0400baa

Browse files
riccardobrascariccardobrasca
committed
this is done
1 parent 2efb0a3 commit 0400baa

File tree

1 file changed

+33
-20
lines changed

1 file changed

+33
-20
lines changed

‎FltRegular/NumberTheory/KummersLemma/Field.lean

+33-20
Original file line numberDiff line numberDiff line change
@@ -12,8 +12,6 @@ variable (hp : p ≠ 2)
1212
variable {ζ : K} (hζ : IsPrimitiveRoot ζ p) (u : (𝓞 K)ˣ)
1313
(hcong : (hζ.unit' - 1 : 𝓞 K) ^ (p : ℕ) ∣ (↑u : 𝓞 K) - 1) (hu : ∀ v : K, v ^ (p : ℕ) ≠ u)
1414

15-
-- attribute [-instance] instCoeOut
16-
1715
open Polynomial
1816

1917
lemma zeta_sub_one_pow_dvd_poly :
@@ -75,21 +73,28 @@ lemma map_poly : (poly hp hζ u hcong).map (algebraMap (𝓞 K) K) =
7573
have := congr_arg (fun P : (𝓞 K)[X] ↦ (↑(coeff P i) : K)) (poly_spec hp hζ u hcong)
7674
change _ = algebraMap (𝓞 K) K _ at this
7775
rw [← coeff_map] at this
78-
-- TODO: this simp is not simplifying nearly enough ↓
79-
simp only [coeff_C_mul, Submonoid.coe_mul, Subsemiring.coe_toSubmonoid,
80-
Subalgebra.coe_toSubsemiring, SubmonoidClass.coe_pow, AddSubgroupClass.coe_sub,
81-
IsPrimitiveRoot.val_unit'_coe, OneMemClass.coe_one, Polynomial.map_add, Polynomial.map_pow,
82-
Polynomial.map_sub, Polynomial.map_mul, map_C, map_sub, map_one, map_X, Polynomial.map_one,
83-
coeff_add] at this
76+
replace this : (ζ - 1) ^ (p : ℕ) * ↑((poly hp hζ u hcong).coeff i) =
77+
(((C ((algebraMap ((𝓞 K)) K) ↑hζ.unit') - 1) * X - 1) ^ (p : ℕ)).coeff i +
78+
(C ((algebraMap ((𝓞 K)) K) ↑u)).coeff i := by
79+
simp only [map_pow, map_sub, map_one, Polynomial.map_add, Polynomial.map_pow,
80+
Polynomial.map_sub, Polynomial.map_mul, map_C, IsPrimitiveRoot.coe_unit'_coe,
81+
Polynomial.map_one, map_X, coeff_add] at this
82+
convert this
83+
simp only [NumberField.RingOfIntegers.coe_eq_algebraMap, ← Polynomial.coeff_map]
84+
simp only [coeff_map, Polynomial.map_mul, Polynomial.map_pow, Polynomial.map_sub, map_C,
85+
IsPrimitiveRoot.coe_unit'_coe, Polynomial.map_one]
86+
rw [← Polynomial.coeff_map, mul_comm, ← Polynomial.coeff_mul_C, mul_comm]
87+
simp
8488
apply mul_right_injective₀ (pow_ne_zero p (hζ.sub_one_ne_zero hpri.out.one_lt))
8589
simp only [Subalgebra.algebraMap_eq, Algebra.id.map_eq_id, RingHomCompTriple.comp_eq, coeff_map,
8690
RingHom.coe_coe, Subalgebra.coe_val, one_div, map_sub, map_one, coeff_add, coeff_sub,
87-
PNat.pos, pow_eq_zero_iff, this, mul_add, IsPrimitiveRoot.val_unit'_coe]
91+
PNat.pos, pow_eq_zero_iff, this, mul_add, IsPrimitiveRoot.val_unit'_coe,
92+
IsPrimitiveRoot.coe_unit'_coe]
8893
simp_rw [← smul_eq_mul K, ← coeff_smul]
8994
rw [smul_C, smul_eq_mul, ← smul_pow, ← mul_div_assoc, mul_div_cancel_left₀, smul_sub, smul_C,
9095
smul_eq_mul, mul_inv_cancel, map_one, Algebra.smul_def, ← C_eq_algebraMap, map_sub, map_one]
91-
exact hζ.sub_one_ne_zero hpri.out.one_lt
92-
exact pow_ne_zero _ (hζ.sub_one_ne_zero hpri.out.one_lt)
96+
· exact hζ.sub_one_ne_zero hpri.out.one_lt
97+
· exact pow_ne_zero _ (hζ.sub_one_ne_zero hpri.out.one_lt)
9398

9499
lemma irreducible_map_poly :
95100
Irreducible ((poly hp hζ u hcong).map (algebraMap (𝓞 K) K)) := by
@@ -103,6 +108,12 @@ lemma irreducible_map_poly :
103108
rw [mul_pow, (hpri.out.odd_of_ne_two (PNat.coe_injective.ne hp)).neg_pow, hb, neg_neg,
104109
div_mul_cancel₀ _ (pow_ne_zero _ (hζ.sub_one_ne_zero hpri.out.one_lt))]
105110

111+
--Add to mathlib
112+
instance {K L : Type*} [Field K] [Ring L] [Algebra K L] : Algebra (𝓞 K) L :=
113+
inferInstanceAs (Algebra (integralClosure _ _) L)
114+
instance {K L : Type*} [Field K] [Ring L] [Algebra K L] : IsScalarTower (𝓞 K) K L :=
115+
inferInstanceAs (IsScalarTower (integralClosure _ _) K L)
116+
106117
theorem aeval_poly {L : Type*} [Field L] [Algebra K L] (α : L)
107118
(e : α ^ (p : ℕ) = algebraMap K L u) (m : ℕ) :
108119
aeval (((1 : L) - ζ ^ m • α) / (algebraMap K L (ζ - 1))) (poly hp hζ u hcong) = 0 := by
@@ -111,8 +122,11 @@ theorem aeval_poly {L : Type*} [Field L] [Algebra K L] (α : L)
111122
rw [map_sub, map_one]
112123
have := congr_arg (aeval ((1 - ζ ^ m • α) / (algebraMap K L (ζ - 1))))
113124
(poly_spec hp hζ u hcong)
125+
-- also add to mathlib
126+
have hcoe : (algebraMap (𝓞 K) L) (↑hζ.unit') = algebraMap K L ζ := rfl
127+
have hcoe1 : (algebraMap (𝓞 K) L) ↑u = algebraMap K L ↑↑u := rfl
114128
simp only [map_sub, map_one, map_pow, map_mul, aeval_C, Subalgebra.algebraMap_eq, smul_pow,
115-
RingHom.coe_comp, RingHom.coe_coe, Subalgebra.coe_val, Function.comp_apply, e,
129+
hcoe, RingHom.coe_comp, RingHom.coe_coe, Subalgebra.coe_val, Function.comp_apply, e, hcoe1,
116130
IsPrimitiveRoot.val_unit'_coe, map_add, aeval_X, ← mul_div_assoc, mul_div_cancel_left₀ _ hζ',
117131
sub_sub_cancel_left, (hpri.out.odd_of_ne_two (PNat.coe_injective.ne hp)).neg_pow] at this
118132
rw [← pow_mul, mul_comm m, pow_mul, hζ.pow_eq_one, one_pow, one_smul, add_left_neg,
@@ -237,10 +251,9 @@ lemma separable_poly_aux {L : Type*} [Field L] [Algebra K L] (α : L)
237251
· rw [mem_nthRootsFinset p.pos, ← pow_mul, mul_comm, pow_mul, hζ.unit'_coe.pow_eq_one, one_pow]
238252
· rw [mem_nthRootsFinset p.pos, ← pow_mul, mul_comm, pow_mul, hζ.unit'_coe.pow_eq_one, one_pow]
239253
· exact mt (hζ.unit'_coe.injOn_pow hj hi) hij.symm
240-
apply_fun Subtype.val at hv
241-
simp only [Submonoid.coe_mul, Subsemiring.coe_toSubmonoid, Subalgebra.coe_toSubsemiring,
242-
AddSubgroupClass.coe_sub, IsPrimitiveRoot.val_unit'_coe, OneMemClass.coe_one,
243-
SubmonoidClass.coe_pow] at hv
254+
rw [NumberField.RingOfIntegers.ext_iff] at hv
255+
have hcoe : (algebraMap (𝓞 K) K) (↑hζ.unit') = ζ := rfl
256+
simp only [map_mul, map_sub, IsPrimitiveRoot.val_unit'_coe, map_one, map_pow, hcoe] at hv
244257
have hα : IsIntegral (𝓞 K) α := by
245258
apply IsIntegral.of_pow p.pos; rw [e]; exact isIntegral_algebraMap
246259
have : IsUnit (⟨α, isIntegral_trans (IsIntegralClosure.isIntegral_algebra ℤ K) _ hα⟩ : 𝓞 L) := by
@@ -249,9 +262,8 @@ lemma separable_poly_aux {L : Type*} [Field L] [Algebra K L] (α : L)
249262
ext; simp only [SubmonoidClass.coe_pow, e]; rfl
250263
convert ((algebraMap (𝓞 K) (𝓞 L)).isUnit_map v.isUnit).mul this using 1
251264
ext
252-
simp only [polyRoot, map_sub, map_one, sub_div, one_div, AddSubgroupClass.coe_sub,
253-
sub_sub_sub_cancel_left, Submonoid.coe_mul, Subsemiring.coe_toSubmonoid,
254-
Subalgebra.coe_toSubsemiring]
265+
simp only [polyRoot, map_sub, map_one, sub_div, one_div, map_sub,
266+
sub_sub_sub_cancel_left, map_mul, NumberField.RingOfIntegers.map_mk]
255267
rw [← sub_div, ← sub_smul, ← hv, Algebra.smul_def, map_mul, map_sub, map_one, mul_assoc,
256268
mul_div_cancel_left₀ _ hζ']
257269
rfl
@@ -282,7 +294,8 @@ lemma polyRoot_spec {L : Type*} [Field L] [Algebra K L] (α : L)
282294
(e : α ^ (p : ℕ) = algebraMap K L u) (i) :
283295
α = (ζ ^ i)⁻¹ • (1 - (ζ - 1) • (polyRoot hp hζ u hcong α e i : L)) := by
284296
apply smul_right_injective (M := L) (c := ζ ^ i) (pow_ne_zero _ <| hζ.ne_zero p.pos.ne.symm)
285-
simp only [polyRoot, map_sub, map_one, Algebra.smul_def (ζ - 1), ← mul_div_assoc,
297+
simp only [polyRoot, map_sub, map_one, NumberField.RingOfIntegers.map_mk,
298+
Algebra.smul_def (ζ - 1), ← mul_div_assoc,
286299
mul_div_cancel_left₀ _
287300
((hζ.map_of_injective (algebraMap K L).injective).sub_one_ne_zero hpri.out.one_lt),
288301
sub_sub_cancel, smul_smul, inv_mul_cancel (pow_ne_zero _ <| hζ.ne_zero p.pos.ne.symm), one_smul]

0 commit comments

Comments
 (0)