Algebraic Independence

This file defines algebraic independence of a family of elements of an R algebra.

Main definitions

• AlgebraicIndependent - AlgebraicIndependent R x states the family of elements x is algebraically independent over R, meaning that the canonical map out of the multivariable polynomial ring is injective.

• AlgebraicIndependent.aevalEquiv - The canonical isomorphism from the polynomial ring to the subalgebra generated by an algebraic independent family.

• AlgebraicIndependent.repr - The canonical map from the subalgebra generated by an algebraic independent family into the polynomial ring. It is the inverse of AlgebraicIndependent.aevalEquiv.

• IsTranscendenceBasis R x - a family x is a transcendence basis over R if it is a maximal algebraically independent subset.

Main results

We show that algebraic independence is preserved under injective maps of the indices.

References

• Stacks: Transcendence

def AlgebraicIndependent {ι : Type u_1} (R : Type u_3) {A : Type u_5} (x : ι → A) [CommRing R] [CommRing A] [Algebra R A] : Prop

AlgebraicIndependent R x states the family of elements x is algebraically independent over R, meaning that the canonical map out of the multivariable polynomial ring is injective.

Equations

• AlgebraicIndependent R x = Function.Injective ⇑(MvPolynomial.aeval x)

@[reducible, inline]

abbrev AlgebraicIndepOn {ι : Type u_1} (R : Type u_3) {A : Type u_5} (x : ι → A) [CommRing R] [CommRing A] [Algebra R A] (s : Set ι) : Prop

AlgebraicIndepOn R v s states that the elements in the family v that are indexed by the elements of s are algebraically independent over R.

Equations

• AlgebraicIndepOn R x s = AlgebraicIndependent R fun (i : ↑s) => x ↑i

theorem algebraicIndependent_iff {ι : Type u_1} {R : Type u_3} {A : Type u_5} {x : ι → A} [CommRing R] [CommRing A] [Algebra R A] : AlgebraicIndependent R x ↔ ∀ (p : MvPolynomial ι R), (MvPolynomial.aeval x) p = 0 → p = 0

theorem AlgebraicIndependent.eq_zero_of_aeval_eq_zero {ι : Type u_1} {R : Type u_3} {A : Type u_5} {x : ι → A} [CommRing R] [CommRing A] [Algebra R A] (h : AlgebraicIndependent R x) (p : MvPolynomial ι R) : (MvPolynomial.aeval x) p = 0 → p = 0

theorem algebraicIndependent_iff_injective_aeval {ι : Type u_1} {R : Type u_3} {A : Type u_5} {x : ι → A} [CommRing R] [CommRing A] [Algebra R A] : AlgebraicIndependent R x ↔ Function.Injective ⇑(MvPolynomial.aeval x)

theorem AlgebraicIndependent.of_comp {ι : Type u_1} {R : Type u_3} {A : Type u_5} {A' : Type u_6} {x : ι → A} [CommRing R] [CommRing A] [CommRing A'] [Algebra R A] [Algebra R A'] (f : A →ₐ[R] A') (hfv : AlgebraicIndependent R (⇑f ∘ x)) : AlgebraicIndependent R x

theorem AlgebraicIndependent.comp {ι : Type u_1} {ι' : Type u_2} {R : Type u_3} {A : Type u_5} {x : ι → A} [CommRing R] [CommRing A] [Algebra R A] (hx : AlgebraicIndependent R x) (f : ι' → ι) (hf : Function.Injective f) : AlgebraicIndependent R (x ∘ f)

theorem AlgebraicIndependent.coe_range {ι : Type u_1} {R : Type u_3} {A : Type u_5} {x : ι → A} [CommRing R] [CommRing A] [Algebra R A] (hx : AlgebraicIndependent R x) : AlgebraicIndependent R Subtype.val

