Documentation

theorem algebraicIndependent_iff_ker_eq_bot {ι : Type u} {R : Type u_2} {A : Type v} {x : ι → A} [CommRing R] [CommRing A] [Algebra R A] :

AlgebraicIndependent R x ↔ RingHom.ker (MvPolynomial.aeval x).toRingHom = ⊥

@[simp]

theorem algebraicIndependent_empty_type_iff {ι : Type u} {R : Type u_2} {A : Type v} {x : ι → A} [CommRing R] [CommRing A] [Algebra R A] [IsEmpty ι] :

AlgebraicIndependent R x ↔ Function.Injective ⇑(algebraMap R A)

instance instNonemptySubtypeSetAlgebraicIndepOnIdOfFaithfulSMul {R : Type u_2} {A : Type v} [CommRing R] [CommRing A] [Algebra R A] [FaithfulSMul R A] :

Nonempty { s : Set A // AlgebraicIndepOn R id s }

theorem AlgebraicIndependent.algebraMap_injective {ι : Type u} {R : Type u_2} {A : Type v} {x : ι → A} [CommRing R] [CommRing A] [Algebra R A] (hx : AlgebraicIndependent R x) :

Function.Injective ⇑(algebraMap R A)

theorem AlgebraicIndependent.linearIndependent {ι : Type u} {R : Type u_2} {A : Type v} {x : ι → A} [CommRing R] [CommRing A] [Algebra R A] (hx : AlgebraicIndependent R x) :

LinearIndependent R x

theorem AlgebraicIndependent.injective {ι : Type u} {R : Type u_2} {A : Type v} {x : ι → A} [CommRing R] [CommRing A] [Algebra R A] (hx : AlgebraicIndependent R x) [Nontrivial R] :

Function.Injective x

theorem AlgebraicIndependent.ne_zero {ι : Type u} {R : Type u_2} {A : Type v} {x : ι → A} [CommRing R] [CommRing A] [Algebra R A] (hx : AlgebraicIndependent R x) [Nontrivial R] (i : ι) :

x i ≠ 0

theorem AlgebraicIndependent.map {ι : Type u} {R : Type u_2} {A : Type v} {A' : Type v'} {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} {R : Type u_2} {A : Type v} {A' : Type v'} {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.aeval_of_algebraicIndependent {ι : Type u} {R : Type u_2} {A : Type v} {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} {R : Type u_2} {A : Type v} {x : ι → A} [CommRing R] [CommRing A] [Algebra R A] {f : ι → MvPolynomial ι R} (H : AlgebraicIndependent R fun (i : ι) => (MvPolynomial.aeval x) (f i)) :

AlgebraicIndependent R f

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 isEmpty_algebraicIndependent {R : Type u_2} {A : Type v} [CommRing R] [CommRing A] [Algebra R A] (h : ¬Function.Injective ⇑(algebraMap R A)) :

IsEmpty { s : Set A // AlgebraicIndepOn R id s }

theorem trdeg_eq_zero_of_not_injective {R : Type u_2} {A : Type v} [CommRing R] [CommRing A] [Algebra R A] (h : ¬Function.Injective ⇑(algebraMap R A)) :

Algebra.trdeg R A = 0

theorem MvPolynomial.algebraicIndependent_X (σ : Type u_3) (R : Type u_4) [CommRing R] :

AlgebraicIndependent R X

theorem AlgHom.algebraicIndependent_iff {ι : Type u} {R : Type u_2} {A : Type v} {A' : Type v'} {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} {R : Type u_2} {A : Type v} {x : ι → A} [CommRing R] [CommRing A] [Algebra R A] [Subsingleton R] :

theorem isTranscendenceBasis_iff_of_subsingleton {ι : Type u} {R : Type u_2} {A : Type v} [CommRing R] [CommRing A] [Algebra R A] [Subsingleton R] (x : ι → A) :

IsTranscendenceBasis R x ↔ Nonempty ι

theorem IsTranscendenceBasis.of_subsingleton {ι : Type u} {R : Type u_2} {A : Type v} {x : ι → A} [CommRing R] [CommRing A] [Algebra R A] [Subsingleton R] [Nonempty ι] :

IsTranscendenceBasis R x

theorem trdeg_subsingleton {R : Type u_2} {A : Type v} [CommRing R] [CommRing A] [Algebra R A] [Subsingleton R] :

Algebra.trdeg R A = 1

theorem algebraicIndependent_adjoin {ι : Type u} {R : Type u_2} {A : Type v} {x : ι → A} [CommRing R] [CommRing A] [Algebra R A] (hs : AlgebraicIndependent R x) :

AlgebraicIndependent R fun (i : ι) => ⟨x i, ⋯⟩

theorem AlgebraicIndependent.restrictScalars {ι : Type u} {R : Type u_2} {A : Type v} {x : ι → A} [CommRing R] [CommRing A] [Algebra R A] {K : Type u_3} [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} {R : Type u_2} {A : Type v} {x : ι → A} [CommRing R] [CommRing A] [Algebra R A] {S : Type u_3} {B : Type u_4} {FRS : Type u_5} {FAB : Type u_6} [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} {R : Type u_2} {A : Type v} {x : ι → A} [CommRing R] [CommRing A] [Algebra R A] {S : Type u_3} {B : Type u_4} {FRS : Type u_5} {FAB : Type u_6} [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} {R : Type u_2} {A : Type v} {x : ι → A} [CommRing R] [CommRing A] [Algebra R A] {S : Type u_3} {B : Type u_4} {FRS : Type u_5} {FAB : Type u_6} [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_2} {A : Type v} [CommRing R] [CommRing A] [Algebra R A] (s : Set A) (li : AlgebraicIndependent R Subtype.val) (t : Finset ↑s) :

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

theorem algebraicIndependent_bounded_of_finset_algebraicIndependent_bounded {R : Type u_2} {A : Type v} [CommRing R] [CommRing A] [Algebra R A] {n : ℕ} (H : ∀ (s : Finset A), (AlgebraicIndependent R fun (i : ↥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} {R : Type u_2} {A : Type v} {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_2) (A : Type v) [CommRing R] [CommRing A] [Algebra R A] :

AlgebraicIndependent R Subtype.val ↔ Function.Injective ⇑(algebraMap R A)

theorem AlgebraicIndependent.to_subtype_range {ι : Type u} {R : Type u_2} {A : Type v} {x : ι → A} [CommRing R] [CommRing A] [Algebra R A] (hx : AlgebraicIndependent R x) :

theorem AlgebraicIndependent.to_subtype_range' {ι : Type u} {R : Type u_2} {A : Type v} {x : ι → A} [CommRing R] [CommRing A] [Algebra R A] (hx : AlgebraicIndependent R x) {t : Set A} (ht : Set.range x = t) :

IsTranscendenceBasis R Subtype.val

theorem IsTranscendenceBasis.to_subtype_range {ι : Type u} {R : Type u_2} {A : Type v} {x : ι → A} [CommRing R] [CommRing A] [Algebra R A] (hx : IsTranscendenceBasis R x) :

IsTranscendenceBasis R Subtype.val

theorem IsTranscendenceBasis.to_subtype_range' {ι : Type u} {R : Type u_2} {A : Type v} {x : ι → A} [CommRing R] [CommRing A] [Algebra R A] (hx : IsTranscendenceBasis R x) {t : Set A} (ht : Set.range x = t) :

theorem IsTranscendenceBasis.of_comp {ι : Type u} {R : Type u_2} {A : Type v} {A' : Type v'} [CommRing R] [CommRing A] [CommRing A'] [Algebra R A] [Algebra R A'] {x : ι → A} (f : A →ₐ[R] A') (h : Function.Injective ⇑f) (H : IsTranscendenceBasis R (⇑f ∘ x)) :

IsTranscendenceBasis R x

theorem IsTranscendenceBasis.of_comp_algebraMap {ι : Type u} {R : Type u_2} {A : Type v} {A' : Type v'} [CommRing R] [CommRing A] [CommRing A'] [Algebra R A] [Algebra R A'] [Algebra A A'] [IsScalarTower R A A'] [FaithfulSMul A A'] {x : ι → A} (H : IsTranscendenceBasis R (⇑(algebraMap A A') ∘ x)) :

IsTranscendenceBasis R x

theorem AlgEquiv.isTranscendenceBasis {ι : Type u} {R : Type u_2} {A : Type v} {A' : Type v'} {x : ι → A} [CommRing R] [CommRing A] [CommRing A'] [Algebra R A] [Algebra R A'] (e : A ≃ₐ[R] A') (hx : IsTranscendenceBasis R x) :

IsTranscendenceBasis R (⇑e ∘ x)

Also see IsTranscendenceBasis.algebraMap_comp for the composition with an algebraic extension.

theorem AlgEquiv.isTranscendenceBasis_iff {ι : Type u} {R : Type u_2} {A : Type v} {A' : Type v'} {x : ι → A} [CommRing R] [CommRing A] [CommRing A'] [Algebra R A] [Algebra R A'] (e : A ≃ₐ[R] A') :

IsTranscendenceBasis R (⇑e ∘ x) ↔ IsTranscendenceBasis R x

theorem AlgebraicIndependent.lift_cardinalMk_le_trdeg {ι : Type u} {R : Type u_2} {A : Type v} {x : ι → A} [CommRing R] [CommRing A] [Algebra R A] [Nontrivial R] (hx : AlgebraicIndependent R x) :

Cardinal.lift.{v, u} (Cardinal.mk ι) ≤ Cardinal.lift.{u, v} (Algebra.trdeg R A)

theorem AlgebraicIndependent.cardinalMk_le_trdeg {R : Type u_2} {A : Type v} [CommRing R] [CommRing A] [Algebra R A] [Nontrivial R] {ι : Type v} {x : ι → A} (hx : AlgebraicIndependent R x) :

Cardinal.mk ι ≤ Algebra.trdeg R A

theorem lift_trdeg_le_of_injective {R : Type u_2} {A : Type v} {A' : Type v'} [CommRing R] [CommRing A] [CommRing A'] [Algebra R A] [Algebra R A'] (f : A →ₐ[R] A') (hf : Function.Injective ⇑f) :

Cardinal.lift.{v', v} (Algebra.trdeg R A) ≤ Cardinal.lift.{v, v'} (Algebra.trdeg R A')

theorem trdeg_le_of_injective {R : Type u_2} {A : Type v} [CommRing R] [CommRing A] [Algebra R A] {A' : Type v} [CommRing A'] [Algebra R A'] (f : A →ₐ[R] A') (hf : Function.Injective ⇑f) :

Algebra.trdeg R A ≤ Algebra.trdeg R A'

theorem lift_trdeg_le_of_surjective {R : Type u_2} {A : Type v} {A' : Type v'} [CommRing R] [CommRing A] [CommRing A'] [Algebra R A] [Algebra R A'] (f : A →ₐ[R] A') (hf : Function.Surjective ⇑f) :

Cardinal.lift.{v, v'} (Algebra.trdeg R A') ≤ Cardinal.lift.{v', v} (Algebra.trdeg R A)

theorem trdeg_le_of_surjective {R : Type u_2} {A : Type v} [CommRing R] [CommRing A] [Algebra R A] {A' : Type v} [CommRing A'] [Algebra R A'] (f : A →ₐ[R] A') (hf : Function.Surjective ⇑f) :

Algebra.trdeg R A' ≤ Algebra.trdeg R A

theorem AlgEquiv.lift_trdeg_eq {R : Type u_2} {A : Type v} {A' : Type v'} [CommRing R] [CommRing A] [CommRing A'] [Algebra R A] [Algebra R A'] (e : A ≃ₐ[R] A') :

Cardinal.lift.{v', v} (Algebra.trdeg R A) = Cardinal.lift.{v, v'} (Algebra.trdeg R A')

theorem AlgEquiv.trdeg_eq {R : Type u_2} {A : Type v} [CommRing R] [CommRing A] [Algebra R A] {A' : Type v} [CommRing A'] [Algebra R A'] (e : A ≃ₐ[R] A') :

Algebra.trdeg R A = Algebra.trdeg R A'

theorem algebraicIndependent_comp_subtype {ι : Type u} {R : Type u_2} {A : Type v} {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_2} {A : Type v} [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_2} {A : Type v} [CommRing R] [CommRing A] [Algebra R A] (s : Set A) (H : ∀ t ⊆ s, t.Finite → AlgebraicIndependent R Subtype.val) :

theorem algebraicIndependent_of_finite_type {ι : Type u} {R : Type u_2} {A : Type v} {x : ι → A} [CommRing R] [CommRing A] [Algebra R A] (H : ∀ (t : Set ι), t.Finite → AlgebraicIndependent R fun (i : ↑t) => x ↑i) :

theorem AlgebraicIndependent.image_of_comp {R : Type u_2} {A : Type v} [CommRing R] [CommRing A] [Algebra R A] {ι : Type u_3} {ι' : Type u_4} (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_2} {A : Type v} [CommRing R] [CommRing A] [Algebra R A] {ι : Type u_3} {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_2} {A : Type v} [CommRing R] [CommRing A] [Algebra R A] {η : Type u_3} [Nonempty η] {s : η → Set A} (hs : Directed (fun (x1 x2 : Set A) => x1 ⊆ x2) s) (h : ∀ (i : η), AlgebraicIndependent R Subtype.val) :

theorem algebraicIndependent_sUnion_of_directed {R : Type u_2} {A : Type v} [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) :

theorem exists_maximal_algebraicIndependent {R : Type u_2} {A : Type v} [CommRing R] [CommRing A] [Algebra R A] (s t : Set A) (hst : s ⊆ t) (hs : AlgebraicIndepOn R id s) :

∃ (u : Set A), s ⊆ u ∧ Maximal (fun (x : Set A) => AlgebraicIndepOn R id x ∧ x ⊆ t) u

theorem AlgebraicIndependent.repr_ker {ι : Type u} {R : Type u_2} {A : Type v} {x : ι → A} [CommRing R] [CommRing A] [Algebra R A] (hx : AlgebraicIndependent R x) :

RingHom.ker ↑hx.repr = ⊥

noncomputable def AlgebraicIndependent.mvPolynomialOptionEquivPolynomialAdjoin {ι : Type u} {R : Type u_2} {A : Type v} {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} {R : Type u_2} {A : Type v} {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} {R : Type u_2} {A : Type v} {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} {R : Type u_2} {A : Type v} {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} {R : Type u_2} {A : Type v} {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} {R : Type u_2} {A : Type v} {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} {R : Type u_2} {A : Type v} {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_empty_type {ι : Type u} {A : Type v} {x : ι → A} [CommRing A] {K : Type u_3} [Field K] [Algebra K A] [IsEmpty ι] [Nontrivial A] :

AlgebraicIndependent K x