HepLean Documentation

Mathlib.RingTheory.Algebraic.Integral

Algebraic elements and integral elements #

This file relates algebraic and integral elements of an algebra, by proving every integral element is algebraic and that every algebraic element over a field is integral.

Main results #

source
theorem IsIntegral.isAlgebraic {R : Type u} {A : Type v} [CommRing R] [Ring A] [Algebra R A] [Nontrivial R] {x : A} :
IsIntegral R x → IsAlgebraic R x

An integral element of an algebra is algebraic.

source
instance Algebra.IsIntegral.isAlgebraic {R : Type u} {A : Type v} [CommRing R] [Ring A] [Algebra R A] [Nontrivial R] [Algebra.IsIntegral R A] :
Algebra.IsAlgebraic R A
Equations
  • ⋯ = ⋯
source
theorem isAlgebraic_iff_isIntegral {K : Type u} {A : Type v} [Field K] [Ring A] [Algebra K A] {x : A} :
IsAlgebraic K x ↔ IsIntegral K x

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

source
theorem Algebra.isAlgebraic_iff_isIntegral {K : Type u} {A : Type v} [Field K] [Ring A] [Algebra K A] :
Algebra.IsAlgebraic K A ↔ Algebra.IsIntegral K A
source
theorem IsAlgebraic.isIntegral {K : Type u} {A : Type v} [Field K] [Ring A] [Algebra K A] {x : A} :
IsAlgebraic K x → IsIntegral K x

Alias of the forward direction of isAlgebraic_iff_isIntegral.

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

source
instance Algebra.IsAlgebraic.isIntegral {K : Type u} {A : Type v} [Field K] [Ring A] [Algebra K A] [Algebra.IsAlgebraic K A] :
Algebra.IsIntegral K A

This used to be an alias of Algebra.isAlgebraic_iff_isIntegral but that would make Algebra.IsAlgebraic K A an explicit parameter instead of instance implicit.

Equations
  • ⋯ = ⋯
source
theorem Algebra.IsAlgebraic.of_isIntegralClosure (K : Type u) [Field K] (B : Type u_1) (C : Type u_2) [CommRing B] [CommRing C] [Algebra K B] [Algebra K C] [Algebra B C] [IsScalarTower K B C] [IsIntegralClosure B K C] :
Algebra.IsAlgebraic K B
source
theorem IsAlgebraic.of_finite (K : Type u_1) {A : Type u_5} [Field K] [Ring A] [Algebra K A] (e : A) [FiniteDimensional K A] :
IsAlgebraic K e
source
instance Algebra.IsAlgebraic.of_finite (K : Type u_1) (A : Type u_5) [Field K] [Ring A] [Algebra K A] [FiniteDimensional K A] :
Algebra.IsAlgebraic K A

A field extension is algebraic if it is finite.

Stacks Tag 09GG (first part)

Equations
  • ⋯ = ⋯
source
theorem Algebra.IsAlgebraic.trans {K : Type u_1} {L : Type u_2} {A : Type u_5} [Field K] [Field L] [Ring A] [Algebra K L] [Algebra L A] [Algebra K A] [IsScalarTower K L A] [L_alg : Algebra.IsAlgebraic K L] [A_alg : Algebra.IsAlgebraic L A] :
Algebra.IsAlgebraic 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.

Stacks Tag 09GJ

source
@[simp]
theorem transcendental_aeval_iff {K : Type u_1} {A : Type u_5} [Field K] [Ring A] [Algebra K A] {r : A} {f : Polynomial K} :
Transcendental K ((Polynomial.aeval r) f) ↔ Transcendental K r ∧ Transcendental K f

If K is a field, r : A and f : K[X], then Polynomial.aeval r f is transcendental over K if and only if r and f are both transcendental over K. See also Transcendental.aeval_of_transcendental and Transcendental.of_aeval.

source
theorem AlgHom.bijective {K : Type u_1} {L : Type u_2} [Field K] [Field L] [Algebra K L] [FiniteDimensional K L] (ϕ : L →ₐ[K] L) :
Function.Bijective ⇑ϕ
source
@[reducible, inline]
noncomputable abbrev algEquivEquivAlgHom (K : Type u_1) (L : Type u_2) [Field K] [Field L] [Algebra K L] [FiniteDimensional K L] :
(L ≃ₐ[K] L) ≃* (L →ₐ[K] L)

Bijection between algebra equivalences and algebra homomorphisms

Equations
Instances For
    source
    theorem exists_integral_multiple {R : Type u_1} {S : Type u_2} [CommRing R] [CommRing S] [Algebra R S] {z : S} (hz : IsAlgebraic R z) (inj : ∀ (x : R), (algebraMap R S) x = 0 → x = 0) :
    ∃ (x : ↥(integralClosure R S)) (y : R), y ≠ 0 ∧ (algebraMap R S) y * z = ↑x