Commit 2021-01-27 08:41 7f04253c

View on Github →

feat(field_theory/adjoin): Generalize alg_hom_mk_adjoin_splits to infinite sets (#5860) This PR uses Zorn's lemma to generalize alg_hom_mk_adjoin_splits to infinite sets. The proof is rather long, but I think that the result is worth it. It should allow me to prove that if E/F is any normal extension then any automorphism of F lifts to an automorphism of E.

Estimated changes

Modified src/field_theory/adjoin.lean

modified theorem intermediate_field.alg_hom_mk_adjoin_splits'

added theorem intermediate_field.lifts.eq_of_le

added theorem intermediate_field.lifts.exists_lift_of_splits

added theorem intermediate_field.lifts.exists_max_three

added theorem intermediate_field.lifts.exists_max_two

added theorem intermediate_field.lifts.exists_upper_bound

added theorem intermediate_field.lifts.le_lifts_of_splits

added theorem intermediate_field.lifts.mem_lifts_of_splits

added def intermediate_field.lifts.upper_bound_intermediate_field

added def intermediate_field.lifts

Modified src/field_theory/normal.lean