Documentation

Mathlib.RingTheory.IsAdjoinRoot

A predicate on adjoining roots of polynomial #

This file defines a predicate IsAdjoinRoot S f, which states that the ring S can be constructed by adjoining a specified root of the polynomial f : R[X] to R. This predicate is useful when the same ring can be generated by adjoining the root of different polynomials, and you want to vary which polynomial you're considering.

The results in this file are intended to mirror those in RingTheory.AdjoinRoot, in order to provide an easier way to translate results from one to the other.

Motivation #

AdjoinRoot presents one construction of a ring R[α]. However, it is possible to obtain rings of this form in many ways, such as NumberField.ringOfIntegers ℚ(√-5), or Algebra.adjoin R {α, α^2}, or IntermediateField.adjoin R {α, 2 - α}, or even if we want to view ℂ as adjoining a root of X^2 + 1 to ℝ.

Main definitions #

The two main predicates in this file are:

Using IsAdjoinRoot to map into S:

Using IsAdjoinRoot to map out of S:

Main results #

source
structure IsAdjoinRoot {R : Type u} (S : Type v) [CommSemiring R] [Semiring S] [Algebra R S] (f : Polynomial R) :
Type (max u v)

IsAdjoinRoot S f states that the ring S can be constructed by adjoining a specified root of the polynomial f : R[X] to R.

Compare PowerBasis R S, which does not explicitly specify which polynomial we adjoin a root of (in particular f does not need to be the minimal polynomial of the root we adjoin), and AdjoinRoot which constructs a new type.

This is not a typeclass because the choice of root given S and f is not unique.

