Documentation

Mathlib.RingTheory.Algebraic

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.

def IsAlgebraic (R : Type u) {A : Type v} [CommRing R] [Ring A] [Algebra R A] (x : A) :

An element of an R-algebra is algebraic over R if it is a root of a nonzero polynomial with coefficients in R.

Equations
Instances For
    def Transcendental (R : Type u) {A : Type v} [CommRing R] [Ring A] [Algebra R A] (x : A) :

    An element of an R-algebra is transcendental over R if it is not algebraic over R.

    Equations
    Instances For
      theorem is_transcendental_of_subsingleton (R : Type u) {A : Type v} [CommRing R] [Ring A] [Algebra R A] [Subsingleton R] (x : A) :
      def Subalgebra.IsAlgebraic {R : Type u} {A : Type v} [CommRing R] [Ring A] [Algebra R A] (S : Subalgebra R A) :

      A subalgebra is algebraic if all its elements are algebraic.

      Equations
      Instances For
        class Algebra.IsAlgebraic (R : Type u) (A : Type v) [CommRing R] [Ring A] [Algebra R A] :

        An algebra is algebraic if all its elements are algebraic.

        Instances
          theorem Algebra.IsAlgebraic.isAlgebraic {R : Type u} {A : Type v} :
          ∀ {inst : CommRing R} {inst_1 : Ring A} {inst_2 : Algebra R A} [self : Algebra.IsAlgebraic R A] (x : A), IsAlgebraic R x
          class Algebra.Transcendental (R : Type u) (A : Type v) [CommRing R] [Ring A] [Algebra R A] :

          An algebra is transcendental if some element is transcendental.

          Instances
            theorem Algebra.Transcendental.transcendental {R : Type u} {A : Type v} :
            ∀ {inst : CommRing R} {inst_1 : Ring A} {inst_2 : Algebra R A} [self : Algebra.Transcendental R A], ∃ (x : A), Transcendental R x
            theorem Algebra.isAlgebraic_def {R : Type u} {A : Type v} [CommRing R] [Ring A] [Algebra R A] :
            Algebra.IsAlgebraic R A ∀ (x : A), IsAlgebraic R x
            theorem Algebra.transcendental_def {R : Type u} {A : Type v} [CommRing R] [Ring A] [Algebra R A] :
            theorem Subalgebra.isAlgebraic_iff {R : Type u} {A : Type v} [CommRing R] [Ring A] [Algebra R A] (S : Subalgebra R A) :
            S.IsAlgebraic Algebra.IsAlgebraic R S

            A subalgebra is algebraic if and only if it is algebraic as an algebra.

            theorem Algebra.isAlgebraic_iff {R : Type u} {A : Type v} [CommRing R] [Ring A] [Algebra R A] :
            Algebra.IsAlgebraic R A .IsAlgebraic

            An algebra is algebraic if and only if it is algebraic as a subalgebra.

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

            An integral element of an algebra is algebraic.

            Equations
            • =
            theorem isAlgebraic_zero {R : Type u} {A : Type v} [CommRing R] [Ring A] [Algebra R A] [Nontrivial R] :
            theorem isAlgebraic_algebraMap {R : Type u} {A : Type v} [CommRing R] [Ring A] [Algebra R A] [Nontrivial R] (x : R) :

            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] :
            theorem isAlgebraic_nat {R : Type u} {A : Type v} [CommRing R] [Ring A] [Algebra R A] [Nontrivial R] (n : ) :
            theorem isAlgebraic_int {R : Type u} {A : Type v} [CommRing R] [Ring A] [Algebra R A] [Nontrivial R] (n : ) :
            theorem isAlgebraic_rat (R : Type u) {A : Type v} [DivisionRing A] [Field R] [Algebra R A] (n : ) :
            theorem isAlgebraic_of_mem_rootSet {R : Type u} {A : Type v} [Field R] [Field A] [Algebra R A] {p : Polynomial R} {x : A} (hx : x p.rootSet A) :
            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 aIsAlgebraic 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_algHom_iff {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) {a : 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 AlgEquiv.isAlgebraic_iff {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) :
            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 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)) :
            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) :
            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) :
            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_iff {R : Type u} [CommRing R] {K : Type u_2} [Field K] [Algebra R K] {x : K} :
            theorem IsAlgebraic.inv {R : Type u} [CommRing R] {K : Type u_2} [Field K] [Algebra R K] {x : K} :

            Alias of the reverse direction of IsAlgebraic.inv_iff.

            theorem isAlgebraic_iff_isIntegral {K : Type u} {A : Type v} [Field K] [Ring A] [Algebra K A] {x : A} :

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

            theorem IsAlgebraic.isIntegral {K : Type u} {A : Type v} [Field K] [Ring A] [Algebra K A] {x : A} :

            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.

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

            Equations
            • =
            theorem IsAlgebraic.tower_top_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] (hinj : Function.Injective (algebraMap R S)) {x : A} (A_alg : IsAlgebraic R 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 Algebra.IsAlgebraic.tower_top_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] (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 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) :

            If x is algebraic over K, then x is algebraic over L 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

            theorem IsAlgebraic.of_finite (K : Type u_1) {A : Type u_5} [Field K] [Ring A] [Algebra K A] (e : A) [FiniteDimensional K A] :
            instance Algebra.IsAlgebraic.of_finite (K : Type u_1) (A : Type u_5) [Field K] [Ring A] [Algebra K A] [FiniteDimensional K A] :

            A field extension is algebraic if it is finite.

            Equations
            • =
            theorem Algebra.IsAlgebraic.trans {K : Type u_1} {L : Type u_2} {A : Type u_5} [Field K] [Field L] [Ring A] [Algebra K L] [Algebra L A] [Algebra K A] [IsScalarTower K L A] [L_alg : Algebra.IsAlgebraic K L] [A_alg : Algebra.IsAlgebraic L A] :

            If L is an algebraic field extension of K and A is an algebraic algebra over L, then A is algebraic over K.

            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] [Field R] [Algebra K R] [Algebra.IsAlgebraic K L] (f : L →ₐ[K] R) (g : 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] :
            (L ≃ₐ[K] L) ≃* (L →ₐ[K] L)

            Bijection between algebra equivalences and algebra homomorphisms

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

              Bijection between algebra equivalences and algebra homomorphisms

              Equations
              Instances For
                theorem exists_integral_multiple {R : Type u_1} {S : Type u_2} [CommRing R] [IsDomain R] [CommRing S] [Algebra R S] {z : S} (hz : IsAlgebraic R z) (inj : ∀ (x : R), (algebraMap R S) x = 0x = 0) :
                ∃ (x : (integralClosure R S)) (y : R), y 0 z * (algebraMap R S) y = x
                theorem IsIntegralClosure.exists_smul_eq_mul {R : Type u_1} {S : Type u_2} [CommRing R] [IsDomain R] [CommRing S] {L : Type u_3} [Field L] [Algebra R S] [Algebra S L] [Algebra R L] [IsScalarTower R S L] [IsIntegralClosure S R L] [Algebra.IsAlgebraic R L] (inj : Function.Injective (algebraMap R L)) (a : S) {b : S} (hb : b 0) :
                ∃ (c : S) (d : R), d 0 d a = b * c

                A fraction (a : S) / (b : S) can be reduced to (c : S) / (d : R), if S is the integral closure of R in an algebraic extension L of R.

                theorem inv_eq_of_aeval_divX_ne_zero {K : Type u_3} {L : Type u_4} [Field K] [Field L] [Algebra K L] {x : L} {p : Polynomial K} (aeval_ne : (Polynomial.aeval x) p.divX 0) :
                x⁻¹ = (Polynomial.aeval x) p.divX / ((Polynomial.aeval x) p - (algebraMap K L) (p.coeff 0))
                theorem inv_eq_of_root_of_coeff_zero_ne_zero {K : Type u_3} {L : Type u_4} [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) :
                x⁻¹ = -((Polynomial.aeval x) p.divX / (algebraMap K L) (p.coeff 0))
                theorem Subalgebra.inv_mem_of_root_of_coeff_zero_ne_zero {K : Type u_3} {L : Type u_4} [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) :
                (↑x)⁻¹ A
                theorem Subalgebra.inv_mem_of_algebraic {K : Type u_3} {L : Type u_4} [Field K] [Field L] [Algebra K L] (A : Subalgebra K L) {x : A} (hx : IsAlgebraic K x) :
                (↑x)⁻¹ A
                theorem Subalgebra.isField_of_algebraic {K : Type u_3} {L : Type u_4} [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.

                def Polynomial.hasSMulPi (R' : Type u) (S' : Type v) [Semiring R'] [SMul R' S'] :
                SMul (Polynomial R') (R'S')

                This is not an instance as it forms a diamond with Pi.instSMul.

                See the instance_diamonds test for details.

                Equations
                Instances For
                  noncomputable def Polynomial.hasSMulPi' (R' : Type u) (S' : Type v) (T' : Type w) [CommSemiring R'] [Semiring S'] [Algebra R' S'] [SMul S' T'] :
                  SMul (Polynomial R') (S'T')

                  This is not an instance as it forms a diamond with Pi.instSMul.

                  See the instance_diamonds test for details.

                  Equations
                  Instances For
                    @[simp]
                    theorem polynomial_smul_apply (R' : Type u) (S' : Type v) [Semiring R'] [SMul R' S'] (p : Polynomial R') (f : R'S') (x : R') :
                    (p f) x = Polynomial.eval x p f x
                    @[simp]
                    theorem polynomial_smul_apply' (R' : Type u) (S' : Type v) (T' : Type w) [CommSemiring R'] [Semiring S'] [Algebra R' S'] [SMul S' T'] (p : Polynomial R') (f : S'T') (x : S') :
                    (p f) x = (Polynomial.aeval x) p f x
                    noncomputable def Polynomial.algebraPi (R' : Type u) (S' : Type v) (T' : Type w) [CommSemiring R'] [CommSemiring S'] [CommSemiring T'] [Algebra R' S'] [Algebra S' T'] :
                    Algebra (Polynomial R') (S'T')

                    This is not an instance for the same reasons as Polynomial.hasSMulPi'.

                    Equations
                    • One or more equations did not get rendered due to their size.
                    Instances For
                      @[simp]
                      theorem Polynomial.algebraMap_pi_eq_aeval (R' : Type u) (S' : Type v) (T' : Type w) [CommSemiring R'] [CommSemiring S'] [CommSemiring T'] [Algebra R' S'] [Algebra S' T'] :
                      (algebraMap (Polynomial R') (S'T')) = fun (p : Polynomial R') (z : S') => (algebraMap S' T') ((Polynomial.aeval z) p)
                      @[simp]
                      theorem Polynomial.algebraMap_pi_self_eq_eval (R' : Type u) [CommSemiring R'] :
                      (algebraMap (Polynomial R') (R'R')) = fun (p : Polynomial R') (z : R') => Polynomial.eval z p