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

        Equations
        Instances For

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

          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.

          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 Polynomial.rootSet p 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) (h : 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) (h : 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.

          Alias of the forward direction of Algebra.isAlgebraic_iff_isIntegral.

          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)) (A_alg : 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] (A_alg : 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] :
          theorem 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.

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

          Bijection between algebra equivalences and algebra homomorphisms

          Equations
          • One or more equations did not get rendered due to their size.
          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]
            noncomputable def 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] (h : 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) (Polynomial.divX p) 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 : Polynomial.coeff p 0 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 : Polynomial.coeff p 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) (hKL : 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') :
                  @[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