temp

Author: tb65536

Mathlib/RepresentationTheory/Rep/Basic.lean

@@ -206,7 +206,7 @@ lemma hom_surjective :
     Function.Surjective (Hom.hom : (A ⟶ B) → (A.ρ.IntertwiningMap B.ρ)) :=
   hom_bijective.surjective
 
-/-- The morphisms between two objects in `Rep k G` has an equivalence to the intertwining maps
+/- - Themorphisms between two objects in `Rep k G` has an equivalence to the intertwining maps
   between their underlying representations. -/
 @[simps]
 def homEquiv : (A ⟶ B) ≃ (A.ρ.IntertwiningMap B.ρ) where

Mathlib/RingTheory/Polynomial/Morse.lean

@@ -117,33 +117,22 @@ open IsGaloisGroup
 
 open NumberField
 
-open Ideal IsGaloisGroup Pointwise in
-/-- A Galois group over `ℤ` is generated by its inertia subgroups. -/
-theorem NumberField.supr_inertia_eq_top (S G : Type*) [CommRing S] [Module.Finite ℤ S]
+-- #40955
+theorem NumberField.supr_inertia_primeSpectrum_eq_top (S G : Type*) [CommRing S] [Module.Finite ℤ S]
     [IsDomain S] [FaithfulSMul ℤ S] [Group G] [MulSemiringAction G S] [IsGaloisGroup G ℤ S] :
     ⨆ m : PrimeSpectrum S, m.asIdeal.toAddSubgroup.inertia G = ⊤ := by
   sorry
 
-theorem NumberField.supr_inertia_eq_top' (S G : Type*) [CommRing S] [Module.Finite ℤ S]
+theorem NumberField.supr_inertia_maximalSpectrum_eq_top (S G : Type*) [CommRing S] [Module.Finite ℤ S]
     [IsDomain S] [FaithfulSMul ℤ S] [Group G] [MulSemiringAction G S] [IsGaloisGroup G ℤ S] :
     ⨆ m : MaximalSpectrum S, m.asIdeal.toAddSubgroup.inertia G = ⊤ := by
-  rw [eq_top_iff, ← NumberField.supr_inertia_eq_top S G, iSup_le_iff]
+  rw [eq_top_iff, ← NumberField.supr_inertia_primeSpectrum_eq_top S G, iSup_le_iff]
   intro p
   obtain ⟨m, hm, hpm⟩ := p.1.exists_le_maximal p.2.ne_top
   intro x hx
   apply Subgroup.mem_iSup_of_mem ⟨m, hm⟩
   exact fun x ↦ hpm (hx x)
 
-theorem NumberField.supr_inertia_eq_top'' (K : Type*) [Field K] [NumberField K]
-    (G : Type*) [Group G] [MulSemiringAction G K] [IsGaloisGroup G ℚ K] :
-    ⨆ m : PrimeSpectrum (𝓞 K), m.asIdeal.toAddSubgroup.inertia G = ⊤ := by
-  exact NumberField.supr_inertia_eq_top (𝓞 K) G
-
-theorem NumberField.supr_inertia_eq_top''' (K : Type*) [Field K] [NumberField K]
-    (G : Type*) [Group G] [MulSemiringAction G K] [IsGaloisGroup G ℚ K] :
-    ⨆ m : MaximalSpectrum (𝓞 K), m.asIdeal.toAddSubgroup.inertia G = ⊤ := by
-  exact NumberField.supr_inertia_eq_top' (𝓞 K) G
-
 end ram
 
 end Inertia
@@ -168,8 +157,6 @@ 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
-  -- by_cases nd : f₀.natDegree = 0
-  -- · sorry
   classical
   let f : ℚ[X] := f₀.map (algebraMap ℤ ℚ)
   have hf' : Irreducible f := hf₉'.irreducible_iff_irreducible_map_fraction_map.mp hf₀
@@ -183,20 +170,34 @@ theorem tada' (f₀ : ℤ[X]) (hf₀ : Irreducible f₀) (hf₉' : f₀.Monic)
   let G := f.Gal
   have h_transitive := 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 := Polynomial.Gal.rootsEquivRoots f ℂ
+
     sorry
-  have he (g : G) (x : f₀.rootSet R) : g • e x = e (g • x) := by
+  have he (g : G) (x : f₀.rootSet R) : e (g • x) = g • e x := by
     sorry
-  have : MulAction.IsPretransitive G (f₀.rootSet R) := sorry
-  let e := Polynomial.Gal.rootsEquivRoots f ℂ
+  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 ℤ ℚ)) ℂ
-    sorry
+    change Function.Surjective (MulAction.toPermHom G (f.rootSet ℂ))
+    intro φ
+    obtain ⟨g, hg⟩ := this (e.permCongr.symm φ)
+    use g
+    ext x
+    replace hg := Equiv.Perm.ext_iff.mp hg (e.symm x)
+    apply_fun e at hg
+    simp [he] at hg
+    simpa
   have h1 : (f₀.map (algebraMap ℤ R)).Splits := by
     -- might require monic
     sorry
   have : IsGaloisGroup G ℚ K := IsGaloisGroup.of_isGalois ℚ K
   refine h1.surjective_toPermHom_of_iSup_inertia_eq_top (fun m ↦ ?_)
-    (NumberField.supr_inertia_eq_top' (𝓞 K) G)
+    (NumberField.supr_inertia_maximalSpectrum_eq_top (𝓞 K) G)
   let := Ideal.Quotient.field m.asIdeal
   refine le_trans (f₀.ncard_rootSet_le R) (h (R ⧸ m.asIdeal) ?_)
   rw [IsScalarTower.algebraMap_eq ℤ R, ← Polynomial.map_map]