Commit 2024-01-10 19:15 f2e0c5ba

View on Github →

feat (FieldTheory/Adjoin): generalize IntermediateField.exists_algHom_of_splits (#9392)

  • Extract from Lifts.exists_lift_of_splits a version that assumes integrality and splitting of minimal polynomial over an intermediate field (either actual IntermediateField or middle of IsScalarTower) rather than the base field
  • Generalize exists_algHom_adjoin_of_splits, exists_algHom_of_adjoin_splits, exists_algHom_of_splits to the same setting
  • Prove the extension lemma surjective_comp_algebraMap_of_isAlgebraic/isSeparable to be used in the proof that an epimorphism in the category of fields is a purely inseparable extension.

Estimated changes