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

Define the transcendence degree and show it is independent of the choice of 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.

Equations

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

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).toRingHom = ⊥

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 : ↑s) => f ↑x) ↔ AlgebraicIndependent R fun (x : ↑(f '' s)) => ↑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 := ⋯ }

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 : { x : A // x ∈ s }) => ↑i) → s.card ≤ 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.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.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 ⊆ 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 : ↑s) => g (f ↑x)) : AlgebraicIndependent R fun (x : ↑(f '' s)) => 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 : ↑s) => f ↑x) : AlgebraicIndependent R fun (x : ↑(f '' s)) => ↑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 : Set A) => 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 : Set A) => x ⊆ x_1) s) (h : ∀ 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 : Set A), 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) (b : ↥(Algebra.adjoin R (Set.range x))) : (AlgEquiv.symm (AlgebraicIndependent.aevalEquiv hx)) b = Function.surjInv ⋯ b

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

• AlgebraicIndependent.aevalEquiv hx = AlgEquiv.ofBijective (AlgHom.codRestrict (MvPolynomial.aeval x) (Algebra.adjoin R (Set.range x)) ⋯) ⋯

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) ((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) : ↥(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

• AlgebraicIndependent.repr hx = ↑(AlgEquiv.symm (AlgebraicIndependent.aevalEquiv hx))

@[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) ((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 ↥(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.

Equations

• One or more equations did not get rendered due to their size.

@[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 ι) => 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 ↥(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 ι) => 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 ι) => Option.elim o a x) ↔ ¬IsAlgebraic (↥(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.

Equations

• IsTranscendenceBasis R x = (AlgebraicIndependent R x ∧ ∀ (s : Set A), AlgebraicIndependent R Subtype.val → Set.range x ≤ s → Set.range x = s)

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 : Set A), 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 (↥(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