Conjugate elements in same Galois orbit

Stream: Is there code for X?

[Michail Karatarakis]

Hi, do we have the following theorem?

import field_theory.galois

variables {K L : Type*} [field K] [field L] [algebra K L] [is_galois K L]

example (α₁ : L) (α₂ : L) (hpoly : minpoly K α₁ = minpoly K α₂) :
   ∃ (g : (L ≃ₐ[K] L)), g α₁ = α₂ :=
begin
  sorry
end

[Johan Commelin]

cc @Thomas Browning

[Riccardo Brasca]

I am sure we have it, or maybe something very close. Look for power_basis.

[Eric Rodriguez]

I don't think we have this, I had a big discussion with Anne about how to do this properly (the minpoly condition is a bit too strong, you want something like eval a1 minpoly a2 = 0 & the vice-versa too instead) and I never got around to it

[Eric Rodriguez]

https://leanprover.zulipchat.com/#narrow/stream/116395-maths/topic/the.20power.20basis.20of.20a.20conjugate I think is the previoius discussion

[Riccardo Brasca]

Ah right, the elements are not generators

[Riccardo Brasca]

So one probably has to go through the intermediate field and then extending the iso

[Riccardo Brasca]

@Xavier Roblot am I misremembering or you did something related recently?

[Xavier Roblot]

There is docs#algebra.is_algebraic.range_eval_eq_root_set_minpoly which is related.

[Riccardo Brasca]

In any case I am sure the equiv of intermediate field is there, since we have the power basis. Then I guess we can extend field equivs.

[Thomas Browning]

Yeah, I don't think we have this exactly. One way would be to use docs#alg_equiv.lift_normal

[Michail Karatarakis]

Thanks a lot. I guess the plan is to define something like

def conjugate_roots_to_iso (α₁ α₂ : L) (hpoly : minpoly K α₁ = minpoly K α₂) :
   algebra.adjoin K ({α₁} : set L) ≃ₐ[K] (algebra.adjoin K ({α₂} : set L))  :=  sorry

and then use alg_equiv.lift_normal to lift it and get a g : L ≃ₐ[K] L.

Do we have more code related to this I could use? - I am not very familiar with the Galois theory API.

[Riccardo Brasca]

Give me 10 minutes

[Riccardo Brasca]

Voilà. It can probably be golfed (and of course the existential statement is imprecise, it's better to say that the given map has the required property).

import field_theory.adjoin
import field_theory.galois

variables {K L : Type*} [field K] [field L] [algebra K L] [is_galois K L]

namespace intermediate_field

open adjoin polynomial

lemma foo {α₁ α₂ : L} (hpoly : minpoly K α₁ = minpoly K α₂) :
  (aeval (power_basis (is_galois.integral K α₁)).gen)
  (minpoly K (power_basis (is_galois.integral K α₂)).gen) = 0 :=
begin
  apply (injective_iff_map_eq_zero _).1 (algebra_map K⟮α₁⟯ L).injective,
  have : is_integral K (adjoin_simple.gen K α₂),
  { rw [← is_integral_algebra_map_iff (algebra_map K⟮α₂⟯ L).injective],
    simp [is_galois.integral K α₂],
    all_goals { apply_instance } },
  rw [power_basis_gen, power_basis_gen, ← aeval_algebra_map_apply, adjoin_simple.algebra_map_gen,
    minpoly.eq_of_algebra_map_eq (algebra_map K⟮α₂⟯ L).injective this
    (adjoin_simple.algebra_map_gen K α₂).symm, ← hpoly],
  exact minpoly.aeval _ _
end

@[simps] noncomputable def equiv {α₁ α₂ : L} (hpoly : minpoly K α₁ = minpoly K α₂) : K⟮α₁⟯ ≃ₐ[K] K⟮α₂⟯ :=
power_basis.equiv_of_root (power_basis (is_galois.integral K α₁))
  (power_basis (is_galois.integral K α₂)) (foo hpoly) (foo hpoly.symm)

example (α₁ : L) (α₂ : L) (hpoly : minpoly K α₁ = minpoly K α₂) :
   ∃ (g : (L ≃ₐ[K] L)), g α₁ = α₂ :=
begin
  refine ⟨(equiv hpoly).lift_normal _, _⟩,
  simp_rw [← adjoin_simple.algebra_map_gen K α₁, ← adjoin_simple.algebra_map_gen K α₂],
  rw [alg_equiv.lift_normal_commutes],
  congr,
  simpa [power_basis_gen] using
    power_basis.lift_gen (power_basis (is_galois.integral K α₁)) _ (foo hpoly.symm),
end

end intermediate_field

[Michail Karatarakis]

Brilliant, thank you!

[María Inés de Frutos Fernández]

You may not need this after the previous replies, but in case it is useful, I have some related lemmas here.

[Eric Wieser]

This would be better stated with docs#mul_action.is_pretransitive I think

[Michail Karatarakis]

Oh great, thank you!