# 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.

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
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.

source
theorem Algebra.IsAlgebraic.of_isIntegralClosure (R : Type u_1) (B : Type u_2) (C : Type u_3) [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
source
theorem IsAlgebraic.of_finite (R : Type u_3) {A : Type u_4} [CommRing R] [Nontrivial R] [Ring A] [Algebra R A] (e : A) [Module.Finite R A] :
IsAlgebraic R e
source
instance Algebra.IsAlgebraic.of_finite (R : Type u_3) (A : Type u_4) [CommRing R] [Nontrivial R] [Ring A] [Algebra R A] [Module.Finite R A] :
Algebra.IsAlgebraic R A

A field extension is algebraic if it is finite.

source
@[simp]
theorem transcendental_aeval_iff {K : Type u_1} {A : Type u_4} [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

- algEquivEquivAlgHom K L = Algebra.IsAlgebraic.algEquivEquivAlgHom K L

Instances For

source
theorem IsAlgebraic.exists_integral_multiple {R : Type u_1} {A : Type u_3} [CommRing R] [Ring A] [Algebra R A] {z : A} (hz : IsAlgebraic R z) :
∃ (y : R), y ≠ 0 ∧ IsIntegral R (y • z)
source
theorem Algebra.IsAlgebraic.exists_integral_multiples (R : Type u_1) {A : Type u_3} [CommRing R] [Ring A] [Algebra R A] [NoZeroDivisors R] [alg : Algebra.IsAlgebraic R A] (s : Finset A) :
∃ (y : R), y ≠ 0 ∧ ∀ z ∈ s, IsIntegral R (y • z)
source
theorem IsAlgebraic.of_smul_isIntegral {R : Type u_1} {A : Type u_3} [CommRing R] [Ring A] [Algebra R A] {z : A} {y : R} (hy : ¬IsNilpotent y) (h : IsIntegral R (y • z)) :
IsAlgebraic R z
source
theorem IsAlgebraic.of_smul {R : Type u_1} {A : Type u_3} [CommRing R] [Ring A] [Algebra R A] {z : A} {y : R} (hy : y ∈ nonZeroDivisors R) (h : IsAlgebraic R (y • z)) :
IsAlgebraic R z
source
theorem IsAlgebraic.iff_exists_smul_integral {R : Type u_1} {A : Type u_3} [CommRing R] [Ring A] [Algebra R A] {z : A} [IsReduced R] :
IsAlgebraic R z ↔ ∃ (y : R), y ≠ 0 ∧ IsIntegral R (y • z)

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.

source
theorem IsAlgebraic.restrictScalars_of_isIntegral (R : Type u_1) {S : Type u_2} {A : Type u_3} [CommRing R] [CommRing S] [Ring A] [Algebra R S] [Algebra R A] [Algebra S A] [IsScalarTower R S A] [NoZeroDivisors S] [int : Algebra.IsIntegral R S] {a : A} (h : IsAlgebraic S a) :
IsAlgebraic R a
source
theorem IsAlgebraic.restrictScalars (R : Type u_1) {S : Type u_2} {A : Type u_3} [CommRing R] [CommRing S] [Ring A] [Algebra R S] [Algebra R A] [Algebra S A] [IsScalarTower R S A] [NoZeroDivisors S] [Algebra.IsAlgebraic R S] {a : A} (h : IsAlgebraic S a) :
IsAlgebraic R a
source
theorem IsIntegral.trans_isAlgebraic (R : Type u_1) {S : Type u_2} {A : Type u_3} [CommRing R] [CommRing S] [Ring A] [Algebra R S] [Algebra R A] [Algebra S A] [IsScalarTower R S A] [NoZeroDivisors S] [alg : Algebra.IsAlgebraic R S] {a : A} (h : IsIntegral S a) :
IsAlgebraic R a
source
theorem IsAlgebraic.neg {R : Type u_1} {A : Type u_3} [CommRing R] [Ring A] [Algebra R A] {a : A} (ha : IsAlgebraic R a) :
IsAlgebraic R (-a)
source
theorem IsAlgebraic.smul {R : Type u_1} {A : Type u_3} [CommRing R] [Ring A] [Algebra R A] {a : A} (ha : IsAlgebraic R a) (r : R) :
IsAlgebraic R (r • a)
source
theorem IsAlgebraic.nsmul {R : Type u_1} {A : Type u_3} [CommRing R] [Ring A] [Algebra R A] {a : A} (ha : IsAlgebraic R a) (n : ℕ) :
IsAlgebraic R (n • a)
source
theorem IsAlgebraic.zsmul {R : Type u_1} {A : Type u_3} [CommRing R] [Ring A] [Algebra R A] {a : A} (ha : IsAlgebraic R a) (n : ℤ) :
IsAlgebraic R (n • a)
source
theorem IsAlgebraic.tmul {R : Type u_1} {S : Type u_2} {A : Type u_3} [CommRing R] [CommRing S] [Ring A] [Algebra R S] [Algebra R A] (s : S) {a : A} (ha : IsAlgebraic R a) [FaithfulSMul R S] :
IsAlgebraic S (s ⊗ₜ[R] a)
source
theorem IsAlgebraic.mul {R : Type u_1} {S : Type u_2} [CommRing R] [CommRing S] [Algebra R S] [NoZeroDivisors R] {a b : S} (ha : IsAlgebraic R a) (hb : IsAlgebraic R b) :
IsAlgebraic R (a * b)
source
theorem IsAlgebraic.add {R : Type u_1} {S : Type u_2} [CommRing R] [CommRing S] [Algebra R S] [NoZeroDivisors R] {a b : S} (ha : IsAlgebraic R a) (hb : IsAlgebraic R b) :
IsAlgebraic R (a + b)
source
theorem IsAlgebraic.sub {R : Type u_1} {S : Type u_2} [CommRing R] [CommRing S] [Algebra R S] [NoZeroDivisors R] {a b : S} (ha : IsAlgebraic R a) (hb : IsAlgebraic R b) :
IsAlgebraic R (a - b)
source
theorem IsAlgebraic.pow {R : Type u_1} {S : Type u_2} [CommRing R] [CommRing S] [Algebra R S] [NoZeroDivisors R] {a : S} (ha : IsAlgebraic R a) (n : ℕ) :
IsAlgebraic R (a ^ n)
source
theorem Algebra.IsAlgebraic.trans (R : Type u_1) (S : Type u_2) (A : Type u_3) [CommRing R] [CommRing S] [Ring A] [Algebra R S] [Algebra R A] [Algebra S A] [IsScalarTower R S A] [NoZeroDivisors S] [Algebra.IsAlgebraic R S] [alg : Algebra.IsAlgebraic S A] :
Algebra.IsAlgebraic R A

Transitivity of algebraicity for algebras over domains.

source
theorem Algebra.IsIntegral.trans_isAlgebraic (R : Type u_1) (S : Type u_2) (A : Type u_3) [CommRing R] [CommRing S] [Ring A] [Algebra R S] [Algebra R A] [Algebra S A] [IsScalarTower R S A] [NoZeroDivisors S] [Algebra.IsIntegral R S] [alg : Algebra.IsAlgebraic S A] :
Algebra.IsAlgebraic R A
source
theorem Algebra.IsAlgebraic.trans_isIntegral (R : Type u_1) (S : Type u_2) (A : Type u_3) [CommRing R] [CommRing S] [Ring A] [Algebra R S] [Algebra R A] [Algebra S A] [IsScalarTower R S A] [NoZeroDivisors S] [Algebra.IsAlgebraic R S] [int : Algebra.IsIntegral S A] :
Algebra.IsAlgebraic R A
source
theorem Algebra.IsIntegral.isAlgebraic_iff (R : Type u_1) (S : Type u_2) {A : Type u_3} [CommRing R] [CommRing S] [Ring A] [Algebra R S] [Algebra R A] [Algebra S A] [IsScalarTower R S A] [NoZeroDivisors S] [Algebra.IsIntegral R S] [FaithfulSMul R S] {a : A} :
IsAlgebraic R a ↔ IsAlgebraic S a
source
theorem Algebra.IsIntegral.isAlgebraic_iff_top (R : Type u_1) (S : Type u_2) {A : Type u_3} [CommRing R] [CommRing S] [Ring A] [Algebra R S] [Algebra R A] [Algebra S A] [IsScalarTower R S A] [NoZeroDivisors S] [Algebra.IsIntegral R S] [FaithfulSMul R S] :
Algebra.IsAlgebraic R A ↔ Algebra.IsAlgebraic S A
source
theorem Algebra.IsAlgebraic.isAlgebraic_iff (R : Type u_1) (S : Type u_2) {A : Type u_3} [CommRing R] [CommRing S] [Ring A] [Algebra R S] [Algebra R A] [Algebra S A] [IsScalarTower R S A] [NoZeroDivisors S] [Algebra.IsAlgebraic R S] [FaithfulSMul R S] {a : A} :
IsAlgebraic R a ↔ IsAlgebraic S a
source
theorem Algebra.IsAlgebraic.isAlgebraic_iff_top (R : Type u_1) (S : Type u_2) {A : Type u_3} [CommRing R] [CommRing S] [Ring A] [Algebra R S] [Algebra R A] [Algebra S A] [IsScalarTower R S A] [NoZeroDivisors S] [Algebra.IsAlgebraic R S] [FaithfulSMul R S] :
Algebra.IsAlgebraic R A ↔ Algebra.IsAlgebraic S A
source
theorem Algebra.IsAlgebraic.isAlgebraic_iff_bot (R : Type u_1) (S : Type u_2) {A : Type u_3} [CommRing R] [CommRing S] [Ring A] [Algebra R S] [Algebra R A] [Algebra S A] [IsScalarTower R S A] [NoZeroDivisors S] [Algebra.IsAlgebraic S A] [FaithfulSMul S A] :
Algebra.IsAlgebraic R A ↔ Algebra.IsAlgebraic R S
source
def Subalgebra.algebraicClosure (R : Type u_1) (S : Type u_2) [CommRing R] [CommRing S] [Algebra R S] [IsDomain R] :
Subalgebra R S

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.

Equations

- Subalgebra.algebraicClosure R S = { carrier := {s : S | IsAlgebraic R s}, mul_mem' := ⋯, one_mem' := ⋯, add_mem' := ⋯, zero_mem' := ⋯, algebraMap_mem' := ⋯ }

Instances For

source
theorem Subalgebra.mem_algebraicClosure (R : Type u_1) (S : Type u_2) [CommRing R] [CommRing S] [Algebra R S] [IsDomain R] {x : S} :
x ∈ algebraicClosure R S ↔ IsAlgebraic R x
source
theorem integralClosure_le_algebraicClosure (R : Type u_1) (S : Type u_2) [CommRing R] [CommRing S] [Algebra R S] [IsDomain R] :
integralClosure R S ≤ Subalgebra.algebraicClosure R S
source
theorem Subalgebra.algebraicClosure_eq_integralClosure (S : Type u_2) [CommRing S] {K : Type u_4} [Field K] [Algebra K S] :
algebraicClosure K S = integralClosure K S
source
instance instIsAlgebraicSubtypeMemSubalgebraAlgebraicClosure (R : Type u_1) (S : Type u_2) [CommRing R] [CommRing S] [Algebra R S] [IsDomain R] :
Algebra.IsAlgebraic R ↥(Subalgebra.algebraicClosure R S)
source
theorem Algebra.isAlgebraic_adjoin_iff {R : Type u_1} {S : Type u_2} [CommRing R] [CommRing S] [Algebra R S] [IsDomain R] {s : Set S} :
(adjoin R s).IsAlgebraic ↔ ∀ x ∈ s, IsAlgebraic R x
source
theorem Algebra.isAlgebraic_adjoin_of_nonempty {R : Type u_1} {S : Type u_2} [CommRing R] [CommRing S] [Algebra R S] [NoZeroDivisors R] {s : Set S} (hs : s.Nonempty) :
(adjoin R s).IsAlgebraic ↔ ∀ x ∈ s, IsAlgebraic R x
source
theorem Algebra.isAlgebraic_adjoin_singleton_iff {R : Type u_1} {S : Type u_2} [CommRing R] [CommRing S] [Algebra R S] [NoZeroDivisors R] {s : S} :
(adjoin R {s}).IsAlgebraic ↔ IsAlgebraic R s

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.

source
theorem IsAlgebraic.of_mul {R : Type u_1} {S : Type u_2} [CommRing R] [CommRing S] [Algebra R S] [NoZeroDivisors R] {y z : S} (hy : y ∈ nonZeroDivisors S) (alg_y : IsAlgebraic R y) (alg_yz : IsAlgebraic R (y * z)) :
IsAlgebraic R z
source
theorem IsAlgebraic.adjoin_of_forall_isAlgebraic {R : Type u_1} {S : Type u_2} {A : Type u_3} [CommRing R] [CommRing S] [Ring A] [Algebra R S] [Algebra S A] [NoZeroDivisors S] {s t : Set S} (alg : ∀ x ∈ s \ t, IsAlgebraic (↥(Algebra.adjoin R t)) x) {a : A} (ha : IsAlgebraic (↥(Algebra.adjoin R s)) a) :
IsAlgebraic (↥(Algebra.adjoin R t)) a
source
theorem Transcendental.extendScalars_of_isIntegral {R : Type u_1} (S : Type u_2) {A : Type u_3} [CommRing R] [CommRing S] [Ring A] [Algebra R S] [Algebra R A] [Algebra S A] [IsScalarTower R S A] [NoZeroDivisors S] {a : A} (ha : Transcendental R a) [Algebra.IsIntegral R S] :
Transcendental S a
source
theorem Transcendental.extendScalars {R : Type u_1} (S : Type u_2) {A : Type u_3} [CommRing R] [CommRing S] [Ring A] [Algebra R S] [Algebra R A] [Algebra S A] [IsScalarTower R S A] [NoZeroDivisors S] {a : A} (ha : Transcendental R a) [Algebra.IsAlgebraic R S] :
Transcendental S a
source
theorem Transcendental.integralClosure {R : Type u_1} {S : Type u_2} [CommRing R] [CommRing S] [Algebra R S] [NoZeroDivisors S] {a : S} (ha : Transcendental R a) :
Transcendental (↥(integralClosure R S)) a
source
theorem Transcendental.subalgebraAlgebraicClosure {R : Type u_1} {S : Type u_2} [CommRing R] [CommRing S] [Algebra R S] [NoZeroDivisors S] {a : S} (ha : Transcendental R a) [IsDomain R] :
Transcendental (↥(Subalgebra.algebraicClosure R S)) a
source
theorem Algebra.IsIntegral.transcendental_iff (R : Type u_1) (S : Type u_2) {A : Type u_3} [CommRing R] [CommRing S] [Ring A] [Algebra R S] [Algebra R A] [Algebra S A] [IsScalarTower R S A] [NoZeroDivisors S] [FaithfulSMul R S] {a : A} [Algebra.IsIntegral R S] :
Transcendental R a ↔ Transcendental S a
source
theorem Algebra.IsAlgebraic.transcendental_iff (R : Type u_1) (S : Type u_2) {A : Type u_3} [CommRing R] [CommRing S] [Ring A] [Algebra R S] [Algebra R A] [Algebra S A] [IsScalarTower R S A] [NoZeroDivisors S] [FaithfulSMul R S] {a : A} [Algebra.IsAlgebraic R S] :
Transcendental R a ↔ Transcendental S a
source
instance Algebra.IsAlgebraic.instIsLocalizationAlgebraMapSubmonoidNonZeroDivisors (R : Type u_1) (S : Type u_2) [CommRing R] [CommRing S] [Algebra R S] (S' : Type u_5) [CommRing S'] [FaithfulSMul R S] [alg : Algebra.IsAlgebraic R S] [NoZeroDivisors S] [Algebra S S'] [IsFractionRing S S'] :
IsLocalization (algebraMapSubmonoid S (nonZeroDivisors R)) S'
source
instance Algebra.IsAlgebraic.instIsLocalizedModuleNonZeroDivisorsToLinearMapToAlgHom (R : Type u_1) (S : Type u_2) [CommRing R] [CommRing S] [Algebra R S] (S' : Type u_5) [CommRing S'] [FaithfulSMul R S] [alg : Algebra.IsAlgebraic R S] [NoZeroDivisors S] [Algebra S S'] [IsFractionRing S S'] [Algebra R S'] [IsScalarTower R S S'] :
IsLocalizedModule (nonZeroDivisors R) (IsScalarTower.toAlgHom R S S').toLinearMap
source
theorem Algebra.IsAlgebraic.isBaseChange_of_isFractionRing (R : Type u_1) (S : Type u_2) [CommRing R] [CommRing S] [Algebra R S] (R' : Type u_4) (S' : Type u_5) [CommRing S'] [FaithfulSMul R S] [alg : Algebra.IsAlgebraic R S] [NoZeroDivisors S] [Algebra S S'] [IsFractionRing S S'] [Algebra R S'] [IsScalarTower R S S'] [CommRing R'] [Algebra R R'] [IsFractionRing R R'] [Module R' S'] [IsScalarTower R R' S'] :
IsBaseChange R' (IsScalarTower.toAlgHom R S S').toLinearMap
source
instance Algebra.IsAlgebraic.instIsPushout (R : Type u_1) (S : Type u_2) [CommRing R] [CommRing S] [Algebra R S] (R' : Type u_4) (S' : Type u_5) [CommRing S'] [FaithfulSMul R S] [alg : Algebra.IsAlgebraic R S] [NoZeroDivisors S] [Algebra S S'] [IsFractionRing S S'] [Algebra R S'] [IsScalarTower R S S'] [CommRing R'] [Algebra R R'] [IsFractionRing R R'] [Algebra R' S'] [IsScalarTower R R' S'] :
IsPushout R R' S S'
source
instance Algebra.IsAlgebraic.instIsPushout_1 (R : Type u_1) (S : Type u_2) [CommRing R] [CommRing S] [Algebra R S] (R' : Type u_4) (S' : Type u_5) [CommRing S'] [FaithfulSMul R S] [alg : Algebra.IsAlgebraic R S] [NoZeroDivisors S] [Algebra S S'] [IsFractionRing S S'] [Algebra R S'] [IsScalarTower R S S'] [CommRing R'] [Algebra R R'] [IsFractionRing R R'] [Algebra R' S'] [IsScalarTower R R' S'] :
IsPushout R S R' S'
source
theorem Algebra.IsAlgebraic.lift_rank_of_isFractionRing (R : Type u_1) [CommRing R] (R' : Type u_4) (S : Type u) [CommRing R'] [CommRing S] [Algebra R S] [Algebra R R'] [IsFractionRing R R'] [FaithfulSMul R S] [Algebra.IsAlgebraic R S] [NoZeroDivisors S] (S' : Type v) [CommRing S'] [Algebra R S'] [Algebra S S'] [Module R' S'] [IsScalarTower R R' S'] [IsScalarTower R S S'] [IsFractionRing S S'] :
Cardinal.lift.{u, v} (Module.rank R' S') = Cardinal.lift.{v, u} (Module.rank R S)
source
theorem Algebra.IsAlgebraic.finrank_of_isFractionRing (R : Type u_1) [CommRing R] (R' : Type u_4) (S : Type u) [CommRing R'] [CommRing S] [Algebra R S] [Algebra R R'] [IsFractionRing R R'] [FaithfulSMul R S] [Algebra.IsAlgebraic R S] [NoZeroDivisors S] (S' : Type v) [CommRing S'] [Algebra R S'] [Algebra S S'] [Module R' S'] [IsScalarTower R R' S'] [IsScalarTower R S S'] [IsFractionRing S S'] :
Module.finrank R' S' = Module.finrank R S
source
theorem Algebra.IsAlgebraic.rank_of_isFractionRing (R : Type u_1) [CommRing R] (R' : Type u_4) (S : Type u) [CommRing R'] [CommRing S] [Algebra R S] [Algebra R R'] [IsFractionRing R R'] [FaithfulSMul R S] [Algebra.IsAlgebraic R S] [NoZeroDivisors S] (S' : Type u) [CommRing S'] [Algebra R S'] [Algebra S S'] [Module R' S'] [IsScalarTower R R' S'] [IsScalarTower R S S'] [IsFractionRing S S'] :
Module.rank R' S' = Module.rank R S
source
theorem Algebra.IsAlgebraic.rank_fractionRing (R : Type u_1) [CommRing R] (S : Type u) [CommRing S] [Algebra R S] [FaithfulSMul R S] [Algebra.IsAlgebraic R S] [IsDomain S] :
Module.rank (FractionRing R) (FractionRing S) = Module.rank R S
source
theorem rank_polynomial_polynomial (R : Type u_1) (S : Type u_2) [CommRing R] [CommRing S] [Algebra R S] [NoZeroDivisors R] :
Module.rank (Polynomial R) (Polynomial S) = Module.rank R S
source
theorem rank_mvPolynomial_mvPolynomial (R : Type u_1) (S : Type u_2) [CommRing R] [CommRing S] [Algebra R S] [NoZeroDivisors R] (σ : Type u) :
Module.rank (MvPolynomial σ R) (MvPolynomial σ S) = Cardinal.lift.{u, u_2} (Module.rank R S)
source
instance Algebra.IsAlgebraic.tensorProduct (R : Type u_1) (S : Type u_2) [CommRing R] [CommRing S] [Algebra R S] [alg : Algebra.IsAlgebraic R S] (R' : Type u_4) [CommRing R'] [Algebra R R'] [NoZeroDivisors R'] [FaithfulSMul R R'] :
Algebra.IsAlgebraic R' (TensorProduct R R' S)
source
theorem Algebra.IsPushout.isAlgebraic' (R : Type u_1) (S : Type u_2) [CommRing R] [CommRing S] [Algebra R S] [alg : Algebra.IsAlgebraic R S] (R' : Type u_4) [CommRing R'] [Algebra R R'] [NoZeroDivisors R'] [FaithfulSMul R R'] (S' : Type u_5) [CommRing S'] [Algebra R S'] [Algebra S S'] [Algebra R' S'] [IsScalarTower R R' S'] [IsScalarTower R S S'] [IsPushout R R' S S'] :
Algebra.IsAlgebraic R' S'
source
theorem Algebra.IsPushout.isAlgebraic (R : Type u_1) (S : Type u_2) [CommRing R] [CommRing S] [Algebra R S] [alg : Algebra.IsAlgebraic R S] (R' : Type u_4) [CommRing R'] [Algebra R R'] [NoZeroDivisors R'] [FaithfulSMul R R'] (S' : Type u_5) [CommRing S'] [Algebra R S'] [Algebra S S'] [Algebra R' S'] [IsScalarTower R R' S'] [IsScalarTower R S S'] [h : IsPushout R S R' S'] :
Algebra.IsAlgebraic R' S'
source
instance instIsAlgebraicPolynomialOfNoZeroDivisors {R : Type u_1} {S : Type u_2} [CommRing R] [CommRing S] [Algebra R S] [alg : Algebra.IsAlgebraic R S] [NoZeroDivisors R] :
Algebra.IsAlgebraic (Polynomial R) (Polynomial S)
source
instance instIsAlgebraicPolynomialOfNoZeroDivisors_1 {R : Type u_1} {S : Type u_2} [CommRing R] [CommRing S] [Algebra R S] [alg : Algebra.IsAlgebraic R S] [NoZeroDivisors S] :
Algebra.IsAlgebraic (Polynomial R) (Polynomial S)
source
theorem Polynomial.exists_dvd_map_of_isAlgebraic {R : Type u_1} {S : Type u_2} [CommRing R] [CommRing S] [Algebra R S] [alg : Algebra.IsAlgebraic R S] [NoZeroDivisors S] {f : Polynomial S} (hf : f ≠ 0) :
∃ (g : Polynomial R), g ≠ 0 ∧ f ∣ map (algebraMap R S) g
source
instance instIsAlgebraicMvPolynomialOfNoZeroDivisors {R : Type u_1} {S : Type u_2} [CommRing R] [CommRing S] [Algebra R S] [alg : Algebra.IsAlgebraic R S] {σ : Type u_4} [NoZeroDivisors R] :
Algebra.IsAlgebraic (MvPolynomial σ R) (MvPolynomial σ S)
source
instance instIsAlgebraicMvPolynomialOfNoZeroDivisors_1 {R : Type u_1} {S : Type u_2} [CommRing R] [CommRing S] [Algebra R S] [alg : Algebra.IsAlgebraic R S] {σ : Type u_4} [NoZeroDivisors S] :
Algebra.IsAlgebraic (MvPolynomial σ R) (MvPolynomial σ S)
source
theorem MvPolynomial.exists_dvd_map_of_isAlgebraic {R : Type u_1} {S : Type u_2} [CommRing R] [CommRing S] [Algebra R S] [alg : Algebra.IsAlgebraic R S] {σ : Type u_4} [NoZeroDivisors S] {f : MvPolynomial σ S} (hf : f ≠ 0) :
∃ (g : MvPolynomial σ R), g ≠ 0 ∧ f ∣ (map (algebraMap R S)) g
source
instance instIsPushoutFractionRingPolynomial {R : Type u_1} {S : Type u_2} [CommRing R] [CommRing S] [Algebra R S] [alg : Algebra.IsAlgebraic R S] [IsDomain S] [FaithfulSMul R S] :
Algebra.IsPushout R (FractionRing (Polynomial R)) S (FractionRing (Polynomial S))
source
instance instIsPushoutFractionRingPolynomial_1 {R : Type u_1} {S : Type u_2} [CommRing R] [CommRing S] [Algebra R S] [alg : Algebra.IsAlgebraic R S] [IsDomain S] [FaithfulSMul R S] :
Algebra.IsPushout R S (FractionRing (Polynomial R)) (FractionRing (Polynomial S))
source
instance instIsPushoutFractionRingMvPolynomial {R : Type u_1} {S : Type u_2} [CommRing R] [CommRing S] [Algebra R S] [alg : Algebra.IsAlgebraic R S] [IsDomain S] [FaithfulSMul R S] {σ : Type u_4} :
Algebra.IsPushout R (FractionRing (MvPolynomial σ R)) S (FractionRing (MvPolynomial σ S))
source
instance instIsPushoutFractionRingMvPolynomial_1 {R : Type u_1} {S : Type u_2} [CommRing R] [CommRing S] [Algebra R S] [alg : Algebra.IsAlgebraic R S] [IsDomain S] [FaithfulSMul R S] {σ : Type u_4} :
Algebra.IsPushout R S (FractionRing (MvPolynomial σ R)) (FractionRing (MvPolynomial σ S))
source
theorem Algebra.IsAlgebraic.rank_fractionRing_polynomial {R : Type u_1} {S : Type u_2} [CommRing R] [CommRing S] [Algebra R S] [alg : Algebra.IsAlgebraic R S] [IsDomain S] [FaithfulSMul R S] :
Module.rank (FractionRing (Polynomial R)) (FractionRing (Polynomial S)) = Module.rank R S

Stacks Tag 0G1M

source
theorem Algebra.IsAlgebraic.rank_fractionRing_mvPolynomial {R : Type u_1} {S : Type u_2} [CommRing R] [CommRing S] [Algebra R S] [alg : Algebra.IsAlgebraic R S] [IsDomain S] [FaithfulSMul R S] (σ : Type u) :
Module.rank (FractionRing (MvPolynomial σ R)) (FractionRing (MvPolynomial σ S)) = Cardinal.lift.{u, u_2} (Module.rank R S)

Stacks Tag 0G1M

source
instance instFiniteDimensionalFractionRingOfFinite {R : Type u_1} {S : Type u_2} [CommRing R] [CommRing S] [Algebra R S] [IsDomain R] [IsDomain S] [NoZeroSMulDivisors R S] [Module.Finite R S] :
FiniteDimensional (FractionRing R) (FractionRing S)