Documentation

Mathlib.RingTheory.PowerBasis

Power basis #

This file defines a structure PowerBasis R S, giving a basis of the R-algebra S as a finite list of powers 1, x, ..., x^n. For example, if x is algebraic over a ring/field, adjoining x gives a PowerBasis structure generated by x.

Definitions #

Implementation notes #

Throughout this file, R, S, A, B ... are CommRings, and K, L, ... are Fields. S is an R-algebra, B is an A-algebra, L is a K-algebra.

Tags #

power basis, powerbasis

structure PowerBasis (R : Type u_7) (S : Type u_8) [CommRing R] [Ring S] [Algebra R S] :
Type (max u_7 u_8)
  • gen : S
  • dim :
  • basis : Basis (Fin s.dim) R S
  • basis_eq_pow : ∀ (i : Fin s.dim), s.basis i = s.gen ^ i

pb : PowerBasis R S states that 1, pb.gen, ..., pb.gen ^ (pb.dim - 1) is a basis for the R-algebra S (viewed as R-module).

This is a structure, not a class, since the same algebra can have many power bases. For the common case where S is defined by adjoining an integral element to R, the canonical power basis is given by {Algebra,IntermediateField}.adjoin.powerBasis.

Instances For
    @[simp]
    theorem PowerBasis.coe_basis {R : Type u_1} {S : Type u_2} [CommRing R] [Ring S] [Algebra R S] (pb : PowerBasis R S) :
    pb.basis = fun i => pb.gen ^ i
    theorem PowerBasis.finiteDimensional {S : Type u_2} [Ring S] {K : Type u_6} [Field K] [Algebra K S] (pb : PowerBasis K S) :

    Cannot be an instance because PowerBasis cannot be a class.

    theorem PowerBasis.finrank {S : Type u_2} [Ring S] {K : Type u_6} [Field K] [Algebra K S] (pb : PowerBasis K S) :
    theorem PowerBasis.mem_span_pow' {R : Type u_1} {S : Type u_2} [CommRing R] [Ring S] [Algebra R S] {x : S} {y : S} {d : } :
    y Submodule.span R (Set.range fun i => x ^ i) f, Polynomial.degree f < d y = ↑(Polynomial.aeval x) f
    theorem PowerBasis.mem_span_pow {R : Type u_1} {S : Type u_2} [CommRing R] [Ring S] [Algebra R S] {x : S} {y : S} {d : } (hd : d 0) :
    y Submodule.span R (Set.range fun i => x ^ i) f, Polynomial.natDegree f < d y = ↑(Polynomial.aeval x) f
    theorem PowerBasis.dim_ne_zero {R : Type u_1} {S : Type u_2} [CommRing R] [Ring S] [Algebra R S] [Nontrivial S] (pb : PowerBasis R S) :
    pb.dim 0
    theorem PowerBasis.dim_pos {R : Type u_1} {S : Type u_2} [CommRing R] [Ring S] [Algebra R S] [Nontrivial S] (pb : PowerBasis R S) :
    0 < pb.dim
    theorem PowerBasis.exists_eq_aeval {R : Type u_1} {S : Type u_2} [CommRing R] [Ring S] [Algebra R S] [Nontrivial S] (pb : PowerBasis R S) (y : S) :
    f, Polynomial.natDegree f < pb.dim y = ↑(Polynomial.aeval pb.gen) f
    theorem PowerBasis.exists_eq_aeval' {R : Type u_1} {S : Type u_2} [CommRing R] [Ring S] [Algebra R S] (pb : PowerBasis R S) (y : S) :
    f, y = ↑(Polynomial.aeval pb.gen) f
    theorem PowerBasis.algHom_ext {R : Type u_1} {S : Type u_2} [CommRing R] [Ring S] [Algebra R S] {S' : Type u_7} [Semiring S'] [Algebra R S'] (pb : PowerBasis R S) ⦃f : S →ₐ[R] S' ⦃g : S →ₐ[R] S' (h : f pb.gen = g pb.gen) :
    f = g
    noncomputable def PowerBasis.minpolyGen {S : Type u_2} [Ring S] {A : Type u_4} [CommRing A] [Algebra A S] (pb : PowerBasis A S) :

    pb.minpolyGen is the minimal polynomial for pb.gen.

    Equations
    Instances For
      theorem PowerBasis.aeval_minpolyGen {S : Type u_2} [Ring S] {A : Type u_4} [CommRing A] [Algebra A S] (pb : PowerBasis A S) :
      theorem PowerBasis.dim_le_natDegree_of_root {S : Type u_2} [Ring S] {A : Type u_4} [CommRing A] [Algebra A S] (pb : PowerBasis A S) {p : Polynomial A} (ne_zero : p 0) (root : ↑(Polynomial.aeval pb.gen) p = 0) :
      theorem PowerBasis.dim_le_degree_of_root {S : Type u_2} [Ring S] {A : Type u_4} [CommRing A] [Algebra A S] (h : PowerBasis A S) {p : Polynomial A} (ne_zero : p 0) (root : ↑(Polynomial.aeval h.gen) p = 0) :
      theorem PowerBasis.degree_minpolyGen {S : Type u_2} [Ring S] {A : Type u_4} [CommRing A] [Algebra A S] [Nontrivial A] (pb : PowerBasis A S) :
      @[simp]
      theorem PowerBasis.minpolyGen_eq {S : Type u_2} [Ring S] {A : Type u_4} [CommRing A] [Algebra A S] (pb : PowerBasis A S) :
      theorem PowerBasis.isIntegral_gen {S : Type u_2} [Ring S] {A : Type u_4} [CommRing A] [Algebra A S] (pb : PowerBasis A S) :
      IsIntegral A pb.gen
      @[simp]
      theorem PowerBasis.degree_minpoly {S : Type u_2} [Ring S] {A : Type u_4} [CommRing A] [Algebra A S] [Nontrivial A] (pb : PowerBasis A S) :
      Polynomial.degree (minpoly A pb.gen) = pb.dim
      @[simp]
      theorem PowerBasis.natDegree_minpoly {S : Type u_2} [Ring S] {A : Type u_4} [CommRing A] [Algebra A S] [Nontrivial A] (pb : PowerBasis A S) :
      Polynomial.natDegree (minpoly A pb.gen) = pb.dim
      theorem PowerBasis.leftMulMatrix {S : Type u_2} [Ring S] {A : Type u_4} [CommRing A] [Algebra A S] (pb : PowerBasis A S) :
      ↑(Algebra.leftMulMatrix pb.basis) pb.gen = Matrix.of fun i j => if j + 1 = pb.dim then -Polynomial.coeff (PowerBasis.minpolyGen pb) i else if i = j + 1 then 1 else 0
      theorem PowerBasis.constr_pow_aeval {S : Type u_2} [Ring S] {A : Type u_4} [CommRing A] [Algebra A S] {S' : Type u_7} [Ring S'] [Algebra A S'] (pb : PowerBasis A S) {y : S'} (hy : ↑(Polynomial.aeval y) (minpoly A pb.gen) = 0) (f : Polynomial A) :
      ↑(↑(Basis.constr pb.basis A) fun i => y ^ i) (↑(Polynomial.aeval pb.gen) f) = ↑(Polynomial.aeval y) f
      theorem PowerBasis.constr_pow_gen {S : Type u_2} [Ring S] {A : Type u_4} [CommRing A] [Algebra A S] {S' : Type u_7} [Ring S'] [Algebra A S'] (pb : PowerBasis A S) {y : S'} (hy : ↑(Polynomial.aeval y) (minpoly A pb.gen) = 0) :
      ↑(↑(Basis.constr pb.basis A) fun i => y ^ i) pb.gen = y
      theorem PowerBasis.constr_pow_algebraMap {S : Type u_2} [Ring S] {A : Type u_4} [CommRing A] [Algebra A S] {S' : Type u_7} [Ring S'] [Algebra A S'] (pb : PowerBasis A S) {y : S'} (hy : ↑(Polynomial.aeval y) (minpoly A pb.gen) = 0) (x : A) :
      ↑(↑(Basis.constr pb.basis A) fun i => y ^ i) (↑(algebraMap A S) x) = ↑(algebraMap A S') x
      theorem PowerBasis.constr_pow_mul {S : Type u_2} [Ring S] {A : Type u_4} [CommRing A] [Algebra A S] {S' : Type u_7} [Ring S'] [Algebra A S'] (pb : PowerBasis A S) {y : S'} (hy : ↑(Polynomial.aeval y) (minpoly A pb.gen) = 0) (x : S) (x' : S) :
      ↑(↑(Basis.constr pb.basis A) fun i => y ^ i) (x * x') = ↑(↑(Basis.constr pb.basis A) fun i => y ^ i) x * ↑(↑(Basis.constr pb.basis A) fun i => y ^ i) x'
      noncomputable def PowerBasis.lift {S : Type u_2} [Ring S] {A : Type u_4} [CommRing A] [Algebra A S] {S' : Type u_7} [Ring S'] [Algebra A S'] (pb : PowerBasis A S) (y : S') (hy : ↑(Polynomial.aeval y) (minpoly A pb.gen) = 0) :
      S →ₐ[A] S'

      pb.lift y hy is the algebra map sending pb.gen to y, where hy states the higher powers of y are the same as the higher powers of pb.gen.

      See PowerBasis.liftEquiv for a bundled equiv sending ⟨y, hy⟩ to the algebra map.

      Equations
      • One or more equations did not get rendered due to their size.
      Instances For
        @[simp]
        theorem PowerBasis.lift_gen {S : Type u_2} [Ring S] {A : Type u_4} [CommRing A] [Algebra A S] {S' : Type u_7} [Ring S'] [Algebra A S'] (pb : PowerBasis A S) (y : S') (hy : ↑(Polynomial.aeval y) (minpoly A pb.gen) = 0) :
        ↑(PowerBasis.lift pb y hy) pb.gen = y
        @[simp]
        theorem PowerBasis.lift_aeval {S : Type u_2} [Ring S] {A : Type u_4} [CommRing A] [Algebra A S] {S' : Type u_7} [Ring S'] [Algebra A S'] (pb : PowerBasis A S) (y : S') (hy : ↑(Polynomial.aeval y) (minpoly A pb.gen) = 0) (f : Polynomial A) :
        ↑(PowerBasis.lift pb y hy) (↑(Polynomial.aeval pb.gen) f) = ↑(Polynomial.aeval y) f
        @[simp]
        theorem PowerBasis.liftEquiv_apply_coe {S : Type u_2} [Ring S] {A : Type u_4} [CommRing A] [Algebra A S] {S' : Type u_7} [Ring S'] [Algebra A S'] (pb : PowerBasis A S) (f : S →ₐ[A] S') :
        ↑(↑(PowerBasis.liftEquiv pb) f) = f pb.gen
        @[simp]
        theorem PowerBasis.liftEquiv_symm_apply {S : Type u_2} [Ring S] {A : Type u_4} [CommRing A] [Algebra A S] {S' : Type u_7} [Ring S'] [Algebra A S'] (pb : PowerBasis A S) (y : { y // ↑(Polynomial.aeval y) (minpoly A pb.gen) = 0 }) :
        (PowerBasis.liftEquiv pb).symm y = PowerBasis.lift pb y (_ : ↑(Polynomial.aeval y) (minpoly A pb.gen) = 0)
        noncomputable def PowerBasis.liftEquiv {S : Type u_2} [Ring S] {A : Type u_4} [CommRing A] [Algebra A S] {S' : Type u_7} [Ring S'] [Algebra A S'] (pb : PowerBasis A S) :
        (S →ₐ[A] S') { y // ↑(Polynomial.aeval y) (minpoly A pb.gen) = 0 }

        pb.liftEquiv states that roots of the minimal polynomial of pb.gen correspond to maps sending pb.gen to that root.

        This is the bundled equiv version of PowerBasis.lift. If the codomain of the AlgHoms is an integral domain, then the roots form a multiset, see liftEquiv' for the corresponding statement.

        Equations
        • One or more equations did not get rendered due to their size.
        Instances For
          @[simp]
          theorem PowerBasis.liftEquiv'_apply_coe {S : Type u_2} [Ring S] {A : Type u_4} {B : Type u_5} [CommRing A] [CommRing B] [IsDomain B] [Algebra A B] [Algebra A S] (pb : PowerBasis A S) :
          ∀ (a : S →ₐ[A] B), ↑(↑(PowerBasis.liftEquiv' pb) a) = a pb.gen
          @[simp]
          theorem PowerBasis.liftEquiv'_symm_apply_apply {S : Type u_2} [Ring S] {A : Type u_4} {B : Type u_5} [CommRing A] [CommRing B] [IsDomain B] [Algebra A B] [Algebra A S] (pb : PowerBasis A S) :
          ∀ (a : { y // y Polynomial.aroots (minpoly A pb.gen) B }), ↑((PowerBasis.liftEquiv' pb).symm a) = ↑(↑(Basis.constr pb.basis A) fun i => a ^ i)
          noncomputable def PowerBasis.liftEquiv' {S : Type u_2} [Ring S] {A : Type u_4} {B : Type u_5} [CommRing A] [CommRing B] [IsDomain B] [Algebra A B] [Algebra A S] (pb : PowerBasis A S) :
          (S →ₐ[A] B) { y // y Polynomial.aroots (minpoly A pb.gen) B }

          pb.liftEquiv' states that elements of the root set of the minimal polynomial of pb.gen correspond to maps sending pb.gen to that root.

          Equations
          • One or more equations did not get rendered due to their size.
          Instances For
            noncomputable def PowerBasis.AlgHom.fintype {S : Type u_2} [Ring S] {A : Type u_4} {B : Type u_5} [CommRing A] [CommRing B] [IsDomain B] [Algebra A B] [Algebra A S] (pb : PowerBasis A S) :

            There are finitely many algebra homomorphisms S →ₐ[A] B if S is of the form A[x] and B is an integral domain.

            Equations
            Instances For
              theorem PowerBasis.equivOfRoot_apply {S : Type u_2} [Ring S] {A : Type u_4} [CommRing A] [Algebra A S] {S' : Type u_7} [Ring S'] [Algebra A S'] (pb : PowerBasis A S) (pb' : PowerBasis A S') (h₁ : ↑(Polynomial.aeval pb.gen) (minpoly A pb'.gen) = 0) (h₂ : ↑(Polynomial.aeval pb'.gen) (minpoly A pb.gen) = 0) (a : S) :
              ↑(PowerBasis.equivOfRoot pb pb' h₁ h₂) a = ↑(PowerBasis.lift pb pb'.gen h₂) a
              noncomputable def PowerBasis.equivOfRoot {S : Type u_2} [Ring S] {A : Type u_4} [CommRing A] [Algebra A S] {S' : Type u_7} [Ring S'] [Algebra A S'] (pb : PowerBasis A S) (pb' : PowerBasis A S') (h₁ : ↑(Polynomial.aeval pb.gen) (minpoly A pb'.gen) = 0) (h₂ : ↑(Polynomial.aeval pb'.gen) (minpoly A pb.gen) = 0) :
              S ≃ₐ[A] S'

              pb.equivOfRoot pb' h₁ h₂ is an equivalence of algebras with the same power basis, where "the same" means that pb is a root of pb's minimal polynomial and vice versa.

              See also PowerBasis.equivOfMinpoly which takes the hypothesis that the minimal polynomials are identical.

              Equations
              • One or more equations did not get rendered due to their size.
              Instances For
                @[simp]
                theorem PowerBasis.equivOfRoot_aeval {S : Type u_2} [Ring S] {A : Type u_4} [CommRing A] [Algebra A S] {S' : Type u_7} [Ring S'] [Algebra A S'] (pb : PowerBasis A S) (pb' : PowerBasis A S') (h₁ : ↑(Polynomial.aeval pb.gen) (minpoly A pb'.gen) = 0) (h₂ : ↑(Polynomial.aeval pb'.gen) (minpoly A pb.gen) = 0) (f : Polynomial A) :
                ↑(PowerBasis.equivOfRoot pb pb' h₁ h₂) (↑(Polynomial.aeval pb.gen) f) = ↑(Polynomial.aeval pb'.gen) f
                @[simp]
                theorem PowerBasis.equivOfRoot_gen {S : Type u_2} [Ring S] {A : Type u_4} [CommRing A] [Algebra A S] {S' : Type u_7} [Ring S'] [Algebra A S'] (pb : PowerBasis A S) (pb' : PowerBasis A S') (h₁ : ↑(Polynomial.aeval pb.gen) (minpoly A pb'.gen) = 0) (h₂ : ↑(Polynomial.aeval pb'.gen) (minpoly A pb.gen) = 0) :
                ↑(PowerBasis.equivOfRoot pb pb' h₁ h₂) pb.gen = pb'.gen
                @[simp]
                theorem PowerBasis.equivOfRoot_symm {S : Type u_2} [Ring S] {A : Type u_4} [CommRing A] [Algebra A S] {S' : Type u_7} [Ring S'] [Algebra A S'] (pb : PowerBasis A S) (pb' : PowerBasis A S') (h₁ : ↑(Polynomial.aeval pb.gen) (minpoly A pb'.gen) = 0) (h₂ : ↑(Polynomial.aeval pb'.gen) (minpoly A pb.gen) = 0) :
                AlgEquiv.symm (PowerBasis.equivOfRoot pb pb' h₁ h₂) = PowerBasis.equivOfRoot pb' pb h₂ h₁
                theorem PowerBasis.equivOfMinpoly_apply {S : Type u_2} [Ring S] {A : Type u_4} [CommRing A] [Algebra A S] {S' : Type u_7} [Ring S'] [Algebra A S'] (pb : PowerBasis A S) (pb' : PowerBasis A S') (h : minpoly A pb.gen = minpoly A pb'.gen) (a : S) :
                ↑(PowerBasis.equivOfMinpoly pb pb' h) a = ↑(PowerBasis.lift pb pb'.gen (_ : ↑(Polynomial.aeval pb'.gen) (minpoly A pb.gen) = 0)) a
                noncomputable def PowerBasis.equivOfMinpoly {S : Type u_2} [Ring S] {A : Type u_4} [CommRing A] [Algebra A S] {S' : Type u_7} [Ring S'] [Algebra A S'] (pb : PowerBasis A S) (pb' : PowerBasis A S') (h : minpoly A pb.gen = minpoly A pb'.gen) :
                S ≃ₐ[A] S'

                pb.equivOfMinpoly pb' h is an equivalence of algebras with the same power basis, where "the same" means that they have identical minimal polynomials.

                See also PowerBasis.equivOfRoot which takes the hypothesis that each generator is a root of the other basis' minimal polynomial; PowerBasis.equivOfRoot is more general if A is not a field.

                Equations
                Instances For
                  @[simp]
                  theorem PowerBasis.equivOfMinpoly_aeval {S : Type u_2} [Ring S] {A : Type u_4} [CommRing A] [Algebra A S] {S' : Type u_7} [Ring S'] [Algebra A S'] (pb : PowerBasis A S) (pb' : PowerBasis A S') (h : minpoly A pb.gen = minpoly A pb'.gen) (f : Polynomial A) :
                  ↑(PowerBasis.equivOfMinpoly pb pb' h) (↑(Polynomial.aeval pb.gen) f) = ↑(Polynomial.aeval pb'.gen) f
                  @[simp]
                  theorem PowerBasis.equivOfMinpoly_gen {S : Type u_2} [Ring S] {A : Type u_4} [CommRing A] [Algebra A S] {S' : Type u_7} [Ring S'] [Algebra A S'] (pb : PowerBasis A S) (pb' : PowerBasis A S') (h : minpoly A pb.gen = minpoly A pb'.gen) :
                  ↑(PowerBasis.equivOfMinpoly pb pb' h) pb.gen = pb'.gen
                  @[simp]
                  theorem PowerBasis.equivOfMinpoly_symm {S : Type u_2} [Ring S] {A : Type u_4} [CommRing A] [Algebra A S] {S' : Type u_7} [Ring S'] [Algebra A S'] (pb : PowerBasis A S) (pb' : PowerBasis A S') (h : minpoly A pb.gen = minpoly A pb'.gen) :
                  theorem linearIndependent_pow {S : Type u_2} [Ring S] {K : Type u_6} [Field K] [Algebra K S] (x : S) :
                  LinearIndependent K fun i => x ^ i

                  Useful lemma to show x generates a power basis: the powers of x less than the degree of x's minimal polynomial are linearly independent.

                  theorem IsIntegral.mem_span_pow {R : Type u_1} {S : Type u_2} [CommRing R] [Ring S] [Algebra R S] [Nontrivial R] {x : S} {y : S} (hx : IsIntegral R x) (hy : f, y = ↑(Polynomial.aeval x) f) :
                  y Submodule.span R (Set.range fun i => x ^ i)
                  @[simp]
                  theorem PowerBasis.map_gen {R : Type u_1} {S : Type u_2} [CommRing R] [Ring S] [Algebra R S] {S' : Type u_7} [CommRing S'] [Algebra R S'] (pb : PowerBasis R S) (e : S ≃ₐ[R] S') :
                  (PowerBasis.map pb e).gen = e pb.gen
                  @[simp]
                  theorem PowerBasis.map_dim {R : Type u_1} {S : Type u_2} [CommRing R] [Ring S] [Algebra R S] {S' : Type u_7} [CommRing S'] [Algebra R S'] (pb : PowerBasis R S) (e : S ≃ₐ[R] S') :
                  (PowerBasis.map pb e).dim = pb.dim
                  @[simp]
                  theorem PowerBasis.map_basis {R : Type u_1} {S : Type u_2} [CommRing R] [Ring S] [Algebra R S] {S' : Type u_7} [CommRing S'] [Algebra R S'] (pb : PowerBasis R S) (e : S ≃ₐ[R] S') :
                  noncomputable def PowerBasis.map {R : Type u_1} {S : Type u_2} [CommRing R] [Ring S] [Algebra R S] {S' : Type u_7} [CommRing S'] [Algebra R S'] (pb : PowerBasis R S) (e : S ≃ₐ[R] S') :

                  PowerBasis.map pb (e : S ≃ₐ[R] S') is the power basis for S' generated by e pb.gen.

                  Equations
                  • One or more equations did not get rendered due to their size.
                  Instances For
                    theorem PowerBasis.minpolyGen_map {S : Type u_2} [Ring S] {A : Type u_4} [CommRing A] {S' : Type u_7} [CommRing S'] [Algebra A S] [Algebra A S'] (pb : PowerBasis A S) (e : S ≃ₐ[A] S') :
                    @[simp]
                    theorem PowerBasis.equivOfRoot_map {S : Type u_2} [Ring S] {A : Type u_4} [CommRing A] {S' : Type u_7} [CommRing S'] [Algebra A S] [Algebra A S'] (pb : PowerBasis A S) (e : S ≃ₐ[A] S') (h₁ : ↑(Polynomial.aeval pb.gen) (minpoly A (PowerBasis.map pb e).gen) = 0) (h₂ : ↑(Polynomial.aeval (PowerBasis.map pb e).gen) (minpoly A pb.gen) = 0) :
                    @[simp]
                    theorem PowerBasis.equivOfMinpoly_map {S : Type u_2} [Ring S] {A : Type u_4} [CommRing A] {S' : Type u_7} [CommRing S'] [Algebra A S] [Algebra A S'] (pb : PowerBasis A S) (e : S ≃ₐ[A] S') (h : minpoly A pb.gen = minpoly A (PowerBasis.map pb e).gen) :
                    theorem PowerBasis.adjoin_gen_eq_top {R : Type u_1} {S : Type u_2} [CommRing R] [Ring S] [Algebra R S] (B : PowerBasis R S) :
                    Algebra.adjoin R {B.gen} =
                    theorem PowerBasis.adjoin_eq_top_of_gen_mem_adjoin {R : Type u_1} {S : Type u_2} [CommRing R] [Ring S] [Algebra R S] {B : PowerBasis R S} {x : S} (hx : B.gen Algebra.adjoin R {x}) :