ring_theory.algebraic - mathlib3 docs

source

def is_algebraic (R : Type u) {A : Type v} [comm_ring R] [ring A] [algebra R A] (x : A) :

Prop

An element of an R-algebra is algebraic over R if it is a root of a nonzero polynomial with coefficients in R.

Equations

is_algebraic R x = ∃ (p : polynomial R), p ≠ 0 ∧ ⇑(polynomial.aeval x) p = 0

source

def transcendental (R : Type u) {A : Type v} [comm_ring R] [ring A] [algebra R A] (x : A) :

Prop

An element of an R-algebra is transcendental over R if it is not algebraic over R.

Equations

transcendental R x = ¬is_algebraic R x

source

theorem is_transcendental_of_subsingleton (R : Type u) {A : Type v} [comm_ring R] [ring A] [algebra R A] [subsingleton R] (x : A) :

transcendental R x

source

def subalgebra.is_algebraic {R : Type u} {A : Type v} [comm_ring R] [ring A] [algebra R A] (S : subalgebra R A) :

Prop

A subalgebra is algebraic if all its elements are algebraic.

Equations

S.is_algebraic = ∀ (x : A), x ∈ S → is_algebraic R x

source

def algebra.is_algebraic (R : Type u) (A : Type v) [comm_ring R] [ring A] [algebra R A] :

Prop

An algebra is algebraic if all its elements are algebraic.

Equations

algebra.is_algebraic R A = ∀ (x : A), is_algebraic R x

source

theorem subalgebra.is_algebraic_iff {R : Type u} {A : Type v} [comm_ring R] [ring A] [algebra R A] (S : subalgebra R A) :

S.is_algebraic ↔ algebra.is_algebraic R ↥S

A subalgebra is algebraic if and only if it is algebraic as an algebra.

source

theorem algebra.is_algebraic_iff {R : Type u} {A : Type v} [comm_ring R] [ring A] [algebra R A] :

algebra.is_algebraic R A ↔ ⊤.is_algebraic

An algebra is algebraic if and only if it is algebraic as a subalgebra.

source

theorem is_algebraic_iff_not_injective {R : Type u} {A : Type v} [comm_ring R] [ring A] [algebra R A] {x : A} :

is_algebraic R x ↔ ¬function.injective ⇑(polynomial.aeval x)

source

theorem is_integral.is_algebraic (R : Type u) {A : Type v} [comm_ring R] [ring A] [algebra R A] [nontrivial R] {x : A} :

is_integral R x → is_algebraic R x

An integral element of an algebra is algebraic.

source

theorem is_algebraic_zero {R : Type u} {A : Type v} [comm_ring R] [ring A] [algebra R A] [nontrivial R] :

is_algebraic R 0

source

theorem is_algebraic_algebra_map {R : Type u} {A : Type v} [comm_ring R] [ring A] [algebra R A] [nontrivial R] (x : R) :

is_algebraic R (⇑(algebra_map R A) x)

An element of R is algebraic, when viewed as an element of the R-algebra A.

source

theorem is_algebraic_one {R : Type u} {A : Type v} [comm_ring R] [ring A] [algebra R A] [nontrivial R] :

is_algebraic R 1

source

theorem is_algebraic_nat {R : Type u} {A : Type v} [comm_ring R] [ring A] [algebra R A] [nontrivial R] (n : ℕ) :

is_algebraic R ↑n

source

theorem is_algebraic_int {R : Type u} {A : Type v} [comm_ring R] [ring A] [algebra R A] [nontrivial R] (n : ℤ) :

is_algebraic R ↑n

source

theorem is_algebraic_rat (R : Type u) {A : Type v} [division_ring A] [field R] [algebra R A] (n : ℚ) :

is_algebraic R ↑n

source

theorem is_algebraic_of_mem_root_set {R : Type u} {A : Type v} [field R] [field A] [algebra R A] {p : polynomial R} {x : A} (hx : x ∈ p.root_set A) :

is_algebraic R x

source

theorem is_algebraic_algebra_map_of_is_algebraic {R : Type u} {S : Type u_1} {A : Type v} [comm_ring R] [comm_ring S] [ring A] [algebra R A] [algebra R S] [algebra S A] [is_scalar_tower R S A] {a : S} :

is_algebraic R a → is_algebraic R (⇑(algebra_map S A) a)

source

theorem is_algebraic_alg_hom_of_is_algebraic {R : Type u} {A : Type v} [comm_ring R] [ring A] [algebra R A] {B : Type u_1} [ring B] [algebra R B] (f : A →ₐ[R] B) {a : A} (h : is_algebraic R a) :

