RealClosedField.PrimitiveElement.PrimitiveElement

source

def AlgHom.liftOfRightInverseAux {R : Type u_1} {A : Type u_2} {B : Type u_3} {C : Type u_4} [CommRing R] [Ring A] [Ring B] [Ring C] [Algebra R A] [Algebra R B] [Algebra R C] (f : A →ₐ[R] B) (f_inv : B → A) (hf : Function.RightInverse f_inv ⇑f) (g : A →ₐ[R] C) (hg : RingHom.ker f ≤ RingHom.ker g) :

B →ₐ[R] C

Auxiliary definition used to define liftOfRightInverse

Equations

f.liftOfRightInverseAux f_inv hf g hg = { toFun := fun (b : B) => g (f_inv b), map_one' := ⋯, map_mul' := ⋯, map_zero' := ⋯, map_add' := ⋯, commutes' := ⋯ }

Instances For

source

@[simp]

theorem AlgHom.liftOfRightInverseAux_comp_apply {R : Type u_1} {A : Type u_2} {B : Type u_3} {C : Type u_4} [CommRing R] [Ring A] [Ring B] [Ring C] [Algebra R A] [Algebra R B] [Algebra R C] (f : A →ₐ[R] B) (f_inv : B → A) (hf : Function.RightInverse f_inv ⇑f) (g : A →ₐ[R] C) (hg : RingHom.ker f ≤ RingHom.ker g) (a : A) :

(f.liftOfRightInverseAux f_inv hf g hg) (f a) = g a

source

def AlgHom.liftOfRightInverse {R : Type u_1} {A : Type u_2} {B : Type u_3} {C : Type u_4} [CommRing R] [Ring A] [Ring B] [Ring C] [Algebra R A] [Algebra R B] [Algebra R C] (f : A →ₐ[R] B) (f_inv : B → A) (hf : Function.RightInverse f_inv ⇑f) :

{ g : A →ₐ[R] C // RingHom.ker f ≤ RingHom.ker g } ≃ (B →ₐ[R] C)

liftOfRightInverse f hf g hg is the unique R-algebra homomorphism φ

such that φ.comp f = g (AlgHom.liftOfRightInverse_comp),
where f : A →ₐ[R] B has a right_inverse f_inv (hf),
and g : B →ₐ[R] C satisfies hg : f.ker ≤ g.ker.

See AlgHom.eq_liftOfRightInverse for the uniqueness lemma.

   A .
   |  \
 f |   \ g
   |    \
   v     \⌟
   B ----> C
      ∃!φ

Equations

One or more equations did not get rendered due to their size.

Instances For

source

@[reducible, inline]

noncomputable abbrev AlgHom.liftOfSurjective' {R : Type u_1} {A : Type u_2} {B : Type u_3} {C : Type u_4} [CommRing R] [Ring A] [Ring B] [Ring C] [Algebra R A] [Algebra R B] [Algebra R C] (f : A →ₐ[R] B) (hf : Function.Surjective ⇑f) :

{ g : A →ₐ[R] C // RingHom.ker f ≤ RingHom.ker g } ≃ (B →ₐ[R] C)

A non-computable version of AlgHom.liftOfRightInverse for when no computable right inverse is available, that uses Function.surjInv.

Equations

f.liftOfSurjective' hf = f.liftOfRightInverse (Function.surjInv hf) ⋯

Instances For

source

theorem AlgHom.liftOfRightInverse_comp_apply {R : Type u_1} {A : Type u_2} {B : Type u_3} {C : Type u_4} [CommRing R] [Ring A] [Ring B] [Ring C] [Algebra R A] [Algebra R B] [Algebra R C] (f : A →ₐ[R] B) (f_inv : B → A) (hf : Function.RightInverse f_inv ⇑f) (g : { g : A →ₐ[R] C // RingHom.ker f ≤ RingHom.ker g }) (x : A) :

((f.liftOfRightInverse f_inv hf) g) (f x) = ↑g x

source

theorem AlgHom.liftOfRightInverse_comp {R : Type u_1} {A : Type u_2} {B : Type u_3} {C : Type u_4} [CommRing R] [Ring A] [Ring B] [Ring C] [Algebra R A] [Algebra R B] [Algebra R C] (f : A →ₐ[R] B) (f_inv : B → A) (hf : Function.RightInverse f_inv ⇑f) (g : { g : A →ₐ[R] C // RingHom.ker f ≤ RingHom.ker g }) :

((f.liftOfRightInverse f_inv hf) g).comp f = ↑g

source

theorem AlgHom.liftOfRightInverse_symm {R : Type u_1} {A : Type u_2} {B : Type u_3} {C : Type u_4} [CommRing R] [Ring A] [Ring B] [Ring C] [Algebra R A] [Algebra R B] [Algebra R C] (f : A →ₐ[R] B) (f_inv : B → A) (hf : Function.RightInverse f_inv ⇑f) (φ : B →ₐ[R] C) :

↑((f.liftOfRightInverse f_inv hf).symm φ) = φ.comp f

source

theorem AlgHom.eq_liftOfRightInverse {R : Type u_1} {A : Type u_2} {B : Type u_3} {C : Type u_4} [CommRing R] [Ring A] [Ring B] [Ring C] [Algebra R A] [Algebra R B] [Algebra R C] (f : A →ₐ[R] B) (f_inv : B → A) (hf : Function.RightInverse f_inv ⇑f) (g : A →ₐ[R] C) (hg : RingHom.ker f ≤ RingHom.ker g) (h : B →ₐ[R] C) (hh : h.comp f = g) :

h = (f.liftOfRightInverse f_inv hf) ⟨g, hg⟩

source

theorem Polynomial.aeval_dvd {S : Type u_1} {T : Type u_2} [CommSemiring S] [Semiring T] [Algebra S T] {p q : Polynomial S} (a : T) :

p ∣ q → (aeval a) p ∣ (aeval a) q

source

theorem Polynomial.aeval_eq_zero_of_dvd_aeval_eq_zero' {S : Type u_1} {T : Type u_2} [CommSemiring S] [Semiring T] [Algebra S T] {p q : Polynomial S} (h₁ : p ∣ q) {a : T} (h₂ : (aeval a) p = 0) :

(aeval a) q = 0

source

@[simp]

theorem Polynomial.modByMonic_self {R : Type u_1} [Ring R] {p : Polynomial R} (hp : p.Monic) :

p %ₘ p = 0

source

theorem Polynomial.dvd_modByMonic_sub {R : Type u_1} [Ring R] (p q : Polynomial R) :

q ∣ p %ₘ q - p

source

theorem Polynomial.dvd_iff_dvd_modByMonic {R : Type u_1} [Ring R] {p q : Polynomial R} :

q ∣ p %ₘ q ↔ q ∣ p

source

theorem Polynomial.aeval_modByMonic_eq_self_of_root' {R : Type u_1} {S : Type u_2} [CommRing R] [Ring S] [Algebra R S] (p : Polynomial R) {q : Polynomial R} {x : S} (hx : (aeval x) q = 0) :

(aeval x) (p %ₘ q) = (aeval x) p

source

theorem Polynomial.aeval_modByMonic_minpoly {R : Type u_1} {S : Type u_2} [CommRing R] [Ring S] [Algebra R S] (p : Polynomial R) (x : S) :

(aeval x) (p %ₘ minpoly R x) = (aeval x) p

source

@[simp]

theorem Polynomial.aeval_apply_X {A : Type u_1} {B : Type u_2} [CommSemiring A] [Semiring B] [Algebra A B] (φ : Polynomial A →ₐ[A] B) :

aeval (φ X) = φ

source

theorem Polynomial.degree_sub_lt' {R : Type u_1} [Ring R] {p q : Polynomial R} (hd : p.degree = q.degree) (hq0 : q ≠ 0) (hlc : p.leadingCoeff = q.leadingCoeff) :

(p - q).degree < q.degree

source

theorem Polynomial.natDegree_le_of_monic_of_dvd {R : Type u_1} [Semiring R] {p q : Polynomial R} (hp : p.Monic) (hq : q ≠ 0) (hdvd : p ∣ q) :

p.natDegree ≤ q.natDegree

source

theorem Polynomial.eq_of_ideal_span_eq_of_monic {R : Type u_1} [CommSemiring R] {p q : Polynomial R} (hp : p.Monic) (hq : q.Monic) (h : Ideal.span {p} = Ideal.span {q}) :

p = q

source

theorem RingHom.subsingleton {R : Type u_1} {S : Type u_2} [Semiring R] [Semiring S] {f : R →+* S} :

f 1 = 0 ↔ Subsingleton S

source

theorem RingHom.ker_eq_top_iff {R : Type u_1} {S : Type u_2} [Semiring R] [Semiring S] {f : R →+* S} :

ker f = ⊤ ↔ Subsingleton S

source

theorem RingHom.subsingleton_of_ker_eq_top {R : Type u_1} {S : Type u_2} [Semiring R] [Semiring S] {f : R →+* S} :

ker f = ⊤ → Subsingleton S

Alias of the forward direction of RingHom.ker_eq_top_iff.

source

theorem RingHom.ker_eq_top_of_subsingleton' {R : Type u_1} {S : Type u_2} [Semiring R] [Semiring S] [Subsingleton S] {f : R →+* S} :

ker f = ⊤

source

noncomputable def Polynomial.AlgHomEquiv (A : Type u_1) (B : Type u_2) [CommSemiring A] [Semiring B] [Algebra A B] :

B ≃ (Polynomial A →ₐ[A] B)

Equations

Polynomial.AlgHomEquiv A B = { toFun := fun (y : B) => Polynomial.aeval y, invFun := fun (f : Polynomial A →ₐ[A] B) => f Polynomial.X, left_inv := ⋯, right_inv := ⋯ }

Instances For

source

@[simp]

theorem Polynomial.AlgHomEquiv_apply (A : Type u_1) (B : Type u_2) [CommSemiring A] [Semiring B] [Algebra A B] (y : B) :

(AlgHomEquiv A B) y = aeval y

source

@[simp]

theorem Polynomial.AlgHomEquiv_symm_apply (A : Type u_1) (B : Type u_2) [CommSemiring A] [Semiring B] [Algebra A B] (f : Polynomial A →ₐ[A] B) :

(AlgHomEquiv A B).symm f = f X

source

noncomputable def MvPolynomial.AlgHomEquiv (A : Type u_1) (B : Type u_2) (σ : Type u_3) [CommSemiring A] [CommSemiring B] [Algebra A B] :

(σ → B) ≃ (MvPolynomial σ A →ₐ[A] B)

Equations

One or more equations did not get rendered due to their size.

Instances For

source

@[simp]

theorem MvPolynomial.AlgHomEquiv_apply (A : Type u_1) (B : Type u_2) (σ : Type u_3) [CommSemiring A] [CommSemiring B] [Algebra A B] (y : σ → B) :

(AlgHomEquiv A B σ) y = aeval y

source

@[simp]

theorem MvPolynomial.AlgHomEquiv_symm_apply (A : Type u_1) (B : Type u_2) (σ : Type u_3) [CommSemiring A] [CommSemiring B] [Algebra A B] (f : MvPolynomial σ A →ₐ[A] B) (i : σ) :

(AlgHomEquiv A B σ).symm f i = f (X i)

source

structure Algebra.IsGenerator (R : Type u_1) {S : Type u_2} [CommRing R] [Ring S] [Algebra R S] (x : S) :

Prop

adjoin_eq_top : adjoin R {x} = ⊤

Instances For

source

theorem Algebra.IsGenerator.def (R : Type u_1) {S : Type u_2} [CommRing R] [Ring S] [Algebra R S] (x : S) :

IsGenerator R x ↔ adjoin R {x} = ⊤

source

theorem Algebra.isGenerator_iff_aeval_surjective (R : Type u_1) {S : Type u_2} [CommRing R] [Ring S] [Algebra R S] (x : S) :

IsGenerator R x ↔ Function.Surjective ⇑(Polynomial.aeval x)

source

theorem Algebra.IsGenerator.aeval_surjective {R : Type u_1} {S : Type u_2} [CommRing R] [Ring S] [Algebra R S] {x : S} (hx : IsGenerator R x) :

Function.Surjective ⇑(Polynomial.aeval x)

source

noncomputable def Algebra.IsGenerator.adjoinEquiv {R : Type u_1} {S : Type u_2} [CommRing R] [Ring S] [Algebra R S] {x : S} (hx : IsGenerator R x) :

↥(adjoin R {x}) ≃ₐ[R] S

Equations

hx.adjoinEquiv = ((Algebra.adjoin R {x}).equivOfEq ⊤ ⋯).trans Subalgebra.topEquiv

Instances For

source

theorem Algebra.IsGenerator.adjoinEquiv_apply {R : Type u_1} {S : Type u_2} [CommRing R] [Ring S] [Algebra R S] {x : S} (hx : IsGenerator R x) (y : ↥(adjoin R {x})) :

hx.adjoinEquiv y = ↑y

source

theorem Algebra.IsGenerator.adjoinEquiv_symm_apply {R : Type u_1} {S : Type u_2} [CommRing R] [Ring S] [Algebra R S] {x : S} (hx : IsGenerator R x) (y : S) :

↑(hx.adjoinEquiv.symm y) = y

source

theorem Algebra.IsGenerator.finite_iff_isIntegral {R : Type u_1} {S : Type u_2} [CommRing R] [Ring S] [Algebra R S] {x : S} (hx : IsGenerator R x) :

Module.Finite R S ↔ IsIntegral R x

source

theorem Algebra.IsGenerator.of_root_mem_adjoin {R : Type u_1} {S : Type u_2} [CommRing R] [Ring S] [Algebra R S] {x : S} (hx : IsGenerator R x) {y : S} (hy : x ∈ adjoin R {y}) :

IsGenerator R y

source

theorem Algebra.IsGenerator.add_algebraMap {R : Type u_1} {S : Type u_2} [CommRing R] [Ring S] [Algebra R S] {x : S} (hx : IsGenerator R x) (r : R) :

IsGenerator R (x + (algebraMap R S) r)

source

theorem Algebra.IsGenerator.algberaMap_mul {S : Type u_2} [Ring S] {F : Type u_3} [Field F] [Algebra F S] {x : S} (hx : IsGenerator F x) {r : F} (hr : r ≠ 0) :

IsGenerator F ((algebraMap F S) r * x)

source

noncomputable def Algebra.IsGenerator.liftEquiv {R : Type u_1} {S : Type u_2} [CommRing R] [Ring S] [Algebra R S] {x : S} (hx : IsGenerator R x) {T : Type u_3} [Ring T] [Algebra R T] :

{ y : T // ∀ (g : Polynomial R), (Polynomial.aeval x) g = 0 → (Polynomial.aeval y) g = 0 } ≃ (S →ₐ[R] T)

Equations

hx.liftEquiv = ((Polynomial.AlgHomEquiv R T).subtypeEquiv ⋯).trans ((Polynomial.aeval x).liftOfSurjective' ⋯)

Instances For

source

@[simp]

theorem Algebra.IsGenerator.liftEquiv_symm_apply {R : Type u_1} {S : Type u_2} [CommRing R] [Ring S] [Algebra R S] {x : S} (hx : IsGenerator R x) {T : Type u_3} [Ring T] [Algebra R T] (φ : S →ₐ[R] T) :

↑(hx.liftEquiv.symm φ) = φ x

source

theorem Algebra.IsGenerator.algHom_ext {R : Type u_1} {S : Type u_2} [CommRing R] [Ring S] [Algebra R S] {x : S} (hx : IsGenerator R x) {T : Type u_3} [Ring T] [Algebra R T] ⦃φ ψ : S →ₐ[R] T⦄ (h : φ x = ψ x) :

φ = ψ

source

@[simp]

theorem Algebra.IsGenerator.liftEquiv_aeval_apply {R : Type u_1} {S : Type u_2} [CommRing R] [Ring S] [Algebra R S] {x : S} (hx : IsGenerator R x) {T : Type u_3} [Ring T] [Algebra R T] {y : T} (hy : ∀ (g : Polynomial R), (Polynomial.aeval x) g = 0 → (Polynomial.aeval y) g = 0) (g : Polynomial R) :

(hx.liftEquiv ⟨y, hy⟩) ((Polynomial.aeval x) g) = (Polynomial.aeval y) g

source

@[simp]

theorem Algebra.IsGenerator.liftEquiv_comp_aeval {R : Type u_1} {S : Type u_2} [CommRing R] [Ring S] [Algebra R S] {x : S} (hx : IsGenerator R x) {T : Type u_3} [Ring T] [Algebra R T] {y : T} (hy : ∀ (g : Polynomial R), (Polynomial.aeval x) g = 0 → (Polynomial.aeval y) g = 0) :

(hx.liftEquiv ⟨y, hy⟩).comp (Polynomial.aeval x) = Polynomial.aeval y

source

@[simp]

theorem Algebra.IsGenerator.liftEquiv_root {R : Type u_1} {S : Type u_2} [CommRing R] [Ring S] [Algebra R S] {x : S} (hx : IsGenerator R x) {T : Type u_3} [Ring T] [Algebra R T] {y : T} (hy : ∀ (g : Polynomial R), (Polynomial.aeval x) g = 0 → (Polynomial.aeval y) g = 0) :

(hx.liftEquiv ⟨y, hy⟩) x = y

source

theorem Algebra.isUnit_iff_subsingleton_of_ker_aeval {R : Type u_1} {S : Type u_2} [CommRing R] [Ring S] [Algebra R S] {x : S} {g : Polynomial R} (h : RingHom.ker (Polynomial.aeval x) = Ideal.span {g}) :

IsUnit g ↔ Subsingleton S

source

theorem Algebra.subsingleton_of_ker_aeval {R : Type u_1} {S : Type u_2} [CommRing R] [Ring S] [Algebra R S] {x : S} {g : Polynomial R} (h : RingHom.ker (Polynomial.aeval x) = Ideal.span {g}) :

IsUnit g → Subsingleton S

Alias of the forward direction of Algebra.isUnit_iff_subsingleton_of_ker_aeval.

source

theorem Algebra.isUnit_of_ker_aeval {R : Type u_1} {S : Type u_2} [CommRing R] [Ring S] [Algebra R S] {x : S} {g : Polynomial R} [Subsingleton S] (h : RingHom.ker (Polynomial.aeval x) = Ideal.span {g}) :

IsUnit g

source

theorem Algebra.nontrivial_of_ker_aeval {R : Type u_1} {S : Type u_2} [CommRing R] [Ring S] [Algebra R S] {x : S} {g : Polynomial R} (h : RingHom.ker (Polynomial.aeval x) = Ideal.span {g}) (hg : ¬IsUnit g) :

Nontrivial S

source

theorem Algebra.not_isUnit_of_ker_aeval {R : Type u_1} {S : Type u_2} [CommRing R] [Ring S] [Algebra R S] {x : S} {g : Polynomial R} [Nontrivial S] (h : RingHom.ker (Polynomial.aeval x) = Ideal.span {g}) :

¬IsUnit g

source

theorem Algebra.aeval_eq_zero_iff_of_ker_aeval_eq_span_singleton {R : Type u_1} {S : Type u_2} [CommRing R] [Ring S] [Algebra R S] {x : S} {g : Polynomial R} (h : RingHom.ker (Polynomial.aeval x) = Ideal.span {g}) {f : Polynomial R} :

(Polynomial.aeval x) f = 0 ↔ g ∣ f

source

structure Algebra.IsSimpleGenerator {R : Type u_1} {S : Type u_2} [CommRing R] [Ring S] [Algebra R S] (x : S) (g : Polynomial R) extends Algebra.IsGenerator R x :

Prop

adjoin_eq_top : adjoin R {x} = ⊤
ker_aeval : RingHom.ker (Polynomial.aeval x) = Ideal.span {g}

Instances For

source

theorem Algebra.IsSimpleGenerator.def {R : Type u_1} {S : Type u_2} [CommRing R] [Ring S] [Algebra R S] (x : S) (g : Polynomial R) :

IsSimpleGenerator x g ↔ IsGenerator R x ∧ RingHom.ker (Polynomial.aeval x) = Ideal.span {g}

source

theorem Algebra.IsSimpleGenerator.aeval_eq_zero_iff {R : Type u_1} {S : Type u_2} [CommRing R] [Ring S] [Algebra R S] {x : S} {g : Polynomial R} (h : IsSimpleGenerator x g) {f : Polynomial R} :

(Polynomial.aeval x) f = 0 ↔ g ∣ f

source

theorem Algebra.IsSimpleGenerator.aeval_self {R : Type u_1} {S : Type u_2} [CommRing R] [Ring S] [Algebra R S] {x : S} {g : Polynomial R} (h : IsSimpleGenerator x g) :

(Polynomial.aeval x) g = 0

source

theorem Algebra.IsSimpleGenerator.aeval_gen_eq_zero_iff {R : Type u_1} {S : Type u_2} [CommRing R] [Ring S] [Algebra R S] {x : S} {g : Polynomial R} (h : IsSimpleGenerator x g) {T : Type u_3} [Ring T] [Algebra R T] (y : T) :

(Polynomial.aeval y) g = 0 ↔ ∀ (f : Polynomial R), (Polynomial.aeval x) f = 0 → (Polynomial.aeval y) f = 0

source

noncomputable def Algebra.IsSimpleGenerator.liftEquiv {R : Type u_1} {S : Type u_2} [CommRing R] [Ring S] [Algebra R S] {x : S} {g : Polynomial R} (h : IsSimpleGenerator x g) {T : Type u_3} [Ring T] [Algebra R T] :

{ y : T // (Polynomial.aeval y) g = 0 } ≃ (S →ₐ[R] T)

Equations

h.liftEquiv = ((Equiv.refl T).subtypeEquiv ⋯).trans ⋯.liftEquiv

Instances For

source

@[simp]

theorem Algebra.IsSimpleGenerator.liftEquiv_symm_apply {R : Type u_1} {S : Type u_2} [CommRing R] [Ring S] [Algebra R S] {x : S} {g : Polynomial R} (h : IsSimpleGenerator x g) {T : Type u_3} [Ring T] [Algebra R T] (φ : S →ₐ[R] T) :

↑(h.liftEquiv.symm φ) = φ x

source

noncomputable def Algebra.IsSimpleGenerator.lift {R : Type u_1} {S : Type u_2} [CommRing R] [Ring S] [Algebra R S] {x : S} {g : Polynomial R} (h : IsSimpleGenerator x g) {T : Type u_3} [Ring T] [Algebra R T] {y : T} (hy : (Polynomial.aeval y) g = 0) :

S →ₐ[R] T

Equations

h.lift hy = h.liftEquiv ⟨y, hy⟩

Instances For

source

@[simp]

theorem Algebra.IsSimpleGenerator.lift_aeval {R : Type u_1} {S : Type u_2} [CommRing R] [Ring S] [Algebra R S] {x : S} {g : Polynomial R} (h : IsSimpleGenerator x g) {T : Type u_3} [Ring T] [Algebra R T] {y : T} (hy : (Polynomial.aeval y) g = 0) (f : Polynomial R) :

(h.lift hy) ((Polynomial.aeval x) f) = (Polynomial.aeval y) f

source

@[simp]

theorem Algebra.IsSimpleGenerator.lift_root {R : Type u_1} {S : Type u_2} [CommRing R] [Ring S] [Algebra R S] {x : S} {g : Polynomial R} (h : IsSimpleGenerator x g) {T : Type u_3} [Ring T] [Algebra R T] {y : T} (hy : (Polynomial.aeval y) g = 0) :

(h.lift hy) x = y

source

@[simp]

theorem Algebra.IsSimpleGenerator.liftEquiv_apply {R : Type u_1} {S : Type u_2} [CommRing R] [Ring S] [Algebra R S] {x : S} {g : Polynomial R} (h : IsSimpleGenerator x g) {T : Type u_3} [Ring T] [Algebra R T] {y : T} (hy : (Polynomial.aeval y) g = 0) (z : S) :

(h.liftEquiv ⟨y, hy⟩) z = (h.lift hy) z

source

noncomputable def Algebra.IsSimpleGenerator.equivOfRoot {R : Type u_1} {S : Type u_2} [CommRing R] [Ring S] [Algebra R S] {x : S} {g : Polynomial R} (h : IsSimpleGenerator x g) {S' : Type u_4} [Ring S'] [Algebra R S'] {x' : S'} {g' : Polynomial R} (h' : IsSimpleGenerator x' g') (hx : (Polynomial.aeval x) g' = 0) (hx' : (Polynomial.aeval x') g = 0) :

S ≃ₐ[R] S'

Equations

h.equivOfRoot h' hx hx' = AlgEquiv.ofAlgHom (h.lift hx') (h'.lift hx) ⋯ ⋯

Instances For

source

theorem Algebra.IsSimpleGenerator.equivOfRoot_apply {R : Type u_1} {S : Type u_2} [CommRing R] [Ring S] [Algebra R S] {x : S} {g : Polynomial R} (h : IsSimpleGenerator x g) {S' : Type u_4} [Ring S'] [Algebra R S'] {x' : S'} {g' : Polynomial R} (h' : IsSimpleGenerator x' g') (hx : (Polynomial.aeval x) g' = 0) (hx' : (Polynomial.aeval x') g = 0) (a : S) :

(h.equivOfRoot h' hx hx') a = (h.lift hx') a

source

@[simp]

theorem Algebra.IsSimpleGenerator.equivOfRoot_symm {R : Type u_1} {S : Type u_2} [CommRing R] [Ring S] [Algebra R S] {x : S} {g : Polynomial R} (h : IsSimpleGenerator x g) {S' : Type u_4} [Ring S'] [Algebra R S'] {x' : S'} {g' : Polynomial R} (h' : IsSimpleGenerator x' g') (hx : (Polynomial.aeval x) g' = 0) (hx' : (Polynomial.aeval x') g = 0) :

(h.equivOfRoot h' hx hx').symm = h'.equivOfRoot h hx' hx

source

@[simp]

theorem Algebra.IsSimpleGenerator.equivOfRoot_aeval {R : Type u_1} {S : Type u_2} [CommRing R] [Ring S] [Algebra R S] {x : S} {g : Polynomial R} (h : IsSimpleGenerator x g) {S' : Type u_4} [Ring S'] [Algebra R S'] {x' : S'} {g' : Polynomial R} (h' : IsSimpleGenerator x' g') (hx : (Polynomial.aeval x) g' = 0) (hx' : (Polynomial.aeval x') g = 0) (f : Polynomial R) :

(h.equivOfRoot h' hx hx') ((Polynomial.aeval x) f) = (Polynomial.aeval x') f

source

@[simp]

theorem Algebra.IsSimpleGenerator.equivOfRoot_root {R : Type u_1} {S : Type u_2} [CommRing R] [Ring S] [Algebra R S] {x : S} {g : Polynomial R} (h : IsSimpleGenerator x g) {S' : Type u_4} [Ring S'] [Algebra R S'] {x' : S'} {g' : Polynomial R} (h' : IsSimpleGenerator x' g') (hx : (Polynomial.aeval x) g' = 0) (hx' : (Polynomial.aeval x') g = 0) :

(h.equivOfRoot h' hx hx') x = x'

source

noncomputable def Algebra.IsSimpleGenerator.equiv {R : Type u_1} {S : Type u_2} [CommRing R] [Ring S] [Algebra R S] {x : S} {g : Polynomial R} (h : IsSimpleGenerator x g) {S' : Type u_4} [Ring S'] [Algebra R S'] {x' : S'} (h' : IsSimpleGenerator x' g) :

S ≃ₐ[R] S'

Equations

h.equiv h' = h.equivOfRoot h' ⋯ ⋯

Instances For

source

@[simp]

theorem Algebra.IsSimpleGenerator.equiv_apply {R : Type u_1} {S : Type u_2} [CommRing R] [Ring S] [Algebra R S] {x : S} {g : Polynomial R} (h : IsSimpleGenerator x g) {S' : Type u_4} [Ring S'] [Algebra R S'] {x' : S'} (h' : IsSimpleGenerator x' g) (z : S) :

(h.equiv h') z = (h.equivOfRoot h' ⋯ ⋯) z

source

@[simp]

theorem Algebra.IsSimpleGenerator.equiv_symm {R : Type u_1} {S : Type u_2} [CommRing R] [Ring S] [Algebra R S] {x : S} {g : Polynomial R} (h : IsSimpleGenerator x g) {S' : Type u_4} [Ring S'] [Algebra R S'] {x' : S'} (h' : IsSimpleGenerator x' g) :

(h.equiv h').symm = h'.equiv h

source

noncomputable def Algebra.IsSimpleGenerator.map {R : Type u_1} {S : Type u_2} [CommRing R] [Ring S] [Algebra R S] {x : S} {g : Polynomial R} (h : IsSimpleGenerator x g) {T : Type u_4} [Ring T] [Algebra R T] (φ : S ≃ₐ[R] T) :

IsSimpleGenerator (φ x) g

Equations

⋯ = ⋯

Instances For

source

@[simp]

theorem Algebra.IsSimpleGenerator.equivOfRoot_map {R : Type u_1} {S : Type u_2} [CommRing R] [Ring S] [Algebra R S] {x : S} {g : Polynomial R} (h : IsSimpleGenerator x g) {T : Type u_4} [Ring T] [Algebra R T] (φ : S ≃ₐ[R] T) :

h.equivOfRoot ⋯ ⋯ ⋯ = φ

source

structure IsIntegralUnique {R : Type u_1} {S : Type u_2} [CommRing R] [Ring S] [Algebra R S] (x : S) (g : Polynomial R) :

Prop

monic : g.Monic
ker_aeval : RingHom.ker (Polynomial.aeval x) = Ideal.span {g}

Instances For

source

theorem IsIntegralUnique.of_subsingleton {R : Type u_1} {S : Type u_2} [CommRing R] [Ring S] [Algebra R S] (x : S) (g : Polynomial R) [Subsingleton R] :

IsIntegralUnique x g

source

theorem IsIntegralUnique.of_subsingleton_gen_one (R : Type u_1) {S : Type u_2} [CommRing R] [Ring S] [Algebra R S] (x : S) [Subsingleton S] :

IsIntegralUnique x 1

source

theorem IsIntegralUnique.of_ker_aeval_eq_span_minpoly {R : Type u_1} {S : Type u_2} [CommRing R] [Ring S] [Algebra R S] {x : S} (hx : IsIntegral R x) (h : RingHom.ker (Polynomial.aeval x) = Ideal.span {minpoly R x}) :

IsIntegralUnique x (minpoly R x)

source

theorem IsIntegralUnique.of_ker_aeval_eq_span' {R : Type u_1} {S : Type u_2} [CommRing R] [Ring S] [Algebra R S] {x : S} {g : Polynomial R} [IsDomain R] (hx : IsIntegral R x) (h : RingHom.ker (Polynomial.aeval x) = Ideal.span {g}) :

have hu := ⋯; IsIntegralUnique x (Polynomial.C ↑hu.unit⁻¹ * g)

source

theorem IsIntegralUnique.of_ker_aeval_eq_span {R : Type u_1} {S : Type u_2} [CommRing R] [Ring S] [Algebra R S] {x : S} {g : Polynomial R} [IsDomain R] [NormalizationMonoid R] (hx : IsIntegral R x) (h : RingHom.ker (Polynomial.aeval x) = Ideal.span {g}) :

IsIntegralUnique x (normalize g)

source

theorem IsIntegralUnique.of_aeval_eq_zero_imp_minpoly_dvd {R : Type u_1} {S : Type u_2} [CommRing R] [Ring S] [Algebra R S] {x : S} (hx : IsIntegral R x) (h : ∀ {f : Polynomial R}, (Polynomial.aeval x) f = 0 → minpoly R x ∣ f) :

IsIntegralUnique x (minpoly R x)

source

theorem IsIntegralUnique.of_unique_of_degree_le_degree_minpoly {R : Type u_1} {S : Type u_2} [CommRing R] [Ring S] [Algebra R S] {x : S} (hx : IsIntegral R x) (h : ∀ (f : Polynomial R), f.Monic → (Polynomial.aeval x) f = 0 → f.degree ≤ (minpoly R x).degree → f = minpoly R x) :

IsIntegralUnique x (minpoly R x)

source

theorem IsIntegralUnique.aeval_eq_zero_iff {R : Type u_1} {S : Type u_2} [CommRing R] [Ring S] [Algebra R S] {x : S} {g : Polynomial R} (h : IsIntegralUnique x g) {f : Polynomial R} :

(Polynomial.aeval x) f = 0 ↔ g ∣ f

source

theorem IsIntegralUnique.aeval_gen {R : Type u_1} {S : Type u_2} [CommRing R] [Ring S] [Algebra R S] {x : S} {g : Polynomial R} (h : IsIntegralUnique x g) :

(Polynomial.aeval x) g = 0

source

theorem IsIntegralUnique.isIntegral {R : Type u_1} {S : Type u_2} [CommRing R] [Ring S] [Algebra R S] {x : S} {g : Polynomial R} (h : IsIntegralUnique x g) :

IsIntegral R x

source

theorem IsIntegralUnique.gen_eq_one_iff_subsingleton {R : Type u_1} {S : Type u_2} [CommRing R] [Ring S] [Algebra R S] {x : S} {g : Polynomial R} (h : IsIntegralUnique x g) :

g = 1 ↔ Subsingleton S

source

theorem IsIntegralUnique.subsingleton {R : Type u_1} {S : Type u_2} [CommRing R] [Ring S] [Algebra R S] {x : S} {g : Polynomial R} (h : IsIntegralUnique x g) :

g = 1 → Subsingleton S

Alias of the forward direction of IsIntegralUnique.gen_eq_one_iff_subsingleton.

source

theorem IsIntegralUnique.gen_eq_one {R : Type u_1} {S : Type u_2} [CommRing R] [Ring S] [Algebra R S] {x : S} {g : Polynomial R} (h : IsIntegralUnique x g) [Subsingleton S] :

g = 1

source

theorem IsIntegralUnique.nontrivial {R : Type u_1} {S : Type u_2} [CommRing R] [Ring S] [Algebra R S] {x : S} {g : Polynomial R} (h : IsIntegralUnique x g) (hg : g ≠ 1) :

Nontrivial S

source

theorem IsIntegralUnique.gen_ne_one {R : Type u_1} {S : Type u_2} [CommRing R] [Ring S] [Algebra R S] {x : S} {g : Polynomial R} (h : IsIntegralUnique x g) [Nontrivial S] :

g ≠ 1

source

theorem IsIntegralUnique.natDegree_gen_pos {R : Type u_1} {S : Type u_2} [CommRing R] [Ring S] [Algebra R S] {x : S} {g : Polynomial R} (h : IsIntegralUnique x g) [Nontrivial S] :

0 < g.natDegree

source

theorem IsIntegralUnique.degree_gen_pos {R : Type u_1} {S : Type u_2} [CommRing R] [Ring S] [Algebra R S] {x : S} {g : Polynomial R} (h : IsIntegralUnique x g) [Nontrivial S] :

0 < g.degree

source

theorem IsIntegralUnique.minpoly_eq_gen {R : Type u_1} {S : Type u_2} [CommRing R] [Ring S] [Algebra R S] {x : S} {g : Polynomial R} (h : IsIntegralUnique x g) :

minpoly R x = g

source

theorem IsIntegralUnique.gen_unique {R : Type u_1} {S : Type u_2} [CommRing R] [Ring S] [Algebra R S] {x : S} {g : Polynomial R} (h : IsIntegralUnique x g) {g' : Polynomial R} (h' : IsIntegralUnique x g') :

g = g'

source

theorem IsIntegralUnique.irreducible_gen {R : Type u_1} {S : Type u_2} [CommRing R] [Ring S] [Algebra R S] {x : S} {g : Polynomial R} (h : IsIntegralUnique x g) [IsDomain R] [IsDomain S] :

Irreducible g

source

theorem IsIntegralUnique.isIntegralUnique_minpoly {R : Type u_1} {S : Type u_2} [CommRing R] [Ring S] [Algebra R S] {x : S} {g : Polynomial R} (h : IsIntegralUnique x g) :

IsIntegralUnique x (minpoly R x)

source

theorem IsIntegralUnique.eq_gen_of_degree_le_degree_gen {R : Type u_1} {S : Type u_2} [CommRing R] [Ring S] [Algebra R S] {x : S} {g : Polynomial R} (h : IsIntegralUnique x g) {f : Polynomial R} (hmo : f.Monic) (hf : (Polynomial.aeval x) f = 0) (fmin : f.degree ≤ g.degree) :

f = g

source

theorem IsIntegralUnique.eq_gen_of_aeval_eq_zero_imp_degree_ge {R : Type u_1} {S : Type u_2} [CommRing R] [Ring S] [Algebra R S] {x : S} {g : Polynomial R} (h : IsIntegralUnique x g) {f : Polynomial R} (hmo : f.Monic) (hf : (Polynomial.aeval x) f = 0) (hmin : ∀ (k : Polynomial R), k.Monic → (Polynomial.aeval x) k = 0 → f.degree ≤ k.degree) :

f = g

source

theorem IsIntegralUnique.eq_gen_of_ker_aeval_eq_span {R : Type u_1} {S : Type u_2} [CommRing R] [Ring S] [Algebra R S] {x : S} {g : Polynomial R} (h : IsIntegralUnique x g) {f : Polynomial R} (hf : f.Monic) (hker : RingHom.ker (Polynomial.aeval x) = Ideal.span {f}) :

f = g

source

theorem IsIntegralUnique.modByMonic_gen_eq_iff_aeval_eq {R : Type u_1} {S : Type u_2} [CommRing R] [Ring S] [Algebra R S] {x : S} {g : Polynomial R} (h : IsIntegralUnique x g) (f₁ f₂ : Polynomial R) :

f₁ %ₘ g = f₂ %ₘ g ↔ (Polynomial.aeval x) f₁ = (Polynomial.aeval x) f₂

source

structure IsIntegralUniqueGen {R : Type u_1} {S : Type u_2} [CommRing R] [Ring S] [Algebra R S] (x : S) (g : Polynomial R) extends Algebra.IsSimpleGenerator x g, IsIntegralUnique x g :

Prop

adjoin_eq_top : adjoin R {x} = ⊤
ker_aeval : RingHom.ker (Polynomial.aeval x) = Ideal.span {g}
monic : g.Monic

Instances For

source

theorem IsIntegralUniqueGen.of_basis {R : Type u_1} {S : Type u_2} [CommRing R] [Ring S] [Algebra R S] {x : S} [Module.Finite R S] {n : ℕ} (B : Module.Basis (Fin n) R S) (hB : ∀ (i : Fin n), B i = x ^ ↑i) :

IsIntegralUniqueGen x (Polynomial.X ^ n - ∑ i : Fin n, Polynomial.C ((B.repr (x ^ n)) i) * Polynomial.X ^ ↑i)

source

theorem IsIntegralUniqueGen.of_free {R : Type u_1} {S : Type u_2} [CommRing R] [Ring S] [Algebra R S] {x : S} [Module.Finite R S] [Module.Free R S] (hx : Algebra.IsGenerator R x) :

∃ (g' : Polynomial R), IsIntegralUniqueGen x g'

source

noncomputable def IsIntegralUniqueGen.repr {R : Type u_1} {S : Type u_2} [CommRing R] [Ring S] [Algebra R S] {x : S} {g : Polynomial R} (h : IsIntegralUniqueGen x g) :

S →ₗ[R] Polynomial R

Equations

h.repr = { toFun := fun (y : S) => Classical.choose ⋯ %ₘ g, map_add' := ⋯, map_smul' := ⋯ }

Instances For

source

@[simp]

theorem IsIntegralUniqueGen.aeval_repr {R : Type u_1} {S : Type u_2} [CommRing R] [Ring S] [Algebra R S] {x : S} {g : Polynomial R} (h : IsIntegralUniqueGen x g) (y : S) :

(Polynomial.aeval x) (h.repr y) = y

source

@[simp]

theorem IsIntegralUniqueGen.repr_aeval {R : Type u_1} {S : Type u_2} [CommRing R] [Ring S] [Algebra R S] {x : S} {g : Polynomial R} (h : IsIntegralUniqueGen x g) (f : Polynomial R) :

h.repr ((Polynomial.aeval x) f) = f %ₘ g

source

theorem IsIntegralUniqueGen.repr_aeval_eq_self_iff {R : Type u_1} {S : Type u_2} [CommRing R] [Ring S] [Algebra R S] {x : S} {g : Polynomial R} (h : IsIntegralUniqueGen x g) [Nontrivial R] (f : Polynomial R) :

h.repr ((Polynomial.aeval x) f) = f ↔ f.degree < g.degree

source

theorem IsIntegralUniqueGen.repr_aeval_eq_self {R : Type u_1} {S : Type u_2} [CommRing R] [Ring S] [Algebra R S] {x : S} {g : Polynomial R} (h : IsIntegralUniqueGen x g) {f : Polynomial R} (hf : f.degree < g.degree) :

h.repr ((Polynomial.aeval x) f) = f

source

@[simp]

theorem IsIntegralUniqueGen.repr_root_pow {R : Type u_1} {S : Type u_2} [CommRing R] [Ring S] [Algebra R S] {x : S} {g : Polynomial R} (h : IsIntegralUniqueGen x g) {n : ℕ} (hdeg : n < g.natDegree) :

h.repr (x ^ n) = Polynomial.X ^ n

source

@[simp]

theorem IsIntegralUniqueGen.repr_root {R : Type u_1} {S : Type u_2} [CommRing R] [Ring S] [Algebra R S] {x : S} {g : Polynomial R} (h : IsIntegralUniqueGen x g) (hdeg : 1 < g.natDegree) :

h.repr x = Polynomial.X

source

@[simp]

theorem IsIntegralUniqueGen.repr_one {R : Type u_1} {S : Type u_2} [CommRing R] [Ring S] [Algebra R S] {x : S} {g : Polynomial R} (h : IsIntegralUniqueGen x g) [Nontrivial S] :

h.repr 1 = 1

source

@[simp]

theorem IsIntegralUniqueGen.repr_algebraMap {R : Type u_1} {S : Type u_2} [CommRing R] [Ring S] [Algebra R S] {x : S} {g : Polynomial R} (h : IsIntegralUniqueGen x g) [Nontrivial S] (r : R) :

h.repr ((algebraMap R S) r) = (algebraMap R (Polynomial R)) r

source

@[simp]

theorem IsIntegralUniqueGen.repr_ofNat {R : Type u_1} {S : Type u_2} [CommRing R] [Ring S] [Algebra R S] {x : S} {g : Polynomial R} (h : IsIntegralUniqueGen x g) [Nontrivial S] (n : ℕ) [n.AtLeastTwo] :

h.repr (OfNat.ofNat n) = ↑↑n

source

@[simp]

theorem IsIntegralUniqueGen.repr_root_pow_algebraMap {R : Type u_1} {S : Type u_2} [CommRing R] [Ring S] [Algebra R S] {x : S} {g : Polynomial R} (h : IsIntegralUniqueGen x g) :

h.repr (x ^ g.natDegree) = Polynomial.X ^ g.natDegree - g

source

theorem IsIntegralUniqueGen.degree_repr_le {R : Type u_1} {S : Type u_2} [CommRing R] [Ring S] [Algebra R S] {x : S} {g : Polynomial R} (h : IsIntegralUniqueGen x g) [Nontrivial R] (y : S) :

(h.repr y).degree < g.degree

source

theorem IsIntegralUniqueGen.natDegree_repr_le {R : Type u_1} {S : Type u_2} [CommRing R] [Ring S] [Algebra R S] {x : S} {g : Polynomial R} (h : IsIntegralUniqueGen x g) [Nontrivial S] (y : S) :

(h.repr y).natDegree < g.natDegree

source

theorem IsIntegralUniqueGen.repr_coeff_of_natDegree_le {R : Type u_1} {S : Type u_2} [CommRing R] [Ring S] [Algebra R S] {x : S} {g : Polynomial R} (h : IsIntegralUniqueGen x g) (y : S) {i : ℕ} (hi : g.natDegree ≤ i) :

(h.repr y).coeff i = 0

source

noncomputable def IsIntegralUniqueGen.liftEquivAroots {R : Type u_1} {S : Type u_2} [CommRing R] [Ring S] [Algebra R S] {x : S} {g : Polynomial R} (h : IsIntegralUniqueGen x g) {T : Type u_3} [CommRing T] [IsDomain T] [Algebra R T] :

{ y : T // y ∈ g.aroots T } ≃ (S →ₐ[R] T)

Equations

h.liftEquivAroots = ((Equiv.refl T).subtypeEquiv ⋯).trans ⋯.liftEquiv

Instances For

source

@[simp]

theorem IsIntegralUniqueGen.liftEquivAroots_symm_apply {R : Type u_1} {S : Type u_2} [CommRing R] [Ring S] [Algebra R S] {x : S} {g : Polynomial R} (h : IsIntegralUniqueGen x g) {T : Type u_3} [CommRing T] [IsDomain T] [Algebra R T] (φ : S →ₐ[R] T) :

↑(h.liftEquivAroots.symm φ) = φ x

source

@[simp]

theorem IsIntegralUniqueGen.liftEquivAroots_apply_apply {R : Type u_1} {S : Type u_2} [CommRing R] [Ring S] [Algebra R S] {x : S} {g : Polynomial R} (h : IsIntegralUniqueGen x g) {T : Type u_3} [CommRing T] [IsDomain T] [Algebra R T] {y : T} (hy : y ∈ g.aroots T) (z : S) :

(h.liftEquivAroots ⟨y, hy⟩) z = (⋯.lift ⋯) z

source

noncomputable def IsIntegralUniqueGen.fintypeAlgHom {R : Type u_1} {S : Type u_2} [CommRing R] [Ring S] [Algebra R S] {x : S} {g : Polynomial R} (h : IsIntegralUniqueGen x g) {T : Type u_3} [CommRing T] [IsDomain T] [Algebra R T] :

Fintype (S →ₐ[R] T)

Equations

h.fintypeAlgHom = Fintype.ofEquiv { y : T // y ∈ g.aroots T } h.liftEquivAroots

Instances For

source

noncomputable def IsIntegralUniqueGen.equiv {R : Type u_1} {S : Type u_2} [CommRing R] [Ring S] [Algebra R S] {x : S} {g : Polynomial R} (h : IsIntegralUniqueGen x g) {S' : Type u_3} [Ring S'] [Algebra R S'] {x' : S'} (h' : IsIntegralUniqueGen x' g) :

S ≃ₐ[R] S'

Equations

h.equiv h' = ⋯.equiv ⋯

Instances For

source

@[simp]

theorem IsIntegralUniqueGen.equiv_apply {R : Type u_1} {S : Type u_2} [CommRing R] [Ring S] [Algebra R S] {x : S} {g : Polynomial R} (h : IsIntegralUniqueGen x g) {S' : Type u_3} [Ring S'] [Algebra R S'] {x' : S'} (h' : IsIntegralUniqueGen x' g) (z : S) :

(h.equiv h') z = (⋯.equiv ⋯) z

source

@[simp]

theorem IsIntegralUniqueGen.equiv_symm {R : Type u_1} {S : Type u_2} [CommRing R] [Ring S] [Algebra R S] {x : S} {g : Polynomial R} (h : IsIntegralUniqueGen x g) {S' : Type u_3} [Ring S'] [Algebra R S'] {x' : S'} (h' : IsIntegralUniqueGen x' g) :

(h.equiv h').symm = h'.equiv h

source

noncomputable def IsIntegralUniqueGen.map {R : Type u_1} {S : Type u_2} [CommRing R] [Ring S] [Algebra R S] {x : S} {g : Polynomial R} (h : IsIntegralUniqueGen x g) {T : Type u_3} [Ring T] [Algebra R T] (φ : S ≃ₐ[R] T) :

IsIntegralUniqueGen (φ x) g

Equations

⋯ = ⋯

Instances For

source

@[simp]

theorem IsIntegralUniqueGen.equivOfRoot_map {R : Type u_1} {S : Type u_2} [CommRing R] [Ring S] [Algebra R S] {x : S} {g : Polynomial R} (h : IsIntegralUniqueGen x g) {T : Type u_3} [Ring T] [Algebra R T] (φ : S ≃ₐ[R] T) :

⋯.equivOfRoot ⋯ ⋯ ⋯ = φ

source

noncomputable def IsIntegralUniqueGen.coeff {R : Type u_1} {S : Type u_2} [CommRing R] [Ring S] [Algebra R S] {x : S} {g : Polynomial R} (h : IsIntegralUniqueGen x g) :

S →ₗ[R] ℕ → R

Equations

h.coeff = { toFun := Polynomial.coeff, map_add' := ⋯, map_smul' := ⋯ } ∘ₗ h.repr

Instances For

source

theorem IsIntegralUniqueGen.coeff_apply_of_natDegree_le {R : Type u_1} {S : Type u_2} [CommRing R] [Ring S] [Algebra R S] {x : S} {g : Polynomial R} (h : IsIntegralUniqueGen x g) (z : S) {i : ℕ} (hi : g.natDegree ≤ i) :

h.coeff z i = 0

source

theorem IsIntegralUniqueGen.coeff_root_pow {R : Type u_1} {S : Type u_2} [CommRing R] [Ring S] [Algebra R S] {x : S} {g : Polynomial R} (h : IsIntegralUniqueGen x g) {n : ℕ} (hn : n < g.natDegree) :

h.coeff (x ^ n) = Pi.single n 1

source

theorem IsIntegralUniqueGen.coeff_root_pow_natDegree {R : Type u_1} {S : Type u_2} [CommRing R] [Ring S] [Algebra R S] {x : S} {g : Polynomial R} (h : IsIntegralUniqueGen x g) {i : ℕ} (hi : i < g.natDegree) :

h.coeff (x ^ g.natDegree) i = -g.coeff i

source

theorem IsIntegralUniqueGen.coeff_root {R : Type u_1} {S : Type u_2} [CommRing R] [Ring S] [Algebra R S] {x : S} {g : Polynomial R} (h : IsIntegralUniqueGen x g) (hdeg : 1 < g.natDegree) :

h.coeff x = Pi.single 1 1

source

@[simp]

theorem IsIntegralUniqueGen.coeff_one {R : Type u_1} {S : Type u_2} [CommRing R] [Ring S] [Algebra R S] {x : S} {g : Polynomial R} (h : IsIntegralUniqueGen x g) [Nontrivial S] :

h.coeff 1 = Pi.single 0 1

source

@[simp]

theorem IsIntegralUniqueGen.coeff_algebraMap {R : Type u_1} {S : Type u_2} [CommRing R] [Ring S] [Algebra R S] {x : S} {g : Polynomial R} (h : IsIntegralUniqueGen x g) [Nontrivial S] (r : R) :

h.coeff ((algebraMap R S) r) = Pi.single 0 r

source

@[simp]

theorem IsIntegralUniqueGen.coeff_ofNat {R : Type u_1} {S : Type u_2} [CommRing R] [Ring S] [Algebra R S] {x : S} {g : Polynomial R} (h : IsIntegralUniqueGen x g) [Nontrivial S] (n : ℕ) [n.AtLeastTwo] :

h.coeff (OfNat.ofNat n) = Pi.single 0 ↑n

source

noncomputable def IsIntegralUniqueGen.basis {R : Type u_1} {S : Type u_2} [CommRing R] [Ring S] [Algebra R S] {x : S} {g : Polynomial R} (h : IsIntegralUniqueGen x g) :

Module.Basis (Fin g.natDegree) R S

Equations

One or more equations did not get rendered due to their size.

Instances For

source

@[simp]

theorem IsIntegralUniqueGen.coe_basis {R : Type u_1} {S : Type u_2} [CommRing R] [Ring S] [Algebra R S] {x : S} {g : Polynomial R} (h : IsIntegralUniqueGen x g) :

⇑h.basis = fun (i : Fin g.natDegree) => x ^ ↑i

source

theorem IsIntegralUniqueGen.basis_apply {R : Type u_1} {S : Type u_2} [CommRing R] [Ring S] [Algebra R S] {x : S} {g : Polynomial R} (h : IsIntegralUniqueGen x g) (i : Fin g.natDegree) :

h.basis i = x ^ ↑i

source

theorem IsIntegralUniqueGen.root_pow_eq_basis_apply {R : Type u_1} {S : Type u_2} [CommRing R] [Ring S] [Algebra R S] {x : S} {g : Polynomial R} (h : IsIntegralUniqueGen x g) {i : ℕ} (hdeg : i < g.natDegree) :

x ^ i = h.basis ⟨i, hdeg⟩

source

theorem IsIntegralUniqueGen.root_eq_basis_one {R : Type u_1} {S : Type u_2} [CommRing R] [Ring S] [Algebra R S] {x : S} {g : Polynomial R} (h : IsIntegralUniqueGen x g) (hdeg : 1 < g.natDegree) :

x = h.basis ⟨1, hdeg⟩

source

theorem IsIntegralUniqueGen.one_eq_basis_zero {R : Type u_1} {S : Type u_2} [CommRing R] [Ring S] [Algebra R S] {x : S} {g : Polynomial R} (h : IsIntegralUniqueGen x g) [Nontrivial S] :

1 = h.basis ⟨0, ⋯⟩

source

theorem IsIntegralUniqueGen.free {R : Type u_1} {S : Type u_2} [CommRing R] [Ring S] [Algebra R S] {x : S} {g : Polynomial R} (h : IsIntegralUniqueGen x g) :

Module.Free R S

source

theorem IsIntegralUniqueGen.finite {R : Type u_1} {S : Type u_2} [CommRing R] [Ring S] [Algebra R S] {x : S} {g : Polynomial R} (h : IsIntegralUniqueGen x g) :

Module.Finite R S

source

theorem IsIntegralUniqueGen.finrank_eq_natDegree {R : Type u_1} {S : Type u_2} [CommRing R] [Ring S] [Algebra R S] {x : S} {g : Polynomial R} (h : IsIntegralUniqueGen x g) [Nontrivial R] :

Module.finrank R S = g.natDegree

source

theorem IsIntegralUniqueGen.finrank_eq_degree {R : Type u_1} {S : Type u_2} [CommRing R] [Ring S] [Algebra R S] {x : S} {g : Polynomial R} (h : IsIntegralUniqueGen x g) [Nontrivial R] :

↑(Module.finrank R S) = g.degree

source

theorem IsIntegralUniqueGen.leftMulMatrix {R : Type u_1} {S : Type u_2} [CommRing R] [Ring S] [Algebra R S] {x : S} {g : Polynomial R} (h : IsIntegralUniqueGen x g) :

(Algebra.leftMulMatrix h.basis) x = Matrix.of fun (i j : Fin g.natDegree) => if ↑j + 1 = g.natDegree then -g.coeff ↑i else if ↑i = ↑j + 1 then 1 else 0

source

theorem IsIntegralUniqueGen.basis_repr_eq_coeff {R : Type u_1} {S : Type u_2} [CommRing R] [Ring S] [Algebra R S] {x : S} {g : Polynomial R} (h : IsIntegralUniqueGen x g) (y : S) (i : Fin g.natDegree) :

(h.basis.repr y) i = h.coeff y ↑i

source

theorem IsIntegralUniqueGen.coeff_eq_basis_repr_of_lt_natDegree {R : Type u_1} {S : Type u_2} [CommRing R] [Ring S] [Algebra R S] {x : S} {g : Polynomial R} (h : IsIntegralUniqueGen x g) (z : S) (i : ℕ) (hi : i < g.natDegree) :

h.coeff z i = (h.basis.repr z) ⟨i, hi⟩

source

theorem IsIntegralUniqueGen.coeff_eq_basis_repr {R : Type u_1} {S : Type u_2} [CommRing R] [Ring S] [Algebra R S] {x : S} {g : Polynomial R} (h : IsIntegralUniqueGen x g) (z : S) (i : ℕ) :

h.coeff z i = if hi : i < g.natDegree then (h.basis.repr z) ⟨i, hi⟩ else 0

source

theorem IsIntegralUniqueGen.ext_elem {R : Type u_1} {S : Type u_2} [CommRing R] [Ring S] [Algebra R S] {x : S} {g : Polynomial R} (h : IsIntegralUniqueGen x g) ⦃y z : S⦄ (hyz : ∀ i < g.natDegree, h.coeff y i = h.coeff z i) :

y = z

source

theorem IsIntegralUniqueGen.ext_elem_iff {R : Type u_1} {S : Type u_2} [CommRing R] [Ring S] [Algebra R S] {x : S} {g : Polynomial R} (h : IsIntegralUniqueGen x g) {y z : S} :

y = z ↔ ∀ i < g.natDegree, h.coeff y i = h.coeff z i

source

theorem IsIntegralUniqueGen.coeff_injective {R : Type u_1} {S : Type u_2} [CommRing R] [Ring S] [Algebra R S] {x : S} {g : Polynomial R} (h : IsIntegralUniqueGen x g) :

Function.Injective ⇑h.coeff

source

structure IsAdjoinRoot' {R : Type u_1} (S : Type u_2) [CommRing R] [Ring S] [Algebra R S] (f : Polynomial R) :

Prop

exists_root : ∃ (x : S), Algebra.IsSimpleGenerator x f

Instances For

source

noncomputable def IsAdjoinRoot'.root {R : Type u_1} {S : Type u_2} [CommRing R] [Ring S] [Algebra R S] {f : Polynomial R} (h : IsAdjoinRoot' S f) :

Equations

h.root = ⋯.choose

Instances For

source

theorem IsAdjoinRoot'.pe {R : Type u_1} {S : Type u_2} [CommRing R] [Ring S] [Algebra R S] {f : Polynomial R} (h : IsAdjoinRoot' S f) :

Algebra.IsSimpleGenerator h.root f

source

noncomputable def IsAdjoinRoot'.liftEquiv {R : Type u_1} {S : Type u_2} [CommRing R] [Ring S] [Algebra R S] {f : Polynomial R} (h : IsAdjoinRoot' S f) {T : Type u_3} [Ring T] [Algebra R T] :

{ y : T // (Polynomial.aeval y) f = 0 } ≃ (S →ₐ[R] T)

Equations

h.liftEquiv = ((Equiv.refl T).subtypeEquiv ⋯).trans ⋯.liftEquiv

Instances For

source

noncomputable def IsAdjoinRoot'.lift {R : Type u_1} {S : Type u_2} [CommRing R] [Ring S] [Algebra R S] {f : Polynomial R} (h : IsAdjoinRoot' S f) {T : Type u_3} [Ring T] [Algebra R T] {y : T} (hy : (Polynomial.aeval y) f = 0) :

S →ₐ[R] T

Equations

h.lift hy = ⋯.lift hy

Instances For

source

noncomputable def IsAdjoinRoot'.equiv {R : Type u_1} {S : Type u_2} [CommRing R] [Ring S] [Algebra R S] {f : Polynomial R} (h : IsAdjoinRoot' S f) {T : Type u_3} [Ring T] [Algebra R T] (h' : IsAdjoinRoot' T f) :

S ≃ₐ[R] T

Equations

h.equiv h' = ⋯.equiv ⋯

Instances For

source

noncomputable def IsAdjoinRoot'.map {R : Type u_1} {S : Type u_2} [CommRing R] [Ring S] [Algebra R S] {f : Polynomial R} (h : IsAdjoinRoot' S f) {T : Type u_3} [Ring T] [Algebra R T] (φ : S ≃ₐ[R] T) :

IsAdjoinRoot' T f

Equations

⋯ = ⋯

Instances For

source

structure IsAdjoinRootMonic' {R : Type u_1} (S : Type u_2) [CommRing R] [Ring S] [Algebra R S] (f : Polynomial R) extends IsAdjoinRoot' S f :

Prop

exists_root : ∃ (x : S), Algebra.IsSimpleGenerator x f
f_monic : f.Monic

Instances For

source

theorem IsAdjoinRootMonic'.ofIsIntegralUniqueGen {R : Type u_1} {S : Type u_2} [CommRing R] [Ring S] [Algebra R S] {f : Polynomial R} {x : S} (hx : IsIntegralUniqueGen x f) :

IsAdjoinRootMonic' S f

source

theorem IsAdjoinRootMonic'.pe {R : Type u_1} {S : Type u_2} [CommRing R] [Ring S] [Algebra R S] {f : Polynomial R} (h : IsAdjoinRootMonic' S f) :

IsIntegralUniqueGen ⋯.root f

source

@[simp]

theorem IsAdjoinRootMonic'.minpoly_root {R : Type u_1} {S : Type u_2} [CommRing R] [Ring S] [Algebra R S] {f : Polynomial R} (h : IsAdjoinRootMonic' S f) :

minpoly R ⋯.root = f

source

theorem IsAdjoinRootMonic'.irreducible {R : Type u_1} {S : Type u_2} [CommRing R] [Ring S] [Algebra R S] {f : Polynomial R} (h : IsAdjoinRootMonic' S f) [IsDomain R] [IsDomain S] :

Irreducible f

source

theorem IsAdjoinRootMonic'.subsingleton {R : Type u_1} {S : Type u_2} [CommRing R] [Ring S] [Algebra R S] {f : Polynomial R} (h : IsAdjoinRootMonic' S f) (hf : f = 1) :

Subsingleton S

source

theorem IsAdjoinRootMonic'.nontrivial {R : Type u_1} {S : Type u_2} [CommRing R] [Ring S] [Algebra R S] {f : Polynomial R} (h : IsAdjoinRootMonic' S f) (hf : f ≠ 1) :

Nontrivial S

source

noncomputable def IsAdjoinRootMonic'.liftEquivAroots {R : Type u_1} {S : Type u_2} [CommRing R] [Ring S] [Algebra R S] {f : Polynomial R} (h : IsAdjoinRootMonic' S f) {T : Type u_3} [CommRing T] [IsDomain T] [Algebra R T] :

{ y : T // y ∈ f.aroots T } ≃ (S →ₐ[R] T)

Equations

h.liftEquivAroots = ⋯.liftEquivAroots

Instances For

source

noncomputable def IsAdjoinRootMonic'.fintypeAlgHom {R : Type u_1} {S : Type u_2} [CommRing R] [Ring S] [Algebra R S] {f : Polynomial R} (h : IsAdjoinRootMonic' S f) {T : Type u_3} [CommRing T] [IsDomain T] [Algebra R T] :

Fintype (S →ₐ[R] T)

Equations

h.fintypeAlgHom = ⋯.fintypeAlgHom

Instances For

source

noncomputable def IsAdjoinRootMonic'.map {R : Type u_1} {S : Type u_2} [CommRing R] [Ring S] [Algebra R S] {f : Polynomial R} (h : IsAdjoinRootMonic' S f) {T : Type u_3} [Ring T] [Algebra R T] (φ : S ≃ₐ[R] T) :

IsAdjoinRootMonic' T f

Equations

⋯ = ⋯

Instances For

source

theorem IsAdjoinRootMonic'.free {R : Type u_1} {S : Type u_2} [CommRing R] [Ring S] [Algebra R S] {f : Polynomial R} (h : IsAdjoinRootMonic' S f) :

Module.Free R S

source

theorem IsAdjoinRootMonic'.finite {R : Type u_1} {S : Type u_2} [CommRing R] [Ring S] [Algebra R S] {f : Polynomial R} (h : IsAdjoinRootMonic' S f) :

Module.Finite R S

source

theorem IsAdjoinRootMonic'.finrank_eq_natDegree {R : Type u_1} {S : Type u_2} [CommRing R] [Ring S] [Algebra R S] {f : Polynomial R} (h : IsAdjoinRootMonic' S f) [Nontrivial R] :

Module.finrank R S = f.natDegree

source

theorem IsAdjoinRootMonic'.finrank_eq_degree {R : Type u_1} {S : Type u_2} [CommRing R] [Ring S] [Algebra R S] {f : Polynomial R} (h : IsAdjoinRootMonic' S f) [Nontrivial R] :

↑(Module.finrank R S) = f.degree