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.

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.

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

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.

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

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.

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.

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

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

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.

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

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 ⇑ϕ

@[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

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)

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)

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

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

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.

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

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

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

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)

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)

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)

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)

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)

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)

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)

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)

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)

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.

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

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

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

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

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

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

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

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' := ⋯ }

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

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

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

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)

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

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

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.

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

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

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

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

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

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

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

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

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'

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

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

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'

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'

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)

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

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

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

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

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)

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)

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'

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'

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)

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)

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

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)

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)

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

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

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

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

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

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

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