is_algebraic R (⇑f a)

This is slightly more general than is_algebraic_algebra_map_of_is_algebraic in that it allows noncommutative intermediate rings A.

source

theorem alg_equiv.is_algebraic {R : Type u} {A : Type v} [comm_ring R] [ring A] [algebra R A] {B : Type u_1} [ring B] [algebra R B] (e : A ≃ₐ[R] B) (h : algebra.is_algebraic R A) :

algebra.is_algebraic R B

Transfer algebra.is_algebraic across an alg_equiv.

source

theorem alg_equiv.is_algebraic_iff {R : Type u} {A : Type v} [comm_ring R] [ring A] [algebra R A] {B : Type u_1} [ring B] [algebra R B] (e : A ≃ₐ[R] B) :

algebra.is_algebraic R A ↔ algebra.is_algebraic R B

source

theorem is_algebraic_algebra_map_iff {R : Type u} {S : Type u_1} {A : Type v} [comm_ring R] [comm_ring S] [ring A] [algebra R A] [algebra R S] [algebra S A] [is_scalar_tower R S A] {a : S} (h : function.injective ⇑(algebra_map S A)) :

is_algebraic R (⇑(algebra_map S A) a) ↔ is_algebraic R a

source

theorem is_algebraic_of_pow {R : Type u} {A : Type v} [comm_ring R] [ring A] [algebra R A] {r : A} {n : ℕ} (hn : 0 < n) (ht : is_algebraic R (r ^ n)) :

is_algebraic R r

source

theorem transcendental.pow {R : Type u} {A : Type v} [comm_ring R] [ring A] [algebra R A] {r : A} (ht : transcendental R r) {n : ℕ} (hn : 0 < n) :

transcendental R (r ^ n)

source

theorem is_algebraic_iff_is_integral {K : Type u} {A : Type v} [field K] [ring A] [algebra K A] {x : A} :

is_algebraic K x ↔ is_integral K x

An element of an algebra over a field is algebraic if and only if it is integral.

source

@[protected]

theorem algebra.is_algebraic_iff_is_integral {K : Type u} {A : Type v} [field K] [ring A] [algebra K A] :

algebra.is_algebraic K A ↔ algebra.is_integral K A

source

theorem algebra.is_algebraic_trans {K : Type u_1} {L : Type u_2} {A : Type u_5} [field K] [field L] [comm_ring A] [algebra K L] [algebra L A] [algebra K A] [is_scalar_tower K L A] (L_alg : algebra.is_algebraic K L) (A_alg : algebra.is_algebraic L A) :

algebra.is_algebraic K A

If L is an algebraic field extension of K and A is an algebraic algebra over L, then A is algebraic over K.

source

theorem is_algebraic_of_larger_base_of_injective {R : Type u_3} {S : Type u_4} {A : Type u_5} [comm_ring R] [comm_ring S] [comm_ring A] [algebra R S] [algebra S A] [algebra R A] [is_scalar_tower R S A] (hinj : function.injective ⇑(algebra_map R S)) {x : A} (A_alg : is_algebraic R x) :

is_algebraic S x

If x is algebraic over R, then x is algebraic over S when S is an extension of R, and the map from R to S is injective.

source

theorem algebra.is_algebraic_of_larger_base_of_injective {R : Type u_3} {S : Type u_4} {A : Type u_5} [comm_ring R] [comm_ring S] [comm_ring A] [algebra R S] [algebra S A] [algebra R A] [is_scalar_tower R S A] (hinj : function.injective ⇑(algebra_map R S)) (A_alg : algebra.is_algebraic R A) :

algebra.is_algebraic S A

If A is an algebraic algebra over R, then A is algebraic over S when S is an extension of R, and the map from R to S is injective.

source

theorem is_algebraic_of_larger_base (K : Type u_1) (L : Type u_2) {A : Type u_5} [field K] [field L] [comm_ring A] [algebra K L] [algebra L A] [algebra K A] [is_scalar_tower K L A] {x : A} (A_alg : is_algebraic K x) :

is_algebraic L x

If x is a algebraic over K, then x is algebraic over L when L is an extension of K

source

theorem algebra.is_algebraic_of_larger_base (K : Type u_1) (L : Type u_2) {A : Type u_5} [field K] [field L] [comm_ring A] [algebra K L] [algebra L A] [algebra K A] [is_scalar_tower K L A] (A_alg : algebra.is_algebraic K A) :

algebra.is_algebraic L A

If A is an algebraic algebra over K, then A is algebraic over L when L is an extension of K

