Algebraic Independence

This file defines algebraic independence of a family of element 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.repr - The canonical map from the subalgebra generated by an algebraic independent family into the polynomial ring.

References

• Stacks: Transcendence

TODO

Prove that a ring is an algebraic extension of the subalgebra generated by a transcendence basis.

Tags

transcendence basis, transcendence degree, 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.

theorem algebraicIndependent_iff_ker_eq_bot {ι : Type u_1} {R : Type u_3} {A : Type u_5} {x : ι → A} [CommRing R] [CommRing A] [Algebra R A] : AlgebraicIndependent R x ↔ RingHom.ker ↑(MvPolynomial.aeval x) = ⊥

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)

@[simp]

theorem algebraicIndependent_empty_type_iff {ι : Type u_1} {R : Type u_3} {A : Type u_5} {x : ι → A} [CommRing R] [CommRing A] [Algebra R A] [IsEmpty ι] : AlgebraicIndependent R x ↔ Function.Injective ↑(algebraMap R A)

theorem AlgebraicIndependent.algebraMap_injective {ι : Type u_1} {R : Type u_3} {A : Type u_5} {x : ι → A} [CommRing R] [CommRing A] [Algebra R A] (hx : AlgebraicIndependent R x) : Function.Injective ↑(algebraMap R A)

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

theorem AlgebraicIndependent.injective {ι : Type u_1} {R : Type u_3} {A : Type u_5} {x : ι → A} [CommRing R] [CommRing A] [Algebra R A] (hx : AlgebraicIndependent R x) [Nontrivial R] : Function.Injective x

theorem AlgebraicIndependent.ne_zero {ι : Type u_1} {R : Type u_3} {A : Type u_5} {x : ι → A} [CommRing R] [CommRing A] [Algebra R A] (hx : AlgebraicIndependent R x) [Nontrivial R] (i : ι) : x i ≠ 0

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.map {ι : 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'] (hx : AlgebraicIndependent R x) {f : A →ₐ[R] A'} (hf_inj : Set.InjOn ↑f ↑(Algebra.adjoin R (Set.range x))) : AlgebraicIndependent R (↑f ∘ x)

theorem AlgebraicIndependent.map' {ι : 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'] (hx : AlgebraicIndependent R x) {f : A →ₐ[R] A'} (hf_inj : Function.Injective ↑f) : AlgebraicIndependent R (↑f ∘ 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 AlgHom.algebraicIndependent_iff {ι : 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') (hf : Function.Injective ↑f) : AlgebraicIndependent R (↑f ∘ x) ↔ AlgebraicIndependent R x

theorem algebraicIndependent_of_subsingleton {ι : Type u_1} {R : Type u_3} {A : Type u_5} {x : ι → A} [CommRing R] [CommRing A] [Algebra R A] [Subsingleton R] : AlgebraicIndependent R x

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_9} {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_9} {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_9} {s : Set ι} {f : ι → A} (hf : Set.InjOn f s) : (AlgebraicIndependent R fun x => f ↑x) ↔ AlgebraicIndependent R fun x => ↑x

theorem algebraicIndependent_adjoin {ι : Type u_1} {R : Type u_3} {A : Type u_5} {x : ι → A} [CommRing R] [CommRing A] [Algebra R A] (hs : AlgebraicIndependent R x) : AlgebraicIndependent R fun i => { val := x i, property := (_ : x i ∈ ↑(Algebra.adjoin R (Set.range x))) }

theorem AlgebraicIndependent.restrictScalars {ι : Type u_1} {R : Type u_3} {A : Type u_5} {x : ι → A} [CommRing R] [CommRing A] [Algebra R A] {K : Type u_9} [CommRing K] [Algebra R K] [Algebra K A] [IsScalarTower R K A] (hinj : Function.Injective ↑(algebraMap R K)) (ai : AlgebraicIndependent K x) : AlgebraicIndependent R x

A set of algebraically independent elements in an algebra A over a ring K is also algebraically independent over a subring R of K.

