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.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 ofAlgebraicIndependent.aevalEquiv.AlgebraicIndependent.aevalEquivField- The canonical isomorphism from the rational function field ring to the intermediate field generated by an algebraic independent family.AlgebraicIndependent.reprField- The canonical map from the intermediate field generated by an algebraic independent family into the rational function field. It is the inverse ofAlgebraicIndependent.aevalEquivField.IsTranscendenceBasis R x- a familyxis a transcendence basis overRif it is a maximal algebraically independent subset.
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
AlgebraicIndependent.aeval_of_algebraicIndependent
{ι : Type u_1}
{R : Type u_3}
{A : Type u_5}
{x : ι → A}
[CommRing R]
[CommRing A]
[Algebra R A]
(hx : AlgebraicIndependent R x)
{f : ι → MvPolynomial ι R}
(hf : AlgebraicIndependent R f)
:
AlgebraicIndependent R fun (i : ι) => (MvPolynomial.aeval x) (f i)
If x = {x_i : A | i : ι} and f = {f_i : MvPolynomial ι R | i : ι} are algebraically
independent over R, then {f_i(x) | i : ι} is also algebraically independent over R.
For the partial converse, see AlgebraicIndependent.of_aeval.
theorem
AlgebraicIndependent.of_aeval
{ι : Type u_1}
{R : Type u_3}
{A : Type u_5}
{x : ι → A}
[CommRing R]
[CommRing A]
[Algebra R A]
{f : ι → MvPolynomial ι R}
(H : AlgebraicIndependent R fun (i : ι) => (MvPolynomial.aeval x) (f i))
:
If {f_i(x) | i : ι} is algebraically independent over R, then
{f_i : MvPolynomial ι R | i : ι} is also algebraically independent over R.
In fact, the x = {x_i : A | i : ι} is also transcendental over R provided that R
is a field and ι is finite; the proof needs transcendence degree.
theorem
AlgebraicIndependent.isEmpty_of_isAlgebraic
{ι : 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.IsAlgebraic R A]
:
IsEmpty ι
If A/R is algebraic, then all algebraically independent families are empty.
theorem
MvPolynomial.algebraicIndependent_X
(σ : Type u_7)
(R : Type u_8)
[CommRing R]
:
AlgebraicIndependent R MvPolynomial.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]
:
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.of_ringHom_of_comp_eq
{ι : Type u_1}
{R : Type u_3}
{A : Type u_5}
{x : ι → A}
[CommRing R]
[CommRing A]
[Algebra R A]
{S : Type u_7}
{B : Type u_8}
{FRS : Type u_9}
{FAB : Type u_10}
[CommRing S]
[CommRing B]
[Algebra S B]
[FunLike FRS R S]
[RingHomClass FRS R S]
[FunLike FAB A B]
[RingHomClass FAB A B]
(f : FRS)
(g : FAB)
(H : AlgebraicIndependent S (⇑g ∘ x))
(hf : Function.Injective ⇑f)
(h : (algebraMap S B).comp ↑f = (↑g).comp (algebraMap R A))
:
theorem
AlgebraicIndependent.ringHom_of_comp_eq
{ι : Type u_1}
{R : Type u_3}
{A : Type u_5}
{x : ι → A}
[CommRing R]
[CommRing A]
[Algebra R A]
{S : Type u_7}
{B : Type u_8}
{FRS : Type u_9}
{FAB : Type u_10}
[CommRing S]
[CommRing B]
[Algebra S B]
[FunLike FRS R S]
[RingHomClass FRS R S]
[FunLike FAB A B]
[RingHomClass FAB A B]
(f : FRS)
(g : FAB)
(H : AlgebraicIndependent R x)
(hf : Function.Surjective ⇑f)
(hg : Function.Injective ⇑g)
(h : (algebraMap S B).comp ↑f = (↑g).comp (algebraMap R A))
:
AlgebraicIndependent S (⇑g ∘ x)
theorem
algebraicIndependent_ringHom_iff_of_comp_eq
{ι : Type u_1}
{R : Type u_3}
{A : Type u_5}
{x : ι → A}
[CommRing R]
[CommRing A]
[Algebra R A]
{S : Type u_7}
{B : Type u_8}
{FRS : Type u_9}
{FAB : Type u_10}
[CommRing S]
[CommRing B]
[Algebra S B]
[EquivLike FRS R S]
[RingEquivClass FRS R S]
[FunLike FAB A B]
[RingHomClass FAB A B]
(f : FRS)
(g : FAB)
(hg : Function.Injective ⇑g)
(h : (algebraMap S B).comp ↑f = (↑g).comp (algebraMap R A))
:
AlgebraicIndependent S (⇑g ∘ x) ↔ AlgebraicIndependent R x
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 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.ofInjective (MvPolynomial.aeval x) ⋯).trans ((MvPolynomial.aeval x).range.equivOfEq (Algebra.adjoin R (Set.range x)) ⋯)
Instances For
@[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.aevalEquivField
{ι : Type u_1}
{F : Type u_7}
{E : Type u_8}
{x : ι → E}
[Field F]
[Field E]
[Algebra F E]
(hx : AlgebraicIndependent F x)
:
FractionRing (MvPolynomial ι F) ≃ₐ[F] ↥(IntermediateField.adjoin F (Set.range x))
Canonical isomorphism between rational function field and the intermediate field generated by algebraically independent elements.
Equations
- hx.aevalEquivField = (let_fun this := AlgEquiv.ofInjectiveField (IsFractionRing.liftAlgHom ⋯); this).trans (IntermediateField.equivOfEq ⋯)
Instances For
@[simp]
theorem
AlgebraicIndependent.aevalEquivField_apply_coe
{ι : Type u_1}
{F : Type u_7}
{E : Type u_8}
{x : ι → E}
[Field F]
[Field E]
[Algebra F E]
(hx : AlgebraicIndependent F x)
(a : FractionRing (MvPolynomial ι F))
:
↑(hx.aevalEquivField a) = (IsFractionRing.lift ⋯) a
theorem
AlgebraicIndependent.aevalEquivField_algebraMap_apply_coe
{ι : Type u_1}
{F : Type u_7}
{E : Type u_8}
{x : ι → E}
[Field F]
[Field E]
[Algebra F E]
(hx : AlgebraicIndependent F x)
(a : MvPolynomial ι F)
:
↑(hx.aevalEquivField ((algebraMap (MvPolynomial ι F) (FractionRing (MvPolynomial ι F))) a)) = (MvPolynomial.aeval x) a
def
AlgebraicIndependent.reprField
{ι : Type u_1}
{F : Type u_7}
{E : Type u_8}
{x : ι → E}
[Field F]
[Field E]
[Algebra F E]
(hx : AlgebraicIndependent F x)
:
↥(IntermediateField.adjoin F (Set.range x)) →ₐ[F] FractionRing (MvPolynomial ι F)
The canonical map from the intermediate field generated by an algebraic independent family into the rational function field.
Equations
- hx.reprField = ↑hx.aevalEquivField.symm
Instances For
@[simp]
theorem
AlgebraicIndependent.lift_reprField
{ι : Type u_1}
{F : Type u_7}
{E : Type u_8}
{x : ι → E}
[Field F]
[Field E]
[Algebra F E]
(hx : AlgebraicIndependent F x)
(p : ↥(IntermediateField.adjoin F (Set.range x)))
:
(IsFractionRing.lift ⋯) (hx.reprField p) = ↑p
theorem
AlgebraicIndependent.liftAlgHom_comp_reprField
{ι : Type u_1}
{F : Type u_7}
{E : Type u_8}
{x : ι → E}
[Field F]
[Field E]
[Algebra F E]
(hx : AlgebraicIndependent F x)
:
(IsFractionRing.liftAlgHom ⋯).comp hx.reprField = (IntermediateField.adjoin F (Set.range x)).val
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.
theorem
algebraicIndependent_of_finite_type'
{ι : Type u_1}
{R : Type u_3}
{A : Type u_5}
{x : ι → A}
[CommRing R]
[CommRing A]
[Algebra R A]
(hinj : Function.Injective ⇑(algebraMap R A))
(H : ∀ (t : Set ι), t.Finite → ∀ i ∉ t, Transcendental (↥(Algebra.adjoin R (x '' t))) (x i))
:
Type version of algebraicIndependent_of_finite'.
theorem
MvPolynomial.algebraicIndependent_polynomial_aeval_X
{ι : Type u_1}
{R : Type u_3}
[CommRing R]
(f : ι → Polynomial R)
(hf : ∀ (i : ι), Transcendental R (f i))
:
AlgebraicIndependent R fun (i : ι) => (Polynomial.aeval (MvPolynomial.X i)) (f i)
If for each i : ι, f_i : R[X] is transcendental over R, then {f_i(X_i) | i : ι}
in MvPolynomial ι R is algebraically independent over R.
theorem
AlgebraicIndependent.polynomial_aeval_of_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)
{f : ι → Polynomial R}
(hf : ∀ (i : ι), Transcendental R (f i))
:
AlgebraicIndependent R fun (i : ι) => (Polynomial.aeval (x i)) (f i)
If {x_i : A | i : ι} is algebraically independent over R, and for each i,
f_i : R[X] is transcendental over R, then {f_i(x_i) | i : ι} is also
algebraically independent over R.
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
IsTranscendenceBasis.isEmpty_iff_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)
:
IsEmpty ι ↔ Algebra.IsAlgebraic R A
If x is a transcendence basis of A/R, then it is empty if and only if
A/R is algebraic.
theorem
IsTranscendenceBasis.nonempty_iff_transcendental
{ι : 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)
:
Nonempty ι ↔ Algebra.Transcendental R A
If x is a transcendence basis of A/R, then it is not empty if and only if
A/R is transcendental.
theorem
IsTranscendenceBasis.isAlgebraic_field
{ι : Type u_1}
{F : Type u_7}
{E : Type u_8}
{x : ι → E}
[Field F]
[Field E]
[Algebra F E]
(hx : IsTranscendenceBasis F x)
:
Algebra.IsAlgebraic (↥(IntermediateField.adjoin F (Set.range x))) E
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
theorem
IsTranscendenceBasis.lift_cardinalMk_eq_max_lift
{F : Type u}
{E : Type v}
[CommRing F]
[Nontrivial F]
[CommRing E]
[IsDomain E]
[Algebra F E]
{ι : Type w}
{x : ι → E}
[Nonempty ι]
(hx : IsTranscendenceBasis F x)
:
theorem
IsTranscendenceBasis.lift_rank_eq_max_lift
{F : Type u}
{E : Type v}
[Field F]
[Field E]
[Algebra F E]
{ι : Type w}
{x : ι → E}
[Nonempty ι]
(hx : IsTranscendenceBasis F x)
:
theorem
Algebra.Transcendental.rank_eq_cardinalMk
(F : Type u)
(E : Type v)
[Field F]
[Field E]
[Algebra F E]
[Algebra.Transcendental F E]
:
Module.rank F E = Cardinal.mk E
theorem
IntermediateField.rank_sup_le
{F : Type u}
{E : Type v}
[Field F]
[Field E]
[Algebra F E]
(A B : IntermediateField F E)
:
Module.rank F ↥(A ⊔ B) ≤ Module.rank F ↥A * Module.rank F ↥B