Documentation

noncomputable def RatFunc.C {K : Type u} [CommRing K] [IsDomain K] :

K →+* RatFunc K

RatFunc.C a is the constant rational function a.

Instances For

@[simp]

theorem RatFunc.algebraMap_eq_C {K : Type u} [CommRing K] [IsDomain K] :

algebraMap K (RatFunc K) = C

@[simp]

theorem RatFunc.algebraMap_C {K : Type u} [CommRing K] [IsDomain K] (a : K) :

(algebraMap (Polynomial K) (RatFunc K)) (Polynomial.C a) = C a

@[simp]

theorem RatFunc.algebraMap_comp_C {K : Type u} [CommRing K] [IsDomain K] :

(algebraMap (Polynomial K) (RatFunc K)).comp Polynomial.C = C

theorem RatFunc.smul_eq_C_mul {K : Type u} [CommRing K] [IsDomain K] (r : K) (x : RatFunc K) :

r • x = C r * x

theorem RatFunc.C_injective {K : Type u} [CommRing K] [IsDomain K] :

Function.Injective ⇑C

noncomputable def RatFunc.X {K : Type u} [CommRing K] [IsDomain K] :

RatFunc K

RatFunc.X is the polynomial variable (aka indeterminate).

Instances For

@[simp]

theorem RatFunc.algebraMap_X {K : Type u} [CommRing K] [IsDomain K] :

(algebraMap (Polynomial K) (RatFunc K)) Polynomial.X = X

@[simp]

theorem RatFunc.algebraMap_monomial {K : Type u} [CommRing K] [IsDomain K] (n : ℕ) (a : K) :

(algebraMap (Polynomial K) (RatFunc K)) ((Polynomial.monomial n) a) = C a * X ^ n

@[simp]

theorem RatFunc.aeval_X_left_eq_algebraMap {K : Type u} [CommRing K] [IsDomain K] (p : Polynomial K) :

(Polynomial.aeval X) p = (algebraMap (Polynomial K) (RatFunc K)) p

@[simp]

theorem RatFunc.coePolynomial_eq_algebraMap {K : Type u} [CommRing K] [IsDomain K] (p : Polynomial K) :

↑p = (algebraMap (Polynomial K) (RatFunc K)) p

@[simp]

theorem RatFunc.liftRingHom_C {K : Type u} [CommRing K] [IsDomain K] {L : Type u_1} [Field L] (φ : Polynomial K →+* L) (hφ : nonZeroDivisors (Polynomial K) ≤ Submonoid.comap φ (nonZeroDivisors L)) (x : K) :

(liftRingHom φ hφ) (C x) = φ (Polynomial.C x)

@[simp]

theorem RatFunc.liftRingHom_X {K : Type u} [CommRing K] [IsDomain K] {L : Type u_1} [Field L] (φ : Polynomial K →+* L) (hφ : nonZeroDivisors (Polynomial K) ≤ Submonoid.comap φ (nonZeroDivisors L)) :

(liftRingHom φ hφ) X = φ Polynomial.X

@[simp]

theorem RatFunc.num_C {K : Type u} [Field K] (c : K) :

(C c).num = Polynomial.C c

@[simp]

theorem RatFunc.denom_C {K : Type u} [Field K] (c : K) :

(C c).denom = 1

@[simp]

theorem RatFunc.num_X {K : Type u} [Field K] :

X.num = Polynomial.X

@[simp]

theorem RatFunc.denom_X {K : Type u} [Field K] :

X.denom = 1

theorem RatFunc.X_ne_zero {K : Type u} [Field K] :

X ≠ 0

theorem RatFunc.eq_C_iff {K : Type u} [Field K] (f : RatFunc K) :

(∃ (c : K), f = C c) ↔ f.num.natDegree = 0 ∧ f.denom.natDegree = 0

noncomputable def RatFunc.eval {K : Type u} [Field K] {L : Type u} [Field L] (f : K →+* L) (a : L) (p : RatFunc K) :

Evaluate a rational function p given a ring hom f from the scalar field to the target and a value x for the variable in the target.

Fractions are reduced by clearing common denominators before evaluating: eval id 1 ((X^2 - 1) / (X - 1)) = eval id 1 (X + 1) = 2, not 0 / 0 = 0.

Instances For

theorem RatFunc.eval_eq_zero_of_eval₂_denom_eq_zero {K : Type u} [Field K] {L : Type u} [Field L] {f : K →+* L} {a : L} {x : RatFunc K} (h : Polynomial.eval₂ f a x.denom = 0) :

eval f a x = 0

theorem RatFunc.eval₂_denom_ne_zero {K : Type u} [Field K] {L : Type u} [Field L] {f : K →+* L} {a : L} {x : RatFunc K} (h : eval f a x ≠ 0) :

