Commit 2024-11-14 05:52 cc3181fb

feat: lifting Ring/AlgHom to purely inseparable extension (#18811) The existing theorem IsPurelyInseparable.injective_comp_algebraMap says that if E/F is purely inseparable, then every RingHom from F to a reduced commutative ring L lifts in at most one way to E. This PR shows if L is a perfect field, then such a RingHom always lifts to E, and also add AlgHom versions. For this purpose we slightly generalize natSepDegree_map and deduce PerfectField.splits_of_natSepDegree_eq_one. Also add theorem Field.Emb.cardinal_separableClosure saying that the F-embeddings of an algebraic extension E/F are equipotent with F-embeddings of separableClosure F E. Since Algebra.IsAlgebraic is now a class, two theorems are made instances.