Instances For
    source
    theorem IsAdjoinRoot.map_surjective {R : Type u} {S : Type v} [CommSemiring R] [Semiring S] [Algebra R S] {f : Polynomial R} (self : IsAdjoinRoot S f) :
    Function.Surjective ⇑self.map
    source
    theorem IsAdjoinRoot.ker_map {R : Type u} {S : Type v} [CommSemiring R] [Semiring S] [Algebra R S] {f : Polynomial R} (self : IsAdjoinRoot S f) :
    RingHom.ker self.map = Ideal.span {f}
    source
    theorem IsAdjoinRoot.algebraMap_eq {R : Type u} {S : Type v} [CommSemiring R] [Semiring S] [Algebra R S] {f : Polynomial R} (self : IsAdjoinRoot S f) :
    algebraMap R S = self.map.comp Polynomial.C
    source
    structure IsAdjoinRootMonic {R : Type u} (S : Type v) [CommSemiring R] [Semiring S] [Algebra R S] (f : Polynomial R) extends IsAdjoinRoot :
    Type (max u v)

    IsAdjoinRootMonic S f states that the ring S can be constructed by adjoining a specified root of the monic polynomial f : R[X] to R.

    As long as f is monic, there is a well-defined representation of elements of S as polynomials in R[X] of degree lower than deg f (see modByMonicHom and coeff). In particular, we have IsAdjoinRootMonic.powerBasis.

    Bundling Monic into this structure is very useful when working with explicit fs such as X^2 - C a * X - C b since it saves you carrying around the proofs of monicity.

    Instances For
      source
      theorem IsAdjoinRootMonic.Monic {R : Type u} {S : Type v} [CommSemiring R] [Semiring S] [Algebra R S] {f : Polynomial R} (self : IsAdjoinRootMonic S f) :
      f.Monic
      source
      def IsAdjoinRoot.root {R : Type u} {S : Type v} [CommRing R] [Ring S] {f : Polynomial R} [Algebra R S] (h : IsAdjoinRoot S f) :
      S

      (h : IsAdjoinRoot S f).root is the root of f that can be adjoined to generate S.

      Equations
      • h.root = h.map Polynomial.X
      Instances For
        source
        theorem IsAdjoinRoot.subsingleton {R : Type u} {S : Type v} [CommRing R] [Ring S] {f : Polynomial R} [Algebra R S] (h : IsAdjoinRoot S f) [Subsingleton R] :
        Subsingleton S
        source
        theorem IsAdjoinRoot.algebraMap_apply {R : Type u} {S : Type v} [CommRing R] [Ring S] {f : Polynomial R} [Algebra R S] (h : IsAdjoinRoot S f) (x : R) :
        (algebraMap R S) x = h.map (Polynomial.C x)
        source
        @[simp]
        theorem IsAdjoinRoot.mem_ker_map {R : Type u} {S : Type v} [CommRing R] [Ring S] {f : Polynomial R} [Algebra R S] (h : IsAdjoinRoot S f) {p : Polynomial R} :
        p ∈ RingHom.ker h.map ↔ f ∣ p
        source
        theorem IsAdjoinRoot.map_eq_zero_iff {R : Type u} {S : Type v} [CommRing R] [Ring S] {f : Polynomial R} [Algebra R S] (h : IsAdjoinRoot S f) {p : Polynomial R} :
        h.map p = 0 ↔ f ∣ p
        source
        @[simp]
        theorem IsAdjoinRoot.map_X {R : Type u} {S : Type v} [CommRing R] [Ring S] {f : Polynomial R} [Algebra R S] (h : IsAdjoinRoot S f) :
        h.map Polynomial.X = h.root
        source
        @[simp]
        theorem IsAdjoinRoot.map_self {R : Type u} {S : Type v} [CommRing R] [Ring S] {f : Polynomial R} [Algebra R S] (h : IsAdjoinRoot S f) :
        h.map f = 0
        source
        @[simp]
        theorem IsAdjoinRoot.aeval_eq {R : Type u} {S : Type v} [CommRing R] [Ring S] {f : Polynomial R} [Algebra R S] (h : IsAdjoinRoot S f) (p : Polynomial R) :
        (Polynomial.aeval h.root) p = h.map p
        source
        theorem IsAdjoinRoot.aeval_root {R : Type u} {S : Type v} [CommRing R] [Ring S] {f : Polynomial R} [Algebra R S] (h : IsAdjoinRoot S f) :
        (Polynomial.aeval h.root) f = 0
        source
        def IsAdjoinRoot.repr {R : Type u} {S : Type v} [CommRing R] [Ring S] {f : Polynomial R} [Algebra R S] (h : IsAdjoinRoot S f) (x : S) :
        Polynomial R

        Choose an arbitrary representative so that h.map (h.repr x) = x.

        If f is monic, use IsAdjoinRootMonic.modByMonicHom for a unique choice of representative.

        Equations
        • h.repr x = ⋯.choose
        Instances For
          source
          theorem IsAdjoinRoot.map_repr {R : Type u} {S : Type v} [CommRing R] [Ring S] {f : Polynomial R} [Algebra R S] (h : IsAdjoinRoot S f) (x : S) :
          h.map (h.repr x) = x
          source
          theorem IsAdjoinRoot.repr_zero_mem_span {R : Type u} {S : Type v} [CommRing R] [Ring S] {f : Polynomial R} [Algebra R S] (h : IsAdjoinRoot S f) :
          h.repr 0 ∈ Ideal.span {f}

          repr preserves zero, up to multiples of f

          source
          theorem IsAdjoinRoot.repr_add_sub_repr_add_repr_mem_span {R : Type u} {S : Type v} [CommRing R] [Ring S] {f : Polynomial R} [Algebra R S] (h : IsAdjoinRoot S f) (x : S) (y : S) :
          h.repr (x + y) - (h.repr x + h.repr y) ∈ Ideal.span {f}

          repr preserves addition, up to multiples of f

          source
          theorem IsAdjoinRoot.ext_map {R : Type u} {S : Type v} [CommRing R] [Ring S] {f : Polynomial R} [Algebra R S] (h : IsAdjoinRoot S f) (h' : IsAdjoinRoot S f) (eq : ∀ (x : Polynomial R), h.map x = h'.map x) :
          h = h'

          Extensionality of the IsAdjoinRoot structure itself. See IsAdjoinRootMonic.ext_elem for extensionality of the ring elements.

          source
          theorem IsAdjoinRoot.ext {R : Type u} {S : Type v} [CommRing R] [Ring S] {f : Polynomial R} [Algebra R S] (h : IsAdjoinRoot S f) (h' : IsAdjoinRoot S f) (eq : h.root = h'.root) :
          h = h'

          Extensionality of the IsAdjoinRoot structure itself. See IsAdjoinRootMonic.ext_elem for extensionality of the ring elements.

          source
          theorem IsAdjoinRoot.eval₂_repr_eq_eval₂_of_map_eq {R : Type u} {S : Type v} [CommRing R] [Ring S] {f : Polynomial R} [Algebra R S] {T : Type u_1} [CommRing T] {i : R →+* T} {x : T} (hx : Polynomial.eval₂ i x f = 0) (h : IsAdjoinRoot S f) (z : S) (w : Polynomial R) (hzw : h.map w = z) :
          Polynomial.eval₂ i x (h.repr z) = Polynomial.eval₂ i x w

          Auxiliary lemma for IsAdjoinRoot.lift

          source
          def IsAdjoinRoot.lift {R : Type u} {S : Type v} [CommRing R] [Ring S] {f : Polynomial R} [Algebra R S] {T : Type u_1} [CommRing T] (i : R →+* T) (x : T) (hx : Polynomial.eval₂ i x f = 0) (h : IsAdjoinRoot S f) :
          S →+* T

          Lift a ring homomorphism R →+* T to S →+* T by specifying a root x of f in T, where S is given by adjoining a root of f to R.

          Equations
          Instances For
            source
            @[simp]
            theorem IsAdjoinRoot.lift_map {R : Type u} {S : Type v} [CommRing R] [Ring S] {f : Polynomial R} [Algebra R S] {T : Type u_1} [CommRing T] {i : R →+* T} {x : T} (hx : Polynomial.eval₂ i x f = 0) (h : IsAdjoinRoot S f) (z : Polynomial R) :
            (IsAdjoinRoot.lift i x hx h) (h.map z) = Polynomial.eval₂ i x z
            source
            @[simp]
            theorem IsAdjoinRoot.lift_root {R : Type u} {S : Type v} [CommRing R] [Ring S] {f : Polynomial R} [Algebra R S] {T : Type u_1} [CommRing T] {i : R →+* T} {x : T} (hx : Polynomial.eval₂ i x f = 0) (h : IsAdjoinRoot S f) :
            (IsAdjoinRoot.lift i x hx h) h.root = x
            source
            @[simp]
            theorem IsAdjoinRoot.lift_algebraMap {R : Type u} {S : Type v} [CommRing R] [Ring S] {f : Polynomial R} [Algebra R S] {T : Type u_1} [CommRing T] {i : R →+* T} {x : T} (hx : Polynomial.eval₂ i x f = 0) (h : IsAdjoinRoot S f) (a : R) :
            (IsAdjoinRoot.lift i x hx h) ((algebraMap R S) a) = i a
            source
            theorem IsAdjoinRoot.apply_eq_lift {R : Type u} {S : Type v} [CommRing R] [Ring S] {f : Polynomial R} [Algebra R S] {T : Type u_1} [CommRing T] {i : R →+* T} {x : T} (hx : Polynomial.eval₂ i x f = 0) (h : IsAdjoinRoot S f) (g : S →+* T) (hmap : ∀ (a : R), g ((algebraMap R S) a) = i a) (hroot : g h.root = x) (a : S) :
            g a = (IsAdjoinRoot.lift i x hx h) a

            Auxiliary lemma for apply_eq_lift

            source
            theorem IsAdjoinRoot.eq_lift {R : Type u} {S : Type v} [CommRing R] [Ring S] {f : Polynomial R} [Algebra R S] {T : Type u_1} [CommRing T] {i : R →+* T} {x : T} (hx : Polynomial.eval₂ i x f = 0) (h : IsAdjoinRoot S f) (g : S →+* T) (hmap : ∀ (a : R), g ((algebraMap R S) a) = i a) (hroot : g h.root = x) :
            g = IsAdjoinRoot.lift i x hx h

            Unicity of lift: a map that agrees on R and h.root agrees with lift everywhere.

            source
            def IsAdjoinRoot.liftHom {R : Type u} {S : Type v} [CommRing R] [Ring S] {f : Polynomial R} [Algebra R S] {T : Type u_1} [CommRing T] (x : T) [Algebra R T] (hx' : (Polynomial.aeval x) f = 0) (h : IsAdjoinRoot S f) :
            S →ₐ[R] T

            Lift the algebra map R → T to S →ₐ[R] T by specifying a root x of f in T, where S is given by adjoining a root of f to R.

            Equations
            Instances For
              source
              @[simp]
              theorem IsAdjoinRoot.coe_liftHom {R : Type u} {S : Type v} [CommRing R] [Ring S] {f : Polynomial R} [Algebra R S] {T : Type u_1} [CommRing T] {x : T} [Algebra R T] (hx' : (Polynomial.aeval x) f = 0) (h : IsAdjoinRoot S f) :
              ↑(IsAdjoinRoot.liftHom x hx' h) = IsAdjoinRoot.lift (algebraMap R T) x hx' h
              source
              theorem IsAdjoinRoot.lift_algebraMap_apply {R : Type u} {S : Type v} [CommRing R] [Ring S] {f : Polynomial R} [Algebra R S] {T : Type u_1} [CommRing T] {x : T} [Algebra R T] (hx' : (Polynomial.aeval x) f = 0) (h : IsAdjoinRoot S f) (z : S) :
              (IsAdjoinRoot.lift (algebraMap R T) x hx' h) z = (IsAdjoinRoot.liftHom x hx' h) z
              source
              @[simp]
              theorem IsAdjoinRoot.liftHom_map {R : Type u} {S : Type v} [CommRing R] [Ring S] {f : Polynomial R} [Algebra R S] {T : Type u_1} [CommRing T] {x : T} [Algebra R T] (hx' : (Polynomial.aeval x) f = 0) (h : IsAdjoinRoot S f) (z : Polynomial R) :
              (IsAdjoinRoot.liftHom x hx' h) (h.map z) = (Polynomial.aeval x) z
              source
              @[simp]
              theorem IsAdjoinRoot.liftHom_root {R : Type u} {S : Type v} [CommRing R] [Ring S] {f : Polynomial R} [Algebra R S] {T : Type u_1} [CommRing T] {x : T} [Algebra R T] (hx' : (Polynomial.aeval x) f = 0) (h : IsAdjoinRoot S f) :
              (IsAdjoinRoot.liftHom x hx' h) h.root = x
              source
              theorem IsAdjoinRoot.eq_liftHom {R : Type u} {S : Type v} [CommRing R] [Ring S] {f : Polynomial R} [Algebra R S] {T : Type u_1} [CommRing T] {x : T} [Algebra R T] (hx' : (Polynomial.aeval x) f = 0) (h : IsAdjoinRoot S f) (g : S →ₐ[R] T) (hroot : g h.root = x) :
              g = IsAdjoinRoot.liftHom x hx' h

              Unicity of liftHom: a map that agrees on h.root agrees with liftHom everywhere.

              source
              def AdjoinRoot.isAdjoinRoot {R : Type u} [CommRing R] (f : Polynomial R) :
              IsAdjoinRoot (AdjoinRoot f) f

              AdjoinRoot f is indeed given by adjoining a root of f.

              Equations
              Instances For
                source
                def AdjoinRoot.isAdjoinRootMonic {R : Type u} [CommRing R] (f : Polynomial R) (hf : f.Monic) :
                IsAdjoinRootMonic (AdjoinRoot f) f

                AdjoinRoot f is indeed given by adjoining a root of f. If f is monic this is more powerful than AdjoinRoot.isAdjoinRoot.

                Equations
                Instances For
                  source
                  @[simp]
                  theorem AdjoinRoot.isAdjoinRoot_map_eq_mk {R : Type u} [CommRing R] (f : Polynomial R) :
                  (AdjoinRoot.isAdjoinRoot f).map = AdjoinRoot.mk f
                  source
                  @[simp]
                  theorem AdjoinRoot.isAdjoinRootMonic_map_eq_mk {R : Type u} [CommRing R] (f : Polynomial R) (hf : f.Monic) :
                  (AdjoinRoot.isAdjoinRootMonic f hf).map = AdjoinRoot.mk f
                  source
                  @[simp]
                  theorem AdjoinRoot.isAdjoinRoot_root_eq_root {R : Type u} [CommRing R] (f : Polynomial R) :
                  (AdjoinRoot.isAdjoinRoot f).root = AdjoinRoot.root f
                  source
                  @[simp]
                  theorem AdjoinRoot.isAdjoinRootMonic_root_eq_root {R : Type u} [CommRing R] (f : Polynomial R) (hf : f.Monic) :
                  (AdjoinRoot.isAdjoinRootMonic f hf).root = AdjoinRoot.root f
                  source
                  theorem IsAdjoinRootMonic.map_modByMonic {R : Type u} {S : Type v} [CommRing R] [Ring S] {f : Polynomial R} [Algebra R S] (h : IsAdjoinRootMonic S f) (g : Polynomial R) :
                  h.map (g %ₘ f) = h.map g
                  source
                  theorem IsAdjoinRootMonic.modByMonic_repr_map {R : Type u} {S : Type v} [CommRing R] [Ring S] {f : Polynomial R} [Algebra R S] (h : IsAdjoinRootMonic S f) (g : Polynomial R) :
                  h.repr (h.map g) %ₘ f = g %ₘ f
                  source
                  def IsAdjoinRootMonic.modByMonicHom {R : Type u} {S : Type v} [CommRing R] [Ring S] {f : Polynomial R} [Algebra R S] (h : IsAdjoinRootMonic S f) :
                  S →ₗ[R] Polynomial R

                  IsAdjoinRoot.modByMonicHom sends the equivalence class of f mod g to f %ₘ g.

                  Equations
                  • h.modByMonicHom = { toFun := fun (x : S) => h.repr x %ₘ f, map_add' := ⋯, map_smul' := ⋯ }
                  Instances For
                    source
                    @[simp]
                    theorem IsAdjoinRootMonic.modByMonicHom_map {R : Type u} {S : Type v} [CommRing R] [Ring S] {f : Polynomial R} [Algebra R S] (h : IsAdjoinRootMonic S f) (g : Polynomial R) :
                    h.modByMonicHom (h.map g) = g %ₘ f
                    source
                    @[simp]
                    theorem IsAdjoinRootMonic.map_modByMonicHom {R : Type u} {S : Type v} [CommRing R] [Ring S] {f : Polynomial R} [Algebra R S] (h : IsAdjoinRootMonic S f) (x : S) :
                    h.map (h.modByMonicHom x) = x
                    source
                    @[simp]
                    theorem IsAdjoinRootMonic.modByMonicHom_root_pow {R : Type u} {S : Type v} [CommRing R] [Ring S] {f : Polynomial R} [Algebra R S] (h : IsAdjoinRootMonic S f) {n : ℕ} (hdeg : n < f.natDegree) :
                    h.modByMonicHom (h.root ^ n) = Polynomial.X ^ n
                    source
                    @[simp]
                    theorem IsAdjoinRootMonic.modByMonicHom_root {R : Type u} {S : Type v} [CommRing R] [Ring S] {f : Polynomial R} [Algebra R S] (h : IsAdjoinRootMonic S f) (hdeg : 1 < f.natDegree) :
                    h.modByMonicHom h.root = Polynomial.X
                    source
                    def IsAdjoinRootMonic.basis {R : Type u} {S : Type v} [CommRing R] [Ring S] {f : Polynomial R} [Algebra R S] (h : IsAdjoinRootMonic S f) :
                    Basis (Fin f.natDegree) R S

                    The basis on S generated by powers of h.root.

                    Auxiliary definition for IsAdjoinRootMonic.powerBasis.

                    Equations
                    • One or more equations did not get rendered due to their size.
                    Instances For
                      source
                      @[simp]
                      theorem IsAdjoinRootMonic.basis_apply {R : Type u} {S : Type v} [CommRing R] [Ring S] {f : Polynomial R} [Algebra R S] (h : IsAdjoinRootMonic S f) (i : Fin f.natDegree) :
                      h.basis i = h.root ^ ↑i
                      source
                      theorem IsAdjoinRootMonic.deg_pos {R : Type u} {S : Type v} [CommRing R] [Ring S] {f : Polynomial R} [Algebra R S] [Nontrivial S] (h : IsAdjoinRootMonic S f) :
                      0 < f.natDegree
                      source
                      theorem IsAdjoinRootMonic.deg_ne_zero {R : Type u} {S : Type v} [CommRing R] [Ring S] {f : Polynomial R} [Algebra R S] [Nontrivial S] (h : IsAdjoinRootMonic S f) :
                      f.natDegree ≠ 0
                      source
                      @[simp]
                      theorem IsAdjoinRootMonic.powerBasis_dim {R : Type u} {S : Type v} [CommRing R] [Ring S] {f : Polynomial R} [Algebra R S] (h : IsAdjoinRootMonic S f) :
                      h.powerBasis.dim = f.natDegree
                      source
                      @[simp]
                      theorem IsAdjoinRootMonic.powerBasis_gen {R : Type u} {S : Type v} [CommRing R] [Ring S] {f : Polynomial R} [Algebra R S] (h : IsAdjoinRootMonic S f) :
                      h.powerBasis.gen = h.root
                      source
                      @[simp]
                      theorem IsAdjoinRootMonic.powerBasis_basis {R : Type u} {S : Type v} [CommRing R] [Ring S] {f : Polynomial R} [Algebra R S] (h : IsAdjoinRootMonic S f) :
                      h.powerBasis.basis = h.basis
                      source
                      def IsAdjoinRootMonic.powerBasis {R : Type u} {S : Type v} [CommRing R] [Ring S] {f : Polynomial R} [Algebra R S] (h : IsAdjoinRootMonic S f) :
                      PowerBasis R S

                      If f is monic, the powers of h.root form a basis.

                      Equations
                      • h.powerBasis = { gen := h.root, dim := f.natDegree, basis := h.basis, basis_eq_pow := ⋯ }
                      Instances For
                        source
                        @[simp]
                        theorem IsAdjoinRootMonic.basis_repr {R : Type u} {S : Type v} [CommRing R] [Ring S] {f : Polynomial R} [Algebra R S] (h : IsAdjoinRootMonic S f) (x : S) (i : Fin f.natDegree) :
                        (h.basis.repr x) i = (h.modByMonicHom x).coeff ↑i
                        source
                        theorem IsAdjoinRootMonic.basis_one {R : Type u} {S : Type v} [CommRing R] [Ring S] {f : Polynomial R} [Algebra R S] (h : IsAdjoinRootMonic S f) (hdeg : 1 < f.natDegree) :
                        h.basis ⟨1, hdeg⟩ = h.root
                        source
                        @[simp]
                        theorem IsAdjoinRootMonic.liftPolyₗ_apply {R : Type u} {S : Type v} [CommRing R] [Ring S] {f : Polynomial R} [Algebra R S] {T : Type u_1} [AddCommGroup T] [Module R T] (h : IsAdjoinRootMonic S f) (g : Polynomial R →ₗ[R] T) :
                        ∀ (a : S), (h.liftPolyₗ g) a = g (h.modByMonicHom a)
                        source
                        def IsAdjoinRootMonic.liftPolyₗ {R : Type u} {S : Type v} [CommRing R] [Ring S] {f : Polynomial R} [Algebra R S] {T : Type u_1} [AddCommGroup T] [Module R T] (h : IsAdjoinRootMonic S f) (g : Polynomial R →ₗ[R] T) :
                        S →ₗ[R] T

                        IsAdjoinRootMonic.liftPolyₗ lifts a linear map on polynomials to a linear map on S.

                        Equations
                        • h.liftPolyₗ g = g ∘ₗ h.modByMonicHom
                        Instances For
                          source
                          def IsAdjoinRootMonic.coeff {R : Type u} {S : Type v} [CommRing R] [Ring S] {f : Polynomial R} [Algebra R S] (h : IsAdjoinRootMonic S f) :
                          S →ₗ[R] ℕ → R

                          IsAdjoinRootMonic.coeff h x i is the ith coefficient of the representative of x : S.

                          Equations
                          • h.coeff = h.liftPolyₗ { toFun := Polynomial.coeff, map_add' := ⋯, map_smul' := ⋯ }
                          Instances For
                            source
                            theorem IsAdjoinRootMonic.coeff_apply_lt {R : Type u} {S : Type v} [CommRing R] [Ring S] {f : Polynomial R} [Algebra R S] (h : IsAdjoinRootMonic S f) (z : S) (i : ℕ) (hi : i < f.natDegree) :
                            h.coeff z i = (h.basis.repr z) ⟨i, hi⟩
                            source
                            theorem IsAdjoinRootMonic.coeff_apply_coe {R : Type u} {S : Type v} [CommRing R] [Ring S] {f : Polynomial R} [Algebra R S] (h : IsAdjoinRootMonic S f) (z : S) (i : Fin f.natDegree) :
                            h.coeff z ↑i = (h.basis.repr z) i
                            source
                            theorem IsAdjoinRootMonic.coeff_apply_le {R : Type u} {S : Type v} [CommRing R] [Ring S] {f : Polynomial R} [Algebra R S] (h : IsAdjoinRootMonic S f) (z : S) (i : ℕ) (hi : f.natDegree ≤ i) :
                            h.coeff z i = 0
                            source
                            theorem IsAdjoinRootMonic.coeff_apply {R : Type u} {S : Type v} [CommRing R] [Ring S] {f : Polynomial R} [Algebra R S] (h : IsAdjoinRootMonic S f) (z : S) (i : ℕ) :
                            h.coeff z i = if hi : i < f.natDegree then (h.basis.repr z) ⟨i, hi⟩ else 0
                            source
                            theorem IsAdjoinRootMonic.coeff_root_pow {R : Type u} {S : Type v} [CommRing R] [Ring S] {f : Polynomial R} [Algebra R S] (h : IsAdjoinRootMonic S f) {n : ℕ} (hn : n < f.natDegree) :
                            h.coeff (h.root ^ n) = Pi.single n 1
                            source
                            theorem IsAdjoinRootMonic.coeff_one {R : Type u} {S : Type v} [CommRing R] [Ring S] {f : Polynomial R} [Algebra R S] [Nontrivial S] (h : IsAdjoinRootMonic S f) :
                            h.coeff 1 = Pi.single 0 1
                            source
                            theorem IsAdjoinRootMonic.coeff_root {R : Type u} {S : Type v} [CommRing R] [Ring S] {f : Polynomial R} [Algebra R S] (h : IsAdjoinRootMonic S f) (hdeg : 1 < f.natDegree) :
                            h.coeff h.root = Pi.single 1 1
                            source
                            theorem IsAdjoinRootMonic.coeff_algebraMap {R : Type u} {S : Type v} [CommRing R] [Ring S] {f : Polynomial R} [Algebra R S] [Nontrivial S] (h : IsAdjoinRootMonic S f) (x : R) :
                            h.coeff ((algebraMap R S) x) = Pi.single 0 x
                            source
                            theorem IsAdjoinRootMonic.ext_elem {R : Type u} {S : Type v} [CommRing R] [Ring S] {f : Polynomial R} [Algebra R S] (h : IsAdjoinRootMonic S f) ⦃x : S⦄ ⦃y : S⦄ (hxy : ∀ i < f.natDegree, h.coeff x i = h.coeff y i) :
                            x = y
                            source
                            theorem IsAdjoinRootMonic.ext_elem_iff {R : Type u} {S : Type v} [CommRing R] [Ring S] {f : Polynomial R} [Algebra R S] (h : IsAdjoinRootMonic S f) {x : S} {y : S} :
                            x = y ↔ ∀ i < f.natDegree, h.coeff x i = h.coeff y i
                            source
                            theorem IsAdjoinRootMonic.coeff_injective {R : Type u} {S : Type v} [CommRing R] [Ring S] {f : Polynomial R} [Algebra R S] (h : IsAdjoinRootMonic S f) :
                            Function.Injective ⇑h.coeff
                            source
                            theorem IsAdjoinRootMonic.isIntegral_root {R : Type u} {S : Type v} [CommRing R] [Ring S] {f : Polynomial R} [Algebra R S] (h : IsAdjoinRootMonic S f) :
                            IsIntegral R h.root
                            source
                            @[simp]
                            theorem IsAdjoinRoot.lift_self_apply {R : Type u} {S : Type v} [CommRing R] [CommRing S] [Algebra R S] {f : Polynomial R} (h : IsAdjoinRoot S f) (x : S) :
                            (IsAdjoinRoot.lift (algebraMap R S) h.root ⋯ h) x = x
                            source
                            theorem IsAdjoinRoot.lift_self {R : Type u} {S : Type v} [CommRing R] [CommRing S] [Algebra R S] {f : Polynomial R} (h : IsAdjoinRoot S f) :
                            IsAdjoinRoot.lift (algebraMap R S) h.root ⋯ h = RingHom.id S
                            source
                            def IsAdjoinRoot.aequiv {R : Type u} {S : Type v} [CommRing R] [CommRing S] [Algebra R S] {f : Polynomial R} {T : Type u_1} [CommRing T] [Algebra R T] (h : IsAdjoinRoot S f) (h' : IsAdjoinRoot T f) :
                            S ≃ₐ[R] T

                            Adjoining a root gives a unique ring up to algebra isomorphism.

                            This is the converse of IsAdjoinRoot.ofEquiv: this turns an IsAdjoinRoot into an AlgEquiv, and IsAdjoinRoot.ofEquiv turns an AlgEquiv into an IsAdjoinRoot.

                            Equations
                            • One or more equations did not get rendered due to their size.
                            Instances For
                              source
                              @[simp]
                              theorem IsAdjoinRoot.aequiv_map {R : Type u} {S : Type v} [CommRing R] [CommRing S] [Algebra R S] {f : Polynomial R} {T : Type u_1} [CommRing T] [Algebra R T] (h : IsAdjoinRoot S f) (h' : IsAdjoinRoot T f) (z : Polynomial R) :
                              (h.aequiv h') (h.map z) = h'.map z
                              source
                              @[simp]
                              theorem IsAdjoinRoot.aequiv_root {R : Type u} {S : Type v} [CommRing R] [CommRing S] [Algebra R S] {f : Polynomial R} {T : Type u_1} [CommRing T] [Algebra R T] (h : IsAdjoinRoot S f) (h' : IsAdjoinRoot T f) :
                              (h.aequiv h') h.root = h'.root
                              source
                              @[simp]
                              theorem IsAdjoinRoot.aequiv_self {R : Type u} {S : Type v} [CommRing R] [CommRing S] [Algebra R S] {f : Polynomial R} (h : IsAdjoinRoot S f) :
                              h.aequiv h = AlgEquiv.refl
                              source
                              @[simp]
                              theorem IsAdjoinRoot.aequiv_symm {R : Type u} {S : Type v} [CommRing R] [CommRing S] [Algebra R S] {f : Polynomial R} {T : Type u_1} [CommRing T] [Algebra R T] (h : IsAdjoinRoot S f) (h' : IsAdjoinRoot T f) :
                              (h.aequiv h').symm = h'.aequiv h
                              source
                              @[simp]
                              theorem IsAdjoinRoot.lift_aequiv {R : Type u} {S : Type v} [CommRing R] [CommRing S] [Algebra R S] {f : Polynomial R} {T : Type u_1} [CommRing T] [Algebra R T] {U : Type u_2} [CommRing U] (h : IsAdjoinRoot S f) (h' : IsAdjoinRoot T f) (i : R →+* U) (x : U) (hx : Polynomial.eval₂ i x f = 0) (z : S) :
                              (IsAdjoinRoot.lift i x hx h') ((h.aequiv h') z) = (IsAdjoinRoot.lift i x hx h) z
                              source
                              @[simp]
                              theorem IsAdjoinRoot.liftHom_aequiv {R : Type u} {S : Type v} [CommRing R] [CommRing S] [Algebra R S] {f : Polynomial R} {T : Type u_1} [CommRing T] [Algebra R T] {U : Type u_2} [CommRing U] [Algebra R U] (h : IsAdjoinRoot S f) (h' : IsAdjoinRoot T f) (x : U) (hx : (Polynomial.aeval x) f = 0) (z : S) :
                              (IsAdjoinRoot.liftHom x hx h') ((h.aequiv h') z) = (IsAdjoinRoot.liftHom x hx h) z
                              source
                              @[simp]
                              theorem IsAdjoinRoot.aequiv_aequiv {R : Type u} {S : Type v} [CommRing R] [CommRing S] [Algebra R S] {f : Polynomial R} {T : Type u_1} [CommRing T] [Algebra R T] {U : Type u_2} [CommRing U] [Algebra R U] (h : IsAdjoinRoot S f) (h' : IsAdjoinRoot T f) (h'' : IsAdjoinRoot U f) (x : S) :
                              (h'.aequiv h'') ((h.aequiv h') x) = (h.aequiv h'') x
                              source
                              @[simp]
                              theorem IsAdjoinRoot.aequiv_trans {R : Type u} {S : Type v} [CommRing R] [CommRing S] [Algebra R S] {f : Polynomial R} {T : Type u_1} [CommRing T] [Algebra R T] {U : Type u_2} [CommRing U] [Algebra R U] (h : IsAdjoinRoot S f) (h' : IsAdjoinRoot T f) (h'' : IsAdjoinRoot U f) :
                              (h.aequiv h').trans (h'.aequiv h'') = h.aequiv h''
                              source
                              @[simp]
                              theorem IsAdjoinRoot.ofEquiv_map_apply {R : Type u} {S : Type v} [CommRing R] [CommRing S] [Algebra R S] {f : Polynomial R} {T : Type u_1} [CommRing T] [Algebra R T] (h : IsAdjoinRoot S f) (e : S ≃ₐ[R] T) :
                              ∀ (a : Polynomial R), (h.ofEquiv e).map a = e (h.map a)
                              source
                              def IsAdjoinRoot.ofEquiv {R : Type u} {S : Type v} [CommRing R] [CommRing S] [Algebra R S] {f : Polynomial R} {T : Type u_1} [CommRing T] [Algebra R T] (h : IsAdjoinRoot S f) (e : S ≃ₐ[R] T) :
                              IsAdjoinRoot T f

                              Transfer IsAdjoinRoot across an algebra isomorphism.

                              This is the converse of IsAdjoinRoot.aequiv: this turns an AlgEquiv into an IsAdjoinRoot, and IsAdjoinRoot.aequiv turns an IsAdjoinRoot into an AlgEquiv.

                              Equations
                              • h.ofEquiv e = { map := (↑↑e).comp h.map, map_surjective := ⋯, ker_map := ⋯, algebraMap_eq := ⋯ }
                              Instances For
                                source
                                @[simp]
                                theorem IsAdjoinRoot.ofEquiv_root {R : Type u} {S : Type v} [CommRing R] [CommRing S] [Algebra R S] {f : Polynomial R} {T : Type u_1} [CommRing T] [Algebra R T] (h : IsAdjoinRoot S f) (e : S ≃ₐ[R] T) :
                                (h.ofEquiv e).root = e h.root
                                source
                                @[simp]
                                theorem IsAdjoinRoot.aequiv_ofEquiv {R : Type u} {S : Type v} [CommRing R] [CommRing S] [Algebra R S] {f : Polynomial R} {T : Type u_1} [CommRing T] [Algebra R T] {U : Type u_2} [CommRing U] [Algebra R U] (h : IsAdjoinRoot S f) (h' : IsAdjoinRoot T f) (e : T ≃ₐ[R] U) :
                                h.aequiv (h'.ofEquiv e) = (h.aequiv h').trans e
                                source
                                @[simp]
                                theorem IsAdjoinRoot.ofEquiv_aequiv {R : Type u} {S : Type v} [CommRing R] [CommRing S] [Algebra R S] {f : Polynomial R} {T : Type u_1} [CommRing T] [Algebra R T] {U : Type u_2} [CommRing U] [Algebra R U] (h : IsAdjoinRoot S f) (h' : IsAdjoinRoot U f) (e : S ≃ₐ[R] T) :
                                (h.ofEquiv e).aequiv h' = e.symm.trans (h.aequiv h')
                                source
                                theorem IsAdjoinRootMonic.minpoly_eq {R : Type u} {S : Type v} [CommRing R] [CommRing S] [Algebra R S] {f : Polynomial R} [IsDomain R] [IsDomain S] [NoZeroSMulDivisors R S] [IsIntegrallyClosed R] (h : IsAdjoinRootMonic S f) (hirr : Irreducible f) :
                                minpoly R h.root = f
                                source
                                theorem Algebra.adjoin.powerBasis'_minpoly_gen {R : Type u} {S : Type v} [CommRing R] [CommRing S] [Algebra R S] [IsDomain R] [IsDomain S] [NoZeroSMulDivisors R S] [IsIntegrallyClosed R] {x : S} (hx' : IsIntegral R x) :
                                minpoly R x = minpoly R (Algebra.adjoin.powerBasis' hx').gen