Polynomial.eval₂ f a x.denom ≠ 0

@[simp]

theorem RatFunc.eval_C {K : Type u} [Field K] {L : Type u} [Field L] (f : K →+* L) (a : L) {c : K} :

eval f a (C c) = f c

@[simp]

theorem RatFunc.eval_X {K : Type u} [Field K] {L : Type u} [Field L] (f : K →+* L) (a : L) :

eval f a X = a

@[simp]

theorem RatFunc.eval_zero {K : Type u} [Field K] {L : Type u} [Field L] (f : K →+* L) (a : L) :

eval f a 0 = 0

@[simp]

theorem RatFunc.eval_one {K : Type u} [Field K] {L : Type u} [Field L] (f : K →+* L) (a : L) :

eval f a 1 = 1

@[simp]

theorem RatFunc.eval_algebraMap {K : Type u} [Field K] {L : Type u} [Field L] (f : K →+* L) (a : L) {S : Type u_1} [CommSemiring S] [Algebra S (Polynomial K)] (p : S) :

eval f a ((algebraMap S (RatFunc K)) p) = Polynomial.eval₂ f a ((algebraMap S (Polynomial K)) p)

theorem RatFunc.eval_add {K : Type u} [Field K] {L : Type u} [Field L] (f : K →+* L) (a : L) {x y : RatFunc K} (hx : Polynomial.eval₂ f a x.denom ≠ 0) (hy : Polynomial.eval₂ f a y.denom ≠ 0) :

eval f a (x + y) = eval f a x + eval f a y

eval is an additive homomorphism except when a denominator evaluates to 0.

Counterexample: eval _ 1 (X / (X-1)) + eval _ 1 (-1 / (X-1)) = 0 ... ≠ 1 = eval _ 1 ((X-1) / (X-1)).

See also RatFunc.eval₂_denom_ne_zero to make the hypotheses simpler but less general.

theorem RatFunc.eval_mul {K : Type u} [Field K] {L : Type u} [Field L] (f : K →+* L) (a : L) {x y : RatFunc K} (hx : Polynomial.eval₂ f a x.denom ≠ 0) (hy : Polynomial.eval₂ f a y.denom ≠ 0) :

eval f a (x * y) = eval f a x * eval f a y

eval is a multiplicative homomorphism except when a denominator evaluates to 0.

Counterexample: eval _ 0 X * eval _ 0 (1/X) = 0 ≠ 1 = eval _ 0 1 = eval _ 0 (X * 1/X).

See also RatFunc.eval₂_denom_ne_zero to make the hypotheses simpler but less general.

noncomputable def RatFunc.algEquivOfTranscendental {K : Type u_1} {L : Type u_2} [Field K] [Field L] [Algebra K L] (f : L) (h : Transcendental K f) :

RatFunc K ≃ₐ[K] ↥K⟮f⟯

Given a transcendental f : L, the K-algebra isomorphism between RatFunc K and L given by sending X to f.

Instances For

@[simp]

theorem RatFunc.algEquivOfTranscendental_algebraMap {K : Type u_1} {L : Type u_2} [Field K] [Field L] [Algebra K L] (f : L) (h : Transcendental K f) (g : Polynomial K) :

(algEquivOfTranscendental f h) ((algebraMap (Polynomial K) (RatFunc K)) g) = (Polynomial.aeval (IntermediateField.AdjoinSimple.gen K f)) g

@[simp]

theorem RatFunc.algEquivOfTranscendental_X {K : Type u_1} {L : Type u_2} [Field K] [Field L] [Algebra K L] (f : L) (h : Transcendental K f) :

↑((algEquivOfTranscendental f h) X) = f

theorem RatFunc.algEquivOfTranscendental_apply {K : Type u_1} {L : Type u_2} [Field K] [Field L] [Algebra K L] (f : L) (h : Transcendental K f) (u : RatFunc K) :

↑((algEquivOfTranscendental f h) u) = (Polynomial.aeval f) u.num / (Polynomial.aeval f) u.denom

@[simp]

theorem RatFunc.algEquivOfTranscendental_symm_aeval {K : Type u_1} {L : Type u_2} [Field K] [Field L] [Algebra K L] (f : L) (h : Transcendental K f) (g : Polynomial K) :

(algEquivOfTranscendental f h).symm ((Polynomial.aeval (IntermediateField.AdjoinSimple.gen K f)) g) = (algebraMap (Polynomial K) (RatFunc K)) g

@[simp]

theorem RatFunc.algEquivOfTranscendental_symm_gen {K : Type u_1} {L : Type u_2} [Field K] [Field L] [Algebra K L] (f : L) (h : Transcendental K f) :

(algEquivOfTranscendental f h).symm (IntermediateField.AdjoinSimple.gen K f) = X

