Intermediate Fields of Rational Function Fields

Results relating IntermediateField and RatFunc.

theorem RatFunc.adjoin_X {K : Type u_1} [Field K] : K⟮X⟯ = ⊤

theorem RatFunc.IntermediateField.adjoin_X {K : Type u_1} [Field K] (E : IntermediateField K (RatFunc K)) : (↥E)⟮X⟯ = ⊤

noncomputable def RatFunc.IntermediateField.adjoinXEquiv {K : Type u_1} [Field K] (E : IntermediateField K (RatFunc K)) : ↥(↥E)⟮X⟯ ≃ₐ[↥E] RatFunc K

The equivalence between E⟮X⟯ and K⟮X⟯ as E-algebras.

Equations

• RatFunc.IntermediateField.adjoinXEquiv E = (IntermediateField.equivOfEq ⋯).trans IntermediateField.topEquiv

@[reducible, inline]

noncomputable abbrev RatFunc.minpolyX {K : Type u_1} [Field K] (f : RatFunc K) (A : Type u_2) [CommRing A] [Algebra K A] [Algebra (↥K[f]) A] : Polynomial A

The minimal polynomial of X over K⟮f⟯. It is defined as f.num - f * f.denom, viewed as a polynomial with coefficients in A, where A is a K[f]-algebra.

Equations

• f.minpolyX A = Polynomial.map (algebraMap K A) f.num - Polynomial.C ((algebraMap (↥K[f]) A) ⟨f, ⋯⟩) * Polynomial.map (algebraMap K A) f.denom

theorem RatFunc.minpolyX_map {K : Type u_1} [Field K] (f : RatFunc K) (A : Type u_2) [CommRing A] [Algebra K A] [Algebra (↥K[f]) A] (B : Type u_3) [CommRing B] [Algebra K B] [Algebra (↥K[f]) B] [Algebra A B] [IsScalarTower K A B] [IsScalarTower (↥K[f]) A B] : Polynomial.map (algebraMap A B) (f.minpolyX A) = f.minpolyX B

@[simp]

theorem RatFunc.C_minpolyX {K : Type u_1} [Field K] (x : K) : (C x).minpolyX ↥K⟮C x⟯ = 0

theorem RatFunc.minpolyX_aeval_X {K : Type u_1} [Field K] (f : RatFunc K) : (Polynomial.aeval X) (f.minpolyX ↥K⟮f⟯) = 0

theorem RatFunc.eq_C_of_minpolyX_coeff_eq_zero {K : Type u_1} [Field K] (f : RatFunc K) (hf : ↑((f.minpolyX ↥K⟮f⟯).coeff f.denom.natDegree) = 0) : ∃ (c : K), f = C c

theorem RatFunc.minpolyX_eq_zero_iff {K : Type u_1} [Field K] (f : RatFunc K) : f.minpolyX ↥K⟮f⟯ = 0 ↔ ∃ (c : K), f = C c

theorem RatFunc.isAlgebraic_adjoin_simple_X {K : Type u_1} [Field K] (f : RatFunc K) (hf : ¬∃ (c : K), f = C c) : IsAlgebraic (↥K⟮f⟯) X

theorem RatFunc.isAlgebraic_adjoin_simple_X' {K : Type u_1} [Field K] (f : RatFunc K) (hf : ¬∃ (c : K), f = C c) : Algebra.IsAlgebraic (↥K⟮f⟯) (RatFunc K)

theorem RatFunc.natDegree_denom_le_natDegree_minpolyX {K : Type u_1} [Field K] (f : RatFunc K) (hf : ¬∃ (c : K), f = C c) : f.denom.natDegree ≤ (f.minpolyX ↥K⟮f⟯).natDegree

theorem RatFunc.natDegree_num_le_natDegree_minpolyX {K : Type u_1} [Field K] (f : RatFunc K) (hf : ¬∃ (c : K), f = C c) : f.num.natDegree ≤ (f.minpolyX ↥K⟮f⟯).natDegree

theorem RatFunc.natDegree_minpolyX {K : Type u_1} [Field K] (f : RatFunc K) : (f.minpolyX ↥K⟮f⟯).natDegree = max f.num.natDegree f.denom.natDegree

theorem RatFunc.transcendental_of_ne_C {K : Type u_1} [Field K] (f : RatFunc K) (hf : ¬∃ (c : K), f = C c) : Transcendental K f

theorem RatFunc.irreducible_minpolyX' {K : Type u_1} [Field K] (f : RatFunc K) (hf : ¬∃ (c : K), f = C c) : Irreducible (f.minpolyX ↥K[f])

theorem RatFunc.irreducible_minpolyX {K : Type u_1} [Field K] (f : RatFunc K) (hf : ¬∃ (c : K), f = C c) : Irreducible (f.minpolyX ↥K⟮f⟯)

theorem RatFunc.finrank_eq_max_natDegree {K : Type u_1} [Field K] (f : RatFunc K) : Module.finrank (↥K⟮f⟯) (RatFunc K) = max f.num.natDegree f.denom.natDegree

theorem RatFunc.IntermediateField.isAlgebraic_X {K : Type u_1} [Field K] {E : IntermediateField K (RatFunc K)} (hE : E ≠ ⊥) : IsAlgebraic (↥E) X