Algebraic Independence #
This file defines algebraic independence of a family of element of an R algebra.
Main definitions #
AlgebraicIndependent-AlgebraicIndependent R xstates the family of elementsxis algebraically independent overR, 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 #
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]
:
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
Instances For
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
@[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)
@[simp]
theorem
algebraicIndependent_unique_type_iff
{ι : Type u_1}
{R : Type u_3}
{A : Type u_5}
{x : ι → A}
[CommRing R]
[CommRing A]
[Algebra R A]
[Unique ι]
:
AlgebraicIndependent R x ↔ Transcendental R (x default)
A one-element family x is algebraically independent if and only if
its element is transcendental.
theorem
algebraicIndependent_iff_transcendental
{R : Type u_3}
{A : Type u_5}
[CommRing R]
[CommRing A]
[Algebra R A]
{x : A}
:
AlgebraicIndependent R ![x] ↔ Transcendental R x
The one-element family ![x] is algebraically independent if and only if
x is transcendental.
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)
:
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]
:
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.transcendental
{ι : 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 : ι)
:
Transcendental R (x i)
If a family x is algebraically independent, then any of its element is transcendental.
theorem
MvPolynomial.algebraicIndependent_X
(σ : Type u_7)
(R : Type u_8)
[CommRing R]
:
AlgebraicIndependent R MvPolynomial.X
theorem
MvPolynomial.transcendental_X
{σ : Type u_7}
(R : Type u_8)
[CommRing R]
(i : σ)
:
Transcendental R (MvPolynomial.X i)
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]
:
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_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_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 : ι) => ⟨x i, ⋯⟩
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_7}
[CommRing K]
[Algebra R K]
[Algebra K A]
[IsScalarTower R K A]
(hinj : Function.Injective ⇑(algebraMap R K))
(ai : AlgebraicIndependent K 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 (s.restrict 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_7}
{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_7}
{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, t.Finite → 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_7}
{ι' : Type u_8}
(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_7}
{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_7}
[Nonempty η]
{s : η → Set A}
(hs : Directed (fun (x1 x2 : Set A) => x1 ⊆ x2) 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 : s.Nonempty)
(hs : DirectedOn (fun (x1 x2 : Set A) => x1 ⊆ x2) s)
(h : ∀ a ∈ s, 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.ofBijective ((MvPolynomial.aeval x).codRestrict (Algebra.adjoin R (Set.range x)) ⋯) ⋯
Instances For
@[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)))
:
hx.aevalEquiv.symm b = Function.surjInv ⋯ b
@[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
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
Instances For
@[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
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 ↑hx.repr = ⊥
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
- hx.mvPolynomialOptionEquivPolynomialAdjoin = (MvPolynomial.optionEquivLeft R ι).toRingEquiv.trans (Polynomial.mapEquiv hx.aevalEquiv.toRingEquiv)
Instances For
@[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)
:
hx.mvPolynomialOptionEquivPolynomialAdjoin y = Polynomial.map (↑hx.aevalEquiv)
((MvPolynomial.aeval fun (o : Option ι) => o.elim Polynomial.X fun (s : ι) => Polynomial.C (MvPolynomial.X s)) y)
@[simp]
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)
:
Polynomial.C (hx.aevalEquiv (MvPolynomial.C r)) = Polynomial.C ((algebraMap R ↥(Algebra.adjoin R (Set.range x))) r)
simp-normal form of mvPolynomialOptionEquivPolynomialAdjoin_C
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)
:
hx.mvPolynomialOptionEquivPolynomialAdjoin (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)
:
hx.mvPolynomialOptionEquivPolynomialAdjoin (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 : ι)
:
hx.mvPolynomialOptionEquivPolynomialAdjoin (MvPolynomial.X (some i)) = Polynomial.C (hx.aevalEquiv (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)
:
(↑(Polynomial.aeval a)).comp hx.mvPolynomialOptionEquivPolynomialAdjoin.toRingHom = ↑(MvPolynomial.aeval fun (o : Option ι) => o.elim 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 ι) => o.elim a x) ↔ Transcendental (↥(Algebra.adjoin R (Set.range x))) a
theorem
algebraicIndependent_of_finite'
{R : Type u_3}
{A : Type u_5}
[CommRing R]
[CommRing A]
[Algebra R A]
(s : Set A)
(hinj : Function.Injective ⇑(algebraMap R A))
(H : ∀ t ⊆ s, t.Finite → ∀ a ∈ s, a ∉ t → Transcendental (↥(Algebra.adjoin R t)) a)
:
AlgebraicIndependent R Subtype.val
Variant of algebraicIndependent_of_finite using Transcendental.
def
IsTranscendenceBasis
{ι : Type u_1}
(R : Type u_3)
{A : Type u_5}
[CommRing R]
[CommRing A]
[Algebra R A]
(x : ι → A)
:
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)
Instances For
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
exists_isTranscendenceBasis'
(R : Type u)
{A : Type v}
[CommRing R]
[CommRing A]
[Algebra R A]
(h : Function.Injective ⇑(algebraMap R A))
:
∃ (ι : Type v) (x : ι → A), IsTranscendenceBasis R x
Type version of exists_isTranscendenceBasis.
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]
:
theorem
algebraicIndependent_empty
{K : Type u_4}
{A : Type u_5}
[CommRing A]
[Field K]
[Algebra K A]
[Nontrivial A]
:
AlgebraicIndependent K Subtype.val