source

theorem algebra.is_integral_of_finite (K : Type u_1) (L : Type u_2) [field K] [field L] [algebra K L] [finite_dimensional K L] :

algebra.is_integral K L

A field extension is integral if it is finite.

source

theorem algebra.is_algebraic_of_finite (K : Type u_1) (L : Type u_2) [field K] [field L] [algebra K L] [finite : finite_dimensional K L] :

algebra.is_algebraic K L

A field extension is algebraic if it is finite.

source

theorem algebra.is_algebraic.alg_hom_bijective {K : Type u_1} {L : Type u_2} [field K] [field L] [algebra K L] (ha : algebra.is_algebraic K L) (f : L →ₐ[K] L) :

function.bijective ⇑f

source

theorem alg_hom.bijective {K : Type u_1} {L : Type u_2} [field K] [field L] [algebra K L] [finite_dimensional K L] (ϕ : L →ₐ[K] L) :

function.bijective ⇑ϕ

source

@[simp]

theorem algebra.is_algebraic.alg_equiv_equiv_alg_hom_apply (K : Type u_1) (L : Type u_2) [field K] [field L] [algebra K L] (ha : algebra.is_algebraic K L) (ϕ : L ≃ₐ[K] L) :

⇑(algebra.is_algebraic.alg_equiv_equiv_alg_hom K L ha) ϕ = ϕ.to_alg_hom

source

@[simp]

theorem algebra.is_algebraic.alg_equiv_equiv_alg_hom_symm_apply (K : Type u_1) (L : Type u_2) [field K] [field L] [algebra K L] (ha : algebra.is_algebraic K L) (ϕ : L →ₐ[K] L) :

⇑((algebra.is_algebraic.alg_equiv_equiv_alg_hom K L ha).symm) ϕ = alg_equiv.of_bijective ϕ _

source

noncomputable def algebra.is_algebraic.alg_equiv_equiv_alg_hom (K : Type u_1) (L : Type u_2) [field K] [field L] [algebra K L] (ha : algebra.is_algebraic K L) :

(L ≃ₐ[K] L) ≃* (L →ₐ[K] L)

Bijection between algebra equivalences and algebra homomorphisms

Equations

