English
Let pb be a PowerBasis K S. Then the cardinality of the K-algebra homomorphisms from S to L equals the degree of pb, provided separability and splitting conditions hold.
Русский
Пусть pb — базис по степени в отношении K и S. Тогда число гомоморфизмов по K из S в L равно размерности pb, при условии разделимости и разложения минполинома.
LaTeX
$$$\\text{pb} : \\text{PowerBasis } K S \\;\\to\\; \\mathbb{N},\\; \\text{h_sep: IsSeparable } K pb.gen,\\; \\text{h_splits: } (minpoly K pb.gen).Splits (algebraMap K L) \\Rightarrow |S \\to_{K} L| = pb.dim$$$
Lean4
theorem natCard_of_powerBasis (pb : PowerBasis K S) (h_sep : IsSeparable K pb.gen)
(h_splits : (minpoly K pb.gen).Splits (algebraMap K L)) : Nat.card (S →ₐ[K] L) = pb.dim := by
classical
rw [Nat.card_congr pb.liftEquiv', Nat.subtype_card _ (fun x => Multiset.mem_toFinset), ← pb.natDegree_minpoly,
natDegree_eq_card_roots h_splits, Multiset.toFinset_card_of_nodup]
exact nodup_roots ((separable_map (algebraMap K L)).mpr h_sep)
