feat(ring_theory/algebraic_independent): Existence of transcendence b…

…ases and rings are algebraic over transcendence basis (#9377)

Co-authored-by: Chris Hughes <33847686+ChrisHughes24@users.noreply.github.com>

src/ring_theory/algebraic_independent.lean

@@ -39,7 +39,7 @@ noncomputable theory
 open function set subalgebra mv_polynomial algebra
 open_locale classical big_operators
 
-universes u v w x
+universes x u v w
 
 variables {ι : Type*} {ι' : Type*} (R : Type*) {K : Type*}
 variables {A : Type*} {A' A'' : Type*} {V : Type u} {V' : Type*}
@@ -367,6 +367,10 @@ begin
       simp } }
 end
 
+@[simp] lemma algebraic_independent.algebra_map_aeval_equiv (hx : algebraic_independent R x)
+  (p : mv_polynomial ι R) : algebra_map (algebra.adjoin R (range x)) A (hx.aeval_equiv p) =
+  aeval x p := rfl
+
 /-- The canonical map from the subalgebra generated by an algebraic independent family
   into the polynomial ring.  -/
 def algebraic_independent.repr (hx : algebraic_independent R x) :
@@ -385,6 +389,56 @@ lemma algebraic_independent.repr_ker :
 
 end repr
 
+
+-- TODO - make this an `alg_equiv`
+/-- The isomorphism between `mv_polynomial (option ι) R` and the polynomial ring over
+the algebra generated by an algebraically independent family.  -/
+def algebraic_independent.mv_polynomial_option_equiv_polynomial_adjoin
+  (hx : algebraic_independent R x) :
+  mv_polynomial (option ι) R ≃+* polynomial (adjoin R (set.range x)) :=
+(mv_polynomial.option_equiv_left _ _).to_ring_equiv.trans
+  (polynomial.map_equiv hx.aeval_equiv.to_ring_equiv)
+
+lemma algebraic_independent.aeval_comp_mv_polynomial_option_equiv_polynomial_adjoin
+  (hx : algebraic_independent R x) (a : A) :
+  (ring_hom.comp (↑(polynomial.aeval a : polynomial (adjoin R (set.range x)) →ₐ[_] A) :
+      polynomial (adjoin R (set.range x)) →+* A)
+    hx.mv_polynomial_option_equiv_polynomial_adjoin.to_ring_hom) =
+    ↑((mv_polynomial.aeval (λ o : option ι, o.elim a x)) :
+      mv_polynomial (option ι) R →ₐ[R] A) :=
+begin
+  letI : is_scalar_tower R (mv_polynomial ι R) (polynomial (mv_polynomial ι R)) :=
+    @polynomial.is_scalar_tower (mv_polynomial ι R) _ R _ _ _ _ _ _ _,
+  dsimp only [ring_equiv.to_ring_hom_eq_coe, ring_equiv.to_ring_hom_trans,
+    alg_hom.to_ring_hom_eq_coe,
+    algebraic_independent.mv_polynomial_option_equiv_polynomial_adjoin],
+  refine mv_polynomial.ring_hom_ext _ _,
+  { intro r,
+    simp only [ring_hom.comp_apply, alg_equiv.coe_ring_equiv', alg_hom.coe_to_ring_hom,
+      ring_equiv.coe_to_ring_hom, option_equiv_left_apply, aeval_C,
+      is_scalar_tower.algebra_map_eq R (mv_polynomial ι R) (polynomial (mv_polynomial ι R)),
+      ← polynomial.C_eq_algebra_map, polynomial.map_equiv_apply, polynomial.map_C,
+      polynomial.aeval_C, algebraic_independent.algebra_map_aeval_equiv,
+      mv_polynomial.algebra_map_eq] ,},
+  { intro i,
+    simp only [alg_hom.coe_to_ring_hom, aeval_X, ring_hom.comp_apply,
+      ring_equiv.coe_to_ring_hom, alg_equiv.coe_ring_equiv', option_equiv_left_apply,
+      polynomial.map_equiv_apply],
+    cases i,
+    { rw [option.elim, polynomial.map_X, polynomial.aeval_X, option.elim] },
+    { rw [option.elim, polynomial.map_C, polynomial.aeval_C, ring_equiv.coe_to_ring_hom,
+        alg_equiv.coe_ring_equiv', algebraic_independent.algebra_map_aeval_equiv,
+        aeval_X, option.elim] } }
+end
+
+theorem algebraic_independent.option_iff (hx : algebraic_independent R x) (a : A) :
+  (algebraic_independent R (λ o : option ι, o.elim a x)) ↔
+    ¬ is_algebraic (adjoin R (set.range x)) a :=
+by erw [algebraic_independent_iff_injective_aeval, is_algebraic_iff_not_injective, not_not,
+    ← alg_hom.coe_to_ring_hom,
+    ← hx.aeval_comp_mv_polynomial_option_equiv_polynomial_adjoin,
+    ring_hom.coe_comp, injective.of_comp_iff' _ (ring_equiv.bijective _), alg_hom.coe_to_ring_hom]
+
 variable (R)
 /--
   A family is a transcendence basis if it is a maximal algebraically independent subset.
@@ -393,6 +447,17 @@ def is_transcendence_basis (x : ι → A) : Prop :=
 algebraic_independent R x ∧
   ∀ (s : set A) (i' : algebraic_independent R (coe : s → A)) (h : range x ≤ s), range x = s
 
+lemma exists_is_transcendence_basis (h : injective (algebra_map R A)) :
+  ∃ s : set A, is_transcendence_basis R (coe : s → A) :=
+begin
+  cases exists_maximal_algebraic_independent (∅ : set A) set.univ
+    (set.subset_univ _) ((algebraic_independent_empty_iff R A).2 h) with s hs,
+  use [s, hs.1],
+  intros t ht hr,
+  simp only [subtype.range_coe_subtype, set_of_mem_eq] at *,
+  exact eq.symm (hs.2.2.2 t ht hr (set.subset_univ _))
+end
+
 variable {R}
 lemma algebraic_independent.is_transcendence_basis_iff
   {ι : Type w} {R : Type u} [comm_ring R] [nontrivial R]
@@ -417,6 +482,24 @@ begin
     simpa using q, },
 end
 
+lemma is_transcendence_basis.is_algebraic [nontrivial R]
+  (hx : is_transcendence_basis R x) : is_algebraic (adjoin R (range x)) A :=
+begin
+  intro a,
+  rw [← not_iff_comm.1 (hx.1.option_iff _).symm],
+  intro ai,
+  have h₁ : range x ⊆ range (λ o : option ι, o.elim a x),
+  { rintros x ⟨y, rfl⟩, exact ⟨some y, rfl⟩ },
+  have h₂ : range x ≠ range (λ o : option ι, o.elim a x),
+  { intro h,
+    have : a ∈ range x, { rw h, exact ⟨none, rfl⟩ },
+    rcases this with ⟨b, rfl⟩,
+    have : some b = none := ai.injective rfl,
+    simpa },
+  exact h₂ (hx.2 (set.range (λ o : option ι, o.elim a x))
+    ((algebraic_independent_subtype_range ai.injective).2 ai) h₁)
+end
+
 section field
 variables [field K] [algebra K A]