algebra.is_algebraic.alg_equiv_equiv_alg_hom K L ha = {to_fun := λ (ϕ : L ≃ₐ[K] L), ϕ.to_alg_hom, inv_fun := λ (ϕ : L →ₐ[K] L), alg_equiv.of_bijective ϕ _, left_inv := _, right_inv := _, map_mul' := _}

source

@[reducible]

noncomputable def alg_equiv_equiv_alg_hom (K : Type u_1) (L : Type u_2) [field K] [field L] [algebra K L] [finite_dimensional K L] :

(L ≃ₐ[K] L) ≃* (L →ₐ[K] L)

Bijection between algebra equivalences and algebra homomorphisms

Equations

alg_equiv_equiv_alg_hom K L = algebra.is_algebraic.alg_equiv_equiv_alg_hom K L _

source

theorem exists_integral_multiple {R : Type u_1} {S : Type u_2} [comm_ring R] [is_domain R] [comm_ring S] [algebra R S] {z : S} (hz : is_algebraic R z) (inj : ∀ (x : R), ⇑(algebra_map R S) x = 0 → x = 0) :

∃ (x : ↥(integral_closure R S)) (y : R) (H : y ≠ 0), z * ⇑(algebra_map R S) y = ↑x

source

theorem is_integral_closure.exists_smul_eq_mul {R : Type u_1} {S : Type u_2} [comm_ring R] [is_domain R] [comm_ring S] {L : Type u_3} [field L] [algebra R S] [algebra S L] [algebra R L] [is_scalar_tower R S L] [is_integral_closure S R L] (h : algebra.is_algebraic R L) (inj : function.injective ⇑(algebra_map R L)) (a : S) {b : S} (hb : b ≠ 0) :

∃ (c : S) (d : R) (H : d ≠ 0), d • a = b * c

A fraction (a : S) / (b : S) can be reduced to (c : S) / (d : R), if S is the integral closure of R in an algebraic extension L of R.

source

theorem inv_eq_of_aeval_div_X_ne_zero {K : Type u_3} {L : Type u_4} [field K] [field L] [algebra K L] {x : L} {p : polynomial K} (aeval_ne : ⇑(polynomial.aeval x) p.div_X ≠ 0) :

x⁻¹ = ⇑(polynomial.aeval x) p.div_X / (⇑(polynomial.aeval x) p - ⇑(algebra_map K L) (p.coeff 0))

source

theorem inv_eq_of_root_of_coeff_zero_ne_zero {K : Type u_3} {L : Type u_4} [field K] [field L] [algebra K L] {x : L} {p : polynomial K} (aeval_eq : ⇑(polynomial.aeval x) p = 0) (coeff_zero_ne : p.coeff 0 ≠ 0) :

x⁻¹ = -(⇑(polynomial.aeval x) p.div_X / ⇑(algebra_map K L) (p.coeff 0))

source

theorem subalgebra.inv_mem_of_root_of_coeff_zero_ne_zero {K : Type u_3} {L : Type u_4} [field K] [field L] [algebra K L] (A : subalgebra K L) {x : ↥A} {p : polynomial K} (aeval_eq : ⇑(polynomial.aeval x) p = 0) (coeff_zero_ne : p.coeff 0 ≠ 0) :

(↑x)⁻¹ ∈ A

source

theorem subalgebra.inv_mem_of_algebraic {K : Type u_3} {L : Type u_4} [field K] [field L] [algebra K L] (A : subalgebra K L) {x : ↥A} (hx : is_algebraic K ↑x) :

(↑x)⁻¹ ∈ A

source

theorem subalgebra.is_field_of_algebraic {K : Type u_3} {L : Type u_4} [field K] [field L] [algebra K L] (A : subalgebra K L) (hKL : algebra.is_algebraic K L) :

is_field ↥A

In an algebraic extension L/K, an intermediate subalgebra is a field.

source

def polynomial.has_smul_pi (R' : Type u) (S' : Type v) [semiring R'] [has_smul R' S'] :

has_smul (polynomial R') (R' → S')

This is not an instance as it forms a diamond with pi.has_smul.

See the instance_diamonds test for details.

Equations

polynomial.has_smul_pi R' S' = {smul := λ (p : polynomial R') (f : R' → S') (x : R'), polynomial.eval x p • f x}

source

noncomputable def polynomial.has_smul_pi' (R' : Type u) (S' : Type v) (T' : Type w) [comm_semiring R'] [semiring S'] [algebra R' S'] [has_smul S' T'] :

has_smul (polynomial R') (S' → T')

This is not an instance as it forms a diamond with pi.has_smul.

See the instance_diamonds test for details.

Equations

polynomial.has_smul_pi' R' S' T' = {smul := λ (p : polynomial R') (f : S' → T') (x : S'), ⇑(polynomial.aeval x) p • f x}

source

@[simp]

theorem polynomial_smul_apply (R' : Type u) (S' : Type v) [semiring R'] [has_smul R' S'] (p : polynomial R') (f : R' → S') (x : R') :

(p • f) x = polynomial.eval x p • f x

source

@[simp]

theorem polynomial_smul_apply' (R' : Type u) (S' : Type v) (T' : Type w) [comm_semiring R'] [semiring S'] [algebra R' S'] [has_smul S' T'] (p : polynomial R') (f : S' → T') (x : S') :

(p • f) x = ⇑(polynomial.aeval x) p • f x

source

noncomputable def polynomial.algebra_pi (R' : Type u) (S' : Type v) (T' : Type w) [comm_semiring R'] [comm_semiring S'] [comm_semiring T'] [algebra R' S'] [algebra S' T'] :

algebra (polynomial R') (S' → T')

This is not an instance for the same reasons as polynomial.has_smul_pi'.

Equations

polynomial.algebra_pi R' S' T' = {to_has_smul := {smul := has_smul.smul (polynomial.has_smul_pi' R' S' T')}, to_ring_hom := {to_fun := λ (p : polynomial R') (z : S'), ⇑(algebra_map S' T') (⇑(polynomial.aeval z) p), map_one' := _, map_mul' := _, map_zero' := _, map_add' := _}, commutes' := _, smul_def' := _}

source

@[simp]

theorem polynomial.algebra_map_pi_eq_aeval (R' : Type u) (S' : Type v) (T' : Type w) [comm_semiring R'] [comm_semiring S'] [comm_semiring T'] [algebra R' S'] [algebra S' T'] :

⇑(algebra_map (polynomial R') (S' → T')) = λ (p : polynomial R') (z : S'), ⇑(algebra_map S' T') (⇑(polynomial.aeval z) p)

source

@[simp]

theorem polynomial.algebra_map_pi_self_eq_eval (R' : Type u) [comm_semiring R'] :

⇑(algebra_map (polynomial R') (R' → R')) = λ (p : polynomial R') (z : R'), polynomial.eval z p

mathlib3 documentation

Algebraic elements and algebraic extensions #