theorem algebraicIndependent_equiv {ι : Type u_1} {ι' : Type u_2} {R : Type u_3} {A : Type u_5} [CommRing R] [CommRing A] [Algebra R A] (e : ι ≃ ι') {f : ι' → A} : AlgebraicIndependent R (f ∘ ⇑e) ↔ AlgebraicIndependent R f

theorem algebraicIndependent_equiv' {ι : Type u_1} {ι' : Type u_2} {R : Type u_3} {A : Type u_5} [CommRing R] [CommRing A] [Algebra R A] (e : ι ≃ ι') {f : ι' → A} {g : ι → A} (h : f ∘ ⇑e = g) : AlgebraicIndependent R g ↔ AlgebraicIndependent R f

theorem algebraicIndependent_subtype_range {R : Type u_3} {A : Type u_5} [CommRing R] [CommRing A] [Algebra R A] {ι : Type u_7} {f : ι → A} (hf : Function.Injective f) : AlgebraicIndependent R Subtype.val ↔ AlgebraicIndependent R f

theorem AlgebraicIndependent.of_subtype_range {R : Type u_3} {A : Type u_5} [CommRing R] [CommRing A] [Algebra R A] {ι : Type u_7} {f : ι → A} (hf : Function.Injective f) : AlgebraicIndependent R Subtype.val → AlgebraicIndependent R f

Alias of the forward direction of algebraicIndependent_subtype_range.

theorem algebraicIndependent_image {R : Type u_3} {A : Type u_5} [CommRing R] [CommRing A] [Algebra R A] {ι : Type u_7} {s : Set ι} {f : ι → A} (hf : Set.InjOn f s) : (AlgebraicIndependent R fun (x : ↑s) => f ↑x) ↔ AlgebraicIndependent R fun (x : ↑(f '' s)) => ↑x

theorem AlgebraicIndependent.mono {R : Type u_3} {A : Type u_5} [CommRing R] [CommRing A] [Algebra R A] {t s : Set A} (h : t ⊆ s) (hx : AlgebraicIndependent R Subtype.val) : AlgebraicIndependent R Subtype.val

def AlgebraicIndependent.aevalEquiv {ι : Type u_1} {R : Type u_3} {A : Type u_5} {x : ι → A} [CommRing R] [CommRing A] [Algebra R A] (hx : AlgebraicIndependent R x) : MvPolynomial ι R ≃ₐ[R] ↥(Algebra.adjoin R (Set.range x))

Canonical isomorphism between polynomials and the subalgebra generated by algebraically independent elements.

Equations

• hx.aevalEquiv = (AlgEquiv.ofInjective (MvPolynomial.aeval x) ⋯).trans ((MvPolynomial.aeval x).range.equivOfEq (Algebra.adjoin R (Set.range x)) ⋯)

@[simp]

theorem AlgebraicIndependent.aevalEquiv_apply_coe {ι : Type u_1} {R : Type u_3} {A : Type u_5} {x : ι → A} [CommRing R] [CommRing A] [Algebra R A] (hx : AlgebraicIndependent R x) (a✝ : MvPolynomial ι R) : ↑(hx.aevalEquiv a✝) = (MvPolynomial.aeval x) a✝

@[simp]

theorem AlgebraicIndependent.algebraMap_aevalEquiv {ι : Type u_1} {R : Type u_3} {A : Type u_5} {x : ι → A} [CommRing R] [CommRing A] [Algebra R A] (hx : AlgebraicIndependent R x) (p : MvPolynomial ι R) : (algebraMap (↥(Algebra.adjoin R (Set.range x))) A) (hx.aevalEquiv p) = (MvPolynomial.aeval x) p

def AlgebraicIndependent.repr {ι : Type u_1} {R : Type u_3} {A : Type u_5} {x : ι → A} [CommRing R] [CommRing A] [Algebra R A] (hx : AlgebraicIndependent R x) : ↥(Algebra.adjoin R (Set.range x)) →ₐ[R] MvPolynomial ι R