theorem RatFunc.transcendental_X {K : Type u} [CommRing K] [IsDomain K] :

Transcendental K X

instance RatFunc.transcendental {K : Type u} [CommRing K] [IsDomain K] :

Algebra.Transcendental K (RatFunc K)

def Polynomial.idealX (K : Type u_1) [Field K] :

IsDedekindDomain.HeightOneSpectrum (Polynomial K)

This is the principal ideal generated by X in the ring of polynomials over a field K, regarded as an element of the height-one-spectrum.

Instances For

@[simp]

theorem Polynomial.idealX_span (K : Type u_1) [Field K] :

(idealX K).asIdeal = Ideal.span {X}

@[simp]

theorem Polynomial.valuation_X_eq_neg_one (K : Type u_1) [Field K] :

(IsDedekindDomain.HeightOneSpectrum.valuation (RatFunc K) (idealX K)) RatFunc.X = WithZero.exp (-1)

theorem Polynomial.valuation_of_mk (K : Type u_1) [Field K] (f : Polynomial K) {g : Polynomial K} (hg : g ≠ 0) :

(IsDedekindDomain.HeightOneSpectrum.valuation (RatFunc K) (idealX K)) (RatFunc.mk f g) = (idealX K).intValuation f / (idealX K).intValuation g

theorem Polynomial.valuation_aeval_monomial_eq_valuation_pow (K : Type u_1) [Field K] {Γ : Type u_2} [LinearOrderedCommGroupWithZero Γ] (L : Type u_3) [Field L] [Algebra K L] {v : Valuation L Γ} [hv : Valuation.IsTrivialOn K v] (w : L) (n : ℕ) {a : K} (ha : a ≠ 0) :

v ((aeval w) ((monomial n) a)) = v w ^ n

theorem Polynomial.valuation_aeval_eq_valuation_X_pow_natDegree_of_one_lt_valuation_X (K : Type u_1) [Field K] {Γ : Type u_2} [LinearOrderedCommGroupWithZero Γ] (L : Type u_3) [Field L] [Algebra K L] {v : Valuation L Γ} [hv : Valuation.IsTrivialOn K v] (w : L) (hpos : 1 < v w) {p : Polynomial K} (hp : p ≠ 0) :

v ((aeval w) p) = v w ^ p.natDegree

theorem Polynomial.valuation_monomial_eq_valuation_X_pow (K : Type u_1) [Field K] {Γ : Type u_2} [LinearOrderedCommGroupWithZero Γ] {v : Valuation (RatFunc K) Γ} [hv : Valuation.IsTrivialOn K v] (n : ℕ) {a : K} (ha : a ≠ 0) :

v ↑((monomial n) a) = v RatFunc.X ^ n

If a valuation v is trivial on constants then for every n : ℕ the valuation of (monomial n a) is equal to (v RatFunc.X) ^ n.

theorem Polynomial.valuation_eq_valuation_X_pow_natDegree_of_one_lt_valuation_X (K : Type u_1) [Field K] {Γ : Type u_2} [LinearOrderedCommGroupWithZero Γ] {v : Valuation (RatFunc K) Γ} [hv : Valuation.IsTrivialOn K v] (hlt : 1 < v RatFunc.X) {p : Polynomial K} (hp : p ≠ 0) :

v ↑p = v RatFunc.X ^ p.natDegree

If a valuation v is trivial on constants and 1 < v RatFunc.X then for every polynomial p, v p = v RatFunc.X ^ p.natDegree.

Note: The condition 1 < v RatFunc.X is typically satisfied by the valuation at infinity.

theorem Polynomial.valuation_le_one_of_valuation_X_le_one (K : Type u_1) [Field K] {Γ : Type u_2} [LinearOrderedCommGroupWithZero Γ] {v : Valuation (RatFunc K) Γ} [hv : Valuation.IsTrivialOn K v] (hle : v RatFunc.X ≤ 1) (p : Polynomial K) :

v ↑p ≤ 1

If a valuation v is trivial on constants and v RatFunc.X ≤ 1 then for every polynomial p, v p ≤ 1.

theorem Polynomial.valuation_inv_monomial_eq_valuation_X_zpow (K : Type u_1) [Field K] {Γ : Type u_2} [LinearOrderedCommGroupWithZero Γ] {v : Valuation (RatFunc K) Γ} [hv : Valuation.IsTrivialOn K v] (n : ℕ) {a : K} (ha : a ≠ 0) :

v (1 / ↑((monomial n) a)) = v RatFunc.X ^ (-↑n)

If a valuation v is trivial on constants then for every n : ℕ the valuation of 1 / (monomial n a) (as an element of the field of rational functions) is equal to (v RatFunc.X) ^ (- n).