English
The map restrictProd is injective: the simultaneous restriction to p and q uniquely determines an element of Gal(pq).
Русский
Отображение restrictProd инъективно: одновременное ограничение к p и к q однозначно определяет элемент Gal(pq).
LaTeX
$$$\\mathrm{restrictProd}: (p*q).Gal \\to \\mathrm{Gal}(p) \\times \\mathrm{Gal}(q)$ инъективно$$
Lean4
/-- `Polynomial.Gal.restrictProd` is actually a subgroup embedding. -/
theorem restrictProd_injective : Function.Injective (restrictProd p q) :=
by
by_cases hpq : p * q = 0
· have : Unique (p * q).Gal := by rw [hpq]; infer_instance
exact fun f g _ => Eq.trans (Unique.eq_default f) (Unique.eq_default g).symm
intro f g hfg
classical
simp only [restrictProd, restrictDvd_def] at hfg
simp only [dif_neg hpq, MonoidHom.prod_apply, Prod.mk_inj] at hfg
ext (x hx)
rw [rootSet_def, aroots_mul hpq] at hx
rcases Multiset.mem_add.mp (Multiset.mem_toFinset.mp hx) with h | h
· haveI : Fact (p.Splits (algebraMap F (p * q).SplittingField)) :=
⟨splits_of_splits_of_dvd _ hpq (SplittingField.splits (p * q)) (dvd_mul_right p q)⟩
have key :
x =
algebraMap p.SplittingField (p * q).SplittingField
((rootsEquivRoots p _).invFun ⟨x, (@Multiset.mem_toFinset _ (Classical.decEq _) _ _).mpr h⟩) :=
Subtype.ext_iff.mp (Equiv.apply_symm_apply (rootsEquivRoots p _) ⟨x, _⟩).symm
rw [key, ← AlgEquiv.restrictNormal_commutes, ← AlgEquiv.restrictNormal_commutes]
exact congr_arg _ (AlgEquiv.ext_iff.mp hfg.1 _)
· haveI : Fact (q.Splits (algebraMap F (p * q).SplittingField)) :=
⟨splits_of_splits_of_dvd _ hpq (SplittingField.splits (p * q)) (dvd_mul_left q p)⟩
have key :
x =
algebraMap q.SplittingField (p * q).SplittingField
((rootsEquivRoots q _).invFun ⟨x, (@Multiset.mem_toFinset _ (Classical.decEq _) _ _).mpr h⟩) :=
Subtype.ext_iff.mp (Equiv.apply_symm_apply (rootsEquivRoots q _) ⟨x, _⟩).symm
rw [key, ← AlgEquiv.restrictNormal_commutes, ← AlgEquiv.restrictNormal_commutes]
exact congr_arg _ (AlgEquiv.ext_iff.mp hfg.2 _)
