OAI/GroupTheory/PolycyclicRecognition/Algebra/CountableFieldEmbeddings.lean

GitHub source file

6 declarations, 0 contain sorry, 0 declared as axioms

Extending embeddings into an uncountable algebraically closed field

Finite transcendence bases can be sent to independent elements in an uncountable field over a countable coefficient field. Algebraicity then extends this embedding to the finitely generated field itself.

  1. def OAI.PolycyclicRecognition.independentAdjoinEquiv line 21
  2. theorem OAI.PolycyclicRecognition.independentAdjoinEquiv_generator line 29
  3. theorem OAI.PolycyclicRecognition.countable_adjoin_of_algebraicIndependent line 48
  4. theorem OAI.PolycyclicRecognition.exists_transcendental_of_countable line 58
  5. theorem OAI.PolycyclicRecognition.exists_finite_algebraicIndependent line 69
  6. theorem OAI.PolycyclicRecognition.nonempty_algHom_of_countable_finite_trdeg line 85