English
If p splits over E, the map mapRoots p E is a bijection between the root sets of p in p.SplittingField and in E.
Русский
Если p распадается над E, отображение mapRoots p E образует биекцию между множеством корней p в p.SplittingField и в E.
LaTeX
$$$\\mathrm{mapRoots}_{p,E}$ является биекцией$$
Lean4
theorem mapRoots_bijective [h : Fact (p.Splits (algebraMap F E))] : Function.Bijective (mapRoots p E) :=
by
constructor
· exact fun _ _ h => Subtype.ext (RingHom.injective _ (Subtype.ext_iff.mp h))
· intro y
have key :=
roots_map (IsScalarTower.toAlgHom F p.SplittingField E : p.SplittingField →+* E)
((splits_id_iff_splits _).mpr (IsSplittingField.splits p.SplittingField p))
rw [map_map, AlgHom.comp_algebraMap] at key
have hy := Subtype.mem y
simp only [rootSet, Finset.mem_coe, Multiset.mem_toFinset, key, Multiset.mem_map] at hy
rcases hy with ⟨x, hx1, hx2⟩
exact ⟨⟨x, (@Multiset.mem_toFinset _ (Classical.decEq _) _ _).mpr hx1⟩, Subtype.ext hx2⟩
