-
Notifications
You must be signed in to change notification settings - Fork 0
/
Copy pathProject.lean
1392 lines (1262 loc) · 51.8 KB
/
Project.lean
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108
109
110
111
112
113
114
115
116
117
118
119
120
121
122
123
124
125
126
127
128
129
130
131
132
133
134
135
136
137
138
139
140
141
142
143
144
145
146
147
148
149
150
151
152
153
154
155
156
157
158
159
160
161
162
163
164
165
166
167
168
169
170
171
172
173
174
175
176
177
178
179
180
181
182
183
184
185
186
187
188
189
190
191
192
193
194
195
196
197
198
199
200
201
202
203
204
205
206
207
208
209
210
211
212
213
214
215
216
217
218
219
220
221
222
223
224
225
226
227
228
229
230
231
232
233
234
235
236
237
238
239
240
241
242
243
244
245
246
247
248
249
250
251
252
253
254
255
256
257
258
259
260
261
262
263
264
265
266
267
268
269
270
271
272
273
274
275
276
277
278
279
280
281
282
283
284
285
286
287
288
289
290
291
292
293
294
295
296
297
298
299
300
301
302
303
304
305
306
307
308
309
310
311
312
313
314
315
316
317
318
319
320
321
322
323
324
325
326
327
328
329
330
331
332
333
334
335
336
337
338
339
340
341
342
343
344
345
346
347
348
349
350
351
352
353
354
355
356
357
358
359
360
361
362
363
364
365
366
367
368
369
370
371
372
373
374
375
376
377
378
379
380
381
382
383
384
385
386
387
388
389
390
391
392
393
394
395
396
397
398
399
400
401
402
403
404
405
406
407
408
409
410
411
412
413
414
415
416
417
418
419
420
421
422
423
424
425
426
427
428
429
430
431
432
433
434
435
436
437
438
439
440
441
442
443
444
445
446
447
448
449
450
451
452
453
454
455
456
457
458
459
460
461
462
463
464
465
466
467
468
469
470
471
472
473
474
475
476
477
478
479
480
481
482
483
484
485
486
487
488
489
490
491
492
493
494
495
496
497
498
499
500
501
502
503
504
505
506
507
508
509
510
511
512
513
514
515
516
517
518
519
520
521
522
523
524
525
526
527
528
529
530
531
532
533
534
535
536
537
538
539
540
541
542
543
544
545
546
547
548
549
550
551
552
553
554
555
556
557
558
559
560
561
562
563
564
565
566
567
568
569
570
571
572
573
574
575
576
577
578
579
580
581
582
583
584
585
586
587
588
589
590
591
592
593
594
595
596
597
598
599
600
601
602
603
604
605
606
607
608
609
610
611
612
613
614
615
616
617
618
619
620
621
622
623
624
625
626
627
628
629
630
631
632
633
634
635
636
637
638
639
640
641
642
643
644
645
646
647
648
649
650
651
652
653
654
655
656
657
658
659
660
661
662
663
664
665
666
667
668
669
670
671
672
673
674
675
676
677
678
679
680
681
682
683
684
685
686
687
688
689
690
691
692
693
694
695
696
697
698
699
700
701
702
703
704
705
706
707
708
709
710
711
712
713
714
715
716
717
718
719
720
721
722
723
724
725
726
727
728
729
730
731
732
733
734
735
736
737
738
739
740
741
742
743
744
745
746
747
748
749
750
751
752
753
754
755
756
757
758
759
760
761
762
763
764
765
766
767
768
769
770
771
772
773
774
775
776
777
778
779
780
781
782
783
784
785
786
787
788
789
790
791
792
793
794
795
796
797
798
799
800
801
802
803
804
805
806
807
808
809
810
811
812
813
814
815
816
817
818
819
820
821
822
823
824
825
826
827
828
829
830
831
832
833
834
835
836
837
838
839
840
841
842
843
844
845
846
847
848
849
850
851
852
853
854
855
856
857
858
859
860
861
862
863
864
865
866
867
868
869
870
871
872
873
874
875
876
877
878
879
880
881
882
883
884
885
886
887
888
889
890
891
892
893
894
895
896
897
898
899
900
901
902
903
904
905
906
907
908
909
910
911
912
913
914
915
916
917
918
919
920
921
922
923
924
925
926
927
928
929
930
931
932
933
934
935
936
937
938
939
940
941
942
943
944
945
946
947
948
949
950
951
952
953
954
955
956
957
958
959
960
961
962
963
964
965
966
967
968
969
970
971
972
973
974
975
976
977
978
979
980
981
982
983
984
985
986
987
988
989
990
991
992
993
994
995
996
997
998
999
1000
import Mathlib.RingTheory.Ideal.Basic
import Mathlib.Data.Polynomial.Basic
import Mathlib.Data.Polynomial.Div
import Mathlib.NumberTheory.NumberField.Basic
import Mathlib.RingTheory.AdjoinRoot
import Mathlib.Data.Real.Basic
import Mathlib.RingTheory.IsAdjoinRoot
import Mathlib.RingTheory.Polynomial.Eisenstein.Basic
import Mathlib.NumberTheory.Zsqrtd.Basic
import Mathlib.RingTheory.Polynomial.GaussLemma
import Mathlib.Algebra.Algebra.Basic
open Polynomial
open BigOperators
noncomputable section
#check ofFinsupp
#check AddMonoidAlgebra ℚ ℕ
def fz : ℤ[X] := X ^ 2 + C 3
def fq : ℚ[X] := X ^ 2 + C 3
def S :=({(3 : Int)} : Set Int)
def I := Ideal.span S
lemma deg_fz : natDegree fz = 2 := by
unfold fz
compute_degree
norm_num
lemma deg_fq : natDegree fq = 2 := by
unfold fq
compute_degree
norm_num
lemma non_zero_fq : fq ≠ 0 := by
intro con
have con_deg : natDegree 0 = 2 := by rw [<- con, deg_fq]
rw [natDegree_zero] at con_deg
contradiction
lemma I3_prime : Ideal.IsPrime I := by
apply Ideal.isPrime_iff.mpr
constructor
· apply Ideal.span_singleton_ne_top
intro h
apply Int.isUnit_iff.mp at h
rcases h with h | h <;> revert h <;> norm_num
· intro x y hxy
apply Ideal.mem_span_singleton'.mp at hxy
rcases hxy with ⟨a , ha⟩
have : Int.natAbs (a * 3) = Int.natAbs (x * y) := by congr
simp [Int.natAbs_mul] at this
rw [(by simp [Int.natAbs] : Int.natAbs 3 = 3)] at this
have h : 3∣Int.natAbs x * Int.natAbs y := by
rw[← this]
norm_num
obtain h := (Nat.Prime.dvd_mul Nat.prime_three).mp h
rw[I, S]
rcases h with (h1 | h2)
· left
apply Ideal.mem_span_singleton'.mpr
rw[← (by simp [Int.natAbs] : Int.natAbs 3 = 3)] at h1
obtain h1 := Int.natAbs_dvd_natAbs.mp h1
dsimp [Dvd.dvd] at h
rcases h1 with ⟨a, ha⟩
use a
rw[mul_comm, ha]
· right
apply Ideal.mem_span_singleton'.mpr
rw[← (by simp [Int.natAbs] : Int.natAbs 3 = 3)] at h2
obtain h1 := Int.natAbs_dvd_natAbs.mp h2
dsimp [Dvd.dvd] at h2
rcases h1 with ⟨a, ha⟩
use a
rw [mul_comm, ha]
def fz_ess : IsEisensteinAt fz I where
leading := by
simp only [Polynomial.leadingCoeff, deg_fz]
simp [fz]
intro h
apply Ideal.mem_span_singleton'.mp at h
rcases h with ⟨a, ha⟩
apply Int.mul_eq_one_iff_eq_one_or_neg_one.mp at ha
rcases ha with (ha1 | ha2)
· linarith
· linarith
mem := by
intro n hn
rw[deg_fz] at hn
apply Nat.le_of_lt_succ at hn
rcases Nat.of_le_succ hn with (h1 | h2)
· simp at h1
rw [h1]
simp [fz]
rw [I, S]
apply Ideal.mem_span_singleton'.mpr
use 1
ring
· rw [h2]
simp [fz]
not_mem := by
simp [fz, pow_two,I]
intro h
rw [Ideal.span_mul_span] at h
rw [S] at h
simp [Set.mem_iUnion] at h
apply Ideal.mem_span_singleton'.mp at h
rcases h with ⟨a, ha⟩
norm_num at ha
have : ( a * 9 ).natAbs = 3 := by
congr
rw [ha]
simp [Int.natAbs]
simp [Int.natAbs_mul] at this
rw [(by simp [Int.natAbs] : Int.natAbs 9 = 9)] at this
have h : 9 ∣ Int.natAbs a * 9 := by apply Nat.dvd_mul_left
rw [this] at h
apply Nat.le_of_dvd at h <;> linarith
lemma fz_monic : Polynomial.Monic fz := by
simp only [Monic,Polynomial.leadingCoeff]
rw [deg_fz]
have h1 : Polynomial.coeff fz 2 = 1 := by
simp [fz]
rw [h1]
lemma fq_monic :Polynomial.Monic fq := by
simp only [Monic, Polynomial.leadingCoeff]
rw [deg_fq]
have h1 : Polynomial.coeff fq 2 = 1 := by
simp [fq]
rw [h1]
lemma fz_Irr: Irreducible fz := by
apply IsEisensteinAt.irreducible
pick_goal 5
· apply I
pick_goal 2
· apply I3_prime
pick_goal 3
· have :natDegree fz = 2 := by
unfold fz
compute_degree
norm_num
rw [this]
linarith
· apply fz_ess
· apply Polynomial.Monic.isPrimitive
apply fz_monic
instance : Fact (Irreducible fz) := ⟨ fz_Irr ⟩
lemma fq_Irr : Irreducible fq := by
have hzq:fq=map (algebraMap ℤ ℚ) fz := by
ext n
· by_cases hd : n ≤ 2
· rcases Nat.of_le_succ hd with (h1 | h2)
· rcases Nat.of_le_succ h1 with (h11 | h12)
· simp at *
rw [h11]
simp [fq, fz]
rw [← Rat.coe_int_num 3]
congr
· rw [h12]
simp [fq, fz]
· rw [h2]
simp [fq, fz]
· push_neg at hd
simp [fz, fq]
· by_cases hd: n ≤ 2
· rcases Nat.of_le_succ hd with (h1 | h2)
· rcases Nat.of_le_succ h1 with (h11 | h12)
· simp at *
rw [h11]
simp [fq,fz]
norm_num
show 1 = 1
rfl
· rw [h12]
simp [fq, fz]
· rw[h2]
simp [fq, fz]
· push_neg at hd
simp [fz, fq]
rw [hzq]
apply (Polynomial.Monic.irreducible_iff_irreducible_map_fraction_map fz_monic).mp
apply fz_Irr
@[reducible]
def K := @AdjoinRoot _ _ fq
#check K
example : Polynomial.coeff fz 0 = 3 := by
simp [fz]
#check K
theorem K_ringOfIntegers [hf : Fact (Irreducible fq)] (x : K) :
x ∈ NumberField.ringOfIntegers K ↔ IsIntegral ℤ x :=by
apply NumberField.mem_ringOfIntegers
lemma get_PrimitiveOfQX {f:ℚ[X]} (nzf:f≠(0:ℚ[X])):
∃f_pri:ℤ[X],∃k:ℚ , (((C k)*(map (algebraMap ℤ ℚ) f_pri)=f)∧ (IsPrimitive f_pri∧ natDegree f_pri=natDegree f)∧(Polynomial.Monic f →k= Rat.divInt 1 (leadingCoeff f_pri))) :=by
let f_frange :=f.toFinsupp.frange
let f_commDen:=∏ x in f_frange, x.den
have commDen_nonzero:f_commDen≠0:=by
intro h
apply Finset.prod_eq_zero_iff.mp at h
rcases h with ⟨a,ha⟩
apply a.den_nz ha.2
have hf:(algebraMap ℤ ℚ) 0=0:=by norm_num
have div_commDen:∀ n∈f.support ,∃ m:ℤ ,(algebraMap ℤ ℚ) m=f_commDen*(Polynomial.coeff f n):=by
intro n hn
have h1:Polynomial.coeff f n∈ f_frange:=by
apply Polynomial.mem_frange_iff.mpr
use n
obtain hdvd:= Finset.dvd_prod_of_mem (fun x => x.den) h1
simp only[Dvd.dvd] at *
rcases hdvd with ⟨c,hc ⟩
rw[hc]
use c*(coeff f n).num
simp only [algebraMap_int_eq, map_mul, map_natCast, eq_intCast, Nat.cast_mul]
have : coeff f n * ↑(coeff f n).den = ↑(coeff f n).num := by simp only [Rat.mul_den_eq_num]
rw [← this]
ring_nf
choose m hm using div_commDen
--let (ff:ℕ → ℤ ):= (fun n:ℕ => if n∈support f then m n else 0)
set f_reduction:=({toFinsupp:=⟨
f.support,
fun n:ℕ =>
if h : n∈ f.support then m n h
else 0
,
by
intro a
constructor
· intro ha
dsimp
intro h
split_ifs at h with h1
specialize hm a ha
rw[h] at hm
dsimp at hm
dsimp at commDen_nonzero
push_neg at commDen_nonzero
have :coeff f a≠ 0:=by apply Polynomial.mem_support_iff.mp ha
have :↑f_commDen * coeff f a≠ 0:=by
simp only [ne_eq, mul_eq_zero,this,commDen_nonzero,or_false]
contrapose! commDen_nonzero
rw[Nat.cast_zero.symm] at commDen_nonzero
simp only [Nat.cast_inj] at commDen_nonzero
assumption
rw[Nat.cast_zero.symm] at this
apply this hm.symm
· contradiction
· intro ha
contrapose! ha
split_ifs with h1
rfl
⟩ }:ℤ[X]) with t
set f_pri:=Polynomial.primPart f_reduction with t1
have h_supp: f_pri.support= f.support:=by
rw[t1,primPart] at *
split_ifs with h
· have :f_reduction.support=∅:=by rw[h];apply support_zero
exfalso
apply nzf (support_eq_empty.mp this)
· split_ifs at t1 with ht
contradiction
· ext a
calc
a ∈ support (Classical.choose (_ : C (content f_reduction) ∣ f_reduction))
↔ coeff (Classical.choose (_ : C (content f_reduction) ∣ f_reduction)) a ≠0:=by apply mem_support_iff
_ ↔ coeff f a ≠ 0 :=by sorry
_ ↔ a ∈ support f:= by apply mem_support_iff.symm
--obtain h_pri:=Classical.choose_spec (Classical.choose (hp : C (content f_reduction) ∣ f_reduction))
--obtain h_pri:= (primPart f_reduction)
-- simp only[support_ofFinsupp]
-- ext a
-- by_cases h:a∈ f.support
-- pick_goal 2
-- simp only [mem_support_iff, ne_eq,not_mem_support_iff.mp h]
-- · sorry
-- · sorry
have h_deg: degree f=degree f_pri:=by
apply le_antisymm
· apply degree_mono (superset_of_eq h_supp)
· apply degree_mono (subset_of_eq h_supp)
set k:=mkRat f_reduction.content f_commDen with t2
use f_pri,k
constructor
· ext n
by_cases h:n∈ f.support
pick_goal 2
· rw[coeff_C_mul,coeff_map,not_mem_support_iff.mp h ]
rw[← h_supp] at h
apply not_mem_support_iff.mp at h
rw[h]
simp only [mem_support_iff, ne_eq, dite_not, algebraMap_int_eq, map_zero, mul_zero,
Rat.zero_num]
· sorry
· sorry
-- rw[t2,Polynomial.coeff_C_mul (map (algebraMap ℤ ℚ) f_pri)]
-- simp only [f_pri,primPart,content]
· unfold leadingCoeff natDegree
obtain hd:= congrArg (WithBot.unbot' 0) h_deg.symm
rw[hd] at *
constructor
· constructor
· apply isPrimitive_primPart f_reduction
· exact hd
· intro f_monic
rw[t2,t1,← natDegree]
unfold primPart
split_ifs with h
· rw[h,primPart_zero] at t1
have :f.support=f_reduction.support:=by rfl
rw[h,support_zero] at this
apply support_eq_empty.mp at this
contradiction
· sorry
theorem InZ_of_monic_dvdMinpoly (f :ℤ[X]) (hf:Polynomial.Monic f) (g:ℚ[X]) (hg:Polynomial.Monic g) (h:g ∣map (algebraMap ℤ ℚ) f) : ∃ g₁:ℤ[X],g=map (algebraMap ℤ ℚ) g₁ :=by
by_cases gnz:g=(0:ℚ[X])
· rw[gnz]
use (0:ℤ [X])
simp only [algebraMap_int_eq, Polynomial.map_zero]
· simp only [Dvd.dvd] at h
rcases h with ⟨h,hdvd⟩
by_cases hnz:h=(0:ℚ[X])
· rw[hnz] at hdvd
have h1:map (algebraMap ℤ ℚ) f=(0:ℚ[X]):= by rw[hdvd];simp only [mul_zero]
have h2:map (algebraMap ℤ ℚ) f≠(0:ℚ[X]):=by apply (map_monic_ne_zero hf)
contradiction
obtain ⟨g_pri,kg,⟨g1,⟨⟨ g2,g3⟩,g4⟩⟩⟩:=get_PrimitiveOfQX gnz
obtain ⟨h_pri,kh,⟨h1,⟨⟨ h2,h3⟩,h4⟩⟩⟩:=get_PrimitiveOfQX hnz
obtain g4:= g4 hg
have mapMonic:(algebraMap ℤ ℚ) (Polynomial.leadingCoeff f) ≠ 0:=by
unfold Monic at hf
rw[hf]
simp only [algebraMap_int_eq, map_one, ne_eq, one_ne_zero, not_false_eq_true]
have lead:leadingCoeff (map (algebraMap ℤ ℚ) f) = leadingCoeff h:=by
rw[hdvd]
apply leadingCoeff_monic_mul hg
obtain mapMonic:=leadingCoeff_map_of_leadingCoeff_ne_zero (algebraMap ℤ ℚ) mapMonic
have mapMonic:Monic (map (algebraMap ℤ ℚ) f):=by
unfold Monic at *
rw[mapMonic,hf]
simp only [algebraMap_int_eq, map_one]
have h_monic: Monic h :=by
unfold Monic at *
rw[← lead,mapMonic]
obtain h4:= h4 h_monic
rw[← h1,← g1] at hdvd
have mapz_eq:map (algebraMap ℤ ℚ) ((leadingCoeff g_pri)*(leadingCoeff h_pri)*f-g_pri*h_pri)=0:=by
simp only [Polynomial.map_sub, Polynomial.map_mul, map_int_cast]
rw[hdvd,h4,g4]
ext n
rw[mul_comm]
simp only [ coeff_sub, coeff_zero, Rat.zero_num, Rat.num_eq_zero]
calc
coeff (C (Rat.divInt 1 (leadingCoeff g_pri)) * map (algebraMap ℤ ℚ) g_pri *
(C (Rat.divInt 1 (leadingCoeff h_pri)) * map (algebraMap ℤ ℚ) h_pri) *
(↑(leadingCoeff g_pri) * ↑(leadingCoeff h_pri))) n -
coeff (map (algebraMap ℤ ℚ) g_pri * map (algebraMap ℤ ℚ) h_pri) n
=coeff (map (algebraMap ℤ ℚ) g_pri * map (algebraMap ℤ ℚ) h_pri *
(C (Rat.divInt 1 (leadingCoeff h_pri)) *C (Rat.divInt 1 (leadingCoeff g_pri))) *
(↑(leadingCoeff g_pri) * ↑(leadingCoeff h_pri))) n -
coeff (map (algebraMap ℤ ℚ) g_pri * map (algebraMap ℤ ℚ) h_pri) n:=by ring
_= coeff (map (algebraMap ℤ ℚ) g_pri * map (algebraMap ℤ ℚ) h_pri *
(C ((Rat.divInt 1 (leadingCoeff h_pri))*(Rat.divInt 1 (leadingCoeff g_pri))) ) *
(C (↑(leadingCoeff g_pri) * ↑(leadingCoeff h_pri)))) n -
coeff (map (algebraMap ℤ ℚ) g_pri * map (algebraMap ℤ ℚ) h_pri) n:= by simp only [map_mul, map_intCast]
_= coeff (map (algebraMap ℤ ℚ) g_pri * map (algebraMap ℤ ℚ) h_pri *
(C ((Rat.divInt 1 (leadingCoeff h_pri))*(Rat.divInt 1 (leadingCoeff g_pri))) *
C (↑(leadingCoeff g_pri) * ↑(leadingCoeff h_pri))) ) n -
coeff (map (algebraMap ℤ ℚ) g_pri * map (algebraMap ℤ ℚ) h_pri) n:= by ring
_= coeff (map (algebraMap ℤ ℚ) g_pri * map (algebraMap ℤ ℚ) h_pri *
C (((Rat.divInt 1 (leadingCoeff h_pri))*(Rat.divInt 1 (leadingCoeff g_pri))) *
(↑(leadingCoeff g_pri) * ↑(leadingCoeff h_pri))) ) n -
coeff (map (algebraMap ℤ ℚ) g_pri * map (algebraMap ℤ ℚ) h_pri) n:= by simp only[C_mul]
_= coeff (map (algebraMap ℤ ℚ) g_pri * map (algebraMap ℤ ℚ) h_pri *
C (((Rat.divInt 1 (leadingCoeff h_pri))*(Rat.divInt 1 (leadingCoeff g_pri))) *
↑(leadingCoeff g_pri) * ↑(leadingCoeff h_pri) ) ) n -
coeff (map (algebraMap ℤ ℚ) g_pri * map (algebraMap ℤ ℚ) h_pri) n:= by ring
_= coeff (map (algebraMap ℤ ℚ) g_pri * map (algebraMap ℤ ℚ) h_pri *
C (((Rat.divInt 1 (leadingCoeff h_pri))*(Rat.divInt 1 (leadingCoeff g_pri))) *
↑(leadingCoeff g_pri) * ↑(leadingCoeff h_pri) ) ) n -
coeff (map (algebraMap ℤ ℚ) g_pri * map (algebraMap ℤ ℚ) h_pri) n:= by simp only [algebraMap_int_eq,
map_mul, map_intCast]
_= coeff ( (map (algebraMap ℤ ℚ) g_pri * map (algebraMap ℤ ℚ) h_pri) *
C ((((Rat.divInt 1 (leadingCoeff h_pri))*(Rat.divInt (leadingCoeff h_pri) 1) )) *
(Rat.divInt 1 (leadingCoeff g_pri)) *(Rat.divInt (leadingCoeff g_pri) 1) ) ) n -
coeff (map (algebraMap ℤ ℚ) g_pri * map (algebraMap ℤ ℚ) h_pri) n:= by
have h1:↑(leadingCoeff g_pri)=(Rat.divInt (leadingCoeff g_pri) 1):=by simp only[Rat.divInt_one]
have h2:↑(leadingCoeff h_pri)=(Rat.divInt (leadingCoeff h_pri) 1):=by simp only[Rat.divInt_one]
rw[h1,h2]
ring
_= coeff (map (algebraMap ℤ ℚ) g_pri * map (algebraMap ℤ ℚ) h_pri *
C (1) ) n - coeff (map (algebraMap ℤ ℚ) g_pri * map (algebraMap ℤ ℚ) h_pri) n:= by
have e1 :(leadingCoeff g_pri)≠ 0:=by
intro h
apply leadingCoeff_eq_zero.mp at h
apply g2.ne_zero h
have e2:(leadingCoeff h_pri)≠0:= by
intro h
apply leadingCoeff_eq_zero.mp at h
apply h2.ne_zero h
rw[Rat.divInt_mul_divInt_cancel (e2) 1 _,Rat.divInt_one_one, one_mul,Rat.divInt_mul_divInt_cancel (e1),Rat.divInt_one_one]
_=0:=by simp only [algebraMap_int_eq, map_one, mul_one, sub_self]
· simp only[coeff_zero]
congr
calc
coeff (↑(leadingCoeff g_pri) * ↑(leadingCoeff h_pri) *
(C (Rat.divInt 1 (leadingCoeff g_pri)) * map (algebraMap ℤ ℚ) g_pri *
(C (Rat.divInt 1 (leadingCoeff h_pri)) * map (algebraMap ℤ ℚ) h_pri)) -
map (algebraMap ℤ ℚ) g_pri * map (algebraMap ℤ ℚ) h_pri) n
=coeff (C (Rat.divInt 1 (leadingCoeff g_pri)) * map (algebraMap ℤ ℚ) g_pri *
(C (Rat.divInt 1 (leadingCoeff h_pri)) * map (algebraMap ℤ ℚ) h_pri) *
(↑(leadingCoeff g_pri) * ↑(leadingCoeff h_pri))) n -
coeff (map (algebraMap ℤ ℚ) g_pri * map (algebraMap ℤ ℚ) h_pri) n:= by ring;simp only [ coeff_sub]
_=coeff (map (algebraMap ℤ ℚ) g_pri * map (algebraMap ℤ ℚ) h_pri *
(C (Rat.divInt 1 (leadingCoeff h_pri)) *C (Rat.divInt 1 (leadingCoeff g_pri))) *
(↑(leadingCoeff g_pri) * ↑(leadingCoeff h_pri))) n -
coeff (map (algebraMap ℤ ℚ) g_pri * map (algebraMap ℤ ℚ) h_pri) n:=by ring
_= coeff (map (algebraMap ℤ ℚ) g_pri * map (algebraMap ℤ ℚ) h_pri *
(C ((Rat.divInt 1 (leadingCoeff h_pri))*(Rat.divInt 1 (leadingCoeff g_pri))) ) *
(C (↑(leadingCoeff g_pri) * ↑(leadingCoeff h_pri)))) n -
coeff (map (algebraMap ℤ ℚ) g_pri * map (algebraMap ℤ ℚ) h_pri) n:= by simp only [map_mul, map_intCast]
_= coeff (map (algebraMap ℤ ℚ) g_pri * map (algebraMap ℤ ℚ) h_pri *
(C ((Rat.divInt 1 (leadingCoeff h_pri))*(Rat.divInt 1 (leadingCoeff g_pri))) *
C (↑(leadingCoeff g_pri) * ↑(leadingCoeff h_pri))) ) n -
coeff (map (algebraMap ℤ ℚ) g_pri * map (algebraMap ℤ ℚ) h_pri) n:= by ring
_= coeff (map (algebraMap ℤ ℚ) g_pri * map (algebraMap ℤ ℚ) h_pri *
C (((Rat.divInt 1 (leadingCoeff h_pri))*(Rat.divInt 1 (leadingCoeff g_pri))) *
(↑(leadingCoeff g_pri) * ↑(leadingCoeff h_pri))) ) n -
coeff (map (algebraMap ℤ ℚ) g_pri * map (algebraMap ℤ ℚ) h_pri) n:= by simp only[C_mul]
_= coeff (map (algebraMap ℤ ℚ) g_pri * map (algebraMap ℤ ℚ) h_pri *
C (((Rat.divInt 1 (leadingCoeff h_pri))*(Rat.divInt 1 (leadingCoeff g_pri))) *
↑(leadingCoeff g_pri) * ↑(leadingCoeff h_pri) ) ) n -
coeff (map (algebraMap ℤ ℚ) g_pri * map (algebraMap ℤ ℚ) h_pri) n:= by ring
_= coeff (map (algebraMap ℤ ℚ) g_pri * map (algebraMap ℤ ℚ) h_pri *
C (((Rat.divInt 1 (leadingCoeff h_pri))*(Rat.divInt 1 (leadingCoeff g_pri))) *
↑(leadingCoeff g_pri) * ↑(leadingCoeff h_pri) ) ) n -
coeff (map (algebraMap ℤ ℚ) g_pri * map (algebraMap ℤ ℚ) h_pri) n:= by simp only [algebraMap_int_eq,
map_mul, map_intCast]
_= coeff ( (map (algebraMap ℤ ℚ) g_pri * map (algebraMap ℤ ℚ) h_pri) *
C ((((Rat.divInt 1 (leadingCoeff h_pri))*(Rat.divInt (leadingCoeff h_pri) 1) )) *
(Rat.divInt 1 (leadingCoeff g_pri)) *(Rat.divInt (leadingCoeff g_pri) 1) ) ) n -
coeff (map (algebraMap ℤ ℚ) g_pri * map (algebraMap ℤ ℚ) h_pri) n:= by
have h1:↑(leadingCoeff g_pri)=(Rat.divInt (leadingCoeff g_pri) 1):=by simp only[Rat.divInt_one]
have h2:↑(leadingCoeff h_pri)=(Rat.divInt (leadingCoeff h_pri) 1):=by simp only[Rat.divInt_one]
rw[h1,h2]
ring
_= coeff (map (algebraMap ℤ ℚ) g_pri * map (algebraMap ℤ ℚ) h_pri *
C (1) ) n - coeff (map (algebraMap ℤ ℚ) g_pri * map (algebraMap ℤ ℚ) h_pri) n:= by
have e1 :(leadingCoeff g_pri)≠ 0:=by
intro h
apply leadingCoeff_eq_zero.mp at h
apply g2.ne_zero h
have e2:(leadingCoeff h_pri)≠0:= by
intro h
apply leadingCoeff_eq_zero.mp at h
apply h2.ne_zero h
rw[Rat.divInt_mul_divInt_cancel (e2) 1 _,Rat.divInt_one_one, one_mul,Rat.divInt_mul_divInt_cancel (e1),Rat.divInt_one_one]
_=0:=by simp only [algebraMap_int_eq, map_one, mul_one, sub_self]
have mapInj:Function.Injective ⇑(algebraMap ℤ ℚ) := by apply NoZeroSMulDivisors.algebraMap_injective
have z_eq:(leadingCoeff g_pri)*(leadingCoeff h_pri)*f-g_pri*h_pri=0 :=by apply (Polynomial.map_eq_zero_iff mapInj).mp mapz_eq
have z_eq:(leadingCoeff g_pri)*(leadingCoeff h_pri)*f=g_pri*h_pri:=by apply sub_eq_zero.mp z_eq
have pri:IsPrimitive ((leadingCoeff g_pri) * (leadingCoeff h_pri) * f :ℤ[X]) :=by
rw[z_eq]
apply Polynomial.IsPrimitive.mul g2 h2
obtain isUnit_of_C_dvd:= isPrimitive_iff_isUnit_of_C_dvd.mp pri
have :(C (leadingCoeff g_pri))∣ (leadingCoeff g_pri) * (leadingCoeff h_pri) * f:=by
simp only [Dvd.dvd]
use (leadingCoeff h_pri) * f
simp only [eq_intCast]
ring
specialize isUnit_of_C_dvd (leadingCoeff g_pri) this
apply Int.isUnit_iff.mp at isUnit_of_C_dvd
rcases isUnit_of_C_dvd with (u1|u2)
· use g_pri
rw[← g1,g4,u1,Rat.divInt_one_one]
simp only [map_one, algebraMap_int_eq, one_mul]
· use -g_pri
rw[← g1,g4,u2]
simp only [Rat.divInt_neg_den, Rat.divInt_neg_one_one, map_neg, map_one, algebraMap_int_eq,
neg_mul, one_mul, Polynomial.map_neg]
#check minpoly.dvd
#check IsAdjoinRootMonic.isIntegral_root
#check Polynomial.isCoprime_map
theorem Integral_iff_minpolyInZ (x : K) (algebraic:IsIntegral ℚ x) : IsIntegral ℤ x ↔ ∃ g:ℤ[X], map (algebraMap ℤ ℚ) g= (minpoly ℚ x) :=by
obtain monic:=minpoly.monic algebraic
unfold Monic at monic
constructor
· intro hZ
simp[IsIntegral] at hZ
rcases hZ with ⟨p,⟨ p_monic,hp⟩ ⟩
have h: (minpoly ℚ x) ∣map (algebraMap ℤ ℚ) p:=by sorry
obtain get_g:=InZ_of_monic_dvdMinpoly p p_monic (minpoly ℚ x) monic h
rcases get_g with ⟨g₁,hg1⟩
use g₁
exact hg1.symm
· rintro ⟨g,hg⟩
unfold IsIntegral RingHom.IsIntegralElem
use g
constructor
· have lead:leadingCoeff (map (algebraMap ℤ ℚ) g) =leadingCoeff (minpoly ℚ x):=by congr
rw[monic] at lead
unfold leadingCoeff at lead
have mapInj:Function.Injective ⇑(algebraMap ℤ ℚ) := by apply NoZeroSMulDivisors.algebraMap_injective
obtain eq_supp:=Polynomial.support_map_of_injective g mapInj
have eq_deg: degree (map (algebraMap ℤ ℚ) g)=degree g:=by
apply le_antisymm
· apply degree_mono (subset_of_eq eq_supp)
· apply degree_mono (superset_of_eq eq_supp)
have eq_ndeg:natDegree (map (algebraMap ℤ ℚ) g)=natDegree g:=by
unfold natDegree
obtain hd:= congrArg (WithBot.unbot' 0) eq_deg.symm
rw[hd] at *
rw[eq_ndeg] at lead
obtain eq_coeff:= coeff_map (p:=g) (algebraMap ℤ ℚ)
rw[eq_coeff (natDegree g)] at lead
unfold Monic leadingCoeff
apply mapInj
rw[lead]
simp only [algebraMap_int_eq, map_one]
· obtain root:=minpoly.aeval ℚ x
rw[← hg] at root
rw[← root]
unfold aeval map
sorry
#check 1
-- 证明K中任一元素都可以表示为如下形式（在K中运算）
lemma FormOfmem (x : K) : ∃ a b : ℚ, (AdjoinRoot.mk fq) ((monomial 1) b + C a) = x := by
set K_powbasis := AdjoinRoot.powerBasis non_zero_fq with eq₁
have K_dim : K_powbasis.dim = 2 := by rw [eq₁, AdjoinRoot.powerBasis_dim non_zero_fq, deg_fq]
set K_basis := K_powbasis.basis with eq₂
have type_same : Basis (Fin K_powbasis.dim) ℚ (AdjoinRoot fq) = Basis (Fin 2) ℚ (AdjoinRoot fq) := by rw [K_dim]
rw [K_dim] at K_basis
rw [<-Basis.sum_equivFun K_basis x]
use K_basis.repr x 0, K_basis.repr x 1
simp [Finset.univ, Fintype.elems, List.map]
have zero_base : (⇑K_basis 0) = 1 := by sorry
have one_base : ⇑K_basis 1 = AdjoinRoot.root fq := by sorry
rw [zero_base, one_base]
have mul_x : ∀ (β : ℚ), ((monomial 1) β) = ((monomial 0) β) * Polynomial.X := by
intro t
calc
(monomial 1) t = (monomial (0 + 1) t) := by norm_num
(monomial (0 + 1) t) = ((monomial 0) t) * Polynomial.X := by rw [<-Polynomial.monomial_mul_X 0]
rw [mul_x (K_basis.repr x 1)]
simp
have K_mul_one₀ : ((K_basis.repr x) 0) = ((K_basis.repr x) 0) • 1 := by simp
have K_mul_one₁ : ((K_basis.repr x) 1) = ((K_basis.repr x) 1) • 1 := by simp
rw [K_mul_one₀, K_mul_one₁]
rw [<-AdjoinRoot.smul_of, <-AdjoinRoot.smul_of]
simp
rw [add_comm]
-- 上述定理在ℚ中的形式
lemma K_basis_sum (m : K) : ∃ α β : ℚ, m = α + β * (AdjoinRoot.root fq) := by
have ⟨a, b, hab⟩ := FormOfmem m
use a, b
rw [<-hab]
simp
have mul_x : ∀ (β : ℚ), ((monomial 1) β) = ((monomial 0) β) * Polynomial.X := by
intro t
calc
(monomial 1) t = (monomial (0 + 1) t) := by norm_num
(monomial (0 + 1) t) = ((monomial 0) t) * Polynomial.X := by rw [<-Polynomial.monomial_mul_X 0]
rw [mul_x b]
simp
rw [add_comm]
-- 设置最大反应时长
set_option maxHeartbeats 2000000
--证明若给定K中元素x如上所述的形式，那么x具有可以由该形式中的a和b（既K作为ℚ线性空间时，x的坐标）表示的如下极小多项式
lemma mem_K_minpoly (x : K) : ∃ a b : ℚ, (AdjoinRoot.mk fq) ((monomial 1) b + C a) = x ∧ minpoly ℚ x = (monomial 2 1 - monomial 1 (2 * a) + C (a ^ 2 + 3 * b ^ 2)) := by
have ⟨a, b, hab⟩ := K_basis_sum x
set fx : Polynomial ℚ := (monomial 2 1 - monomial 1 (2 * a) + C (a ^ 2 + 3 * b ^ 2)) with eq_fx
have deg_fx : degree fx = 2 := by rw[eq_fx]; compute_degree; norm_num
use a, b
constructor
· simp
have mul_x : ∀ (β : ℚ), ((monomial 1) β) = ((monomial 0) β) * Polynomial.X := by
intro t
calc
(monomial 1) t = (monomial (0 + 1) t) := by norm_num
(monomial (0 + 1) t) = ((monomial 0) t) * Polynomial.X := by rw [<-Polynomial.monomial_mul_X 0]
rw [mul_x b]
simp
rw [hab]
rw [add_comm]
rw [<-eq_fx]
have fx_deg : natDegree fx = 2 := by
rw [eq_fx]
compute_degree
norm_num
symm
apply minpoly.unique' ℚ x _ _ _
rw [Monic.def]
unfold leadingCoeff
rw [fx_deg]
rw [eq_fx]
simp
repeat' rw[<-Polynomial.monomial_zero_left, pow_two]
repeat' rw [Polynomial.coeff_monomial]
simp
· have nat_to_rat : (1 : ℚ) = (1 : AdjoinRoot fq) := by simp
rw [hab]
simp
ring
rw [<-mul_add]
let is_root := AdjoinRoot.isAdjoinRoot fq
let root_of := IsAdjoinRoot.aeval_root is_root
rw [AdjoinRoot.isAdjoinRoot_root_eq_root fq] at root_of
have root_trans : (aeval (AdjoinRoot.root fq)) fq =
Finset.sum (Finset.range (Polynomial.natDegree fq + 1)) fun (i : ℕ) => Polynomial.coeff fq i • AdjoinRoot.root fq ^ i := by
rw [Polynomial.aeval_eq_sum_range (AdjoinRoot.root fq)]
rw [root_trans] at root_of
rw [deg_fq] at root_of
simp [Finset.sum] at root_of
rw [fq] at root_of
simp at root_of
have one_eq : (3 : ℚ) • (1 : AdjoinRoot fq) = (3 :AdjoinRoot fq) := by rw [<-nat_to_rat, AdjoinRoot.smul_of]; simp
have fq_rw : X ^ 2 + C 3 = fq := by rw [fq]
rw [one_eq] at root_of
simp [fq]
rw [add_comm 3, root_of, mul_zero]
· rw[deg_fx]
intro q h
have two_eq_succ_one : (2 : WithBot ℕ) = Nat.succ 1 := by simp; norm_num
by_contra! h'
have q_deg : natDegree q ≤ 1 := by
rw [degree_eq_natDegree _, two_eq_succ_one] at h
norm_cast at h
rw [Nat.lt_succ] at h
exact h
exact h'.1
obtain ⟨c1, c0, rfl⟩ := exists_eq_X_add_C_of_natDegree_le_one q_deg
have deg_ff : natDegree (C c1 * (C a + C b * X) + C c0) ≤ 1 := by compute_degree
have deg_lt : Polynomial.natDegree (C c1 * (C a + C b * X) + C c0) < Polynomial.natDegree fq := by
rw [deg_fq]
linarith [deg_ff]
have ⟨h₁, h₂⟩ := h'
rw [hab] at h₂
simp at h₂
rw [<-AdjoinRoot.mk_C, <-AdjoinRoot.mk_C, <-AdjoinRoot.mk_C, <-AdjoinRoot.mk_C, <-AdjoinRoot.mk_X] at h₂
rw [<-map_mul (AdjoinRoot.mk fq) (C b) X, <-map_add (AdjoinRoot.mk fq) (C a) (C b * X), <-map_mul (AdjoinRoot.mk fq) (C c1) (C a + C b * X), <-map_add (AdjoinRoot.mk fq) (C c1 * (C a + C b * X)) (C c0)] at h₂
rw [AdjoinRoot.mk_eq_zero] at h₂
have ne_zero : C c1 * (C a + C b * X) + C c0 ≠ 0 := by sorry -- 当x=0时，极小多项式不一样
have ne_dvd := Polynomial.not_dvd_of_natDegree_lt ne_zero deg_lt
contradiction
-- 由a+b√-3为（代数）整数，可推出极小多项式的系数都是整数，即有以下关系式
def a_b_int (a b : ℚ) := ∃ n₁ n₂ : ℤ, (2 * a = n₁) ∧ (a ^ 2 + 3 * b ^ 2 = n₂)
-- 将前述a，b具有的所有性质和上述关系式打包为如下定理
lemma a_b_propeties (x : K) (h : ∀ n : ℕ ,∃ m : ℤ , (Polynomial.coeff (minpoly ℚ x) n) = m) : ∃ a b : ℚ, (AdjoinRoot.mk fq) ((monomial 1) b + C a) = x ∧ a_b_int a b := by
have ⟨a, b, hab⟩ := mem_K_minpoly x
have ⟨n₀, nh₀⟩ := h 0
have ⟨n₁, nh₁⟩ := h 1
rw [hab.2] at nh₀ nh₁
simp at nh₀ nh₁
use a, b
constructor
· exact hab.1
repeat' rw [<-Polynomial.monomial_zero_left] at nh₁
repeat' rw [pow_two] at nh₁
repeat' rw [Polynomial.coeff_monomial] at nh₁
simp at nh₁
have co₀ : coeff (C a ^ 2) 0 + 3 * coeff (C b ^ 2) 0 = a ^ 2 + 3 * b ^ 2 := by rw [pow_two, pow_two]; simp; ring
rw [co₀] at nh₀
use -n₁, n₀
constructor
· simp
rw [<-nh₁]
simp
rw [<-nh₀]
-- 接下来开始推导a和b由以上关系式导出的性质
-- 由以上关系式推出-3*(2*b)^2是整数
lemma two_b_sq_mul_neg_three_in_z {a b : ℚ} (h : a_b_int a b) : ∃ n : ℤ, 3 * (2 * b) ^ 2 = n := by
have ⟨n₁, n₂, h₁, h₂⟩ := h
have h' : (2 * a) ^ 2 + 3 * (2 * b) ^ 2 = 4 * n₂ := by
rw [mul_pow, mul_pow, <-h₂]
simp only [<-mul_assoc, mul_add]
norm_num
use (- n₁ ^ 2 + 4 * n₂)
simp
rw [<-h', <-h₁]
simp
-- 设2*b（有理数）为q，写成分子（整数）除分母（自然数）的形式（由定义）
-- 再将分母乘至等式另一侧，得到在ℤ中关于分子和分母的等式
lemma den_mul_right {q : ℚ} (h : ∃ n : ℤ, 3 * q ^ 2 = n) : ∃ n : ℤ, 3 * q.num ^ 2 = n * ↑q.den ^ 2 := by
rw [<-Rat.num_div_den q, div_pow, mul_div] at h
have qden_nz : (↑q.den : ℚ) ≠ (↑(0 : ℕ) : ℚ) := by norm_cast; exact q.den_nz
have q_pow_nz : (↑q.den : ℚ) ^ (2 : ℤ) ≠ (0 : ℤ) := by norm_cast; apply pow_ne_zero 2 q.den_nz
have ⟨n, hn⟩ := h
use n
apply (div_eq_iff q_pow_nz).1 at hn
norm_cast at *
-- 通过分析整除关系，得出上述等式中的n可被3整除
lemma n_of_fac_three {q : ℚ} {n : ℤ} : (3 * q.num ^ 2 = n * ↑q.den ^ 2) → 3 ∣ n := by
intro nh
have int_to_nat : (3 : ℕ) = (3 : ℤ) := by norm_num -- 自然数的3（通过强制类型转换）等于整数的3
have three_dvd_left : ((3 : ℕ) : ℤ) ∣ (3 * q.num ^ 2) := by rw [int_to_nat]; apply dvd_mul_right
rw [nh] at three_dvd_left
have three_pr : Nat.Prime 3 := by apply Nat.prime_three
rcases Int.Prime.dvd_mul' three_pr three_dvd_left with h' | h'
· rw [int_to_nat] at h'
exact h'
by_contra -- 由条件即可得出矛盾，无需假设原结论为假
rw [pow_two] at h'
rcases Int.Prime.dvd_mul' three_pr h' with h'' | h'' <;> (
-- 括号后进行分情况讨论，但是两个情况相同
rw [dvd_def] at h''
have ⟨c, ch⟩ :=h''
---- 代入由整除引入的等式，化简 ----
rw [ch, mul_pow, <-int_to_nat] at nh
have nh' : ↑3 * q.num ^ 2 = ↑3 * (↑3 * n * c ^ 2) := by
repeat' rw [<-int_to_nat]
calc
_ = n * (↑3 ^ 2 * c ^ 2) := by rw [nh]; rfl
_ = ↑3 * (↑3 * n * c ^ 2) := by ring
have nh'' : q.num ^ 2 = 3 * n * c ^ 2 := by apply (Int.eq_of_mul_eq_mul_left _ nh'); norm_num
---- 化简结束 ----
symm at nh''
have three_dvd_left' : ((3 : ℕ) : ℤ) ∣ (3 * n * c ^ 2) := by rw [int_to_nat, mul_assoc]; apply dvd_mul_right
rw [nh''] at three_dvd_left'
rcases Int.Prime.dvd_mul' three_pr three_dvd_left' with h''' | h''' <;> (
-- 括号后进行分情况讨论，但是两个情况相同
simp at h'''
rw [<-dvd_def] at h''
apply Int.ofNat_dvd_left.1 at h'''
apply Int.ofNat_dvd_left.1 at h''
-- 接下来通过3分别整除分子和分母，得到矛盾
simp at h''
apply (Nat.dvd_gcd h''') at h''
have cop : Nat.Coprime (Int.natAbs q.num) q.den := q.reduced
rw [cop] at h''
contradiction
))
--将n表示成n'和3的乘积，等式两边约去3，接着证明分母整除分子，再有分子分母互质知分母为1，因此q是整数
lemma q_in_z {q : ℚ} : (∃ n : ℤ, 3 * q.num ^ 2 = n * ↑q.den ^ 2) → ∃ n : ℤ, q = ↑n := by
rintro ⟨n, nh⟩
have n_fac_three : 3 ∣ n := n_of_fac_three nh
have ⟨c, ch⟩ := n_fac_three
rw [ch] at nh
rw [mul_assoc] at nh
have nh' : q.num ^ 2 = c * ↑q.den ^ 2 := by apply (Int.eq_of_mul_eq_mul_left _ nh); norm_num
have sq_dvd : (q.den : ℤ) ^ 2∣q.num ^ 2 := by rw [nh']; apply dvd_mul_left
have two_gt_zero : 0 < 2 := by norm_num
have den_dvd_num : (q.den : ℤ) ∣ q.num := by apply (Int.pow_dvd_pow_iff two_gt_zero).1; exact sq_dvd
apply Int.ofNat_dvd_left.1 at den_dvd_num
have den_dvd_self : q.den ∣ q.den := by rfl
apply (Nat.dvd_gcd den_dvd_num) at den_dvd_self
have cop : Nat.Coprime (Int.natAbs q.num) q.den := q.reduced
rw [cop] at den_dvd_self
rw [Nat.dvd_one] at den_dvd_self
use q.num
rw [<-Rat.num_div_den q]
rw [den_dvd_self]
simp
--还原q为2 * b，既有2 * b是整数
lemma two_b_in_z {a b : ℚ} (h : a_b_int a b) : ∃ n : ℤ, 2 * b = n := by
have ⟨n, hn⟩ := (q_in_z (den_mul_right (two_b_sq_mul_neg_three_in_z h)))
use n
-- 知2 * a和2 * b都是整数，通过关系式2得到2 * a和2 * b对模4同余
lemma asque_eq_bsqu {a b :ℚ} (h : a_b_int a b) :
(∃ n₁ n₂ : ℤ , 2 * a = n₁ ∧ 2 * b = n₂ ∧ ∃ n : ℤ, n₁ * n₁ - n₂ * n₂ = 4 * n) := by
-- 把2 * a和2 * b分别化为n₁和n₂
have ⟨n₁, n, hn₁, hn⟩ := h
have hn₁ := hn₁
have ⟨n₂, hn₂⟩ := two_b_in_z h
use n₁, n₂
constructor
· exact hn₁
constructor
· exact hn₂
have h' : (2 * a) ^ 2 + 3 * (2 * b) ^ 2 = 4 * n := by
rw [mul_pow, mul_pow, <-hn]
simp only [<-mul_assoc, mul_add]
norm_num
rw [hn₁, hn₂, pow_two, pow_two] at h'
norm_cast at h'
use n - n₂ * n₂
rw [mul_sub, <-h']
ring
#check AdjoinRoot.aeval_eq
-- 通过2 * a和2 * b对模4同余，得知2 * a - 2 * b是偶数
-- 在本定理中，用a代表2 * a，用b代表2 * b
lemma quadratic_four_mod_eq {a b : ℤ} (asque_eq_bsqu: ∃ n : ℤ , a * a - b * b = 4 * n) :
Even (a - b) := by
obtain ha := Int.even_or_odd a
have ⟨n, hn⟩ := asque_eq_bsqu
have hn' : b * b = a * a - 4 * n := by rw [← hn]; ring
have eq : Even (4 : ℤ) := by
apply Int.even_iff.2
simp
norm_num
have h4 : Even (4 * n) := Int.even_mul.mpr (Or.inl eq)
have pow_mul : b * b = b ^ 2 := by ring
have hne : 2 ≠ 0 := by norm_num
rcases ha with haeven | haodd
· have ha' : Even (a * a) := Int.even_mul.mpr (Or.inl haeven)
have hb : Even (b * b) := by
rw[hn']
apply Int.even_sub.2
tauto
have hb' : Even b := by
rw[pow_mul] at hb
apply (Int.even_pow' hne).1
assumption
have : (Even a ↔ Even b) := by tauto
have g1 : Even (a - b) := Int.even_sub.2 this
exact g1
· have ha' : Odd (a * a) := by
apply Int.odd_mul.2
exact ⟨haodd , haodd⟩
have hb : Odd (b * b) := by
rw[hn']
apply Int.odd_sub.2
tauto
have hb' : Odd b := by
rw[pow_mul] at hb
apply (Int.odd_pow' hne).1
assumption
have :(Odd a ↔ Odd b) := by tauto
have g1 : Even (a - b) := Int.even_sub'.2 this
exact g1
lemma pre [hf : Fact (Irreducible fq)] (x : K)
(hab: ∃ (a b :ℤ ), AdjoinRoot.mk fq (monomial 1 (b/2 :ℚ) + C (a+b/2:ℚ)) = x ):
(∀ n:ℕ ,∃ m : ℤ , (Polynomial.coeff (minpoly ℚ x) n) = m):= by
have ⟨ a , b , hab' ⟩ := hab
by_cases b_neg_zero : b = 0
· have :minpoly ℚ x = map (algebraMap ℤ ℚ) ( monomial 1 1 - C a ) := by sorry
sorry
· have :minpoly ℚ x = map (algebraMap ℤ ℚ) ( monomial 2 1 - monomial 1 ( 2 * a + b ) + C ( a ^ 2 + a * b + b ^ 2) ) := by
let p := map (algebraMap ℤ ℚ) (monomial 2 1 - monomial 1 (2 * a + b) + C ( a ^ 2 + a * b + b ^ 2) )
have deg_p : Polynomial.degree p = 2 := by
sorry
have hm : Polynomial.Monic p := by
simp only[Monic,Polynomial.leadingCoeff]
have h1:Polynomial.coeff p 2 = 1 := by
simp [p]
sorry
sorry
have hp : (Polynomial.aeval x) p = 0 := by
rw[← hab']
have hpoly : aeval ( ( C (↑b / 2 : ℚ) ) * X+ C (↑a + ↑b / 2 : ℚ ) ) p = (C ( ↑b ^ 2 /4 : ℚ ) ) * fq := by
rw[ fq ]
sorry
sorry
have hl : ∀ (q : Polynomial ℚ), Polynomial.degree q < Polynomial.degree p →
q = 0 ∨ (Polynomial.aeval x) q ≠ 0 := by
rw[deg_p]
intro q h
have : natDegree q ≤ 1 := sorry
obtain ⟨c1, c0, rfl⟩ := exists_eq_X_add_C_of_natDegree_le_one this
by_contra! h
subst hab'
simp at h
have : AdjoinRoot.mk fq ((c1 • (monomial 1 (↑b / 2 : ℚ) + C (↑a + ↑b / 2 : ℚ))) + C c0 : ℚ[X]) = 0
· rw [map_add, ← AdjoinRoot.smul_mk, map_add, Algebra.smul_def]
convert h.2
norm_cast
absurd this
apply AdjoinRoot.mk_ne_zero_of_degree_lt
· apply fq_monic
· intro c1_c0_zero
have c1_eq_zero : c1 * b / 2 = 0 := by sorry
have c1_c0_eq_zero : c1 * ( a + b / 2) + c0 = 0 := by sorry
have c1_eq_zero' : c1 = 0 := by sorry
have c0_eq_zero : c0 = 0 := by sorry
--和h.1 矛盾
sorry
· suffices : degree (c1 • ((monomial 1) (↑b / 2 : ℚ) + C (↑a + ↑b / 2 : ℚ)) + C c0) ≤ 1
· sorry
compute_degree
obtain ans := minpoly.unique' ℚ x hm hp hl
symm
exact ans
rw[this]
intro n
cases' n with d1
· use a ^ 2 + a * b + b ^ 2
--simp
sorry
· cases' d1 with d2
· use -(2 * a + b)
--simp
sorry
· cases' d2 with d3
· use 1
--simp
sorry
· sorry
theorem Integral_Of_Form_iff [hf : Fact (Irreducible fq)] (x : K) :
(∀ n : ℕ ,∃ m : ℤ , (Polynomial.coeff (minpoly ℚ x) n) = m) ↔
∃ (a b : ℤ ), AdjoinRoot.mk fq (monomial 1 (b / 2 : ℚ) + C (a + b / 2 : ℚ)) = x := by
constructor
· intro h
have ⟨a, b, Adjoin_Root, a_b_int'⟩ := a_b_propeties x h
have ⟨_, _⟩ := two_b_in_z a_b_int'
have ⟨n₁', n₂', ah, bh, asque_eq_bsqu'⟩ := asque_eq_bsqu a_b_int'
have ⟨n'', nh''⟩ := quadratic_four_mod_eq asque_eq_bsqu'
use n'', n₂'
have new_nh'' : 2 * (a - b) = 2 * ↑n'' := by
symm; rw [two_mul]
norm_cast; rw [<-nh'']; simp
rw [<-ah, <-bh]; ring
simp at new_nh''
have rw_n : ((monomial 1) (n₂' / 2 : ℚ)) + C (↑n'' + ↑n₂' / 2 : ℚ) = ((monomial 1) b) + C a := by
rw [<-bh, <-new_nh'']
ring
rw [rw_n]
rw [Adjoin_Root]
· apply pre
theorem MinpolyOfmem :∀ a b: ℚ, (minpoly ℚ (AdjoinRoot.mk fq ((C a : ℚ[X]) + (C b * (X : ℚ[X])) )))=(X^2 - monomial 1 (2*a) + C (a^2+3*b^2):ℚ[X]) :=by sorry
theorem Intergral_iff_minpoly (x : K) (algebraic:IsIntegral ℚ x) : IsIntegral ℤ x ↔ ∃(a b:ℤ),(((monomial 2 1) - (monomial 1 (2*a:ℚ)) + C (a^2 + 3*b^2 :ℚ)):ℚ[X])=(minpoly ℚ x):=by
sorry
lemma memInK_isAlgebraic :∀ x : K, IsIntegral ℚ x :=by sorry
theorem Integral_Of_Form [hf : Fact (Irreducible fq)] (x : K) : IsIntegral ℤ x ↔ ∃ (a b :ℤ ), AdjoinRoot.mk fq (monomial 1 (b/2 :ℚ) + C (a+b/2:ℚ)) = x :=by sorry
theorem main_thm_ringOfIntegers [f_Irr : Fact (Irreducible fq)] (x : K) :
x ∈ NumberField.ringOfIntegers K ↔ ∃ (a b :ℤ ), AdjoinRoot.mk fq (monomial 1 (b/2 :ℚ) + C (a+b/2:ℚ)) = x :=by
obtain algebraic:= memInK_isAlgebraic x
constructor
· intro memOf_RingofIntegral
obtain IsIntegral:=(K_ringOfIntegers x).mp memOf_RingofIntegral
obtain minpolyInZ:=(Integral_iff_minpolyInZ x algebraic).mp IsIntegral
rcases minpolyInZ with ⟨minZ,hz_minpolyInQ⟩
have IntForm:∃ (a b : ℤ ), AdjoinRoot.mk fq (monomial 1 (b / 2 : ℚ) + C (a + b / 2 : ℚ)) = x:=by
apply (Integral_Of_Form_iff x).mp
intro n
use coeff minZ n
rw[← hz_minpolyInQ]
obtain h:=(coeff_map (algebraMap ℤ ℚ) n (p:=minZ))
rw[h]
rfl
exact IntForm
· intro IntForm
obtain minploy_coeff:=(Integral_Of_Form_iff x).mpr IntForm
have getMinpolyInZ: ∃ g:ℤ[X], map (algebraMap ℤ ℚ) g= (minpoly ℚ x) := by sorry
rcases getMinpolyInZ with ⟨minZ,hz_minpolyInQ⟩
obtain IsIntegral : IsIntegral ℤ x :=by
apply (Integral_iff_minpolyInZ x algebraic).mpr
use minZ
apply (K_ringOfIntegers x).mp IsIntegral
@[ext]
structure eisensteinInt where
re : ℤ
im : ℤ
namespace eisensteinInt
instance : Zero eisensteinInt :=