Polynomials and adjoining transcendental elements

This file establishes some basic properties about R[s] when s is transcendental over R. These are mostly just carried over from the polynomial ring R[X].

Main definitions:

• Polynomial.algEquivOfTranscendental: Given a transcendental element s : S over R, the R-algebra equivalence between R[X] and R[s] given by sending X to s.
• Algebra.adjoin.evalOfTranscendental: If s : S is transcendental over R, we get an R-algebra homomorphism given by evaluation at some element c.

Main results

• Transcendental.euclideanDomainAdjoin: Given a transcendental element s : S over F, F[s] is a euclidean domain.
• Transcendental.uniqueFactorizationMonoid_adjoin: Given a transcendental element s : S over R, a unique factorization monoid, R[s] is a unique factorization monoid as well.

noncomputable def Polynomial.algEquivOfTranscendental (R : Type u_1) {S : Type u_2} [CommRing R] [Ring S] [Algebra R S] (s : S) (h : Transcendental R s) : Polynomial R ≃ₐ[R] ↥R[s]

Given a transcendental element s : S over R, the R-algebra equivalence between R[X] and R[s] given by sending X to s.

Equations

• Polynomial.algEquivOfTranscendental R s h = AlgEquiv.ofBijective (Polynomial.aeval ⟨s, ⋯⟩) ⋯

@[simp]

theorem Polynomial.algEquivOfTranscendental_coe {R : Type u_1} {S : Type u_2} [CommRing R] [Ring S] [Algebra R S] (s : S) (h : Transcendental R s) : ↑(algEquivOfTranscendental R s h) = ↑(aeval ⟨s, ⋯⟩)

@[simp]

theorem Polynomial.algEquivOfTranscendental_apply {R : Type u_1} {S : Type u_2} [CommRing R] [Ring S] [Algebra R S] (s : S) (h : Transcendental R s) (f : Polynomial R) : (algEquivOfTranscendental R s h) f = (aeval ⟨s, ⋯⟩) f

theorem Polynomial.algEquivOfTranscendental_apply_X {R : Type u_1} {S : Type u_2} [CommRing R] [Ring S] [Algebra R S] (s : S) (h : Transcendental R s) : (algEquivOfTranscendental R s h) X = ⟨s, ⋯⟩

@[simp]

theorem Polynomial.algEquivOfTranscendental_symm_aeval {R : Type u_1} {S : Type u_2} [CommRing R] [Ring S] [Algebra R S] (s : S) (h : Transcendental R s) (f : Polynomial R) : (algEquivOfTranscendental R s h).symm ((aeval ⟨s, ⋯⟩) f) = f

@[simp]

theorem Polynomial.algEquivOfTranscendental_symm_gen {R : Type u_1} {S : Type u_2} [CommRing R] [Ring S] [Algebra R S] (s : S) (h : Transcendental R s) : (algEquivOfTranscendental R s h).symm ⟨s, ⋯⟩ = X

noncomputable def Algebra.adjoin.evalOfTranscendental {R : Type u_1} {S : Type u_2} [CommRing R] [Ring S] [Algebra R S] (s : S) {T : Type u_3} [CommRing T] [Algebra R T] (ht : Transcendental R s) (c : T) : ↥R[s] →ₐ[R] T

If s : S is transcendental over R, we get an R-algebra homomorphism given by evaluation at some element c.

For the more general case where s is not nec. transcendental see Algebra.adjoin.liftSingleton.

Equations

• Algebra.adjoin.evalOfTranscendental s ht c = (Polynomial.aeval c).comp ↑(Polynomial.algEquivOfTranscendental R s ht).symm

@[simp]

theorem Algebra.adjoin.evalOfTranscendental_aeval {R : Type u_1} {S : Type u_2} [CommRing R] [Ring S] [Algebra R S] (s : S) {T : Type u_3} [CommRing T] [Algebra R T] {p : Polynomial R} (ht : Transcendental R s) (c : T) : (evalOfTranscendental s ht c) ((Polynomial.aeval ⟨s, ⋯⟩) p) = (Polynomial.aeval c) p

theorem Algebra.adjoin.evalOfTranscendental_eq_zero_iff {R : Type u_1} {S : Type u_2} [CommRing R] [Ring S] [Algebra R S] (s : S) (ht : Transcendental R s) (x : ↥R[s]) (c : R) : (evalOfTranscendental s ht c) x = 0 ↔ ⟨s, ⋯⟩ - (algebraMap R ↥R[s]) c ∣ x

Instances

We can not directly get the instances on R[s] from (h : Transcendental R s) because it is an explicit argument.

Since this can be cumbersome in a file where these instances are often needed, we also provide Fact versions that are instances.

@[reducible, inline]

noncomputable abbrev Transcendental.euclideanDomainAdjoin {S : Type u_2} [Ring S] {s : S} {F : Type u_3} [Field F] [Algebra F S] (h : Transcendental F s) : EuclideanDomain ↥F[s]

Given a transcendental element s : S over F, F[s] is a euclidean domain.

Equations

• h.euclideanDomainAdjoin = (Polynomial.algEquivOfTranscendental F s h).symm.toRingEquiv.euclideanDomain

@[instance_reducible]

noncomputable instance instEuclideanDomainSubtypeMemSubalgebraAdjoinSingletonSetOfFactTranscendental {S : Type u_2} [Ring S] {s : S} {F : Type u_3} [Field F] [Algebra F S] [h : Fact (Transcendental F s)] : EuclideanDomain ↥F[s]

Equations

• instEuclideanDomainSubtypeMemSubalgebraAdjoinSingletonSetOfFactTranscendental = ⋯.euclideanDomainAdjoin

theorem Transcendental.uniqueFactorizationMonoid_adjoin {R : Type u_1} {S : Type u_2} [CommRing R] [Ring S] [Algebra R S] {s : S} [UniqueFactorizationMonoid R] (h : Transcendental R s) : UniqueFactorizationMonoid ↥R[s]

Given a transcendental element s : S over R, a unique factorization monoid, R[s] is a unique factorization monoid as well.

instance instUniqueFactorizationMonoidSubtypeMemSubalgebraAdjoinSingletonSetOfFactTranscendental {R : Type u_1} {S : Type u_2} [CommRing R] [Ring S] [Algebra R S] {s : S} [UniqueFactorizationMonoid R] [h : Fact (Transcendental R s)] : UniqueFactorizationMonoid ↥R[s]

theorem Transcendental.wfDvdMonoid_adjoin {R : Type u_1} {S : Type u_2} [CommRing R] [Ring S] [Algebra R S] {s : S} [UniqueFactorizationMonoid R] (ht : Transcendental R s) : WfDvdMonoid ↥R[s]