theorem algebraicIndependent_finset_map_embedding_subtype {R : Type u_3} {A : Type u_5} [CommRing R] [CommRing A] [Algebra R A] (s : Set A) (li : AlgebraicIndependent R Subtype.val) (t : Finset ↑s) : AlgebraicIndependent R Subtype.val

Every finite subset of an algebraically independent set is algebraically independent.

theorem algebraicIndependent_bounded_of_finset_algebraicIndependent_bounded {R : Type u_3} {A : Type u_5} [CommRing R] [CommRing A] [Algebra R A] {n : ℕ} (H : ∀ (s : Finset A), (AlgebraicIndependent R fun i => ↑i) → Finset.card s ≤ n) (s : Set A) : AlgebraicIndependent R Subtype.val → Cardinal.mk ↑s ≤ ↑n

If every finite set of algebraically independent element has cardinality at most n, then the same is true for arbitrary sets of algebraically independent elements.

theorem AlgebraicIndependent.restrict_of_comp_subtype {ι : Type u_1} {R : Type u_3} {A : Type u_5} {x : ι → A} [CommRing R] [CommRing A] [Algebra R A] {s : Set ι} (hs : AlgebraicIndependent R (x ∘ Subtype.val)) : AlgebraicIndependent R (Set.restrict s x)

theorem algebraicIndependent_empty_iff (R : Type u_3) (A : Type u_5) [CommRing R] [CommRing A] [Algebra R A] : AlgebraicIndependent R Subtype.val ↔ Function.Injective ↑(algebraMap R A)

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

theorem AlgebraicIndependent.to_subtype_range {R : Type u_3} {A : Type u_5} [CommRing R] [CommRing A] [Algebra R A] {ι : Type u_9} {f : ι → A} (hf : AlgebraicIndependent R f) : AlgebraicIndependent R Subtype.val

theorem AlgebraicIndependent.to_subtype_range' {R : Type u_3} {A : Type u_5} [CommRing R] [CommRing A] [Algebra R A] {ι : Type u_9} {f : ι → A} (hf : AlgebraicIndependent R f) {t : Set A} (ht : Set.range f = t) : AlgebraicIndependent R Subtype.val

theorem algebraicIndependent_comp_subtype {ι : Type u_1} {R : Type u_3} {A : Type u_5} {x : ι → A} [CommRing R] [CommRing A] [Algebra R A] {s : Set ι} : AlgebraicIndependent R (x ∘ Subtype.val) ↔ ∀ (p : MvPolynomial ι R), p ∈ MvPolynomial.supported R s → ↑(MvPolynomial.aeval x) p = 0 → p = 0

theorem algebraicIndependent_subtype {R : Type u_3} {A : Type u_5} [CommRing R] [CommRing A] [Algebra R A] {s : Set A} : AlgebraicIndependent R Subtype.val ↔ ∀ (p : MvPolynomial A R), p ∈ MvPolynomial.supported R s → ↑(MvPolynomial.aeval id) p = 0 → p = 0

theorem algebraicIndependent_of_finite {R : Type u_3} {A : Type u_5} [CommRing R] [CommRing A] [Algebra R A] (s : Set A) (H : ∀ (t : Set A), t ⊆ s → Set.Finite t → AlgebraicIndependent R Subtype.val) : AlgebraicIndependent R Subtype.val