The canonical map from the subalgebra generated by an algebraic independent family into the polynomial ring.

Equations

• hx.repr = ↑hx.aevalEquiv.symm

@[simp]

theorem AlgebraicIndependent.aeval_repr {ι : Type u_1} {R : Type u_3} {A : Type u_5} {x : ι → A} [CommRing R] [CommRing A] [Algebra R A] (hx : AlgebraicIndependent R x) (p : ↥(Algebra.adjoin R (Set.range x))) : (MvPolynomial.aeval x) (hx.repr p) = ↑p

theorem AlgebraicIndependent.aeval_comp_repr {ι : Type u_1} {R : Type u_3} {A : Type u_5} {x : ι → A} [CommRing R] [CommRing A] [Algebra R A] (hx : AlgebraicIndependent R x) : (MvPolynomial.aeval x).comp hx.repr = (Algebra.adjoin R (Set.range x)).val

def IsTranscendenceBasis {ι : Type u_1} (R : Type u_3) {A : Type u_5} [CommRing R] [CommRing A] [Algebra R A] (x : ι → A) : Prop

A family is a transcendence basis if it is a maximal algebraically independent subset.

Equations

• IsTranscendenceBasis R x = (AlgebraicIndependent R x ∧ ∀ (s : Set A), AlgebraicIndepOn R id s → Set.range x ⊆ s → Set.range x = s)

theorem isTranscendenceBasis_iff_maximal {R : Type u_3} {A : Type u_5} [CommRing R] [CommRing A] [Algebra R A] {s : Set A} : IsTranscendenceBasis R Subtype.val ↔ Maximal (AlgebraicIndepOn R id) s

theorem isTranscendenceBasis_equiv {ι : Type u_1} {ι' : Type u_2} {R : Type u_3} {A : Type u_5} [CommRing R] [CommRing A] [Algebra R A] (e : ι ≃ ι') {f : ι' → A} : IsTranscendenceBasis R (f ∘ ⇑e) ↔ IsTranscendenceBasis R f

theorem IsTranscendenceBasis.comp_equiv {ι : Type u_1} {ι' : Type u_2} {R : Type u_3} {A : Type u_5} [CommRing R] [CommRing A] [Algebra R A] (e : ι ≃ ι') {f : ι' → A} : IsTranscendenceBasis R f → IsTranscendenceBasis R (f ∘ ⇑e)

Alias of the reverse direction of isTranscendenceBasis_equiv.

theorem isTranscendenceBasis_equiv' {ι : Type u_1} {ι' : Type u_2} {R : Type u_3} {A : Type u_5} [CommRing R] [CommRing A] [Algebra R A] (e : ι ≃ ι') {f : ι' → A} {g : ι → A} (h : f ∘ ⇑e = g) : IsTranscendenceBasis R g ↔ IsTranscendenceBasis R f

theorem isTranscendenceBasis_subtype_range {R : Type u_3} {A : Type u_5} [CommRing R] [CommRing A] [Algebra R A] {ι : Type u_7} {f : ι → A} (hf : Function.Injective f) : IsTranscendenceBasis R Subtype.val ↔ IsTranscendenceBasis R f

theorem IsTranscendenceBasis.of_subtype_range {R : Type u_3} {A : Type u_5} [CommRing R] [CommRing A] [Algebra R A] {ι : Type u_7} {f : ι → A} (hf : Function.Injective f) : IsTranscendenceBasis R Subtype.val → IsTranscendenceBasis R f

Alias of the forward direction of isTranscendenceBasis_subtype_range.

theorem isTranscendenceBasis_image {R : Type u_3} {A : Type u_5} [CommRing R] [CommRing A] [Algebra R A] {ι : Type u_7} {s : Set ι} {f : ι → A} (hf : Set.InjOn f s) : (IsTranscendenceBasis R fun (x : ↑s) => f ↑x) ↔ IsTranscendenceBasis R fun (x : ↑(f '' s)) => ↑x