From 1faf964e1857bfb011eab68e5af4f61505d2f76f Mon Sep 17 00:00:00 2001 From: Chris Hughes Date: Mon, 4 Oct 2021 09:48:16 +0000 Subject: [PATCH] feat(ring_theory/algebraic_independent): Existence of transcendence bases 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 | 85 +++++++++++++++++++++- 1 file changed, 84 insertions(+), 1 deletion(-) diff --git a/src/ring_theory/algebraic_independent.lean b/src/ring_theory/algebraic_independent.lean index a950c24fc6d32..88ef89d4296c0 100644 --- a/src/ring_theory/algebraic_independent.lean +++ b/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]