RadicalAutomorphisms.lean

theorem algEquiv_eq_of_rootRatio_eq {r : L} (hr : r ≠ 0) {S : Set L}
    (hgen : IntermediateField.adjoin K (insert r S) = ⊤)
    {σ τ : L ≃ₐ[K] L} (hS : ∀ x ∈ S, σ x = τ x)
    (h : rootRatio r σ = rootRatio r τ) : σ = τ

theorem rootRatio_injective_on_fixingSubgroup {r : L} (hr : r ≠ 0) {S : Set L}
    (hgen : IntermediateField.adjoin K (insert r S) = ⊤) :
    Function.Injective (fun σ : (IntermediateField.adjoin K S).fixingSubgroup =>
      rootRatio r σ.val) := by
  intro σ τ h
  apply Subtype.ext
  apply algEquiv_eq_of_rootRatio_eq hr hgen ?_ h
  intro x hx
  have hx' := IntermediateField.subset_adjoin K S hx
  have hσ := (IntermediateField.mem_fixingSubgroup_iff
    (IntermediateField.adjoin K S) σ.val).mp σ.property x hx'
  have hτ := (IntermediateField.mem_fixingSubgroup_iff
    (IntermediateField.adjoin K S) τ.val).mp τ.property x hx'
  exact hσ.trans hτ.symm

theorem radical_conjugate_eq_pow {r : L} (hr : r ≠ 0) {S : Set L}
    (hgen : IntermediateField.adjoin K (insert r S) = ⊤)
    {n m : ℕ} {a : K} (ha : r ^ n = algebraMap K L a)
    (σ τ : L ≃ₐ[K] L)
    (hτ : ∀ x ∈ S, τ x = x)
    (hstable : ∀ x ∈ S, σ⁻¹ x ∈ S)
    (hroots : ∀ ξ : L, ξ ^ n = 1 → ξ ∈ S)
    (hσ : ∀ ξ : L, ξ ^ n = 1 → σ ξ = ξ ^ m) :
    σ * τ * σ⁻¹ = τ ^ m