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. The main result in this file proves transitivity of algebraicity: a tower of algebraic field extensions is algebraic.
theorem
is_transcendental_of_subsingleton
(R : Type u)
{A : Type v}
[CommRing R]
[Ring A]
[Algebra R A]
[Subsingleton R]
(x : A)
:
Transcendental R x
theorem
IsAlgebraic.nontrivial
{R : Type u}
{A : Type v}
[CommRing R]
[Ring A]
[Algebra R A]
{a : A}
(h : IsAlgebraic R a)
:
theorem
Algebra.IsAlgebraic.nontrivial
(R : Type u)
(A : Type v)
[CommRing R]
[Ring A]
[Algebra R A]
[alg : Algebra.IsAlgebraic R A]
:
@[instance 100]
instance
Algebra.transcendental_of_subsingleton
(R : Type u)
(A : Type v)
[CommRing R]
[Ring A]
[Algebra R A]
[Subsingleton R]
:
theorem
IsAlgebraic.of_aeval
{R : Type u}
{A : Type v}
[CommRing R]
[Ring A]
[Algebra R A]
{r : A}
(f : Polynomial R)
(hf : f.natDegree ≠ 0)
(hf' : f.leadingCoeff ∈ nonZeroDivisors R)
(H : IsAlgebraic R ((Polynomial.aeval r) f))
:
IsAlgebraic R r
theorem
Transcendental.aeval
{R : Type u}
{A : Type v}
[CommRing R]
[Ring A]
[Algebra R A]
{r : A}
(H : Transcendental R r)
(f : Polynomial R)
(hf : f.natDegree ≠ 0)
(hf' : f.leadingCoeff ∈ nonZeroDivisors R)
:
Transcendental R ((Polynomial.aeval r) f)
theorem
Transcendental.aeval_of_transcendental
{R : Type u}
{A : Type v}
[CommRing R]
[Ring A]
[Algebra R A]
{r : A}
(H : Transcendental R r)
{f : Polynomial R}
(hf : Transcendental R f)
:
Transcendental R ((Polynomial.aeval r) f)
If r : A and f : R[X] are transcendental over R, then Polynomial.aeval r f is also
transcendental over R. For the converse, see Transcendental.of_aeval and
transcendental_aeval_iff.
theorem
Transcendental.of_aeval
{R : Type u}
{A : Type v}
[CommRing R]
[Ring A]
[Algebra R A]
{r : A}
{f : Polynomial R}
(H : Transcendental R ((Polynomial.aeval r) f))
:
Transcendental R f
If Polynomial.aeval r f is transcendental over R, then f : R[X] is also
transcendental over R. In fact, the r is also transcendental over R provided that R
is a field (see transcendental_aeval_iff).
theorem
IsAlgebraic.of_aeval_of_transcendental
{R : Type u}
{A : Type v}
[CommRing R]
[Ring A]
[Algebra R A]
{r : A}
{f : Polynomial R}
(H : IsAlgebraic R ((Polynomial.aeval r) f))
(hf : Transcendental R f)
:
IsAlgebraic R r
theorem
Polynomial.transcendental
{R : Type u}
[CommRing R]
(f : Polynomial R)
(hf : f.natDegree ≠ 0)
(hf' : f.leadingCoeff ∈ nonZeroDivisors R)
:
Transcendental R f
theorem
transcendental_iff_injective
{R : Type u}
{A : Type v}
[CommRing R]
[Ring A]
[Algebra R A]
{x : A}
:
An element x is transcendental over R if and only if the map Polynomial.aeval x
is injective. This is similar to algebraicIndependent_iff_injective_aeval.
theorem
transcendental_iff_ker_eq_bot
{R : Type u}
{A : Type v}
[CommRing R]
[Ring A]
[Algebra R A]
{x : A}
:
An element x is transcendental over R if and only if the kernel of the ring homomorphism
Polynomial.aeval x is the zero ideal. This is similar to algebraicIndependent_iff_ker_eq_bot.
theorem
Algebra.isAlgebraic_of_not_injective
{R : Type u}
{A : Type v}
[CommRing R]
[Ring A]
[Algebra R A]
(h : ¬Function.Injective ⇑(algebraMap R A))
:
theorem
Algebra.injective_of_transcendental
{R : Type u}
{A : Type v}
[CommRing R]
[Ring A]
[Algebra R A]
[h : Algebra.Transcendental R A]
:
Function.Injective ⇑(algebraMap R A)
theorem
isAlgebraic_zero
{R : Type u}
{A : Type v}
[CommRing R]
[Ring A]
[Algebra R A]
[Nontrivial R]
:
IsAlgebraic R 0
theorem
isAlgebraic_algebraMap
{R : Type u}
{A : Type v}
[CommRing R]
[Ring A]
[Algebra R A]
[Nontrivial R]
(x : R)
:
IsAlgebraic R ((algebraMap R A) x)
An element of R is algebraic, when viewed as an element of the R-algebra A.
theorem
isAlgebraic_one
{R : Type u}
{A : Type v}
[CommRing R]
[Ring A]
[Algebra R A]
[Nontrivial R]
:
IsAlgebraic R 1
theorem
isAlgebraic_nat
{R : Type u}
{A : Type v}
[CommRing R]
[Ring A]
[Algebra R A]
[Nontrivial R]
(n : ℕ)
:
IsAlgebraic R ↑n
theorem
isAlgebraic_int
{R : Type u}
{A : Type v}
[CommRing R]
[Ring A]
[Algebra R A]
[Nontrivial R]
(n : ℤ)
:
IsAlgebraic R ↑n
theorem
isAlgebraic_rat
(R : Type u)
{A : Type v}
[DivisionRing A]
[Field R]
[Algebra R A]
(n : ℚ)
:
IsAlgebraic R ↑n
theorem
isAlgebraic_of_mem_rootSet
{R : Type u}
{A : Type v}
[CommRing R]
[Field A]
[Algebra R A]
{p : Polynomial R}
{x : A}
(hx : x ∈ p.rootSet A)
:
IsAlgebraic R x
theorem
IsLocalization.isAlgebraic
{R : Type u}
(S : Type u_1)
[CommRing R]
[CommRing S]
[Algebra R S]
[Nontrivial R]
(M : Submonoid R)
[IsLocalization M S]
:
theorem
IsAlgebraic.algebraMap
{R : Type u}
{S : Type u_1}
{A : Type v}
[CommRing R]
[CommRing S]
[Ring A]
[Algebra R A]
[Algebra R S]
[Algebra S A]
[IsScalarTower R S A]
{a : S}
:
IsAlgebraic R a → IsAlgebraic R ((algebraMap S A) a)
theorem
IsAlgebraic.algHom
{R : Type u}
{A : Type v}
[CommRing R]
[Ring A]
[Algebra R A]
{B : Type u_2}
[Ring B]
[Algebra R B]
(f : A →ₐ[R] B)
{a : A}
(h : IsAlgebraic R a)
:
IsAlgebraic R (f a)
This is slightly more general than IsAlgebraic.algebraMap in that it
allows noncommutative intermediate rings A.
theorem
IsAlgebraic.ringHom_of_comp_eq
{R : Type u}
{S : Type u_1}
{A : Type v}
[CommRing R]
[CommRing S]
[Ring A]
[Algebra R A]
{B : Type u_2}
[Ring B]
[Algebra S B]
{FRS : Type u_3}
{FAB : Type u_4}
[FunLike FRS R S]
[RingHomClass FRS R S]
[FunLike FAB A B]
[RingHomClass FAB A B]
(f : FRS)
(g : FAB)
{a : A}
(halg : IsAlgebraic R a)
(hf : Function.Injective ⇑f)
(h : (algebraMap S B).comp ↑f = (↑g).comp (algebraMap R A))
:
IsAlgebraic S (g a)
theorem
Transcendental.of_ringHom_of_comp_eq
{R : Type u}
{S : Type u_1}
{A : Type v}
[CommRing R]
[CommRing S]
[Ring A]
[Algebra R A]
{B : Type u_2}
[Ring B]
[Algebra S B]
{FRS : Type u_3}
{FAB : Type u_4}
[FunLike FRS R S]
[RingHomClass FRS R S]
[FunLike FAB A B]
[RingHomClass FAB A B]
(f : FRS)
(g : FAB)
{a : A}
(H : Transcendental S (g a))
(hf : Function.Injective ⇑f)
(h : (algebraMap S B).comp ↑f = (↑g).comp (algebraMap R A))
:
Transcendental R a
theorem
Algebra.IsAlgebraic.ringHom_of_comp_eq
{R : Type u}
{S : Type u_1}
{A : Type v}
[CommRing R]
[CommRing S]
[Ring A]
[Algebra R A]
{B : Type u_2}
[Ring B]
[Algebra S B]
{FRS : Type u_3}
{FAB : Type u_4}
[FunLike FRS R S]
[RingHomClass FRS R S]
[FunLike FAB A B]
[RingHomClass FAB A B]
(f : FRS)
(g : FAB)
[Algebra.IsAlgebraic R A]
(hf : Function.Injective ⇑f)
(hg : Function.Surjective ⇑g)
(h : (algebraMap S B).comp ↑f = (↑g).comp (algebraMap R A))
:
theorem
Algebra.Transcendental.of_ringHom_of_comp_eq
{R : Type u}
{S : Type u_1}
{A : Type v}
[CommRing R]
[CommRing S]
[Ring A]
[Algebra R A]
{B : Type u_2}
[Ring B]
[Algebra S B]
{FRS : Type u_3}
{FAB : Type u_4}
[FunLike FRS R S]
[RingHomClass FRS R S]
[FunLike FAB A B]
[RingHomClass FAB A B]
(f : FRS)
(g : FAB)
[H : Algebra.Transcendental S B]
(hf : Function.Injective ⇑f)
(hg : Function.Surjective ⇑g)
(h : (algebraMap S B).comp ↑f = (↑g).comp (algebraMap R A))
:
theorem
IsAlgebraic.of_ringHom_of_comp_eq
{R : Type u}
{S : Type u_1}
{A : Type v}
[CommRing R]
[CommRing S]
[Ring A]
[Algebra R A]
{B : Type u_2}
[Ring B]
[Algebra S B]
{FRS : Type u_3}
{FAB : Type u_4}
[FunLike FRS R S]
[RingHomClass FRS R S]
[FunLike FAB A B]
[RingHomClass FAB A B]
(f : FRS)
(g : FAB)
{a : A}
(halg : IsAlgebraic S (g a))
(hf : Function.Surjective ⇑f)
(hg : Function.Injective ⇑g)
(h : (algebraMap S B).comp ↑f = (↑g).comp (algebraMap R A))
:
IsAlgebraic R a
theorem
Transcendental.ringHom_of_comp_eq
{R : Type u}
{S : Type u_1}
{A : Type v}
[CommRing R]
[CommRing S]
[Ring A]
[Algebra R A]
{B : Type u_2}
[Ring B]
[Algebra S B]
{FRS : Type u_3}
{FAB : Type u_4}
[FunLike FRS R S]
[RingHomClass FRS R S]
[FunLike FAB A B]
[RingHomClass FAB A B]
(f : FRS)
(g : FAB)
{a : A}
(H : Transcendental R a)
(hf : Function.Surjective ⇑f)
(hg : Function.Injective ⇑g)
(h : (algebraMap S B).comp ↑f = (↑g).comp (algebraMap R A))
:
Transcendental S (g a)
theorem
Algebra.IsAlgebraic.of_ringHom_of_comp_eq
{R : Type u}
{S : Type u_1}
{A : Type v}
[CommRing R]
[CommRing S]
[Ring A]
[Algebra R A]
{B : Type u_2}
[Ring B]
[Algebra S B]
{FRS : Type u_3}
{FAB : Type u_4}
[FunLike FRS R S]
[RingHomClass FRS R S]
[FunLike FAB A B]
[RingHomClass FAB A B]
(f : FRS)
(g : FAB)
[Algebra.IsAlgebraic S B]
(hf : Function.Surjective ⇑f)
(hg : Function.Injective ⇑g)
(h : (algebraMap S B).comp ↑f = (↑g).comp (algebraMap R A))
:
theorem
Algebra.Transcendental.ringHom_of_comp_eq
{R : Type u}
{S : Type u_1}
{A : Type v}
[CommRing R]
[CommRing S]
[Ring A]
[Algebra R A]
{B : Type u_2}
[Ring B]
[Algebra S B]
{FRS : Type u_3}
{FAB : Type u_4}
[FunLike FRS R S]
[RingHomClass FRS R S]
[FunLike FAB A B]
[RingHomClass FAB A B]
(f : FRS)
(g : FAB)
[H : Algebra.Transcendental R A]
(hf : Function.Surjective ⇑f)
(hg : Function.Injective ⇑g)
(h : (algebraMap S B).comp ↑f = (↑g).comp (algebraMap R A))
:
theorem
isAlgebraic_ringHom_iff_of_comp_eq
{R : Type u}
{S : Type u_1}
{A : Type v}
[CommRing R]
[CommRing S]
[Ring A]
[Algebra R A]
{B : Type u_2}
[Ring B]
[Algebra S B]
{FRS : Type u_3}
{FAB : Type u_4}
[EquivLike FRS R S]
[RingEquivClass FRS R S]
[FunLike FAB A B]
[RingHomClass FAB A B]
(f : FRS)
(g : FAB)
(hg : Function.Injective ⇑g)
(h : (algebraMap S B).comp ↑f = (↑g).comp (algebraMap R A))
{a : A}
:
theorem
transcendental_ringHom_iff_of_comp_eq
{R : Type u}
{S : Type u_1}
{A : Type v}
[CommRing R]
[CommRing S]
[Ring A]
[Algebra R A]
{B : Type u_2}
[Ring B]
[Algebra S B]
{FRS : Type u_3}
{FAB : Type u_4}
[EquivLike FRS R S]
[RingEquivClass FRS R S]
[FunLike FAB A B]
[RingHomClass FAB A B]
(f : FRS)
(g : FAB)
(hg : Function.Injective ⇑g)
(h : (algebraMap S B).comp ↑f = (↑g).comp (algebraMap R A))
{a : A}
:
theorem
Algebra.isAlgebraic_ringHom_iff_of_comp_eq
{R : Type u}
{S : Type u_1}
{A : Type v}
[CommRing R]
[CommRing S]
[Ring A]
[Algebra R A]
{B : Type u_2}
[Ring B]
[Algebra S B]
{FRS : Type u_3}
{FAB : Type u_4}
[EquivLike FRS R S]
[RingEquivClass FRS R S]
[EquivLike FAB A B]
[RingEquivClass FAB A B]
(f : FRS)
(g : FAB)
(h : (algebraMap S B).comp ↑f = (↑g).comp (algebraMap R A))
:
theorem
Algebra.transcendental_ringHom_iff_of_comp_eq
{R : Type u}
{S : Type u_1}
{A : Type v}
[CommRing R]
[CommRing S]
[Ring A]
[Algebra R A]
{B : Type u_2}
[Ring B]
[Algebra S B]
{FRS : Type u_3}
{FAB : Type u_4}
[EquivLike FRS R S]
[RingEquivClass FRS R S]
[EquivLike FAB A B]
[RingEquivClass FAB A B]
(f : FRS)
(g : FAB)
(h : (algebraMap S B).comp ↑f = (↑g).comp (algebraMap R A))
:
theorem
Algebra.IsAlgebraic.of_injective
{R : Type u}
{A : Type v}
[CommRing R]
[Ring A]
[Algebra R A]
{B : Type u_2}
[Ring B]
[Algebra R B]
(f : A →ₐ[R] B)
(hf : Function.Injective ⇑f)
[Algebra.IsAlgebraic R B]
:
theorem
AlgEquiv.isAlgebraic
{R : Type u}
{A : Type v}
[CommRing R]
[Ring A]
[Algebra R A]
{B : Type u_2}
[Ring B]
[Algebra R B]
(e : A ≃ₐ[R] B)
[Algebra.IsAlgebraic R A]
:
Transfer Algebra.IsAlgebraic across an AlgEquiv.
theorem
isAlgebraic_algebraMap_iff
{R : Type u}
{S : Type u_1}
{A : Type v}
[CommRing R]
[CommRing S]
[Ring A]
[Algebra R A]
[Algebra R S]
[Algebra S A]
[IsScalarTower R S A]
{a : S}
(h : Function.Injective ⇑(algebraMap S A))
:
theorem
transcendental_algebraMap_iff
{R : Type u}
{S : Type u_1}
{A : Type v}
[CommRing R]
[CommRing S]
[Ring A]
[Algebra R A]
[Algebra R S]
[Algebra S A]
[IsScalarTower R S A]
{a : S}
(h : Function.Injective ⇑(algebraMap S A))
:
theorem
Subalgebra.isAlgebraic_iff_isAlgebraic_val
{R : Type u}
{A : Type v}
[CommRing R]
[Ring A]
[Algebra R A]
{S : Subalgebra R A}
{x : ↥S}
:
theorem
Subalgebra.isAlgebraic_of_isAlgebraic_bot
{R : Type u}
{S : Type u_1}
[CommRing R]
[CommRing S]
[Algebra R S]
{x : S}
(halg : IsAlgebraic (↥⊥) x)
:
IsAlgebraic R x
theorem
Subalgebra.isAlgebraic_bot_iff
{R : Type u}
{S : Type u_1}
[CommRing R]
[CommRing S]
[Algebra R S]
(h : Function.Injective ⇑(algebraMap R S))
{x : S}
:
theorem
Subalgebra.algebra_isAlgebraic_of_algebra_isAlgebraic_bot_left
(R : Type u)
(S : Type u_1)
[CommRing R]
[CommRing S]
[Algebra R S]
[Algebra.IsAlgebraic (↥⊥) S]
:
theorem
Subalgebra.algebra_isAlgebraic_bot_left_iff
{R : Type u}
{S : Type u_1}
[CommRing R]
[CommRing S]
[Algebra R S]
(h : Function.Injective ⇑(algebraMap R S))
:
instance
Subalgebra.algebra_isAlgebraic_bot_right
{R : Type u}
{S : Type u_1}
[CommRing R]
[CommRing S]
[Algebra R S]
[Nontrivial R]
:
theorem
IsAlgebraic.of_pow
{R : Type u}
{A : Type v}
[CommRing R]
[Ring A]
[Algebra R A]
{r : A}
{n : ℕ}
(hn : 0 < n)
(ht : IsAlgebraic R (r ^ n))
:
IsAlgebraic R r
theorem
Transcendental.pow
{R : Type u}
{A : Type v}
[CommRing R]
[Ring A]
[Algebra R A]
{r : A}
(ht : Transcendental R r)
{n : ℕ}
(hn : 0 < n)
:
Transcendental R (r ^ n)
theorem
IsAlgebraic.invOf
{R : Type u}
{S : Type u_1}
[CommRing R]
[CommRing S]
[Algebra R S]
{x : S}
[Invertible x]
(h : IsAlgebraic R x)
:
IsAlgebraic R ⅟x
theorem
IsAlgebraic.invOf_iff
{R : Type u}
{S : Type u_1}
[CommRing R]
[CommRing S]
[Algebra R S]
{x : S}
[Invertible x]
:
theorem
IsAlgebraic.inv
{R : Type u}
[CommRing R]
{K : Type u_2}
[Field K]
[Algebra R K]
{x : K}
:
IsAlgebraic R x → IsAlgebraic R x⁻¹
Alias of the reverse direction of IsAlgebraic.inv_iff.
theorem
IsAlgebraic.extendScalars
{R : Type u_3}
{S : Type u_4}
{A : Type u_5}
[CommRing R]
[CommRing S]
[Ring A]
[Algebra R S]
[Algebra S A]
[Algebra R A]
[IsScalarTower R S A]
(hinj : Function.Injective ⇑(algebraMap R S))
{x : A}
(A_alg : IsAlgebraic R x)
:
IsAlgebraic 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.
theorem
IsAlgebraic.tower_top_of_subalgebra_le
{R : Type u_3}
{S : Type u_4}
[CommRing R]
[CommRing S]
[Algebra R S]
{A B : Subalgebra R S}
(hle : A ≤ B)
{x : S}
(h : IsAlgebraic (↥A) x)
:
IsAlgebraic (↥B) x
A special case of IsAlgebraic.extendScalars. This is extracted as a theorem
because in some cases IsAlgebraic.extendScalars will just runs out of memory.
theorem
Transcendental.restrictScalars
{R : Type u_3}
{S : Type u_4}
{A : Type u_5}
[CommRing R]
[CommRing S]
[Ring A]
[Algebra R S]
[Algebra S A]
[Algebra R A]
[IsScalarTower R S A]
(hinj : Function.Injective ⇑(algebraMap R S))
{x : A}
(h : Transcendental S x)
:
Transcendental R x
If x is transcendental over S, then x is transcendental over R when S is an extension
of R, and the map from R to S is injective.
theorem
Transcendental.of_tower_top_of_subalgebra_le
{R : Type u_3}
{S : Type u_4}
[CommRing R]
[CommRing S]
[Algebra R S]
{A B : Subalgebra R S}
(hle : A ≤ B)
{x : S}
(h : Transcendental (↥B) x)
:
Transcendental (↥A) x
A special case of Transcendental.restrictScalars. This is extracted as a theorem
because in some cases Transcendental.restrictScalars will just runs out of memory.
theorem
Algebra.IsAlgebraic.extendScalars
{R : Type u_3}
{S : Type u_4}
{A : Type u_5}
[CommRing R]
[CommRing S]
[Ring A]
[Algebra R S]
[Algebra S A]
[Algebra R A]
[IsScalarTower R S A]
(hinj : Function.Injective ⇑(algebraMap R S))
[Algebra.IsAlgebraic R 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.
theorem
Algebra.IsAlgebraic.tower_bot_of_injective
{R : Type u_3}
{S : Type u_4}
{A : Type u_5}
[CommRing R]
[CommRing S]
[Ring A]
[Algebra R S]
[Algebra S A]
[Algebra R A]
[IsScalarTower R S A]
[Algebra.IsAlgebraic R A]
(hinj : Function.Injective ⇑(algebraMap S A))
:
theorem
IsAlgebraic.tower_top
{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]
{x : A}
(A_alg : IsAlgebraic K x)
:
IsAlgebraic L x
If x is algebraic over K, then x is algebraic over L when L is an extension of K
Stacks Tag 09GF (part one)
theorem
Transcendental.of_tower_top
(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]
{x : A}
(h : Transcendental L x)
:
Transcendental K x
If x is transcendental over L, then x is transcendental over K when
L is an extension of K
theorem
Algebra.IsAlgebraic.tower_top
{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]
[Algebra.IsAlgebraic K A]
:
If A is an algebraic algebra over K, then A is algebraic over L when L is an extension of K
Stacks Tag 09GF (part two)
theorem
Algebra.IsAlgebraic.tower_bot
(K : Type u_6)
(L : Type u_7)
(A : Type u_8)
[CommRing K]
[Field L]
[Ring A]
[Algebra K L]
[Algebra L A]
[Algebra K A]
[IsScalarTower K L A]
[Nontrivial A]
[Algebra.IsAlgebraic K A]
:
theorem
Algebra.IsAlgebraic.algHom_bijective
{K : Type u_1}
{L : Type u_2}
[CommRing K]
[Field L]
[Algebra K L]
[NoZeroSMulDivisors K L]
[Algebra.IsAlgebraic K L]
(f : L →ₐ[K] L)
:
theorem
Algebra.IsAlgebraic.algHom_bijective₂
{K : Type u_1}
{L : Type u_2}
{R : Type u_3}
[CommRing K]
[Field L]
[Algebra K L]
[NoZeroSMulDivisors K L]
[DivisionRing R]
[Algebra K R]
[Algebra.IsAlgebraic K L]
(f : L →ₐ[K] R)
(g : R →ₐ[K] L)
:
theorem
Algebra.IsAlgebraic.bijective_of_isScalarTower
{K : Type u_1}
{L : Type u_2}
{R : Type u_3}
[CommRing K]
[Field L]
[Algebra K L]
[NoZeroSMulDivisors K L]
[Algebra.IsAlgebraic K L]
[DivisionRing R]
[Algebra K R]
[Algebra L R]
[IsScalarTower K L R]
(f : R →ₐ[K] L)
:
theorem
Algebra.IsAlgebraic.bijective_of_isScalarTower'
{K : Type u_1}
{L : Type u_2}
{R : Type u_3}
[CommRing K]
[Field L]
[Algebra K L]
[Field R]
[Algebra K R]
[NoZeroSMulDivisors K R]
[Algebra.IsAlgebraic K R]
[Algebra L R]
[IsScalarTower K L R]
(f : R →ₐ[K] L)
:
noncomputable def
Algebra.IsAlgebraic.algEquivEquivAlgHom
(K : Type u_1)
(L : Type u_2)
[CommRing K]
[Field L]
[Algebra K L]
[NoZeroSMulDivisors K L]
[Algebra.IsAlgebraic K L]
:
Bijection between algebra equivalences and algebra homomorphisms
Equations
- Algebra.IsAlgebraic.algEquivEquivAlgHom K L = { toFun := fun (ϕ : L ≃ₐ[K] L) => ↑ϕ, invFun := fun (ϕ : L →ₐ[K] L) => AlgEquiv.ofBijective ϕ ⋯, left_inv := ⋯, right_inv := ⋯, map_mul' := ⋯ }
Instances For
@[simp]
theorem
Algebra.IsAlgebraic.algEquivEquivAlgHom_apply
(K : Type u_1)
(L : Type u_2)
[CommRing K]
[Field L]
[Algebra K L]
[NoZeroSMulDivisors K L]
[Algebra.IsAlgebraic K L]
(ϕ : L ≃ₐ[K] L)
:
@[simp]
theorem
Algebra.IsAlgebraic.algEquivEquivAlgHom_symm_apply
(K : Type u_1)
(L : Type u_2)
[CommRing K]
[Field L]
[Algebra K L]
[NoZeroSMulDivisors K L]
[Algebra.IsAlgebraic K L]
(ϕ : L →ₐ[K] L)
:
theorem
IsAlgebraic.exists_nonzero_coeff_and_aeval_eq_zero
{R : Type u_1}
{S : Type u_2}
[CommRing R]
[Ring S]
[Algebra R S]
{s : S}
(hRs : IsAlgebraic R s)
(hs : s ∈ nonZeroDivisors S)
:
∃ (q : Polynomial R), q.coeff 0 ≠ 0 ∧ (Polynomial.aeval s) q = 0
theorem
IsAlgebraic.exists_nonzero_eq_adjoin_mul
{R : Type u_1}
{S : Type u_2}
[CommRing R]
[Ring S]
[Algebra R S]
{s : S}
(hRs : IsAlgebraic R s)
(hs : s ∈ nonZeroDivisors S)
:
∃ t ∈ Algebra.adjoin R {s}, ∃ (r : R), r ≠ 0 ∧ s * t = (algebraMap R S) r
theorem
IsAlgebraic.exists_nonzero_dvd
{R : Type u_1}
{S : Type u_2}
[CommRing R]
[Ring S]
[Algebra R S]
{s : S}
(hRs : IsAlgebraic R s)
(hs : s ∈ nonZeroDivisors S)
:
∃ (r : R), r ≠ 0 ∧ s ∣ (algebraMap R S) r
theorem
IsAlgebraic.exists_smul_eq_mul
{R : Type u_1}
{S : Type u_2}
[CommRing R]
[Ring S]
[Algebra R S]
(a : S)
{b : S}
(hRb : IsAlgebraic R b)
(hb : b ∈ nonZeroDivisors S)
:
A fraction (a : S) / (b : S) can be reduced to (c : S) / (d : R),
if b is algebraic over R.
theorem
Algebra.IsAlgebraic.exists_smul_eq_mul
(R : Type u_1)
{S : Type u_2}
[CommRing R]
[Ring S]
[Algebra R S]
[NoZeroDivisors S]
[Algebra.IsAlgebraic R S]
(a : S)
{b : S}
(hb : b ≠ 0)
:
A fraction (a : S) / (b : S) can be reduced to (c : S) / (d : R),
if b is algebraic over R.
theorem
Algebra.IsAlgebraic.injective_tower_top
{R : Type u_1}
(S : Type u_2)
[CommRing R]
{A : Type u_3}
[CommRing S]
[NoZeroDivisors S]
[Algebra R S]
[alg : Algebra.IsAlgebraic R S]
[Ring A]
[Algebra R A]
[Algebra S A]
[IsScalarTower R S A]
(inj : Function.Injective ⇑(algebraMap R A))
:
Function.Injective ⇑(algebraMap S A)
theorem
Algebra.IsAlgebraic.faithfulSMul_tower_top
(R : Type u_1)
(S : Type u_2)
[CommRing R]
(A : Type u_3)
[CommRing S]
[NoZeroDivisors S]
[Algebra R S]
[alg : Algebra.IsAlgebraic R S]
[Ring A]
[Algebra R A]
[Algebra S A]
[IsScalarTower R S A]
[FaithfulSMul R A]
:
FaithfulSMul S A
theorem
inv_eq_of_aeval_divX_ne_zero
{K : Type u_1}
{L : Type u_2}
[Field K]
[Field L]
[Algebra K L]
{x : L}
{p : Polynomial K}
(aeval_ne : (Polynomial.aeval x) p.divX ≠ 0)
:
theorem
inv_eq_of_root_of_coeff_zero_ne_zero
{K : Type u_1}
{L : Type u_2}
[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)
:
theorem
Subalgebra.inv_mem_of_root_of_coeff_zero_ne_zero
{K : Type u_1}
{L : Type u_2}
[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)
:
theorem
Subalgebra.inv_mem_of_algebraic
{K : Type u_1}
{L : Type u_2}
[Field K]
[Field L]
[Algebra K L]
(A : Subalgebra K L)
{x : ↥A}
(hx : IsAlgebraic K ↑x)
:
theorem
Subalgebra.isField_of_algebraic
{K : Type u_1}
{L : Type u_2}
[Field K]
[Field L]
[Algebra K L]
(A : Subalgebra K L)
[Algebra.IsAlgebraic K L]
:
IsField ↥A
In an algebraic extension L/K, an intermediate subalgebra is a field.
theorem
Transcendental.infinite
{R : Type u_1}
{A : Type u_2}
[CommRing R]
[Ring A]
[Algebra R A]
[Nontrivial R]
{x : A}
(hx : Transcendental R x)
:
Infinite A
theorem
Algebra.Transcendental.infinite
(R : Type u_1)
(A : Type u_2)
[CommRing R]
[Ring A]
[Algebra R A]
[Nontrivial R]
[Algebra.Transcendental R A]
:
Infinite A