theorem AlgebraicIndependent.image_of_comp {R : Type u_3} {A : Type u_5} [CommRing R] [CommRing A] [Algebra R A] {ι : Type u_9} {ι' : Type u_10} (s : Set ι) (f : ι → ι') (g : ι' → A) (hs : AlgebraicIndependent R fun x => g (f ↑x)) : AlgebraicIndependent R fun x => g ↑x

theorem AlgebraicIndependent.image {R : Type u_3} {A : Type u_5} [CommRing R] [CommRing A] [Algebra R A] {ι : Type u_9} {s : Set ι} {f : ι → A} (hs : AlgebraicIndependent R fun x => f ↑x) : AlgebraicIndependent R fun x => ↑x

theorem algebraicIndependent_iUnion_of_directed {R : Type u_3} {A : Type u_5} [CommRing R] [CommRing A] [Algebra R A] {η : Type u_9} [Nonempty η] {s : η → Set A} (hs : Directed (fun x x_1 => x ⊆ x_1) s) (h : ∀ (i : η), AlgebraicIndependent R Subtype.val) : AlgebraicIndependent R Subtype.val

theorem algebraicIndependent_sUnion_of_directed {R : Type u_3} {A : Type u_5} [CommRing R] [CommRing A] [Algebra R A] {s : Set (Set A)} (hsn : Set.Nonempty s) (hs : DirectedOn (fun x x_1 => x ⊆ x_1) s) (h : ∀ (a : Set A), a ∈ s → AlgebraicIndependent R Subtype.val) : AlgebraicIndependent R Subtype.val

theorem exists_maximal_algebraicIndependent {R : Type u_3} {A : Type u_5} [CommRing R] [CommRing A] [Algebra R A] (s : Set A) (t : Set A) (hst : s ⊆ t) (hs : AlgebraicIndependent R Subtype.val) : ∃ u, AlgebraicIndependent R Subtype.val ∧ s ⊆ u ∧ u ⊆ t ∧ ∀ (x : Set A), AlgebraicIndependent R Subtype.val → u ⊆ x → x ⊆ t → x = u

@[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), ↑(↑(AlgebraicIndependent.aevalEquiv hx) a) = ↑(MvPolynomial.aeval x) a

@[simp]

theorem AlgebraicIndependent.aevalEquiv_symm_apply {ι : 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 : { x // x ∈ Algebra.adjoin R (Set.range x) }), ↑(AlgEquiv.symm (AlgebraicIndependent.aevalEquiv hx)) a = ↑(Equiv.ofBijective ↑(AlgHom.codRestrict (MvPolynomial.aeval x) (Algebra.adjoin R (Set.range x)) (_ : ∀ (x : MvPolynomial ι R), ↑(MvPolynomial.aeval x) x ∈ Algebra.adjoin R (Set.range x))) (_ : Function.Injective ↑(AlgHom.codRestrict (MvPolynomial.aeval x) (Algebra.adjoin R (Set.range x)) (_ : ∀ (x : MvPolynomial ι R), ↑(MvPolynomial.aeval x) x ∈ Algebra.adjoin R (Set.range x))) ∧ Function.Surjective ↑(AlgHom.codRestrict (MvPolynomial.aeval x) (Algebra.adjoin R (Set.range x)) (_ : ∀ (x : MvPolynomial ι R), ↑(MvPolynomial.aeval x) x ∈ Algebra.adjoin R (Set.range x))))).symm a

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] { x // x ∈ Algebra.adjoin R (Set.range x) }

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

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 { x // x ∈ Algebra.adjoin R (Set.range x) } A) (↑(AlgebraicIndependent.aevalEquiv hx) 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) : { x // 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.

@[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 : { x // x ∈ Algebra.adjoin R (Set.range x) }) : ↑(MvPolynomial.aeval x) (↑(AlgebraicIndependent.repr hx) 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) : AlgHom.comp (MvPolynomial.aeval x) (AlgebraicIndependent.repr hx) = Subalgebra.val (Algebra.adjoin R (Set.range x))

theorem AlgebraicIndependent.repr_ker {ι : Type u_1} {R : Type u_3} {A : Type u_5} {x : ι → A} [CommRing R] [CommRing A] [Algebra R A] (hx : AlgebraicIndependent R x) : RingHom.ker ↑(AlgebraicIndependent.repr hx) = ⊥

def AlgebraicIndependent.mvPolynomialOptionEquivPolynomialAdjoin {ι : 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 (Option ι) R ≃+* Polynomial { x // x ∈ Algebra.adjoin R (Set.range x) }

The isomorphism between MvPolynomial (Option ι) R and the polynomial ring over the algebra generated by an algebraically independent family.

@[simp]

theorem AlgebraicIndependent.mvPolynomialOptionEquivPolynomialAdjoin_apply {ι : Type u_1} {R : Type u_3} {A : Type u_5} {x : ι → A} [CommRing R] [CommRing A] [Algebra R A] (hx : AlgebraicIndependent R x) (y : MvPolynomial (Option ι) R) : ↑(AlgebraicIndependent.mvPolynomialOptionEquivPolynomialAdjoin hx) y = Polynomial.map (↑(AlgebraicIndependent.aevalEquiv hx)) (↑(MvPolynomial.aeval fun o => Option.elim o Polynomial.X fun s => ↑Polynomial.C (MvPolynomial.X s)) y)

theorem AlgebraicIndependent.mvPolynomialOptionEquivPolynomialAdjoin_C {ι : Type u_1} {R : Type u_3} {A : Type u_5} {x : ι → A} [CommRing R] [CommRing A] [Algebra R A] (hx : AlgebraicIndependent R x) (r : R) : ↑(AlgebraicIndependent.mvPolynomialOptionEquivPolynomialAdjoin hx) (↑MvPolynomial.C r) = ↑Polynomial.C (↑(algebraMap R { x // x ∈ Algebra.adjoin R (Set.range x) }) r)

theorem AlgebraicIndependent.mvPolynomialOptionEquivPolynomialAdjoin_X_none {ι : 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.mvPolynomialOptionEquivPolynomialAdjoin hx) (MvPolynomial.X none) = Polynomial.X

theorem AlgebraicIndependent.mvPolynomialOptionEquivPolynomialAdjoin_X_some {ι : Type u_1} {R : Type u_3} {A : Type u_5} {x : ι → A} [CommRing R] [CommRing A] [Algebra R A] (hx : AlgebraicIndependent R x) (i : ι) : ↑(AlgebraicIndependent.mvPolynomialOptionEquivPolynomialAdjoin hx) (MvPolynomial.X (some i)) = ↑Polynomial.C (↑(AlgebraicIndependent.aevalEquiv hx) (MvPolynomial.X i))

theorem AlgebraicIndependent.aeval_comp_mvPolynomialOptionEquivPolynomialAdjoin {ι : 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 : A) : RingHom.comp (↑(Polynomial.aeval a)) (RingEquiv.toRingHom (AlgebraicIndependent.mvPolynomialOptionEquivPolynomialAdjoin hx)) = ↑(MvPolynomial.aeval fun o => Option.elim o a x)

theorem AlgebraicIndependent.option_iff {ι : 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 : A) : (AlgebraicIndependent R fun o => Option.elim o a x) ↔ ¬IsAlgebraic { x // x ∈ Algebra.adjoin R (Set.range x) } a

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.

theorem exists_isTranscendenceBasis (R : Type u_3) {A : Type u_5} [CommRing R] [CommRing A] [Algebra R A] (h : Function.Injective ↑(algebraMap R A)) : ∃ s, IsTranscendenceBasis R Subtype.val

theorem AlgebraicIndependent.isTranscendenceBasis_iff {ι : Type w} {R : Type u} [CommRing R] [Nontrivial R] {A : Type v} [CommRing A] [Algebra R A] {x : ι → A} (i : AlgebraicIndependent R x) : IsTranscendenceBasis R x ↔ ∀ (κ : Type v) (w : κ → A), AlgebraicIndependent R w → ∀ (j : ι → κ), w ∘ j = x → Function.Surjective j

theorem IsTranscendenceBasis.isAlgebraic {ι : Type u_1} {R : Type u_3} {A : Type u_5} {x : ι → A} [CommRing R] [CommRing A] [Algebra R A] [Nontrivial R] (hx : IsTranscendenceBasis R x) : Algebra.IsAlgebraic { x // x ∈ Algebra.adjoin R (Set.range x) } A

theorem algebraicIndependent_empty_type {ι : Type u_1} {K : Type u_4} {A : Type u_5} {x : ι → A} [CommRing A] [Field K] [Algebra K A] [IsEmpty ι] [Nontrivial A] : AlgebraicIndependent K x

theorem algebraicIndependent_empty {K : Type u_4} {A : Type u_5} [CommRing A] [Field K] [Algebra K A] [Nontrivial A] : AlgebraicIndependent K Subtype.val