add

Author: tb65536

Mathlib/Algebra/Polynomial/Splits.lean

@@ -569,26 +569,34 @@ end
 
 section
 
-variable {A B : Type*} [CommRing R] [Field A] [Algebra R A]
+variable {A B : Type*} [CommRing R] [CommRing A] [IsDomain A] [Algebra R A]
   [CommRing B] [IsDomain B] [Algebra R B] {f : R[X]}
 
-theorem Splits.map_aroots_algebraMap [Algebra A B] [IsScalarTower R A B]
-    (hf : (f.map (algebraMap R A)).Splits) :
-    (f.aroots A).map (algebraMap A B) = f.aroots B := by
-  rw [← aroots_map B A, aroots, aroots, hf.roots_map]
-
-theorem Splits.image_rootSet (hf : (f.map (algebraMap R A)).Splits)
+theorem Splits.image_rootSet [IsSimpleRing A] (hf : (f.map (algebraMap R A)).Splits)
     (g : A →ₐ[R] B) : g '' f.rootSet A = f.rootSet B := by
   classical
   rw [rootSet, ← Finset.coe_image, ← Multiset.toFinset_map, ← g.coe_toRingHom,
-    ← hf.roots_map, map_map, g.comp_algebraMap, ← rootSet]
+    ← hf.roots_map_of_injective, map_map, g.comp_algebraMap, ← rootSet]
+  exact g.injective
 
-theorem Splits.adjoin_rootSet_eq_range
+theorem Splits.adjoin_rootSet_eq_range [IsSimpleRing A]
     (hf : (f.map (algebraMap R A)).Splits) (g : A →ₐ[R] B) :
     Algebra.adjoin R (f.rootSet B) = g.range ↔ Algebra.adjoin R (f.rootSet A) = ⊤ := by
   rw [← hf.image_rootSet g, Algebra.adjoin_image, ← Algebra.map_top]
   exact (Subalgebra.map_injective g.injective).eq_iff
 
+variable [Algebra A B] [FaithfulSMul A B] [IsScalarTower R A B]
+
+theorem Splits.map_aroots_algebraMap (hf : (f.map (algebraMap R A)).Splits) :
+    (f.aroots A).map (algebraMap A B) = f.aroots B := by
+  rw [← aroots_map B A, aroots, aroots,
+    hf.roots_map_of_injective (FaithfulSMul.algebraMap_injective A B)]
+
+theorem Splits.image_rootSet_algebraMap (hf : (f.map (algebraMap R A)).Splits) :
+    (algebraMap A B) '' f.rootSet A = f.rootSet B := by
+  classical
+  rw [rootSet, ← Finset.coe_image, ← Multiset.toFinset_map, hf.map_aroots_algebraMap, ← rootSet]
+
 end
 
 variable [Field R] {f g : R[X]}

Mathlib/RingTheory/Polynomial/Morse.lean

