SeparableRootsDownstairs.lean

theorem exists_moved_separableKummerCharacter_of_finite_primePowerRoots
    (K : Type*) [Field K] {p : ℕ} [NeZero (p : K)] (hp : p.Prime)
    (hfinite : Set.Finite {ξ : K | ∃ m : ℕ, ξ ^ (p ^ m) = 1})
    (ζ : Kˣ) (hζ : IsPrimitiveRoot ζ p)
    (τ : K ≃+* K)
    (hτ : ∀ ξ : K, (∃ m : ℕ, ξ ^ (p ^ m) = 1) → τ ξ = ξ)
    (α : Kˣ) (hα : Units.map τ.toMonoidHom α = ζ * α) :
    ∃ s : ℕ, 1 ≤ s ∧ (primitiveRoots (p ^ s) K).Nonempty ∧
      (∀ m : ℕ, (primitiveRoots (p ^ m) K).Nonempty → m ≤ s) ∧
      ∃ χ : Field.absoluteGaloisGroup K →ₜ* Multiplicative (ZMod (p ^ s)),
        ∃ σ : Field.absoluteGaloisGroup K,
          χ (absoluteGaloisConjugate τ σ) ≠ χ σ

theorem rootsDownstairs_faithful_h1_action_of_char_ne
    {K L : Type*} [Field K] [Field L] [Algebra K L] [IsGalois K L]
    {p : ℕ} (hp : p.Prime) (hchar : ringChar K ≠ p)
    (hdeg : Module.finrank K L = p)
    (hμ : (primitiveRoots p K).Nonempty)
    (hfinite : Set.Finite {ξ : L | ∃ m : ℕ, ξ ^ (p ^ m) = 1})
    (hdown : ∀ ξ : L, (∃ m : ℕ, ξ ^ (p ^ m) = 1) →
      ξ ∈ Set.range (algebraMap K L)) :
    ∃ s : ℕ, 1 ≤ s ∧ (primitiveRoots (p ^ s) L).Nonempty ∧
      (∀ m : ℕ, (primitiveRoots (p ^ m) L).Nonempty → m ≤ s) ∧
      Function.Injective (relativeGaloisH1Action (n := p ^ s) K L)