Mathlib.RingTheory.Algebraic.Defs

Module docstring

{"# Algebraic elements and algebraic extensions

An element of an R-algebra is algebraic over R if it is the root of a nonzero polynomial. An R-algebra is algebraic over R if and only if all its elements are algebraic over R.

Main definitions

IsAlgebraic: algebraic elements of an algebra.
Transcendental: transcendental elements of an algebra are those that are not algebraic.
Subalgebra.IsAlgebraic: a subalgebra is algebraic if all its elements are algebraic.
Algebra.IsAlgebraic: an algebra is algebraic if all its elements are algebraic.
Algebra.Transcendental: an algebra is transcendental if some element is transcendental.

Main results

transcendental_iff: an element x : A is transcendental over R iff out of R[X] only the zero polynomial evaluates to 0 at x.
Subalgebra.isAlgebraic_iff: a subalgebra is algebraic iff it is algebraic as an algebra. "}

IsAlgebraic definition

(x : A) : Prop

Full source

/-- An element of an R-algebra is algebraic over R if it is a root of a nonzero polynomial
with coefficients in R. -/
@[stacks 09GC "Algebraic elements"]
def IsAlgebraic (x : A) : Prop :=
  ∃ p : R[X], p ≠ 0 ∧ aeval x p = 0

Algebraic element over a ring

Informal description

An element $ x $ of an $ R $-algebra $ A $ is called *algebraic* over $ R $ if there exists a nonzero polynomial $ p \in R[X] $ such that $ p(x) = 0 $, where $ p(x) $ denotes the evaluation of $ p $ at $ x $ via the algebra structure.

Transcendental definition

(x : A) : Prop

Full source

/-- An element of an R-algebra is transcendental over R if it is not algebraic over R. -/
def Transcendental (x : A) : Prop :=
  ¬IsAlgebraic R x

Transcendental element over a ring

Informal description

An element $ x $ of an $ R $-algebra $ A $ is called *transcendental* over $ R $ if it is not algebraic over $ R $, i.e., there does not exist any nonzero polynomial $ p \in R[X] $ such that $ p(x) = 0 $.

transcendental_iff theorem

{x : A} : Transcendental R x ↔ ∀ p : R[X], aeval x p = 0 → p = 0

Full source

/-- An element `x` is transcendental over `R` if and only if for any polynomial `p`,
`Polynomial.aeval x p = 0` implies `p = 0`. This is similar to `algebraicIndependent_iff`. -/
theorem transcendental_iff {x : A} :
    TranscendentalTranscendental R x ↔ ∀ p : R[X], aeval x p = 0 → p = 0 := by
  rw [Transcendental, IsAlgebraic, not_exists]
  congr! 1; tauto

Characterization of Transcendental Elements: $\text{Transcendental}(R, x) \leftrightarrow \forall p \in R[X],\, \text{aeval}\, x\, p = 0 \rightarrow p = 0$

Informal description

An element $x$ of an $R$-algebra $A$ is transcendental over $R$ if and only if for every polynomial $p \in R[X]$, the evaluation of $p$ at $x$ via the algebra structure is zero only when $p$ is the zero polynomial. In other words, $x$ is transcendental over $R$ if and only if the only polynomial in $R[X]$ that vanishes at $x$ is the zero polynomial.

Subalgebra.IsAlgebraic definition

(S : Subalgebra R A) : Prop

Full source

/-- A subalgebra is algebraic if all its elements are algebraic. -/
protected def Subalgebra.IsAlgebraic (S : Subalgebra R A) : Prop :=
  ∀ x ∈ S, IsAlgebraic R x

Algebraic subalgebra

Informal description

A subalgebra $ S $ of an $ R $-algebra $ A $ is called *algebraic* if every element $ x \in S $ is algebraic over $ R $, i.e., there exists a nonzero polynomial $ p \in R[X] $ such that $ p(x) = 0 $.

Algebra.IsAlgebraic structure

Full source

/-- An algebra is algebraic if all its elements are algebraic. -/
@[stacks 09GC "Algebraic extensions"]
protected class Algebra.IsAlgebraic : Prop where
  isAlgebraic : ∀ x : A, IsAlgebraic R x

Algebraic algebra over a ring

Informal description

An algebra $A$ over a ring $R$ is called algebraic if every element $x \in A$ is algebraic over $R$, meaning that there exists a nonzero polynomial $p \in R[X]$ such that $p(x) = 0$.

Algebra.Transcendental structure

Full source

/-- An algebra is transcendental if some element is transcendental. -/
protected class Algebra.Transcendental : Prop where
  transcendental : ∃ x : A, Transcendental R x

Transcendental algebra

Informal description

An algebra $A$ over a ring $R$ is called *transcendental* if there exists at least one element in $A$ that is transcendental over $R$, i.e., not algebraic over $R$.

Algebra.isAlgebraic_def theorem

: Algebra.IsAlgebraic R A ↔ ∀ x : A, IsAlgebraic R x

Full source

lemma Algebra.isAlgebraic_def : Algebra.IsAlgebraicAlgebra.IsAlgebraic R A ↔ ∀ x : A, IsAlgebraic R x :=
  ⟨fun ⟨h⟩ ↦ h, fun h ↦ ⟨h⟩⟩

Characterization of Algebraic Algebras: $A$ is algebraic over $R$ iff all elements are algebraic over $R$

Informal description

An algebra $A$ over a ring $R$ is algebraic if and only if every element $x \in A$ is algebraic over $R$.

Algebra.transcendental_def theorem

: Algebra.Transcendental R A ↔ ∃ x : A, Transcendental R x

Full source

lemma Algebra.transcendental_def : Algebra.TranscendentalAlgebra.Transcendental R A ↔ ∃ x : A, Transcendental R x :=
  ⟨fun ⟨h⟩ ↦ h, fun h ↦ ⟨h⟩⟩

Characterization of Transcendental Algebras: $\exists x \in A$, $x$ transcendental over $R$

Informal description

An algebra $A$ over a ring $R$ is transcendental if and only if there exists an element $x \in A$ that is transcendental over $R$.

Algebra.transcendental_iff_not_isAlgebraic theorem

: Algebra.Transcendental R A ↔ ¬Algebra.IsAlgebraic R A

Full source

theorem Algebra.transcendental_iff_not_isAlgebraic :
    Algebra.TranscendentalAlgebra.Transcendental R A ↔ ¬ Algebra.IsAlgebraic R A := by
  simp [isAlgebraic_def, transcendental_def, Transcendental]

Transcendental Algebra Characterization: $A$ is transcendental over $R$ $\leftrightarrow$ $A$ is not algebraic over $R$

Informal description

An algebra $A$ over a ring $R$ is transcendental if and only if it is not algebraic, i.e., there exists at least one element in $A$ that is not algebraic over $R$.

Subalgebra.isAlgebraic_iff theorem

(S : Subalgebra R A) : S.IsAlgebraic ↔ Algebra.IsAlgebraic R S

Full source

/-- A subalgebra is algebraic if and only if it is algebraic as an algebra. -/
theorem Subalgebra.isAlgebraic_iff (S : Subalgebra R A) :
    S.IsAlgebraic ↔ Algebra.IsAlgebraic R S := by
  delta Subalgebra.IsAlgebraic
  rw [Subtype.forall', Algebra.isAlgebraic_def]
  refine forall_congr' fun x => exists_congr fun p => and_congr Iff.rfl ?_
  have h : Function.Injective S.val := Subtype.val_injective
  conv_rhs => rw [← h.eq_iff, map_zero]
  rw [← aeval_algHom_apply, S.val_apply]

Subalgebra is Algebraic iff it is Algebraic as an Algebra

Informal description

A subalgebra $S$ of an $R$-algebra $A$ is algebraic (i.e., every element of $S$ is algebraic over $R$) if and only if $S$ is algebraic as an $R$-algebra (i.e., the algebra structure on $S$ is algebraic over $R$).

Algebra.isAlgebraic_iff theorem

: Algebra.IsAlgebraic R A ↔ (⊤ : Subalgebra R A).IsAlgebraic

Full source

/-- An algebra is algebraic if and only if it is algebraic as a subalgebra. -/
theorem Algebra.isAlgebraic_iff : Algebra.IsAlgebraicAlgebra.IsAlgebraic R A ↔ (⊤ : Subalgebra R A).IsAlgebraic := by
  delta Subalgebra.IsAlgebraic
  simp only [Algebra.isAlgebraic_def, Algebra.mem_top, forall_prop_of_true]

Characterization of Algebraic Algebras via Top Subalgebra

Informal description

An $R$-algebra $A$ is algebraic over $R$ if and only if the top subalgebra of $A$ (i.e., $A$ itself viewed as a subalgebra) is algebraic over $R$.