English
Characterization: f splits over K iff the corresponding subalgebra equals bottom or top in an appropriate sense.
Русский
Характеризация: f распадается над K тогда, когда соответствующая подалгебра равна нижнему/верхнему пределу в нужном смысле.
LaTeX
$$splits_iff$$
Lean4
theorem splits_iff (f : K[X]) [IsSplittingField K L f] : Splits (RingHom.id K) f ↔ (⊤ : Subalgebra K L) = ⊥ :=
⟨fun h =>
by
rw [eq_bot_iff, ← adjoin_rootSet L f, rootSet, aroots, roots_map (algebraMap K L) h, Algebra.adjoin_le_iff]
intro y hy
classical
rw [Multiset.toFinset_map, Finset.mem_coe, Finset.mem_image] at hy
obtain ⟨x : K, -, hxy : algebraMap K L x = y⟩ := hy
rw [← hxy]
exact SetLike.mem_coe.2 <| Subalgebra.algebraMap_mem _ _,
fun h =>
@RingEquiv.toRingHom_refl K _ ▸
RingEquiv.self_trans_symm (RingEquiv.ofBijective _ <| Algebra.bijective_algebraMap_iff.2 h) ▸
by
rw [RingEquiv.toRingHom_trans]
exact splits_comp_of_splits _ _ (splits L f)⟩