@@ -49,7 +49,8 @@ noncomputable def rootsEquivRoots' {F : Type*} [Field F] (p : F[X])
 theorem smul_rootsEquivRoots' {F : Type*} [Field F] (p : F[X])
     (E E' : Type*) [Field E] [Field E'] [Algebra F E] [Algebra F E']
     [Fact (map (algebraMap F E) p).Splits] [Fact (map (algebraMap F E') p).Splits]
-    {g : p.Gal} (x : p.rootSet E) : g • rootsEquivRoots' p E E' x = rootsEquivRoots' p E E' (g • x) := by
+    (g : p.Gal) (x : p.rootSet E) :
+    g • rootsEquivRoots' p E E' x = rootsEquivRoots' p E E' (g • x) := by
   simp [rootsEquivRoots', smul_def]
 
 end Polynomial.Gal
@@ -169,36 +170,65 @@ open scoped Pointwise
 
 #check IsPrimitive.irreducible_iff_irreducible_map_fraction_map
 
-theorem tada' (f₀ : ℤ[X]) (hf₀ : Irreducible f₀) (hf₉' : f₀.Monic)
+theorem tada' (f₀ : ℤ[X]) (hf₀ : Irreducible f₀) (hf₀' : f₀.Monic)
     (h : ∀ (F : Type) [Field F], (f₀.map (algebraMap ℤ F)).Splits →
       f₀.natDegree ≤ (f₀.rootSet F).ncard + 1) :
     Function.Bijective (Gal.galActionHom (f₀.map (algebraMap ℤ ℚ)) ℂ) := by
   classical
   let f : ℚ[X] := f₀.map (algebraMap ℤ ℚ)
-  have hf' : Irreducible f := hf₉'.irreducible_iff_irreducible_map_fraction_map.mp hf₀
+  have hf : Irreducible f := hf₀'.irreducible_iff_irreducible_map_fraction_map.mp hf₀
+  have hf' : Monic f := hf₀'.map (algebraMap ℤ ℚ)
   let K := f.SplittingField
   have : Fact (f.map (algebraMap ℚ K)).Splits := ⟨SplittingField.splits f⟩
   have : NumberField K := by constructor
   have : IsGalois ℚ K :=
   { to_isSeparable := inferInstance
-    to_normal := Polynomial.SplittingField.instNormal f }
+    to_normal := SplittingField.instNormal f }
   let R := 𝓞 K
+  let := Ring.toIntAlgebra R
+  have foo := @aeval_algebraMap_apply (R := ℤ) (A := R) K _ _ _ _ _ _ (IsScalarTower.of_algebraMap_eq' rfl)
   let G := f.Gal
-  have := Gal.galAction_isPretransitive f ℂ hf'
-  let e : f₀.rootSet R ≃ f.rootSet ℂ := by
-    let e₀ : f₀.rootSet R ≃ f.rootSet K := by
-      sorry
-    let e1 : f.rootSet K ≃ f.rootSet ℂ := Polynomial.Gal.rootsEquivRoots f ℂ
+  have := Gal.galAction_isPretransitive f ℂ hf
+  have : Set.BijOn v (f₀.rootSet R) (f.rootSet K) := by
+    rw [rootSet, rootSet, aroots_map, ← rootSet, ← rootSet] -- rootSet_map lemma
+    have := Polynomial.Splits.image_rootSet_algebraMap (f := f₀) (A := R) (B := K) ?_ v
+
+    rw [← Polynomial.Splits.image_rootSet (f := f₀) ?_ v] -- switch to algebraMap version
+    suffices Set.InjOn (algebraMap R K) ∧
+    refine ⟨?_, ?_⟩
+    sorry
+  have hφ : Set.MapsTo (algebraMap R K) (f₀.rootSet R) (f.rootSet K) := by
+    intro x hx
+    rw [hf'.mem_rootSet, aeval_map_algebraMap, foo, aeval_eq_zero_of_mem_rootSet hx, map_zero]
+  let φ : f₀.rootSet R → f.rootSet K := hφ.restrict
+  have hφ2 : Function.Bijective (hφ.restrict) := by
+    rw [Function.Bijective, hφ.restrict_inj, hφ.restrict_surjective_iff]
+    refine ⟨RingOfIntegers.coe_injective.injOn, ?_⟩
+    intro x hx
+    have h0 : aeval x f₀ = 0 := by
+      rwa [mem_rootSet, aeval_map_algebraMap, and_iff_right hf.ne_zero] at hx
+    let y : integralClosure ℤ K := ⟨x, f₀, hf₀', h0⟩
+    refine ⟨y, ?_, rfl⟩
+    rw [mem_rootSet, and_iff_right hf₀.ne_zero]
+    simpa using (foo y f₀).symm.trans h0
+  let e₀ := Equiv.ofBijective hφ.restrict hφ2
+  let e₁ : f₀.rootSet R ≃ f.rootSet K := by
 
     sorry
-  have he (g : G) (x : f₀.rootSet R) : e (g • x) = g • e x := by
+  have he₁ (g : G) (x : f₀.rootSet R) : e₁ (g • x) = g • e₁ x := by
     sorry
+  let e₂ : f.rootSet K ≃ f.rootSet ℂ := Gal.rootsEquivRoots' f K ℂ
+  have he₂ (g : G) (x : f.rootSet K) : e₂ (g • x) = g • e₂ x :=
+    (Gal.smul_rootsEquivRoots' f K ℂ g x).symm
+  let e : f₀.rootSet R ≃ f.rootSet ℂ := e₁.trans e₂
+  have he (g : G) (x : f₀.rootSet R) : e (g • x) = g • e x := by
+    simp [e, he₁, he₂]
   have : MulAction.IsPretransitive G (f₀.rootSet R) := by
     refine ⟨fun x y ↦ ?_⟩
     obtain ⟨g, hg⟩ := MulAction.exists_smul_eq f.Gal (e x) (e y)
     exact ⟨g, e.injective ((he g x).trans hg)⟩
   suffices Function.Surjective (MulAction.toPermHom G (f₀.rootSet R)) by
-    use Polynomial.Gal.galActionHom_injective (f₀.map (algebraMap ℤ ℚ)) ℂ
+    use Gal.galActionHom_injective (f₀.map (algebraMap ℤ ℚ)) ℂ
     intro φ
     obtain ⟨g, hg⟩ := this (e.permCongr.symm φ)
     use g