doc-next-gen

Mathlib.RingTheory.Algebraic.Integral

Module docstring

{"# 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

  • IsIntegral.isAlgebraic, Algebra.IsIntegral.isAlgebraic: integral implies algebraic.
  • isAlgebraic_iff_isIntegral, Algebra.isAlgebraic_iff_isIntegral: integral iff algebraic over a field.
  • IsAlgebraic.of_finite, Algebra.IsAlgebraic.of_finite: finite-dimensional (as module) implies algebraic.
  • IsAlgebraic.exists_integral_multiple: an algebraic element has a multiple which is integral
  • IsAlgebraic.iff_exists_smul_integral: If R is reduced and S is an R-algebra with injective algebraMap, then an element of S is algebraic over R iff some R-multiple is integral over R.
  • Algebra.IsAlgebraic.trans: If A/S/R is a tower of algebras and both A/S and S/R are algebraic, then A/R is also algebraic, provided that S has no zero divisors.
  • Subalgebra.algebraicClosure: If R is a domain and S is an arbitrary R-algebra, then the elements of S that are algebraic over R form a subalgebra.
  • Transcendental.extendScalars: an element of an R-algebra that is transcendental over R remains transcendental over any algebraic R-subalgebra that has no zero divisors. ","The next theorem may fail if only R is assumed to be a domain but S is not: for example, let S = R[X] ⧸ (X² - X) and let A be the subalgebra of S[Y] generated by XY. A is algebraic over S because any element ∑ᵢ sᵢ(XY)ⁱ is a root of the polynomial (X - 1)(Z - s₀) in S[Z], because X(X - 1) = X² - X = 0 in S. However, XY is a transcendental element in A over R, because ∑ᵢ rᵢ(XY)ⁱ = 0 in S[Y] implies all rᵢXⁱ = 0 (i.e., r₀ = 0 and rᵢX = 0 for i > 0) in S, which implies rᵢ = 0 in R. This example is inspired by the comment https://mathoverflow.net/questions/482944/when-do-algebraic-elements-form-a-subalgebra#comment1257632_482944. "}
IsIntegral.isAlgebraic theorem
[Nontrivial R] {x : A} : IsIntegral R x → IsAlgebraic R x
Full source 
/-- An integral element of an algebra is algebraic. -/
theorem IsIntegral.isAlgebraic [Nontrivial R] {x : A} : IsIntegral R x → IsAlgebraic R x :=
  fun ⟨p, hp, hpx⟩ => ⟨p, hp.ne_zero, hpx⟩
Integral Elements are Algebraic
Informal description
Let $R$ be a nontrivial commutative ring and $A$ an $R$-algebra. For any element $x \in A$ that is integral over $R$, $x$ is algebraic over $R$.
isAlgebraic_iff_isIntegral theorem
{x : A} : IsAlgebraic K x ↔ IsIntegral K x
Full source 
/-- An element of an algebra over a field is algebraic if and only if it is integral. -/
theorem isAlgebraic_iff_isIntegral {x : A} : IsAlgebraicIsAlgebraic K x ↔ IsIntegral K x := by
  refine ⟨?_, IsIntegral.isAlgebraic⟩
  rintro ⟨p, hp, hpx⟩
  refine ⟨_, monic_mul_leadingCoeff_inv hp, ?_⟩
  rw [← aeval_def, map_mul, hpx, zero_mul]
Algebraic iff Integral over a Field
Informal description
Let $K$ be a field and $A$ a $K$-algebra. An element $x \in A$ is algebraic over $K$ if and only if it is integral over $K$.
Algebra.isAlgebraic_iff_isIntegral theorem
: Algebra.IsAlgebraic K A ↔ Algebra.IsIntegral K A
Full source 
protected theorem Algebra.isAlgebraic_iff_isIntegral :
    Algebra.IsAlgebraicAlgebra.IsAlgebraic K A ↔ Algebra.IsIntegral K A := by
  rw [Algebra.isAlgebraic_def, Algebra.isIntegral_def,
      forall_congr' fun _ ↦ isAlgebraic_iff_isIntegral]
Algebraic iff Integral for Field Extensions
Informal description
Let $K$ be a field and $A$ a $K$-algebra. Then $A$ is algebraic over $K$ if and only if $A$ is integral over $K$.
Algebra.IsAlgebraic.isIntegral instance
[Algebra.IsAlgebraic K A] : Algebra.IsIntegral K A
Full source 
/-- 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. -/
protected instance Algebra.IsAlgebraic.isIntegral [Algebra.IsAlgebraic K A] :
    Algebra.IsIntegral K A := Algebra.isAlgebraic_iff_isIntegral.mp ‹_›
Algebraic Implies Integral for Field Extensions
Informal description
For any field $K$ and $K$-algebra $A$, if $A$ is algebraic over $K$, then $A$ is integral over $K$.
Algebra.IsAlgebraic.of_isIntegralClosure theorem
(R B C : Type*) [CommRing R] [Nontrivial R] [CommRing B] [CommRing C] [Algebra R B] [Algebra R C] [Algebra B C] [IsScalarTower R B C] [IsIntegralClosure B R C] : Algebra.IsAlgebraic R B
Full source 
theorem Algebra.IsAlgebraic.of_isIntegralClosure (R B C : Type*) [CommRing R] [Nontrivial R]
    [CommRing B] [CommRing C] [Algebra R B] [Algebra R C] [Algebra B C]
    [IsScalarTower R B C] [IsIntegralClosure B R C] : Algebra.IsAlgebraic R B :=
  have := IsIntegralClosure.isIntegral_algebra R (A := B) C
  inferInstance
Algebraicity of Integral Closure Algebra Over a Nontrivial Ring
Informal description
Let $R$ be a nontrivial commutative ring, and let $B$ and $C$ be commutative rings with algebra structures forming a tower $R \to B \to C$. If $B$ is the integral closure of $R$ in $C$, then the $R$-algebra $B$ is algebraic over $R$, meaning every element of $B$ is algebraic over $R$.
IsAlgebraic.of_finite theorem
(e : A) [Module.Finite R A] : IsAlgebraic R e
Full source 
theorem IsAlgebraic.of_finite (e : A) [Module.Finite R A] : IsAlgebraic R e :=
  (IsIntegral.of_finite R e).isAlgebraic
Finitely Generated Module Elements are Algebraic Over Base Ring
Informal description
Let $R$ be a commutative ring and $A$ be an $R$-algebra that is finitely generated as an $R$-module. Then every element $e \in A$ is algebraic over $R$, meaning there exists a nonzero polynomial $p \in R[X]$ such that $p(e) = 0$.
Algebra.IsAlgebraic.of_finite instance
[Module.Finite R A] : Algebra.IsAlgebraic R A
Full source 
/-- A field extension is algebraic if it is finite. -/
@[stacks 09GG "first part"]
instance Algebra.IsAlgebraic.of_finite [Module.Finite R A] : Algebra.IsAlgebraic R A :=
  (IsIntegral.of_finite R A).isAlgebraic
Finite-Dimensional Algebras are Algebraic
Informal description
Every finite-dimensional algebra over a ring $R$ is algebraic over $R$. In other words, if an $R$-algebra $A$ is finitely generated as an $R$-module, then every element of $A$ is algebraic over $R$.
transcendental_aeval_iff theorem
{r : A} {f : K[X]} : Transcendental K (Polynomial.aeval r f) ↔ Transcendental K r ∧ Transcendental K f
Full source 
/-- 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`. -/
@[simp]
theorem transcendental_aeval_iff {r : A} {f : K[X]} :
    TranscendentalTranscendental K (Polynomial.aeval r f) ↔ Transcendental K r ∧ Transcendental K f := by
  refine ⟨fun h ↦ ⟨?_, h.of_aeval⟩, fun ⟨h1, h2⟩ ↦ h1.aeval_of_transcendental h2⟩
  rw [Transcendental] at h ⊢
  contrapose! h
  rw [isAlgebraic_iff_isIntegral] at h ⊢
  exact .of_mem_of_fg _ h.fg_adjoin_singleton _ (aeval_mem_adjoin_singleton _ _)
Transcendence Criterion for Polynomial Evaluation: $\text{Transcendental}(K, \text{aeval}\, r\, f) \leftrightarrow \text{Transcendental}(K, r) \land \text{Transcendental}(K, f)$
Informal description
Let $K$ be a field, $A$ a $K$-algebra, $r \in A$, and $f \in K[X]$. The evaluation $\text{aeval}\, r\, f$ is transcendental over $K$ if and only if both $r$ and $f$ are transcendental over $K$.
algEquivEquivAlgHom abbrev
[FiniteDimensional K L] : (L ≃ₐ[K] L) ≃* (L →ₐ[K] L)
Full source 
/-- Bijection between algebra equivalences and algebra homomorphisms -/
noncomputable abbrev algEquivEquivAlgHom [FiniteDimensional K L] :
    (L ≃ₐ[K] L) ≃* (L →ₐ[K] L) :=
  Algebra.IsAlgebraic.algEquivEquivAlgHom K L
Bijection between algebra automorphisms and algebra homomorphisms in finite extensions
Informal description
For a finite-dimensional field extension $L$ of $K$, there is a multiplicative bijection between the set of $K$-algebra automorphisms of $L$ (i.e., $K$-algebra isomorphisms from $L$ to itself) and the set of $K$-algebra homomorphisms from $L$ to itself.
IsAlgebraic.exists_integral_multiple theorem
(hz : IsAlgebraic R z) : ∃ y ≠ (0 : R), IsIntegral R (y • z)
Full source 
theorem exists_integral_multiple (hz : IsAlgebraic R z) : ∃ y ≠ (0 : R), IsIntegral R (y • z) := by
  by_cases inj : Function.Injective (algebraMap R A); swap
  · rw [injective_iff_map_eq_zero] at inj; push_neg at inj
    have ⟨r, eq, ne⟩ := inj
    exact ⟨r, ne, by simpa [← algebraMap_smul A, eq, zero_smul] using isIntegral_zero⟩
  have ⟨p, p_ne_zero, px⟩ := hz
  set a := p.leadingCoeff
  have a_ne_zero : a ≠ 0 := mt Polynomial.leadingCoeff_eq_zero.mp p_ne_zero
  have x_integral : IsIntegral R (algebraMap R A a * z) :=
    ⟨p.integralNormalization, monic_integralNormalization p_ne_zero,
      integralNormalization_aeval_eq_zero px fun _ ↦ (map_eq_zero_iff _ inj).mp⟩
  exact ⟨_, a_ne_zero, Algebra.smul_def a z ▸ x_integral⟩
Existence of Integral Multiple for Algebraic Elements
Informal description
For any element $z$ in an $R$-algebra $A$ that is algebraic over $R$, there exists a nonzero element $y \in R$ such that the scalar multiple $y \cdot z$ is integral over $R$.
Algebra.IsAlgebraic.exists_integral_multiples theorem
[NoZeroDivisors R] [alg : Algebra.IsAlgebraic R A] (s : Finset A) : ∃ y ≠ (0 : R), ∀ z ∈ s, IsIntegral R (y • z)
Full source 
theorem _root_.Algebra.IsAlgebraic.exists_integral_multiples [NoZeroDivisors R]
    [alg : Algebra.IsAlgebraic R A] (s : Finset A) :
    ∃ y ≠ (0 : R), ∀ z ∈ s, IsIntegral R (y • z) := by
  have := Algebra.IsAlgebraic.nontrivial R A
  choose r hr int using fun x ↦ (alg.1 x).exists_integral_multiple
  refine ⟨∏ x ∈ s, r x, Finset.prod_ne_zero_iff.mpr fun _ _ ↦ hr _, fun _ h ↦ ?_⟩
  classical rw [← Finset.prod_erase_mul _ _ h, mul_smul]
  exact (int _).smul _
Existence of Common Integral Multiple for Finite Sets in Algebraic Algebras over Domains
Informal description
Let $R$ be a ring with no zero divisors and $A$ an $R$-algebra that is algebraic over $R$. For any finite subset $s \subset A$, there exists a nonzero element $y \in R$ such that for every $z \in s$, the scalar multiple $y \cdot z$ is integral over $R$.
IsAlgebraic.of_smul_isIntegral theorem
{y : R} (hy : ¬IsNilpotent y) (h : IsIntegral R (y • z)) : IsAlgebraic R z
Full source 
theorem of_smul_isIntegral {y : R} (hy : ¬ IsNilpotent y)
    (h : IsIntegral R (y • z)) : IsAlgebraic R z := by
  have ⟨p, monic, eval0⟩ := h
  refine ⟨p.comp (C y * X), fun h ↦ ?_, by simpa [aeval_comp, Algebra.smul_def] using eval0⟩
  apply_fun (coeff · p.natDegree) at h
  have hy0 : y ≠ 0 := by rintro rfl; exact hy .zero
  rw [coeff_zero, ← mul_one p.natDegree, ← natDegree_C_mul_X y hy0,
    coeff_comp_degree_mul_degree, monic, one_mul, leadingCoeff_C_mul_X] at h
  · exact hy ⟨_, h⟩
  · rw [natDegree_C_mul_X _ hy0]; rintro ⟨⟩
Algebraicity from Integrality of Scalar Multiple with Non-Nilpotent Coefficient
Informal description
Let $R$ be a commutative ring and $A$ an $R$-algebra. For any element $y \in R$ that is not nilpotent and any element $z \in A$, if the scalar multiple $y \cdot z$ is integral over $R$, then $z$ is algebraic over $R$.
IsAlgebraic.of_smul theorem
{y : R} (hy : y ∈ nonZeroDivisors R) (h : IsAlgebraic R (y • z)) : IsAlgebraic R z
Full source 
theorem of_smul {y : R} (hy : y ∈ nonZeroDivisors R)
    (h : IsAlgebraic R (y • z)) : IsAlgebraic R z :=
  have ⟨p, hp, eval0⟩ := h
  ⟨_, mt (comp_C_mul_X_eq_zero_iff hy).mp hp, by simpa [aeval_comp, Algebra.smul_def] using eval0⟩
Algebraicity of Scalar Multiple Implies Algebraicity of Element
Informal description
Let $R$ be a ring and $A$ an $R$-algebra. For any element $y \in R$ that is a non-zero divisor and any element $z \in A$, if the scalar multiple $y \cdot z$ is algebraic over $R$, then $z$ is also algebraic over $R$.
IsAlgebraic.iff_exists_smul_integral theorem
[IsReduced R] : IsAlgebraic R z ↔ ∃ y ≠ (0 : R), IsIntegral R (y • z)
Full source 
theorem iff_exists_smul_integral [IsReduced R] :
    IsAlgebraicIsAlgebraic R z ↔ ∃ y ≠ (0 : R), IsIntegral R (y • z) :=
  ⟨(exists_integral_multiple ·), fun ⟨_, hy, int⟩ ↦
    of_smul_isIntegral (by rwa [isNilpotent_iff_eq_zero]) int⟩
Algebraic Elements and Integral Multiples over Reduced Rings
Informal description
Let $R$ be a reduced commutative ring and $A$ an $R$-algebra. An element $z \in A$ is algebraic over $R$ if and only if there exists a nonzero element $y \in R$ such that the scalar multiple $y \cdot z$ is integral over $R$.
IsAlgebraic.restrictScalars_of_isIntegral theorem
[int : Algebra.IsIntegral R S] {a : A} (h : IsAlgebraic S a) : IsAlgebraic R a
Full source 
theorem restrictScalars_of_isIntegral [int : Algebra.IsIntegral R S]
    {a : A} (h : IsAlgebraic S a) : IsAlgebraic R a := by
  by_cases hRS : Function.Injective (algebraMap R S)
  on_goal 2 => exact (Algebra.isAlgebraic_of_not_injective
    fun h ↦ hRS <| .of_comp (IsScalarTower.algebraMap_eq R S A ▸ h)).1 _
  have := hRS.noZeroDivisors _ (map_zero _) (map_mul _)
  have ⟨s, hs, int_s⟩ := h.exists_integral_multiple
  cases subsingleton_or_nontrivial R
  · have := Module.subsingleton R S
    exact (is_transcendental_of_subsingleton _ _ h).elim
  have ⟨r, hr, _, e⟩ := (int.1 s).isAlgebraic.exists_nonzero_dvd (mem_nonZeroDivisors_of_ne_zero hs)
  refine .of_smul_isIntegral (y := r) (by rwa [isNilpotent_iff_eq_zero]) ?_
  rw [Algebra.smul_def, IsScalarTower.algebraMap_apply R S,
    e, ← Algebra.smul_def, mul_comm, mul_smul]
  exact isIntegral_trans _ (int_s.smul _)
Algebraicity under Base Change for Integral Algebras
Informal description
Let $R$ be a commutative ring and $S$ an $R$-algebra that is integral over $R$. For any element $a$ in an $S$-algebra $A$, if $a$ is algebraic over $S$, then $a$ is also algebraic over $R$.
IsAlgebraic.restrictScalars theorem
[Algebra.IsAlgebraic R S] {a : A} (h : IsAlgebraic S a) : IsAlgebraic R a
Full source 
theorem restrictScalars [Algebra.IsAlgebraic R S]
    {a : A} (h : IsAlgebraic S a) : IsAlgebraic R a := by
  have ⟨p, hp, eval0⟩ := h
  by_cases hRS : Function.Injective (algebraMap R S)
  on_goal 2 => exact (Algebra.isAlgebraic_of_not_injective
    fun h ↦ hRS <| .of_comp (IsScalarTower.algebraMap_eq R S A ▸ h)).1 _
  have := hRS.noZeroDivisors _ (map_zero _) (map_mul _)
  classical
  have ⟨r, hr, int⟩ := Algebra.IsAlgebraic.exists_integral_multiples R (p.support.image (coeff p))
  let p := (r • p).toSubring (integralClosure R S).toSubring fun s hs ↦ by
    obtain ⟨n, hn, rfl⟩ := mem_coeffs_iff.mp hs
    exact int _ (Finset.mem_image_of_mem _ <| support_smul _ _ hn)
  have : IsAlgebraic (integralClosure R S) a := by
    refine ⟨p, ?_, ?_⟩
    · have : FaithfulSMul R S := (faithfulSMul_iff_algebraMap_injective R S).mpr hRS
      simpa only [← Polynomial.map_ne_zero_iff (f := Subring.subtype _) Subtype.val_injective,
        p, map_toSubring, smul_ne_zero_iff] using And.intro hr hp
    rw [← eval_map_algebraMap, Subalgebra.algebraMap_eq, ← map_map, ← Subalgebra.toSubring_subtype,
      map_toSubring, eval_map_algebraMap, ← AlgHom.restrictScalars_apply R,
      map_smul, AlgHom.restrictScalars_apply, eval0, smul_zero]
  exact restrictScalars_of_isIntegral _ this
Algebraicity under Base Change for Algebraic Algebras
Informal description
Let $R$ be a commutative ring and $S$ an $R$-algebra that is algebraic over $R$. For any element $a$ in an $S$-algebra $A$, if $a$ is algebraic over $S$, then $a$ is also algebraic over $R$.
IsIntegral.trans_isAlgebraic theorem
[alg : Algebra.IsAlgebraic R S] {a : A} (h : IsIntegral S a) : IsAlgebraic R a
Full source 
theorem _root_.IsIntegral.trans_isAlgebraic [alg : Algebra.IsAlgebraic R S]
    {a : A} (h : IsIntegral S a) : IsAlgebraic R a := by
  cases subsingleton_or_nontrivial A
  · have := Algebra.IsAlgebraic.nontrivial R S
    exact Subsingleton.elim a 0 ▸ isAlgebraic_zero
  · have := Module.nontrivial S A
    exact h.isAlgebraic.restrictScalars _
Integral Elements over Algebraic Algebras are Algebraic
Informal description
Let $R$ be a commutative ring and $S$ an $R$-algebra that is algebraic over $R$. For any element $a$ in an $S$-algebra $A$, if $a$ is integral over $S$, then $a$ is algebraic over $R$.
IsAlgebraic.smul theorem
(r : R) : IsAlgebraic R (r • a)
Full source 
protected lemma smul (r : R) : IsAlgebraic R (r • a) :=
  have ⟨_, hp, eval0⟩ := ha
  ⟨_, scaleRoots_ne_zero hp r, Algebra.smul_def r a ▸ scaleRoots_aeval_eq_zero eval0⟩
Scalar multiple of an algebraic element is algebraic
Informal description
Let $R$ be a commutative ring and $A$ an $R$-algebra. For any element $a \in A$ that is algebraic over $R$ and any scalar $r \in R$, the scalar multiple $r \cdot a$ is also algebraic over $R$.
IsAlgebraic.nsmul theorem
(n : ℕ) : IsAlgebraic R (n • a)
Full source 
protected lemma nsmul (n : ℕ) : IsAlgebraic R (n • a) :=
  Nat.cast_smul_eq_nsmul R n a ▸ ha.smul _
Natural Multiple of Algebraic Element is Algebraic
Informal description
For any natural number $n$ and any element $a$ in an $R$-algebra $A$ that is algebraic over $R$, the $n$-th multiple $n \cdot a$ is also algebraic over $R$.
IsAlgebraic.zsmul theorem
(n : ℤ) : IsAlgebraic R (n • a)
Full source 
protected lemma zsmul (n : ℤ) : IsAlgebraic R (n • a) :=
  Int.cast_smul_eq_zsmul R n a ▸ ha.smul _
Integer Multiple of Algebraic Element is Algebraic
Informal description
For any integer $n$ and any element $a$ in an $R$-algebra $A$ that is algebraic over $R$, the integer multiple $n \cdot a$ is also algebraic over $R$.
IsAlgebraic.mul theorem
: IsAlgebraic R (a * b)
Full source 
protected lemma mul : IsAlgebraic R (a * b) := by
  have ⟨ra, a0, int_a⟩ := ha.exists_integral_multiple
  have ⟨rb, b0, int_b⟩ := hb.exists_integral_multiple
  refine IsAlgebraic.iff_exists_smul_integral.mpr ⟨_, mul_ne_zero a0 b0, ?_⟩
  simp_rw [Algebra.smul_def, map_mul, mul_mul_mul_comm, ← Algebra.smul_def]
  exact int_a.mul int_b
Algebraic Elements are Closed under Multiplication
Informal description
Let $R$ be a commutative ring and $A$ an $R$-algebra. For any elements $a, b \in A$ that are algebraic over $R$, their product $a \cdot b$ is also algebraic over $R$.
IsAlgebraic.add theorem
: IsAlgebraic R (a + b)
Full source 
protected lemma add : IsAlgebraic R (a + b) := by
  have ⟨ra, a0, int_a⟩ := ha.exists_integral_multiple
  have ⟨rb, b0, int_b⟩ := hb.exists_integral_multiple
  refine IsAlgebraic.iff_exists_smul_integral.mpr ⟨_, mul_ne_zero b0 a0, ?_⟩
  rw [smul_add, mul_smul, mul_comm, mul_smul]
  exact (int_a.smul _).add (int_b.smul _)
Sum of Algebraic Elements is Algebraic
Informal description
Let $R$ be a commutative ring and $A$ an $R$-algebra. For any elements $a, b \in A$ that are algebraic over $R$, their sum $a + b$ is also algebraic over $R$.
IsAlgebraic.sub theorem
: IsAlgebraic R (a - b)
Full source 
protected lemma sub : IsAlgebraic R (a - b) :=
  sub_eq_add_neg a b ▸ ha.add hb.neg
Difference of Algebraic Elements is Algebraic
Informal description
Let $R$ be a commutative ring and $A$ an $R$-algebra. For any elements $a, b \in A$ that are algebraic over $R$, their difference $a - b$ is also algebraic over $R$.
IsAlgebraic.pow theorem
(n : ℕ) : IsAlgebraic R (a ^ n)
Full source 
protected lemma pow (n : ℕ) : IsAlgebraic R (a ^ n) :=
  have := ha.nontrivial
  n.rec (pow_zero a ▸ isAlgebraic_one) fun _ h ↦ pow_succ a _ ▸ h.mul ha
Powers of algebraic elements are algebraic
Informal description
Let $R$ be a commutative ring and $A$ an $R$-algebra. For any element $a \in A$ that is algebraic over $R$ and any natural number $n$, the power $a^n$ is also algebraic over $R$.
Algebra.IsAlgebraic.trans theorem
[Algebra.IsAlgebraic R S] [alg : Algebra.IsAlgebraic S A] : Algebra.IsAlgebraic R A
Full source 
/-- Transitivity of algebraicity for algebras over domains. -/
@[stacks 09GJ] theorem IsAlgebraic.trans [Algebra.IsAlgebraic R S] [alg : Algebra.IsAlgebraic S A] :
    Algebra.IsAlgebraic R A :=
  ⟨fun _ ↦ (alg.1 _).restrictScalars _⟩
Transitivity of Algebraicity for Algebras over Commutative Rings
Informal description
Let $R$ be a commutative ring, $S$ an $R$-algebra that is algebraic over $R$, and $A$ an $S$-algebra that is algebraic over $S$. Then $A$ is algebraic over $R$.
Algebra.IsIntegral.trans_isAlgebraic theorem
[Algebra.IsIntegral R S] [alg : Algebra.IsAlgebraic S A] : Algebra.IsAlgebraic R A
Full source 
theorem IsIntegral.trans_isAlgebraic [Algebra.IsIntegral R S] [alg : Algebra.IsAlgebraic S A] :
    Algebra.IsAlgebraic R A :=
  ⟨fun _ ↦ (alg.1 _).restrictScalars_of_isIntegral _⟩
Transitivity of Algebraicity under Integral Base Change
Informal description
Let $R$ be a commutative ring, $S$ an $R$-algebra that is integral over $R$, and $A$ an $S$-algebra that is algebraic over $S$. Then $A$ is algebraic over $R$.
Algebra.IsAlgebraic.trans_isIntegral theorem
[Algebra.IsAlgebraic R S] [int : Algebra.IsIntegral S A] : Algebra.IsAlgebraic R A
Full source 
theorem IsAlgebraic.trans_isIntegral [Algebra.IsAlgebraic R S] [int : Algebra.IsIntegral S A] :
    Algebra.IsAlgebraic R A :=
  ⟨fun _ ↦ (int.1 _).trans_isAlgebraic _⟩
Transitivity of Algebraicity under Integral Extension of Algebraic Algebras
Informal description
Let $R$ be a commutative ring, $S$ an $R$-algebra that is algebraic over $R$, and $A$ an $S$-algebra that is integral over $S$. Then $A$ is algebraic over $R$.
Algebra.IsIntegral.isAlgebraic_iff theorem
[Algebra.IsIntegral R S] [FaithfulSMul R S] {a : A} : IsAlgebraic R a ↔ IsAlgebraic S a
Full source 
protected theorem IsIntegral.isAlgebraic_iff [Algebra.IsIntegral R S] [FaithfulSMul R S]
    {a : A} : IsAlgebraicIsAlgebraic R a ↔ IsAlgebraic S a :=
  ⟨.extendScalars (FaithfulSMul.algebraMap_injective ..), .restrictScalars_of_isIntegral _⟩
Equivalence of algebraicity over base ring and integral extension
Informal description
Let $R$ be a commutative ring and $S$ an $R$-algebra that is integral over $R$, with a faithful scalar multiplication action of $R$ on $S$. For any element $a$ in an $S$-algebra $A$, the following are equivalent: 1. $a$ is algebraic over $R$ 2. $a$ is algebraic over $S$
Algebra.IsIntegral.isAlgebraic_iff_top theorem
[Algebra.IsIntegral R S] [FaithfulSMul R S] : Algebra.IsAlgebraic R A ↔ Algebra.IsAlgebraic S A
Full source 
theorem IsIntegral.isAlgebraic_iff_top [Algebra.IsIntegral R S]
    [FaithfulSMul R S] : Algebra.IsAlgebraicAlgebra.IsAlgebraic R A ↔ Algebra.IsAlgebraic S A := by
  simp_rw [Algebra.isAlgebraic_def, Algebra.IsIntegral.isAlgebraic_iff R S]
Equivalence of algebraicity over base ring and integral extension for entire algebra
Informal description
Let $R$ be a commutative ring and $S$ an $R$-algebra that is integral over $R$, with a faithful scalar multiplication action of $R$ on $S$. Then, an $S$-algebra $A$ is algebraic over $R$ if and only if it is algebraic over $S$.
Algebra.IsAlgebraic.isAlgebraic_iff theorem
[Algebra.IsAlgebraic R S] [FaithfulSMul R S] {a : A} : IsAlgebraic R a ↔ IsAlgebraic S a
Full source 
protected theorem IsAlgebraic.isAlgebraic_iff [Algebra.IsAlgebraic R S] [FaithfulSMul R S]
    {a : A} : IsAlgebraicIsAlgebraic R a ↔ IsAlgebraic S a :=
  ⟨.extendScalars (FaithfulSMul.algebraMap_injective ..), .restrictScalars _⟩
Equivalence of algebraicity over base ring and algebraic extension for elements
Informal description
Let $R$ be a commutative ring and $S$ an $R$-algebra that is algebraic over $R$, with a faithful scalar multiplication action of $R$ on $S$. For any element $a$ in an $S$-algebra $A$, the following are equivalent: 1. $a$ is algebraic over $R$. 2. $a$ is algebraic over $S$.
Algebra.IsAlgebraic.isAlgebraic_iff_top theorem
[Algebra.IsAlgebraic R S] [FaithfulSMul R S] : Algebra.IsAlgebraic R A ↔ Algebra.IsAlgebraic S A
Full source 
theorem IsAlgebraic.isAlgebraic_iff_top [Algebra.IsAlgebraic R S]
    [FaithfulSMul R S] : Algebra.IsAlgebraicAlgebra.IsAlgebraic R A ↔ Algebra.IsAlgebraic S A := by
  simp_rw [Algebra.isAlgebraic_def, Algebra.IsAlgebraic.isAlgebraic_iff R S]
Equivalence of Algebraicity in Tower of Algebras
Informal description
Let $R$ be a commutative ring and $S$ an $R$-algebra that is algebraic over $R$, with a faithful scalar multiplication action of $R$ on $S$. Then, an $S$-algebra $A$ is algebraic over $R$ if and only if it is algebraic over $S$.
Algebra.IsAlgebraic.isAlgebraic_iff_bot theorem
[Algebra.IsAlgebraic S A] [FaithfulSMul S A] : Algebra.IsAlgebraic R S ↔ Algebra.IsAlgebraic R A
Full source 
theorem IsAlgebraic.isAlgebraic_iff_bot [Algebra.IsAlgebraic S A] [FaithfulSMul S A] :
    Algebra.IsAlgebraicAlgebra.IsAlgebraic R S ↔ Algebra.IsAlgebraic R A :=
  ⟨fun _ ↦ .trans R S A, fun _ ↦ .tower_bot_of_injective (FaithfulSMul.algebraMap_injective S A)⟩
Equivalence of Algebraicity in Base and Extension with Faithful Action
Informal description
Let $R$ be a commutative ring, $S$ an $R$-algebra, and $A$ an $S$-algebra. Suppose that $A$ is algebraic over $S$ and the scalar multiplication action of $S$ on $A$ is faithful. Then $S$ is algebraic over $R$ if and only if $A$ is algebraic over $R$.
Subalgebra.algebraicClosure definition
[IsDomain R] : Subalgebra R S
Full source 
/-- If `R` is a domain and `S` is an arbitrary `R`-algebra, then the elements of `S`
that are algebraic over `R` form a subalgebra. -/
def Subalgebra.algebraicClosure [IsDomain R] : Subalgebra R S where
  carrier := {s | _root_.IsAlgebraic R s}
  mul_mem' ha hb := ha.mul hb
  add_mem' ha hb := ha.add hb
  algebraMap_mem' := isAlgebraic_algebraMap
Algebraic closure subalgebra over a domain
Informal description
Given a domain \( R \) and an \( R \)-algebra \( S \), the subalgebra \( \text{algebraicClosure} R S \) consists of all elements of \( S \) that are algebraic over \( R \). Specifically, it is the subalgebra whose underlying set is \( \{ s \in S \mid \text{IsAlgebraic} R s \} \), where \( \text{IsAlgebraic} R s \) means there exists a nonzero polynomial \( p \in R[X] \) such that \( p(s) = 0 \). The subalgebra is closed under addition, multiplication, and contains the image of the algebra map from \( R \) to \( S \).
Subalgebra.mem_algebraicClosure theorem
[IsDomain R] {x : S} : x ∈ algebraicClosure R S ↔ IsAlgebraic R x
Full source 
theorem Subalgebra.mem_algebraicClosure [IsDomain R] {x : S} :
    x ∈ algebraicClosure R Sx ∈ algebraicClosure R S ↔ IsAlgebraic R x := Iff.rfl
Characterization of Elements in Algebraic Closure Subalgebra
Informal description
Let $R$ be a domain and $S$ an $R$-algebra. An element $x \in S$ belongs to the algebraic closure subalgebra of $S$ over $R$ if and only if $x$ is algebraic over $R$, meaning there exists a nonzero polynomial $p \in R[X]$ such that $p(x) = 0$.
integralClosure_le_algebraicClosure theorem
[IsDomain R] : integralClosure R S ≤ Subalgebra.algebraicClosure R S
Full source 
theorem integralClosure_le_algebraicClosure [IsDomain R] :
    integralClosure R S ≤ Subalgebra.algebraicClosure R S :=
  fun _ ↦ IsIntegral.isAlgebraic
Integral closure is contained in algebraic closure for domains
Informal description
Let $R$ be a domain and $S$ an $R$-algebra. The integral closure of $R$ in $S$ is contained in the subalgebra of $S$ consisting of all elements algebraic over $R$, i.e., $\text{integralClosure}(R, S) \subseteq \text{algebraicClosure}(R, S)$.
Subalgebra.algebraicClosure_eq_integralClosure theorem
{K} [Field K] [Algebra K S] : algebraicClosure K S = integralClosure K S
Full source 
theorem Subalgebra.algebraicClosure_eq_integralClosure {K} [Field K] [Algebra K S] :
    algebraicClosure K S = integralClosure K S :=
  SetLike.ext fun _ ↦ isAlgebraic_iff_isIntegral
Algebraic Closure Subalgebra Equals Integral Closure over a Field
Informal description
Let $K$ be a field and $S$ a $K$-algebra. The subalgebra of $S$ consisting of all elements algebraic over $K$ is equal to the integral closure of $K$ in $S$. In other words, for any $x \in S$, $x$ is algebraic over $K$ if and only if $x$ is integral over $K$.
instIsAlgebraicSubtypeMemSubalgebraAlgebraicClosure instance
[IsDomain R] : Algebra.IsAlgebraic R (Subalgebra.algebraicClosure R S)
Full source 
instance [IsDomain R] : Algebra.IsAlgebraic R (Subalgebra.algebraicClosure R S) :=
  (Subalgebra.isAlgebraic_iff _).mp fun _ ↦ id
Algebraic Closure Subalgebra is Algebraic
Informal description
For any domain $R$ and $R$-algebra $S$, the subalgebra consisting of all algebraic elements over $R$ is itself algebraic over $R$.
Algebra.isAlgebraic_adjoin_iff theorem
[IsDomain R] {s : Set S} : (adjoin R s).IsAlgebraic ↔ ∀ x ∈ s, IsAlgebraic R x
Full source 
theorem Algebra.isAlgebraic_adjoin_iff [IsDomain R] {s : Set S} :
    (adjoin R s).IsAlgebraic ↔ ∀ x ∈ s, IsAlgebraic R x :=
  Algebra.adjoin_le_iff (S := Subalgebra.algebraicClosure R S)
Algebraic Adjoin Subalgebra Characterization
Informal description
Let $R$ be a domain and $S$ an $R$-algebra. For any subset $s \subseteq S$, the subalgebra $R[s]$ generated by $s$ is algebraic over $R$ if and only if every element $x \in s$ is algebraic over $R$.
Algebra.isAlgebraic_adjoin_of_nonempty theorem
[NoZeroDivisors R] {s : Set S} (hs : s.Nonempty) : (adjoin R s).IsAlgebraic ↔ ∀ x ∈ s, IsAlgebraic R x
Full source 
theorem Algebra.isAlgebraic_adjoin_of_nonempty [NoZeroDivisors R] {s : Set S} (hs : s.Nonempty) :
    (adjoin R s).IsAlgebraic ↔ ∀ x ∈ s, IsAlgebraic R x :=
  ⟨fun h x hx ↦ h _ (subset_adjoin hx), fun h ↦
    have ⟨x, hx⟩ := hs
    have := (isDomain_iff_noZeroDivisors_and_nontrivial _).mpr ⟨‹_›, (h x hx).nontrivial⟩
    isAlgebraic_adjoin_iff.mpr h⟩
Algebraic Adjoin Subalgebra Characterization for Nonempty Sets over Domains
Informal description
Let $R$ be a ring with no zero divisors, and let $S$ be an $R$-algebra. For any nonempty subset $s \subseteq S$, the subalgebra $R[s]$ generated by $s$ is algebraic over $R$ if and only if every element $x \in s$ is algebraic over $R$.
Algebra.isAlgebraic_adjoin_singleton_iff theorem
[NoZeroDivisors R] {s : S} : (adjoin R { s }).IsAlgebraic ↔ IsAlgebraic R s
Full source 
/-- In an algebra generated by a single algebraic element over a domain `R`, every element is
algebraic. This may fail when `R` is not a domain: see https://mathoverflow.net/a/132192/ for
an example. -/
theorem Algebra.isAlgebraic_adjoin_singleton_iff [NoZeroDivisors R] {s : S} :
    (adjoin R {s}).IsAlgebraic ↔ IsAlgebraic R s :=
  (isAlgebraic_adjoin_of_nonempty <| Set.singleton_nonempty s).trans forall_eq
Algebraicity of singly generated subalgebra over a domain
Informal description
Let $R$ be a ring with no zero divisors and $S$ an $R$-algebra. For any element $s \in S$, the subalgebra $R[s]$ generated by $\{s\}$ is algebraic over $R$ if and only if $s$ is algebraic over $R$.
IsAlgebraic.of_mul theorem
[NoZeroDivisors R] {y z : S} (hy : y ∈ nonZeroDivisors S) (alg_y : IsAlgebraic R y) (alg_yz : IsAlgebraic R (y * z)) : IsAlgebraic R z
Full source 
theorem IsAlgebraic.of_mul [NoZeroDivisors R] {y z : S} (hy : y ∈ nonZeroDivisors S)
    (alg_y : IsAlgebraic R y) (alg_yz : IsAlgebraic R (y * z)) : IsAlgebraic R z := by
  have ⟨t, ht, r, hr, eq⟩ := alg_y.exists_nonzero_eq_adjoin_mul hy
  have := alg_yz.mul (Algebra.isAlgebraic_adjoin_singleton_iff.mpr alg_y _ ht)
  rw [mul_right_comm, eq, ← Algebra.smul_def] at this
  exact this.of_smul (mem_nonZeroDivisors_of_ne_zero hr)
Algebraicity of quotient under multiplication by algebraic non-zero divisor
Informal description
Let $R$ be a ring with no zero divisors and $S$ an $R$-algebra. For any elements $y, z \in S$ such that $y$ is a non-zero divisor in $S$, if both $y$ and $y \cdot z$ are algebraic over $R$, then $z$ is also algebraic over $R$.
IsAlgebraic.adjoin_of_forall_isAlgebraic theorem
[NoZeroDivisors S] {s t : Set S} (alg : ∀ x ∈ s \ t, IsAlgebraic (adjoin R t) x) {a : A} (ha : IsAlgebraic (adjoin R s) a) : IsAlgebraic (adjoin R t) a
Full source 
theorem IsAlgebraic.adjoin_of_forall_isAlgebraic [NoZeroDivisors S] {s t : Set S}
    (alg : ∀ x ∈ s \ t, IsAlgebraic (adjoin R t) x) {a : A}
    (ha : IsAlgebraic (adjoin R s) a) : IsAlgebraic (adjoin R t) a := by
  set Rs := adjoin R s
  set Rt := adjoin R t
  let Rts := adjoin Rt s
  let _ : Algebra Rs Rts := (Subalgebra.inclusion
    (T := Rts.restrictScalars R) <| adjoin_le <| by apply subset_adjoin).toAlgebra
  have : IsScalarTower Rs Rts A := .of_algebraMap_eq fun ⟨a, _⟩ ↦ rfl
  have : Algebra.IsAlgebraic Rt Rts := by
    have := ha.nontrivial
    have := Subtype.val_injective (p := (· ∈ Rs)).nontrivial
    have := (isDomain_iff_noZeroDivisors_and_nontrivial Rt).mpr ⟨inferInstance, inferInstance⟩
    rw [← Subalgebra.isAlgebraic_iff, isAlgebraic_adjoin_iff]
    intro x hs
    by_cases ht : x ∈ t
    · exact isAlgebraic_algebraMap (⟨x, subset_adjoin ht⟩ : Rt)
    exact alg _ ⟨hs, ht⟩
  have : IsAlgebraic Rts a := ha.extendScalars (by apply Subalgebra.inclusion_injective)
  exact this.restrictScalars Rt
Algebraicity under Adjoin Extension for Algebraic Elements
Informal description
Let $R$ be a ring and $S$ an $R$-algebra with no zero divisors. Given subsets $s, t \subseteq S$, suppose that for every element $x \in s \setminus t$, $x$ is algebraic over the subalgebra $R[t]$. Then for any element $a$ in an $S$-algebra $A$ that is algebraic over the subalgebra $R[s]$, it follows that $a$ is also algebraic over the subalgebra $R[t]$.
Transcendental.extendScalars_of_isIntegral theorem
[Algebra.IsIntegral R S] : Transcendental S a
Full source 
lemma extendScalars_of_isIntegral [Algebra.IsIntegral R S] :
    Transcendental S a := by
  contrapose ha
  rw [Transcendental, not_not] at ha ⊢
  exact ha.restrictScalars_of_isIntegral _
Transcendence is preserved under extension to integral algebras
Informal description
Let $R$ be a commutative ring and $S$ an $R$-algebra that is integral over $R$. If an element $a$ of an $S$-algebra $A$ is transcendental over $R$, then $a$ remains transcendental over $S$.
Transcendental.extendScalars theorem
[Algebra.IsAlgebraic R S] : Transcendental S a
Full source 
lemma extendScalars [Algebra.IsAlgebraic R S] : Transcendental S a := by
  contrapose ha
  rw [Transcendental, not_not] at ha ⊢
  exact ha.restrictScalars _
Transcendence is preserved under extension to algebraic algebras
Informal description
Let $R$ be a commutative ring and $S$ an $R$-algebra that is algebraic over $R$. If an element $a$ of an $S$-algebra $A$ is transcendental over $R$, then $a$ remains transcendental over $S$.
Transcendental.integralClosure theorem
: Transcendental (integralClosure R S) a
Full source 
protected lemma integralClosure : Transcendental (integralClosure R S) a :=
  ha.extendScalars_of_isIntegral _
Transcendence over Integral Closure Equals Transcendence over Base Ring
Informal description
An element $a$ of an $R$-algebra $A$ is transcendental over the integral closure of $R$ in $S$ if and only if it is transcendental over $R$.
Transcendental.subalgebraAlgebraicClosure theorem
[IsDomain R] : Transcendental (Subalgebra.algebraicClosure R S) a
Full source 
lemma subalgebraAlgebraicClosure [IsDomain R] :
    Transcendental (Subalgebra.algebraicClosure R S) a := ha.extendScalars _
Transcendence over Algebraic Closure Subalgebra Equals Transcendence over Base Ring
Informal description
Let $R$ be a domain and $S$ an $R$-algebra. If an element $a$ of an $S$-algebra $A$ is transcendental over $R$, then $a$ remains transcendental over the subalgebra of $S$ consisting of all algebraic elements over $R$.
Algebra.IsIntegral.transcendental_iff theorem
[Algebra.IsIntegral R S] : Transcendental R a ↔ Transcendental S a
Full source 
protected theorem IsIntegral.transcendental_iff [Algebra.IsIntegral R S] :
    TranscendentalTranscendental R a ↔ Transcendental S a :=
  ⟨(·.extendScalars_of_isIntegral _), (·.restrictScalars (FaithfulSMul.algebraMap_injective R S))⟩
Transcendence Equivalence under Integral Extension: $R$ vs $S$
Informal description
Let $R$ be a ring and $S$ an $R$-algebra that is integral over $R$. For any element $a$ in an $S$-algebra $A$, $a$ is transcendental over $R$ if and only if $a$ is transcendental over $S$.
Algebra.IsAlgebraic.transcendental_iff theorem
[Algebra.IsAlgebraic R S] : Transcendental R a ↔ Transcendental S a
Full source 
protected theorem IsAlgebraic.transcendental_iff [Algebra.IsAlgebraic R S] :
    TranscendentalTranscendental R a ↔ Transcendental S a :=
  ⟨(·.extendScalars _), (·.restrictScalars (FaithfulSMul.algebraMap_injective R S))⟩
Transcendence Equivalence under Algebraic Extension: $R$ vs $S$
Informal description
Let $R$ be a commutative ring and $S$ an $R$-algebra that is algebraic over $R$. For any element $a$ in an $S$-algebra $A$, $a$ is transcendental over $R$ if and only if $a$ is transcendental over $S$.