TITLE: Problem in the Big O notation
QUESTION [0 upvotes]: I have this expression $$ e^{\alpha(x,y)y} -1$$ where $\alpha(x,y)$ is a smoooth function of two variables and is bounded on $\mathbb{R^2}$.

As $y \rightarrow 0$, can I write
$$ e^{\alpha(x,y)y} -1 = O\big(\alpha(x,y)y\big) \quad ?$$

Since $\alpha(x,y)y$ is bounded, can I simply write
$$ e^{\alpha(x,y)y} -1 =O(y) \quad ?$$

If 2) is true, I can  conclude that in a neighborhood of $y=0$
$$ \big| e^{\alpha(x,y)y} -1 \big| \leq A |y|, $$
where $A$ is independent from both $x$ and $y$, right?

REPLY [1 votes]: We have definition that $O(g),x \to x_0$ is set of functions $$\left\lbrace f: \exists C_f>0, \ \exists \delta>0, \forall x, 0< |x-x_0|<\delta \Rightarrow  |f(x)| \leqslant C_f |g(x)\right\rbrace$$.
In your case, taking as variable $y$,  and considering $g(y)=\alpha(x,y)y$ we have: if $\alpha$ is bounded, i.e. $\alpha(x,y) < A$, then $f \in O(g)\Rightarrow  f \in O(y)$, which gives your 2. and 3.


text:
:: On Roots of Polynomials over K[X]/<p>
::  by Christoph Schwarzweller

environ

 vocabularies ARYTM_3, VECTSP_1, ALGSTR_0, TARSKI, GROUP_6, NAT_1, MESFUNC1,
      VECTSP_2, STRUCT_0, SUBSET_1, SUPINF_2, GROUP_1, POLYNOM1, POLYNOM2,
      POLYNOM3, FUNCSDOM, HURWITZ, FINSEQ_1, QUOFIELD, ALGSEQ_1, FUNCT_1,
      RELAT_1, CARD_1, POLYNOM8, IDEAL_1, MOD_4, XBOOLE_0, NUMBERS, MSSUBFAM,
      CARD_3, POLYNOM5, YELLOW_8, WAYBEL20, EQREL_1, RING_2, RLVECT_1, RING_3,
      AFINSQ_1, FUNCT_2, PARTFUN1, XXREAL_0, XCMPLX_0, ORDINAL4, POLYNOM4,
      RATFUNC1, CARD_FIL, NEWTON, ARYTM_1, CALCUL_2, FIELD_1;
 notations TARSKI, XBOOLE_0, SUBSET_1, RELAT_1, FUNCT_1, RELSET_1, PARTFUN1,
      FUNCT_2, BINOP_1, FINSEQ_1, EQREL_1, ORDINAL1, NUMBERS, XCMPLX_0,
      XXREAL_0, NAT_1, NAT_D, GROUP_4, ALGSEQ_1, POLYDIFF, POLYNOM3, POLYNOM4,
      POLYNOM5, VECTSP_1, VECTSP_2, QUOFIELD, STRUCT_0, ALGSTR_0, GROUP_1,
      GROUP_6, RLVECT_1, GCD_1, BINOM, HURWITZ, RATFUNC1, IDEAL_1, MOD_4,
      RING_1, RING_2, RING_3, RING_4;
 constructors HURWITZ, POLYNOM4, RELSET_1, ABIAN, NAT_D, RATFUNC1, GCD_1,
      BINOM, RINGCAT1, RING_3, ALGSEQ_1, RING_4, GROUP_4, POLYDIFF;
 registrations XBOOLE_0, XXREAL_0, XREAL_0, CARD_1, ORDINAL1, RELSET_1, MOD_4,
      FUNCT_1, FUNCT_2, NAT_1, INT_1, INT_2, POLYDIFF, FINSEQ_1, STRUCT_0,
      RLVECT_1, VECTSP_1, ALGSTR_1, GROUP_6, RINGCAT1, GRCAT_1, RING_1, INT_3,
      RING_2, RING_3, RING_4, RING_5, POLYNOM3, POLYNOM4, POLYNOM5, RATFUNC1;
 requirements NUMERALS, SUBSET, BOOLE, REAL, ARITHM;
 definitions TARSKI;
 equalities FINSEQ_1, XCMPLX_0, POLYNOM3, RING_4, POLYDIFF, HURWITZ;
 expansions STRUCT_0, GROUP_1, VECTSP_1, TARSKI, GROUP_6, FUNCT_2, RING_2,
      ALGSEQ_1;
 theorems GROUP_1, GROUP_6, VECTSP_1, RLVECT_1, IDEAL_1, POLYDIFF, GCD_1,
      PARTFUN1, FUNCT_2, TARSKI, FUNCT_1, POLYNOM4, RING_3, RATFUNC1, RING_5,
      ALGSEQ_1, RING_2, FUNCOP_1, POLYNOM3, NAT_1, INT_1, FINSEQ_1, NORMSP_1,
      RING_1, RING_4, XREAL_0, XREAL_1, STRUCT_0, ORDINAL1, UPROOTS, XXREAL_0,
      POLYNOM5, FINSEQ_2, GROUP_4, HURWITZ, BINOM, POLYNOM2, EC_PF_2, FINSEQ_3,
      FINSEQ_5;
 schemes ALGSEQ_1, NAT_1, INT_1, FUNCT_2;

begin :: Preliminaries

 reserve n for Nat;

notation
  let L be non empty ZeroStr;
  let p be Polynomial of L;
  synonym LM p for Leading-Monomial p;
end;

theorem Th2:
  for L being non empty ZeroStr, p being Polynomial of L
  holds deg p is Element of NAT iff p <> 0_.L
proof
  let L be non empty ZeroStr;let p be Polynomial of L;
  now assume p <> 0_.L; then
      len p <> 0 by POLYNOM4:5; then
      len p + 1 > 0 + 1 by XREAL_1:6; then
      len p >= 1 by NAT_1:13;
      hence deg(p) is Element of NAT by INT_1:3;
    end;
  hence thesis by HURWITZ:20;
end;

definition
  let R be non degenerated Ring;
  let p be non zero Polynomial of R;
  redefine func deg p -> Element of NAT;
  coherence
  proof
    p <> 0_.R;
    hence thesis by Th2;
  end;
end;

registration ::: move to RING_2
  let R be add-associative right_zeroed right_complementable
         right-distributive non empty doubleLoopStr;
  let f be additive Function of R,R;
  reduce f.(0.R) to 0.R;
  reducibility by RING_2:6;
end;

theorem Th3:
  for R being Ring,
      I being Ideal of R
  for x being Element of R/I,
      a being Element of R st x = Class(EqRel(R,I),a)
  for n being Nat holds x|^n = Class(EqRel(R,I),a|^n)
  proof
    let R be Ring, I be Ideal of R;
    let x be Element of R/I, a be Element of R;
    assume
A1: x = Class(EqRel(R,I),a);
    let n be Nat;
    defpred P[Nat] means x|^($1) = Class(EqRel(R,I),a|^($1));
    x|^0 = 1_(R/I) by BINOM:8 .= Class(EqRel(R,I),1_R) by RING_1:def 6
        .= Class(EqRel(R,I),a|^0) by BINOM:8; then
A2: P[0];
A3: now let i be Nat;
    assume
A4: P[i];
    Class(EqRel(R,I),a|^(i+1)) = Class(EqRel(R,I),(a|^i)*(a|^1)) by BINOM:10
      .= Class(EqRel(R,I),(a|^i)*a) by BINOM:8
      .= (x|^i) * x by A1,A4,RING_1:14
      .= (x|^i) * (x|^1) by BINOM:8
      .= x|^(i+1) by BINOM:10;
    hence P[i+1];
    end;
    for i being Nat holds P[i] from NAT_1:sch 2(A2,A3);
    hence thesis;
  end;

definition
  let R be Ring, a,b be Element of R;
  pred b is_a_irreducible_factor_of a means
  b divides a & b is irreducible;
end;

registration
  cluster non almost_left_invertible factorial for domRing;
  existence;
end;

theorem Th4:
  for R being non almost_left_invertible factorial domRing,
      a being non zero NonUnit of R
   ex b being Element of R st b is_a_irreducible_factor_of a
    proof
      let R be non almost_left_invertible factorial domRing,
      a be non zero NonUnit of R;
      consider F being non empty FinSequence of R such that
A1:    F is_a_factorization_of a by RING_2:def 12;
      len F <> 0; then
      consider G being FinSequence of R, d being Element of R such that
A2:    F = G ^ <*d*> by FINSEQ_2:19;
      take d;
      Product(G) * Product(<*d*>) = a by A1,A2,GROUP_4:5;then
A3:    Product(<*d*>) divides a by GCD_1:def 1;
      reconsider lf = len F as Element of dom F by FINSEQ_5:6;
      len F = len G + len<*d*> by A2,FINSEQ_1:22
           .= len G + 1 by FINSEQ_1:39; then
      F.lf = d by A2,FINSEQ_1:42;
      hence thesis by A1,A3,GROUP_4:9;
end;

begin :: The polynomials a * x^n

notation
  let R be Ring;
  let a be Element of R;
  let n be Nat;
  synonym anpoly(a,n) for seq(n,a);
end;

Lm1: for R being non degenerated Ring,
          a being non zero Element of R holds deg anpoly(a,n) = n
proof
  let R be non degenerated Ring, a be non zero Element of R;
  len anpoly(a,n) = n+1 by POLYDIFF:27;
  hence thesis;
end;

registration
  let R be non degenerated Ring,
      a be non zero Element of R,
      n be Nat;
  cluster anpoly(a,n) -> non zero;
  coherence
  proof
    deg anpoly(a,n) = n & n <> - 1 by Lm1;
    hence thesis by HURWITZ:20,UPROOTS:def 5;
  end;
end;

registration
  let R be Ring,
      a be zero Element of R,
      n be Nat;
  cluster anpoly(a,n) -> zero;
  coherence
proof
set q = anpoly(a,n);
A1: a = 0.R by STRUCT_0:def 12;
now let i be Element of NAT;
  per cases;
  suppose A2: i = n;
    q.n = 0.R by A1,POLYDIFF:24 .= (0_.R).n by FUNCOP_1:7,ORDINAL1:def 12;
    hence q.i = (0_.R).i by A2;
    end;
  suppose i <> n;
    then q.i = 0.R by POLYDIFF:25 .= (0_.R).i by FUNCOP_1:7;
    hence q.i = (0_.R).i;
    end;
  end;
then q = 0_.R;
hence thesis;
end;
end;

theorem
  for R being non degenerated Ring,
      a being non zero Element of R holds deg anpoly(a,n) = n by Lm1;

theorem
  for R being non degenerated Ring,
    a being Element of R holds LC anpoly(a,n) = a
  proof
    let R be non degenerated Ring, a being Element of R;
    set q = anpoly(a,n);
    per cases;
      suppose
A1:     a = 0.R; then
        q = 0_.R by UPROOTS:def 5; then
        q.(len q -' 1) = 0.R by FUNCOP_1:7;
        hence thesis by A1,RATFUNC1:def 6;
      end;
      suppose a <> 0.R; then
        a is non zero; then
A2:     n = deg q by Lm1 .= len q - 1; then
        n + 1 = len q; then
        len q -' 1 = n by A2,XREAL_1:233,NAT_1:11;
        hence a = q.(len q -' 1) by POLYDIFF:24 .= LC q by RATFUNC1:def 6;
      end;
    end;

theorem
  for R being non degenerated Ring, n being non zero Nat,
    a,x being Element of R holds eval(anpoly(a,n),x) = a * x|^n
    proof
      let R be non degenerated Ring, n be non zero Nat, a,x be Element of R;
      set q = anpoly(a,n);
      per cases;
        suppose
A1:     a = 0.R; then
        q = 0_.R by UPROOTS:def 5;
        hence eval(q,x) = a * x|^n by A1,POLYNOM4:17;
        end;
        suppose a <> 0.R; then
A2:      a is non zero;
        consider F be FinSequence of R such that
A3:     eval(q,x) = Sum F and
A4:     len F = len q and
A5:     for j be Element of NAT st j in dom F holds
        F.j = q.(j-'1) * (power R).(x,j-'1) by POLYNOM4:def 2;
        n = deg q by A2,Lm1 .= len q - 1; then
A7:      dom F = Seg(n+1) by A4,FINSEQ_1:def 3;
A8:      1 <= n + 1 by NAT_1:11;
A9:      n+1-'1 = n+1-1 by NAT_1:11,XREAL_1:233;
A10:     F/.(n+1) = F.(n+1) by A7,FINSEQ_1:3,PARTFUN1:def 6
                .= q.n * (power R).(x,n+1-'1) by A9,A5,A8,A7,FINSEQ_1:1
                .= a * (power R).(x,(n+1)-'1) by POLYDIFF:24
                .= a * x|^ n by A9,BINOM:def 2;
        now let j be Element of NAT;
        assume
A11:    j in dom F & j <> n+1; then
A12:    1 <= j <= n + 1 by A7,FINSEQ_1:1; then
        j < n + 1 by A11,XXREAL_0:1; then
A13:    1 <= j <= n by A11,NAT_1:13,A7,FINSEQ_1:1;
A14:    j -' 1 = j - 1 by A12,XREAL_0:def 2;
A15:    j - 1 < j - 0 by XREAL_1:15;
        thus F/.j = F.j by A11,PARTFUN1:def 6
           .= q.(j-'1) * (power R).(x,j-'1) by A5,A11
           .= 0.R * (power R).(x,j-'1) by A15,A13,A14,POLYDIFF:25
           .= 0.R;
        end;
        hence thesis by A3,A10,A7,FINSEQ_1:3,POLYNOM2:3;
      end;
    end;

theorem
  for R being non degenerated Ring,
      a being Element of R holds anpoly(a,0) = a|R;

theorem Th9:
  for R being non degenerated Ring,
      n being non zero Element of NAT holds anpoly(1.R,n) = rpoly(n,0.R)
proof
  let R be non degenerated Ring, n be non zero Element of NAT;
  set p = anpoly(1.R,n), r = rpoly(n,0.R);
  now let i be Element of NAT;
A1: 1 <= n by NAT_1:53;
  per cases;
  suppose A2: i = 0;
    then r.i = -power(R).(0.R,n) by HURWITZ:25
            .= -((0.R)|^n) by BINOM:def 2
            .= -0.R by A1,EC_PF_2:5
            .= p.i by A2,POLYDIFF:25;
    hence p.i = r.i;
    end;
  suppose A3: i = n;
    then r.i = 1_R by HURWITZ:25
            .= p.i by A3,POLYDIFF:24;
    hence p.i = r.i;
    end;
  suppose A4: i <> 0 & i <> n;
    then r.i = 0.R by HURWITZ:26
            .= p.i by A4,POLYDIFF:25;
    hence p.i = r.i;
    end;
  end;
  hence thesis;
end;

theorem Th10:
  for R being non degenerated comRing,
    a,b being non zero Element of R holds b * anpoly(a,n) = anpoly(a*b,n)
 proof
   let R be non degenerated comRing, a,b be non zero Element of R;
   now let i be Element of NAT;
     set p = anpoly(a,n), q = anpoly(a*b,n);
     per cases;
       suppose
A1:    i = n;
       (b*p).i = b * (p.i) by POLYNOM5:def 4
        .= b * a by A1,POLYDIFF:24
        .= q.i by A1,POLYDIFF:24;
       hence (b*p).i = q.i;
       end;
       suppose
A2:    i <> n;
       (b*p).i = b * (p.i) by POLYNOM5:def 4
        .= b * 0.R by A2,POLYDIFF:25
        .= q.i by A2,POLYDIFF:25;
       hence (b*p).i = q.i;
       end;
    end;
    hence thesis;
   end;

theorem Th11:
  for R being non degenerated comRing,
      a,b being non zero Element of R, n,m being Nat holds
   anpoly(a,n) *' anpoly(b,m) = anpoly(a*b,n+m)
   proof
     let R be non degenerated comRing,
         a,b be non zero Element of R, n,m be Nat;
     set p = anpoly(a,n), q = anpoly(b,m), r = anpoly(a*b,n+m);
     per cases;
       suppose A1: n = 0;
       hence p *' q = (a|R) *' q
              .= (a * 1_.R) *' q by RING_4:16
              .= a * ((1_.R) *' q) by RING_4:10
              .= r by A1,Th10;
       end;
       suppose A2: m = 0;
       hence p *' q = p *' (b|R)
              .= p *' (b * 1_.R) by RING_4:16
              .= b * (p *' 1_.R) by RING_4:10
              .= r by A2,Th10;
       end;
       suppose
A3:    n <> 0 & m <> 0; then
A4:     n >= 0 + 1 & m >= 0 + 1 by NAT_1:13;
       now let i be Element of NAT;
         consider F being FinSequence of the carrier of R such that
A5:       len F = i+1 & (p*'q).i = Sum F & for k being Element of NAT
         st k in dom F holds F.k = p.(k-'1) * q.(i+1-'k) by POLYNOM3:def 9;
A6:     for k being Element of NAT st k in dom F & k <> len p holds F/.k = 0.R
         proof
           let k be Element of NAT;
           assume
A7:        k in dom F & k <> len p;
A8:        deg p = n by Lm1;
           now assume
A9:          k -' 1 = n; then
             k - 1 = k -' 1 by A3,XREAL_0:def 2;
             hence contradiction by A7,A9,A8;
           end; then
A10:       p.(k-'1) = 0.R by POLYDIFF:25;
           thus F/.k = F.k by A7,PARTFUN1:def 6
              .= 0.R * q.(i+1-'k) by A10,A7,A5 .= 0.R;
        end;
A11:    dom F = Seg(i+1) by FINSEQ_1:def 3,A5;
        per cases;
          suppose
A12:        i = n + m;
A13:       deg p = n by Lm1; then
A14:       len p <= n + 1 + m by NAT_1:11;
A15:       dom F = Seg(n+m+1) by A12,A5,FINSEQ_1:def 3;
          len p - 1 + 1 >= 1 + 1 by A13,A4,XREAL_1:6; then
A16:       1 <= len p by XXREAL_0:2;
A17:       len p -' 1 = n by A13,XREAL_0:def 2;
          m = i + 1 - len p by A13,A12; then
A18:       i + 1 -' len p = m by XREAL_0:def 2;
          Sum F = F/.(len p) by A16,A6,A14,A15,FINSEQ_1:1,POLYNOM2:3
          .= F.(len p) by A16,A14,A15,FINSEQ_1:1,PARTFUN1:def 6
          .= p.n * q.m by A16,A14,A15,FINSEQ_1:1,A17,A18,A5
          .= a * q.m by POLYDIFF:24
          .= a * b by POLYDIFF:24;
          hence r.i = (p *' q).i by A5,A12,POLYDIFF:24;
          end;
          suppose
A19:        i <> n + m;
          Sum F = 0.R
          proof
            per cases;
              suppose i < len p - 1; then
A20:          i + 1 < (len p - 1) + 1 by XREAL_1:6;
              now let k be Element of NAT;
                assume
A21:            k in dom F; then
                1 <= k <= i + 1 by A11,FINSEQ_1:1;
                hence 0.R = F/.k by A20,A21,A6 .= F.k by A21,PARTFUN1:def 6;
              end;
              hence thesis by POLYNOM3:1;
            end;
              suppose
A22:            i >= len p - 1;
              now let k be Element of NAT;
                assume
A23:             k in dom F;
                per cases;
                  suppose k <> len p;
                  hence 0.R = F/.k by A23,A6 .= F.k by A23,PARTFUN1:def 6;
                  end;
                  suppose
A24:               k = len p;
A25:               deg p = n by Lm1;
                  i + 1 >= (len p - 1) + 1 by A22,XREAL_1:6; then
                  i + 1 - len p >= len p - len p by XREAL_1:6; then
                  i + 1 -' len p = i - n by A25,XREAL_0:def 2; then
A26:              i + 1 -' len p <> m by A19;
                  thus F.k = p.(len p -'1) * q.(i+1-' len p) by A5,A23,A24
                   .= p.(len p -'1) * 0.R by A26,POLYDIFF:25
                   .= 0.R;
                 end;
               end;
               hence thesis by POLYNOM3:1;
             end;
           end;
           hence r.i = (p *' q).i by A5,A19,POLYDIFF:25;
         end;
       end;
       hence thesis;
     end;
   end;

theorem Th12:
  for R being non degenerated Ring, p being non zero Polynomial of R holds
   LM p = anpoly(p.(deg p),deg p)
   proof
     let R be non degenerated Ring, p be non zero Polynomial of R;
     set q = anpoly(p.(deg p),deg p), r = LM p, n = deg p;
     reconsider degp = deg p as Element of NAT;
A1:   n = len p -' 1 by XREAL_0:def 2;
     now let i be Element of NAT;
     per cases;
       suppose A3: i <> n; then
         r.i = 0.R by A1,POLYNOM4:def 1
            .= q.i by A3,POLYDIFF:25;
         hence r.i = q.i;
       end;
       suppose A4: i = n; then
         r.i = p.n by A1,POLYNOM4:def 1
         .= q.i by A4,POLYDIFF:24;
         hence r.i = q.i;
       end;
     end;
     hence thesis;
   end;

theorem Th13:
  for R being non degenerated comRing
   holds (<%0.R,1.R%>)`^n = anpoly(1.R,n)
   proof
     let R be non degenerated comRing;
     defpred P[Nat] means (<%0.R,1.R%>)`^$1= anpoly(1.R,$1);
A1:  P[0]
     proof
       thus (<%0.R,1.R%>)`^0 = 1_.R by POLYNOM5:15
                    .= anpoly(1.R,0);
     end;
A2:  now let n be Nat;
      assume P[n]; then
      (<%0.R,1.R%>)`^(n+1) = anpoly(1.R,n) *' <%-0.R,1.R%> by POLYNOM5:19
                        .= anpoly(1.R,n) *' rpoly(1,0.R) by RING_5:10
                        .= anpoly(1.R,n) *' anpoly(1.R,1) by Th9
                        .= anpoly(1.R*1.R,n+1) by Th11
                        .= anpoly(1.R,n+1);
      hence P[n+1];
    end;
    for k being Nat holds P[k] from NAT_1:sch 2(A1,A2);
    hence thesis;
   end;

begin :: More on Homomorphisms

theorem Th14:
   for R being Ring, S being R-homomorphic Ring
   for h being Homomorphism of R,S
   for a being Element of R, n being Nat holds h.(a|^n) = (h.a)|^n
   proof
     let R be Ring, S be R-homomorphic Ring; let h be Homomorphism of R,S;
     let a be Element of R, n be Nat;
     defpred P[Nat] means h.(a|^($1)) = (h.a)|^($1);
A1:  P[0]
     proof
       thus
       h.(a|^0) = h.(1_R) by BINOM:8 .= 1_S by GROUP_1:def 13
       .= (h.a)|^0 by BINOM:8;
     end;
A2:  now let k be Nat;
       assume
A3:    P[k];
       h.(a|^(k+1)) = h.((a|^k) * (a|^1)) by BINOM:10
                .= h.(a|^k) * h.(a|^1) by GROUP_6:def 6
                .= (h.a)|^k * (h.a) by A3,BINOM:8
                .= (h.a)|^k * ((h.a)|^1) by BINOM:8
                .= (h.a)|^(k+1) by BINOM:10;
       hence P[k+1];
     end;
     for n being Nat holds P[n] from NAT_1:sch 2(A1,A2);
     hence thesis;
    end;

theorem
   for R being Ring, S being R-homomorphic Ring
   for h being Homomorphism of R,S holds h.(Sum <*>(the carrier of R)) = 0.S
   proof
     let R be Ring, S be R-homomorphic Ring; let h be Homomorphism of R,S;
     thus
     h.(Sum <*>(the carrier of R)) = h.(0.R) by RLVECT_1:43 .= 0.S by RING_2:6;
   end;

theorem
   for R being Ring, S being R-homomorphic Ring
   for h being Homomorphism of R,S
   for F being FinSequence of R, a being Element of R holds
   h.(Sum(<*a*>^F)) = h.a + h.(Sum F)
   proof
      let R be Ring, S be R-homomorphic Ring; let h be Homomorphism of R,S;
      let F be FinSequence of R, a be Element of R;
      thus h.(Sum(<*a*>^F)) = h.(Sum(<*a*>) + Sum F) by RLVECT_1:41
                     .= h.(Sum<*a*>) + h.(Sum F) by VECTSP_1:def 20
                     .= h.a + h.(Sum F) by RLVECT_1:44;
   end;

theorem Th17:
   for R being Ring, S being R-homomorphic Ring
   for h being Homomorphism of R,S
   for F being FinSequence of R, a being Element of R holds
   h.(Sum(F^<*a*>)) = h.(Sum F) + h.a
   proof
     let R be Ring, S be R-homomorphic Ring; let h be Homomorphism of R,S;
     let F be FinSequence of R, a be Element of R;
     thus h.(Sum(F^<*a*>)) = h.(Sum F + Sum(<*a*>)) by RLVECT_1:41
                     .= h.(Sum F) + h.(Sum<*a*>) by VECTSP_1:def 20
                     .= h.(Sum F) + h.a by RLVECT_1:44;
   end;

theorem
   for R being Ring, S being R-homomorphic Ring
   for h being Homomorphism of R,S
   for F,G being FinSequence of R holds h.(Sum(F^G)) = h.(Sum F) + h.(Sum G)
   proof
     let R be Ring, S be R-homomorphic Ring; let h be Homomorphism of R,S;
     let F,G be FinSequence of R;
     thus h.(Sum(F^G)) = h.(Sum F + Sum G) by RLVECT_1:41
     .= h.(Sum F) + h.(Sum G) by VECTSP_1:def 20;
  end;

theorem
   for R being Ring, S being R-homomorphic Ring
   for h being Homomorphism of R,S holds
   h.(Product <*>(the carrier of R)) = 1.S
   proof
     let R be Ring, S be R-homomorphic Ring; let h be Homomorphism of R,S;
     thus h.(Product <*>(the carrier of R)) = h.(1_R) by GROUP_4:8
     .= 1_S by GROUP_1:def 13 .= 1.S;
   end;

theorem
   for R being Ring, S being R-homomorphic Ring
   for h being Homomorphism of R,S
   for F being FinSequence of R, a being Element of R holds
   h.(Product(<*a*>^F)) = h.a * h.(Product F)
   proof
     let R be Ring, S be R-homomorphic Ring; let h be Homomorphism of R,S;
     let F be FinSequence of R, a be Element of R;
     thus
     h.(Product(<*a*>^F)) = h.(Product(<*a*>) * Product F) by GROUP_4:5
                         .= h.(Product<*a*>) * h.(Product F) by GROUP_6:def 6
                         .= h.a * h.(Product F) by GROUP_4:9;
   end;

theorem
   for R being Ring, S being R-homomorphic Ring
   for h being Homomorphism of R,S
   for F being FinSequence of R, a being Element of R holds
   h.(Product(F^<*a*>)) = h.(Product F) * h.a
   proof
     let R be Ring, S be R-homomorphic Ring; let h be Homomorphism of R,S;
     let F be FinSequence of R, a be Element of R;
     thus
     h.(Product(F^<*a*>)) = h.(Product F * Product(<*a*>)) by GROUP_4:5
                         .= h.(Product F) * h.(Product<*a*>) by GROUP_6:def 6
                         .= h.(Product F) * h.a by GROUP_4:9;
   end;

theorem
   for R being Ring, S being R-homomorphic Ring
   for h being Homomorphism of R,S
   for F,G being FinSequence of R
   holds h.(Product(F^G)) = h.(Product F) * h.(Product G)
   proof
     let R be Ring, S be R-homomorphic Ring; let h be Homomorphism of R,S;
     let F,G be FinSequence of R;
     thus h.(Product(F^G)) = h.(Product F * Product G) by GROUP_4:5
     .= h.(Product F) * h.(Product G) by GROUP_6:def 6;
   end;

begin :: Lifting Homomorphisms from R to R[X]

definition
  let R,S be Ring;
  let f be Function of Polynom-Ring R, Polynom-Ring S;
  let p be Element of the carrier of Polynom-Ring R;
  redefine func f.p -> Element of the carrier of Polynom-Ring S;
  coherence
  proof
    f.p is Element of Polynom-Ring S;
    hence thesis;
  end;
end;

definition
  let R be Ring, S be R-homomorphic Ring;
  let h be additive Function of R,S;
   func PolyHom h -> Function of Polynom-Ring R, Polynom-Ring S means  :Def2:
   for f being Element of the carrier of Polynom-Ring R
   for i being Nat holds (it.f).i = h.(f.i);
existence
proof
A1: for f being Polynomial of R ex g being Polynomial of S
     st for i being Nat holds g.i = h.(f.i)
     proof
       let f be Polynomial of R;
       deffunc F(Nat) = h.(f.$1);
       consider q being AlgSequence of S such that
A2:     len q <= len f & for k being Nat st k < len f holds q.k = F(k)
       from ALGSEQ_1:sch 1;
       take q;
       now let i be Nat;
         per cases;
           suppose i < len f;
           hence q.i = h.(f.i) by A2;
           end;
           suppose A3: i >= len f; then
           f.i = 0.R by ALGSEQ_1:8;
           hence h.(f.i) = 0.S by RING_2:6
                 .= q.i by A3,A2,ALGSEQ_1:8,XXREAL_0:2;
           end;
         end;
         hence thesis;
       end;
       defpred P[object,object] means
       ex f being (Polynomial of R), g being Polynomial of S
       st $1 = f & $2 = g & for i being Nat holds g.i = h.(f.i);
A4:     for x being object st x in the carrier of Polynom-Ring R
       ex y being object st y in the carrier of Polynom-Ring S & P[x,y]
       proof
         let x be object;
         assume x in the carrier of Polynom-Ring R; then
         reconsider y = x as Polynomial of R by POLYNOM3:def 10;
         consider z being Polynomial of S such that
A5:      for i being Nat holds z.i = h.(y.i) by A1;
         take z;
         thus thesis by A5,POLYNOM3:def 10;
       end;
       consider F being Function of
       the carrier of Polynom-Ring R, the carrier of Polynom-Ring S such that
A6:     for x being object st x in the carrier of Polynom-Ring R holds P[x,F.x]
       from FUNCT_2:sch 1(A4);
       take F;
       now let f be (Polynomial of R), g be Polynomial of S;
         assume
A7:      g = F.f;
         let i be Nat;
         f in the carrier of Polynom-Ring R by POLYNOM3:def 10; then
         P[f,F.f] by A6;
         hence g.i = h.(f.i) by A7;
       end;
       hence thesis;
     end;
uniqueness
proof
let F,G be Function of Polynom-Ring R, Polynom-Ring S;
assume that
A8: for f being Element of the carrier of Polynom-Ring R
    for i being Nat holds (F.f).i = h.(f.i) and
A9: for f being Element of the carrier of Polynom-Ring R
    for i being Nat holds (G.f).i = h.(f.i);
  now let o be object;
  assume o in the carrier of Polynom-Ring R;
  then reconsider p = o as Element of the carrier of Polynom-Ring R;
  now let u be object;
    assume u in NAT;
    then reconsider m = u as Nat;
    (F.p).m = h.(p.m) by A8 .= (G.p).m by A9;
    hence (F.p).u = (G.p).u;
    end;
  then F.p = G.p;
  hence F.o = G.o;
  end;
hence F = G;
end;
end;

registration
  let R be Ring,
      S be R-homomorphic Ring;
  let h be Homomorphism of R,S;
  cluster PolyHom h -> additive multiplicative unity-preserving;
  coherence
proof
set g = PolyHom h;
set RP = Polynom-Ring R, SP = Polynom-Ring S;
reconsider 1RP = 1_RP as
        Element of the carrier of Polynom-Ring R;
reconsider 1SP = 1_SP as
        Element of the carrier of Polynom-Ring S;
now let a,b be Element of the carrier of Polynom-Ring R;
  reconsider gab = g.a + g.b as Element of the carrier of Polynom-Ring S;
  reconsider a1 = a, b1 = b as sequence of R;
  set ab1 = a1 + b1;
  set ga = g.a, gb = g.b;
  reconsider ga1 = ga, gb1 = gb as sequence of S;
  set gab1 = ga1 + gb1;
  now let m be Element of NAT;
    a1 + b1 = a + b by POLYNOM3:def 10; then
    (g.(a + b)).m = h.(ab1.m) by Def2
                .= h.(a1.m + b1.m) by NORMSP_1:def 2
                 .= h.(a.m) + h.(b.m) by VECTSP_1:def 20
                 .= (g.a).m + h.(b.m) by Def2
                 .= (ga1).m + (gb1).m by Def2
                 .= gab1.m by NORMSP_1:def 2;
    hence (g.(a + b)).m = gab.m by POLYNOM3:def 10;
    end;
  hence g.(a + b) = g.a + g.b by FUNCT_2:63;
  end;
hence g is additive;
now let a,b be Element of the carrier of Polynom-Ring R;
  reconsider ab = a * b as Element of the carrier of Polynom-Ring R;
  reconsider gab = g.a * g.b as Element of the carrier of Polynom-Ring S;
  reconsider a1 = a, b1 = b as sequence of R;
  reconsider ab1 = a1 *' b1 as sequence of R;
  reconsider ga = g.a, gb = g.b as Element of the carrier of Polynom-Ring S;
  reconsider ga1 = ga, gb1 = gb as sequence of S;
  set gab1 = ga1 *' gb1;
  now let m be Element of NAT;
    consider r being FinSequence of the carrier of R such that
A1: len r = m+1 & ab1.m = Sum r & for k being Element of NAT
    st k in dom r holds r.k = a1.(k-'1) * b1.(m+1-'k) by POLYNOM3:def 9;
    consider s being FinSequence of the carrier of S such that
A2: len s = m+1 & gab1.m = Sum s & for k being Element of NAT
    st k in dom s holds s.k = ga1.(k-'1) * gb1.(m+1-'k) by POLYNOM3:def 9;
A5: dom r = Seg(m + 1) by A1,FINSEQ_1:def 3
         .= dom s by A2,FINSEQ_1:def 3;
A3: for k being Element of NAT st k in dom r holds h.(r.k) = s.k
      proof
        let k be Element of NAT;
        assume
A4:     k in dom r;
        hence h.(r.k) = h.(a1.(k-'1) * b1.(m+1-'k)) by A1
               .= h.(a1.(k-'1)) * h.(b1.(m+1-'k)) by GROUP_6:def 6
               .= ga1.(k-'1) * h.(b1.(m+1-'k)) by Def2
               .= ga1.(k-'1) * gb1.(m+1-'k) by Def2
               .= s.k by A5,A4,A2;
      end;
      reconsider m1 = m+1 as Element of NAT;
A6:   1 <= m + 1 by NAT_1:11;
      defpred P[Nat] means h.(Sum(r|$1)) = Sum(s|$1);
A7:   P[1]
      proof
A8:   len(r|1) = 1 by A1,NAT_1:11,FINSEQ_1:59;
A9:   dom(r|1) = Seg 1 by A1,A6,FINSEQ_1:17; then
      (r|1).1 in rng(r|1) by FINSEQ_1:3,FUNCT_1:3; then
      reconsider a = (r|1).1 as Element of the carrier of R;
      r|1 = <*a*> by A8,FINSEQ_1:40; then
A11:  h.(Sum(r|1)) = h.a by RLVECT_1:44;
A12:    len(s|1) = 1 by A2,NAT_1:11,FINSEQ_1:59;
A13:    dom(s|1) = Seg 1 by A2,A6,FINSEQ_1:17; then
        (s|1).1 in rng(s|1) by FINSEQ_1:3,FUNCT_1:3; then
        reconsider b = (s|1).1 as Element of the carrier of S;
A15:    s|1 = <*b*> by A12,FINSEQ_1:40;
A16:    dom r = Seg(m + 1) by A1,FINSEQ_1:def 3;
A17:    1 in dom(s|(Seg 1)) by A13;
        1 in dom(r|(Seg 1)) by A9; then
        h.a = h.(r.1) by FUNCT_1:47
           .= s.1 by A16,A3,A6,FINSEQ_1:1
           .= b by A17,FUNCT_1:47;
        hence thesis by A11,A15,RLVECT_1:44;
        end;
A19:     now let j be Element of NAT;
          assume
A20:      1 <= j & j < m1;
          assume
A21:      P[j];
A22:     j + 1 <= m + 1 by A20,NAT_1:13; then
A23:    len(r|(j+1)) = j + 1 by A1,FINSEQ_1:59;
A24:    r|(Seg j) = r|j; then
        reconsider rj = r|(Seg j) as FinSequence of R;
        (r|(j+1))|j = r|j by NAT_1:11,FINSEQ_1:82; then
        consider q being FinSequence such that
A25:     r|(j+1) = rj ^ q by FINSEQ_1:80;
a26:     1 <= j + 1 by NAT_1:11; then
A27:     r.(j+1) in rng r by FUNCT_1:3,A1,A22,FINSEQ_3:25;
A28:     j + 1 = len(r|(j+1)) by A22,A1,FINSEQ_1:59
            .= len rj + len q by A25,FINSEQ_1:22
            .= j + len q by A20,A24,A1,FINSEQ_1:59; then
        dom q = Seg 1 by FINSEQ_1:def 3; then
A29:    1 in dom q;
A30:    len(r|j) = j by A20,A1,FINSEQ_1:59; then
A31:    (r|(j+1)).(j+1) = q.1 by A25,A29,FINSEQ_1:def 7;
        dom(r|(j+1)) = Seg(j+1) by A23,FINSEQ_1:def 3; then
A32:    r.(j+1) = (r|(j+1)).(j+1) by FUNCT_1:47,FINSEQ_1:3; then
        reconsider a = q.1 as Element of R by A30,A27,A25,A29,FINSEQ_1:def 7;
A33:    h.a = s.(j+1) by A31,A32,a26,A3,A1,A22,FINSEQ_3:25;
        q = <*a*> by A28,FINSEQ_1:40; then
        h.(Sum(r|(j+1))) = h.(Sum rj) + h.a by A25,Th17
        .= Sum(s|j) + Sum<*h.a*> by RLVECT_1:44,A21
        .= Sum((s|j) ^ <*h.a*>) by RLVECT_1:41
        .= Sum(s|(j+1)) by A20,A2,A33,FINSEQ_5:83;
        hence P[j+1];
      end;
A34:  for i being Element of NAT st 1 <= i & i <= m1 holds P[i]
        from INT_1:sch 7(A7,A19);
A35:  Sum s = Sum(s|(m+1)) by A2,FINSEQ_1:58
           .= h.(Sum(r|(m+1))) by A34,A6
           .= h.(Sum r) by A1,FINSEQ_1:58;
      a1 *' b1 = a * b by POLYNOM3:def 10; then
      (g.(a * b)).m = gab1.m by A35,A2,A1,Def2;
      hence (g.(a * b)).m = gab.m by POLYNOM3:def 10;
    end;
    hence g.(a * b) = g.a * g.b by FUNCT_2:63;
  end;
  hence g is multiplicative;
  now let m be Element of NAT;
    per cases;
      suppose
A36:  m = 0; then
      h.(1RP.m) = h.((1_.R).0) by POLYNOM3:def 10
                  .= h.(1_R) by POLYNOM3:30
                  .= 1_S by GROUP_1:def 13
                  .= (1_.S).0 by POLYNOM3:30
                  .= 1SP.m by A36,POLYNOM3:def 10;
      hence (g.(1_RP)).m = 1SP.m by Def2;
      end;
      suppose
A37:    m <> 0;
      h.(1RP.m) = h.((1_.R).m) by POLYNOM3:def 10
             .= h.(0.R) by A37,POLYNOM3:30
             .= 0.S by RING_2:6
             .= (1_.S).m by A37,POLYNOM3:30
             .= 1SP.m by POLYNOM3:def 10;
      hence (g.(1_RP)).m = 1SP.m by Def2;
      end;
    end;
    hence thesis by FUNCT_2:63;
   end;
  end;

theorem Th23:
   for R being Ring, S being R-homomorphic Ring
   for h being Homomorphism of R,S holds (PolyHom h).(0_.R) = 0_.S
   proof
     let R be Ring, S be R-homomorphic Ring;
     let h be Homomorphism of R,S;
A1:   0_.R = 0.(Polynom-Ring R) by POLYNOM3:def 10;
      reconsider f = (PolyHom h).(0.(Polynom-Ring R)) as
         Element of the carrier of Polynom-Ring S;
     now let i be Element of NAT;
       f.i = h.((0_.R).i) by Def2,A1
       .= h.(0.R) by FUNCOP_1:7
       .= 0.S by RING_2:6
       .= (0_.S).i by FUNCOP_1:7;
       hence f.i = (0_.S).i;
     end;
     hence thesis by A1,FUNCT_2:63;
   end;

theorem
   for R being Ring, S being R-homomorphic Ring
   for h being Homomorphism of R,S holds (PolyHom h).(1_.R) = 1_.S
   proof
     let R be Ring, S be R-homomorphic Ring; let h be Homomorphism of R,S;
     thus
     (PolyHom h).(1_.R) = (PolyHom h).(1_(Polynom-Ring R)) by POLYNOM3:def 10
     .= 1_(Polynom-Ring S) by GROUP_1:def 13 .= 1_.S by POLYNOM3:def 10;
   end;

theorem
   for R being Ring, S being R-homomorphic Ring
   for h being Homomorphism of R,S
   for p,q being Element of the carrier of Polynom-Ring R
   holds (PolyHom h).(p+q) = (PolyHom h).p + (PolyHom h).q by VECTSP_1:def 20;

theorem
   for R being Ring, S being R-homomorphic Ring
   for h being Homomorphism of R,S
   for p,q being Element of the carrier of Polynom-Ring R
   holds (PolyHom h).(p*q) = (PolyHom h).p * (PolyHom h).q by GROUP_6:def 6;

theorem Th27:
   for R being Ring, S being R-homomorphic Ring
   for h being Homomorphism of R,S
   for p being Element of the carrier of (Polynom-Ring R), b being Element of R
   holds (PolyHom h).(b*p) = h.b * (PolyHom h).p
   proof
     let R be Ring, S be R-homomorphic Ring; let h be Homomorphism of R,S;
     let p be Element of the carrier of (Polynom-Ring R), b be Element of R;
     reconsider q = b * p as Element of the carrier of Polynom-Ring R
       by POLYNOM3:def 10;
     reconsider f = (PolyHom h).q as Element of the carrier of Polynom-Ring S;
     now let i be Element of NAT;
       f.i = h.(q.i) by Def2
       .= h.(b * (p.i)) by POLYNOM5:def 4
       .= h.b * h.(p.i) by GROUP_6:def 6
       .= h.b * ((PolyHom h).p).i by Def2
       .= (h.b * (PolyHom h).p).i by POLYNOM5:def 4;
       hence f.i = (h.b * (PolyHom h).p).i;
     end;
     hence thesis by FUNCT_2:63;
   end;

Lm2:
   for R being Ring, S being R-homomorphic Ring
   for h being Homomorphism of R,S
   for p being Element of the carrier of Polynom-Ring R
   holds len((PolyHom h).p) <= len p
   proof
     let R be Ring, S be R-homomorphic Ring;
     let h be Homomorphism of R,S;
     let p be Element of the carrier of Polynom-Ring R;
     reconsider f = (PolyHom h).p as Element of the carrier of Polynom-Ring S;
    now let i be Nat;
      assume i >= len p; then
      p.i = 0.R by ALGSEQ_1:8;
      hence f.i = h.(0.R) by Def2 .= 0.S by RING_2:6;
    end; then
    len p is_at_least_length_of f;
    hence thesis by ALGSEQ_1:def 3;
   end;

Lm3:
   for R being Ring, S being R-homomorphic Ring
   for h being Homomorphism of R,S
   for p being Element of the carrier of (Polynom-Ring R) st len p <> 0
   holds len((PolyHom h).p) = len p iff h.(p.(len p-'1)) <> 0.S
   proof
     let R be Ring, S be R-homomorphic Ring; let h be Homomorphism of R,S;
     let p be Element of the carrier of (Polynom-Ring R);
     set lp1 = len p -' 1;
     assume len p <> 0; then
A2:   len p - 1 = len p -' 1 by XREAL_0:def 2; then
A3:   lp1 + 1 = len p;
A4:   len((PolyHom h).p) <= len p by Lm2;
A5:   now assume h.(p.(len p-'1)) <> 0.S; then
A6:     ((PolyHom h).p).(len p-'1) <> 0.S by Def2;
       now assume len((PolyHom h).p) < len p; then
         len((PolyHom h).p) <= lp1 by A3,NAT_1:13;
         hence contradiction by A6,ALGSEQ_1:8;
       end;
       hence len((PolyHom h).p) = len p by A4,XXREAL_0:1;
     end;
     now assume len((PolyHom h).p) = len p; then
       len((PolyHom h).p) = lp1 + 1 by A2; then
       ((PolyHom h).p).lp1 <> 0.S by ALGSEQ_1:10;
       hence h.(p.(len p-'1)) <> 0.S by Def2;
     end;
   hence thesis by A5;
  end;

Lm4:
   for R being Ring, S being R-homomorphic Ring
   for h being Homomorphism of R,S
   for p,L being Element of the carrier of (Polynom-Ring R)
   st L = LM p for a being Element of R holds
   h.eval(LM p,a) = eval((PolyHom h).L, h.a)
   proof
     let R be Ring, S be R-homomorphic Ring; let h be Homomorphism of R,S;
     let p,L be Element of the carrier of (Polynom-Ring R);
     assume
A1:  L = LM p;
     let a be Element of R;
     per cases;
       suppose A2: p = 0_.R; then
A3:    L = 0_.R by A1,POLYNOM4:13;
       thus h.eval(LM p,a) = h.eval(0_.R,a) by A2,POLYNOM4:13
          .= h.(0.R) by POLYNOM4:17
          .= 0.S by RING_2:6
          .= eval(0_.S,h.a) by POLYNOM4:17
          .= eval((PolyHom h).L,h.a) by A3,Th23;
       end;
       suppose A4: p <> 0_.R;
       set f = PolyHom h;
       reconsider q = (PolyHom h).L as Polynomial of S;
       consider F being FinSequence of the carrier of R such that
A5:     eval(LM p,a) = Sum F & len F = len LM p & for n be Element of NAT
       st n in dom F holds F.n = (LM p).(n-'1) * (power R).(a,n-'1)
         by POLYNOM4:def 2;
A6:    Sum F = p.(len p-'1) * (power R).(a,len p-'1) by A5,POLYNOM4:22
         .= (LM p).(len p-'1) * (power R).(a,len p-'1) by POLYNOM4:def 1;
       consider G being FinSequence of the carrier of S such that
A7:     eval(q,h.a) = Sum G & len G = len q & for n be Element of NAT
       st n in dom G holds G.n = q.(n-'1) * (power S).(h.a,n-'1)
       by POLYNOM4:def 2;
A8:    len q <= len L by Lm2;
A9:    len G <= len F by A1,A5,A7,Lm2;
A10:   len F = len p by A5,POLYNOM4:15; then
A11:   len F <> 0 by A4,POLYNOM4:5; then
A12:   0 + 1 <= len F by NAT_1:13;
A13:   len p -' 1 = len p - 1 by A11,A10,XREAL_0:def 2;
A15:   for n being Element of NAT st n in dom G holds n in dom F
       proof
         let n be Element of NAT;
         assume n in dom G; then
         1 <= n <= len q by A7,FINSEQ_3:25; then
         1 <= n <= len L by A8,XXREAL_0:2;
         hence thesis by A1,A5,FINSEQ_3:25;
       end;
A16:   for n being Element of NAT st n in dom G holds h.(F.n) = G.n
       proof
         let n be Element of NAT;
         assume
A17:     n in dom G;
         hence h.(F.n) = h.((LM p).(n-'1) * (power R).(a,n-'1)) by A15,A5
          .= h.(L.(n-'1)) * h.((power R).(a,n-'1)) by A1,GROUP_6:def 6
          .= q.(n-'1) * h.((power R).(a,n-'1)) by Def2
          .= q.(n-'1) * h.(a|^(n-'1)) by BINOM:def 2
          .= q.(n-'1) * (h.a)|^(n-'1) by Th14
          .= q.(n-'1) * (power S).(h.a,(n-'1)) by BINOM:def 2
          .= G.n by A17,A7;
       end;
A18:   for n being Element of NAT st n in dom G & n <> len p holds G/.n = 0.S
       proof
         let n be Element of NAT;
         assume
A19:     n in dom G & n <> len p; then
         1 <= n by FINSEQ_3:25; then
         n - 1 = n -' 1 by XREAL_0:def 2; then
A20:     n-'1 <> len p -'1 by A19,A13;
         thus G/.n = G.n by A19,PARTFUN1:def 6
            .= h.(F.n) by A16,A19
            .= h.((LM p).(n-'1) * (power R).(a,n-'1)) by A5,A19,A15
            .= h.((0.R) * (power R).(a,n-'1)) by A20,POLYNOM4:def 1
            .= 0.S by RING_2:6;
       end;
       per cases by A9,XXREAL_0:1;
         suppose
A21:     len G = len F; then
A22:     len G in dom G by A12,FINSEQ_3:25;
         Sum G = G/.(len G) by A18,A21,A10,POLYNOM2:3,A12,FINSEQ_3:25
            .= G.(len G) by A22,PARTFUN1:def 6
            .= h.(F.(len F)) by A12,FINSEQ_3:25,A16,A21
            .= h.(Sum F) by A6,FINSEQ_3:25,A12,A5,A10;
         hence thesis by A5,A7;
         end;
         suppose
A23:     len G < len F; then
         0.S = h.(L.(len L-'1)) by A7,A5,A1,Lm3
          .= h.(L.(len p-'1)) by A1,POLYNOM4:15
          .= h.(p.(len p-'1)) by A1,POLYNOM4:def 1; then
A24:     0.S = h.(p.(len p-'1)) * h.((power R).(a,len p-'1))
             .= h.(p.(len p-'1) * (power R).(a,len p-'1)) by GROUP_6:def 6
             .= h.eval(LM p,a) by POLYNOM4:22;
         now let n be Element of NAT;
           assume
A25:       n in dom G; then
           n in Seg len G by FINSEQ_1:def 3; then
           n <> len p by A23,A10,FINSEQ_1:1;
           hence 0.S = G/.n by A25,A18 .= G.n by A25,PARTFUN1:def 6;
         end;
         hence thesis by A24,A7,POLYNOM3:1;
       end;
     end;
   end;

theorem Th28:
   for R being Ring, S being R-homomorphic Ring
   for h being Homomorphism of R,S
   for p being Element of the carrier of (Polynom-Ring R), a being Element of R
   holds h.eval(p,a) = eval((PolyHom h).p, h.a)
   proof
     let R be Ring, S be R-homomorphic Ring; let h be Homomorphism of R,S;
     let p be Element of the carrier of (Polynom-Ring R), a be Element of R;
     defpred P[Nat] means
     for p be Element of the carrier of (Polynom-Ring R), a be Element of R
     st len p = $1 holds h.eval(p,a) = eval((PolyHom h).p, h.a);
A1:  P[0]
     proof
       let p be Element of the carrier of (Polynom-Ring R), a be Element of R;
       assume
A2:    len p = 0; then
A3:    p = 0_.R by POLYNOM4:5;
       thus h.eval(p,a) = h.eval(0_.R,a) by A2,POLYNOM4:5
       .= h.(0.R) by POLYNOM4:17 .= 0.S by RING_2:6
       .= eval(0_.S,h.a) by POLYNOM4:17 .= eval((PolyHom h).p, h.a) by A3,Th23;
    end;
A4: now let k be Nat;
    assume
A5: for m being Nat st m < k holds P[m];
    now let p be Element of the carrier of (Polynom-Ring R), a be Element of R;
      assume
A6:   len p = k;
      per cases;
        suppose k = 0;
        hence h.eval(p,a) = eval((PolyHom h).p, h.a) by A6,A1;
        end;
        suppose k > 0; then
        consider q being Polynomial of R such that
A7:      len q < len p & p = q + LM p &
        for n be Element of NAT st n < len p-1 holds q.n = p.n
          by A6,POLYNOM4:16;
        reconsider g = q as Element of the carrier of Polynom-Ring R
          by POLYNOM3:def 10;
        reconsider LMp = LM p as Element of the carrier of Polynom-Ring R
          by POLYNOM3:def 10;
        reconsider g1 = (PolyHom h).g, g2 = (PolyHom h).LMp as Polynomial of S;
A8:      (PolyHom h).g + (PolyHom h).LMp = g1 + g2 by POLYNOM3:def 10;
A9:      h.(eval(q,a)) = eval((PolyHom h).g, h.a) by A6,A7,A5;
        thus h.eval(p,a) = h.(eval(q,a) + eval(LMp,a)) by A7,POLYNOM4:19
        .= h.(eval(q,a)) + h.(eval(LMp,a)) by VECTSP_1:def 20
        .= eval((PolyHom h).g, h.a) + eval((PolyHom h).LMp, h.a) by A9,Lm4
        .= eval(g1+g2,h.a) by POLYNOM4:19
        .= eval((PolyHom h).(g+LMp), h.a) by A8,VECTSP_1:def 20
        .= eval((PolyHom h).p, h.a) by A7,POLYNOM3:def 10;
        end;
      end;
      hence P[k];
    end;
A10:  for k being Nat holds P[k] from NAT_1:sch 4(A4);
    ex n being Nat st n = len p;
    hence thesis by A10;
   end;

:: RING_5:7 is required domRing
theorem
   for R being domRing, S being R-homomorphic domRing
   for h being Homomorphism of R,S
   for p being Element of the carrier of (Polynom-Ring R),
   b,x being Element of R holds
   h.eval(b*p,x) = h.b * eval((PolyHom h).p,h.x)
   proof
     let R be domRing, S be R-homomorphic domRing;
     let h be Homomorphism of R,S;
     let p be Element of the carrier of (Polynom-Ring R), b,x be Element of R;
     reconsider q = b * p as Element of the carrier of Polynom-Ring R
     by POLYNOM3:def 10;
     h.eval(b*p,x) = eval((PolyHom h).q, h.x) by Th28
             .= eval(h.b * (PolyHom h).p,h.x) by Th27
             .= h.b * eval((PolyHom h).p,h.x) by RING_5:7;
     hence thesis;
   end;

registration
  let R be Ring;
  cluster R-homomorphic R-monomorphic for Ring;
  existence
proof
take R;
id R is RingHomomorphism;
hence R is R-homomorphic;
id R is RingMonomorphism;
hence R is R-monomorphic by RING_3:def 3;
end;
cluster R-homomorphic R-isomorphic for Ring;
existence
proof
take R;
id R is RingHomomorphism;
hence R is R-homomorphic;
id R is RingIsomorphism;
hence R is R-isomorphic by RING_3:def 4;
end;
end;

registration
  let R be Ring;
  cluster R-monomorphic -> R-homomorphic for Ring;
  coherence;
end;

registration
  let R be Ring,
      S be R-homomorphic R-monomorphic Ring;
  let h be Monomorphism of R,S;
  cluster PolyHom h -> monomorphism;
coherence
proof
set f = PolyHom h;
now let x1,x2 be object;
  assume A1: x1 in the carrier of Polynom-Ring R &
             x2 in the carrier of Polynom-Ring R & f.x1 = f.x2; then
  reconsider p = x1, q = x2 as Element of the carrier of Polynom-Ring R;
  now let i be Element of NAT;
    h.(p.i) = (f.q).i by A1,Def2 .= h.(q.i) by Def2;
    hence p.i = q.i by FUNCT_2:19;
    end;
  then p = q;
  hence x1 = x2;
  end;
then f is one-to-one by FUNCT_2:19;
hence thesis;
end;
end;

registration
  let R be Ring,
      S be R-isomorphic R-homomorphic Ring;
  let h be Isomorphism of R,S;
  cluster PolyHom h -> isomorphism;
  coherence
proof
set f = PolyHom h;
A1: for o be object st o in rng f holds o in the carrier of Polynom-Ring S;
now let o be object;
  assume o in the carrier of Polynom-Ring S; then
  reconsider p = o as Element of the carrier of Polynom-Ring S;
  deffunc F(object) = (h").(p.($1));
A2: for o be object st o in NAT holds F(o) in the carrier of R
   proof
     let o be object;
     assume o in NAT;
     then reconsider i = o as Element of NAT;
     F(i) = (h").(p.i);
     hence thesis;
     end;
   consider q being Function of NAT,the carrier of R such that
A3: for x being object st x in NAT holds q.x = F(x) from FUNCT_2:sch 2(A2);
   ex n being Nat st for i being Nat st i >= n holds q.i = 0.R
   proof
   take n = len p;
   now let i be Nat;
A4: h" is Isomorphism of S,R by RING_3:73;
   assume i >= n; then
   p.i = 0.S by ALGSEQ_1:8;
   hence q.i = (h").(0.S) by A3,ORDINAL1:def 12 .= 0.R by A4,RING_2:6;
   end;
   hence thesis;
   end; then
   reconsider q as Polynomial of R by ALGSEQ_1:def 1;
   reconsider q as Element of the carrier of Polynom-Ring R by POLYNOM3:def 10;
A5: dom f = the carrier of Polynom-Ring R by FUNCT_2:def 1;
   now let i be Element of NAT;
A6:  dom(h") = the carrier of S by FUNCT_2:def 1;
    (f.q).i = h.(q.i) by Def2
           .= (h"").((h").(p.i)) by A3
           .= p.i by A6,FUNCT_1:34;
    hence (f.q).i = p.i;
    end; then
    f.q = p;
    hence o in rng f by A5,FUNCT_1:def 3;
  end; then
  f is onto by A1,TARSKI:2;
  hence thesis;
end;
end;

theorem
  for R being Ring,
      S being R-homomorphic Ring
  for h being Homomorphism of R,S
  for p being Element of the carrier of (Polynom-Ring R)
  holds deg((PolyHom h).p) <= deg p by Lm2,XREAL_1:6;

theorem
   for R being non degenerated Ring, S being R-homomorphic Ring
   for h being Homomorphism of R,S
   for p being non zero Element of the carrier of (Polynom-Ring R)
   holds deg((PolyHom h).p) = deg p iff h.(LC p) <> 0.S
   proof
     let R be non degenerated Ring, S be R-homomorphic Ring;
     let h be Homomorphism of R,S;
     let p be non zero Element of the carrier of (Polynom-Ring R);
     p <> 0_.R; then
A1:   len p <> 0 by POLYNOM4:5;
     hereby
     assume deg((PolyHom h).p) = deg p; then
     h.(p.(len p-'1)) <> 0.S by A1,Lm3;
     hence h.(LC p) <> 0.S by RATFUNC1:def 6;
     end;
     assume h.(LC p) <> 0.S; then
     h.(p.(len p-'1)) <> 0.S by RATFUNC1:def 6;
     hence deg((PolyHom h).p) = deg p by A1,Lm3;
   end;

theorem Th32:
   for R being Ring, S being R-monomorphic R-homomorphic Ring
   for h being Monomorphism of R,S
   for p being Element of the carrier of (Polynom-Ring R)
   holds deg((PolyHom h).p) = deg p
   proof
     let R be Ring, S be R-monomorphic R-homomorphic Ring;
     let h be Monomorphism of R,S;
     let p be Element of the carrier of (Polynom-Ring R);
     reconsider f = (PolyHom h).p as
       Element of the carrier of Polynom-Ring S;
A1:   now let i be Nat;
       assume i >= len p; then
       p.i = 0.R by ALGSEQ_1:8;
       hence f.i = h.(0.R) by Def2 .= 0.S by RING_2:6;
     end;
     now let m be Nat;
       assume
A2:     m is_at_least_length_of f;
       now assume len p > m; then
         len p - 1 > m - 1 by XREAL_1:6; then
A3:      len p - 1 >= (m - 1) + 1 by INT_1:7; then
         reconsider lp = len p - 1 as Element of NAT by INT_1:3;
A4:      lp + 1 = len p;
         h.(0.R) = 0.S by RING_2:6
           .= f.lp by A3,A2
           .= h.(p.lp) by Def2; then
         p.lp = 0.R by FUNCT_2:19;
         hence contradiction by A4,ALGSEQ_1:10;
       end;
       hence len p <= m;
     end;
     hence thesis by A1,ALGSEQ_1:def 2,def 3;
   end;

theorem Th33:
   for R being Ring, S being R-monomorphic R-homomorphic Ring
   for h being Monomorphism of R,S
   for p being Element of the carrier of (Polynom-Ring R)
   holds LM((PolyHom h).p) = (PolyHom h).(LM p)
   proof
     let R be Ring, S be R-monomorphic R-homomorphic Ring;
     let h be Monomorphism of R,S;
     let p be Element of the carrier of (Polynom-Ring R);
     reconsider f = (PolyHom h).p as
     Element of the carrier of Polynom-Ring S;
     reconsider LMp = LM p as
     Element of the carrier of Polynom-Ring R by POLYNOM3:def 10;
A1:   deg f = deg p by Th32 .= len p - 1;
     now let i be Element of NAT;
       per cases;
         suppose A2: i = len p -'1; then
           (LM f).i = f.(len p -'1) by A1,POLYNOM4:def 1
                 .= h.(p.(len p -'1)) by Def2
                 .= h.((LM p).i) by A2,POLYNOM4:def 1
                 .= ((PolyHom h).(LMp)).i by Def2;
           hence (LM f).i = ((PolyHom h).(LMp)).i;
         end;
         suppose A3: i <> len p -'1; then
           (LM f).i = 0.S by A1,POLYNOM4:def 1
                 .= h.(0.R) by RING_2:6
                 .= h.((LM p).i) by A3,POLYNOM4:def 1
                 .= ((PolyHom h).(LMp)).i by Def2;
           hence (LM f).i = ((PolyHom h).(LMp)).i;
         end;
       end;
       hence thesis by FUNCT_2:63;
    end;

theorem Th34:
   for R being Ring, S being R-homomorphic Ring
   for h being Homomorphism of R,S
   for p be Element of the carrier of (Polynom-Ring R), a be Element of R
   holds a is_a_root_of p implies h.a is_a_root_of (PolyHom h).p
   proof
     let R be Ring, S be R-homomorphic Ring; let h be Homomorphism of R,S;
     let p be Element of the carrier of (Polynom-Ring R), a be Element of R;
     assume a is_a_root_of p; then
     eval(p,a) = 0.R by POLYNOM5:def 7; then
     eval((PolyHom h).p, h.a) = h.(0.R) by Th28 .= 0.S by RING_2:6;
     hence thesis by POLYNOM5:def 7;
   end;

theorem Th35:
   for R being Ring, S being R-monomorphic R-homomorphic Ring
   for h being Monomorphism of R,S
   for p being Element of the carrier of (Polynom-Ring R), a being Element of R
   holds a is_a_root_of p iff h.a is_a_root_of (PolyHom h).p
   proof
     let R be Ring, S be R-monomorphic R-homomorphic Ring;
     let h be Monomorphism of R,S;
     let p be Element of the carrier of (Polynom-Ring R), a be Element of R;
     now assume
A1:    h.a is_a_root_of (PolyHom h).p;
       h.(0.R) = 0.S by RING_2:6
         .= eval((PolyHom h).p,h.a) by A1,POLYNOM5:def 7
         .= h.eval(p,a) by Th28; then
       eval(p,a) = 0.R by FUNCT_2:19;
       hence a is_a_root_of p by POLYNOM5:def 7;
     end;
     hence thesis by Th34;
   end;

theorem Th36:
   for R being Ring, S being R-isomorphic R-homomorphic Ring
   for h being Isomorphism of R,S
   for p being Element of the carrier of (Polynom-Ring R),
   b being Element of S holds b is_a_root_of (PolyHom h).p iff
   ex a being Element of R st a is_a_root_of p & h.a = b
   proof
     let R be Ring, S be R-isomorphic R-homomorphic Ring;
     let h be Isomorphism of R,S;
     let p be Element of the carrier of (Polynom-Ring R), b be Element of S;
A1:   now assume A2: b is_a_root_of (PolyHom h).p;
       set a = (h").b;
A3:    dom(h") = the carrier of S by FUNCT_2:def 1;
A4:    h.a = (h"").((h").b) .= b by A3,FUNCT_1:34;
       h.eval(p,a) = eval((PolyHom h).p,h.a) by Th28
              .= 0.S by A4,A2,POLYNOM5:def 7
              .= h.(0.R) by RING_2:6; then
       eval(p,a) = 0.R by FUNCT_2:19;
       hence ex a being Element of R st h.a = b & a is_a_root_of p
         by A4,POLYNOM5:def 7;
     end;
     now assume ex a being Element of R st h.a = b & a is_a_root_of p; then
       consider a being Element of R such that
A5:     h.a = b & a is_a_root_of p;
       eval((PolyHom h).p,b) = h.(eval(p,a)) by A5,Th28
           .= h.(0.R) by A5,POLYNOM5:def 7
           .= 0.S by RING_2:6;
       hence b is_a_root_of (PolyHom h).p by POLYNOM5:def 7;
     end;
     hence thesis by A1;
   end;

theorem Th37:
   for R being Ring, S being R-homomorphic Ring
   for h being Homomorphism of R,S
   for p being Element of the carrier of (Polynom-Ring R) holds
   Roots p c= {a where a is Element of R : h.a in Roots (PolyHom h).p}
   proof
     let R be Ring, S be R-homomorphic Ring; let h be Homomorphism of R,S;
     let p be Element of the carrier of (Polynom-Ring R);
     let o be object;
     assume
A1:  o in Roots p; then
     reconsider a = o as Element of R;
     a is_a_root_of p by A1,POLYNOM5:def 10; then
     h.a is_a_root_of (PolyHom h).p by Th34; then
     h.a in Roots (PolyHom h).p by POLYNOM5:def 10;
     hence o in {a where a is Element of R : h.a in Roots (PolyHom h).p};
   end;

theorem
   for R being Ring, S being R-monomorphic R-homomorphic Ring
   for h being Monomorphism of R,S
   for p being Element of the carrier of (Polynom-Ring R)
   holds Roots p = {a where a is Element of R : h.a in Roots (PolyHom h).p}
   proof
     let R be Ring, S be R-monomorphic R-homomorphic Ring;
     let h be Monomorphism of R,S;
     let p be Element of the carrier of (Polynom-Ring R);
A1:   Roots p c={a where a is Element of R : h.a in Roots (PolyHom h).p} by
Th37;
     now let o be object;
       assume o in {a where a is Element of R : h.a in Roots (PolyHom h).p};
       then
       consider a being Element of R such that
A2:    o = a & h.a in Roots (PolyHom h).p;
       h.a is_a_root_of (PolyHom h).p by A2,POLYNOM5:def 10; then
       a is_a_root_of p by Th35;
       hence o in Roots p by A2,POLYNOM5:def 10;
     end;
     hence thesis by TARSKI:2,A1;
   end;

theorem Th39:
   for R being Ring, S being R-isomorphic R-homomorphic Ring
   for h being Isomorphism of R,S
   for p being Element of the carrier of (Polynom-Ring R)
   holds Roots (PolyHom h).p = {h.a where a is Element of R : a in Roots p}
   proof
     let R be Ring, S be R-isomorphic R-homomorphic Ring;
     let h be Isomorphism of R,S;
     let p be Element of the carrier of (Polynom-Ring R);
A1:   now let o be object;
       assume
A2:     o in Roots (PolyHom h).p; then
       reconsider b = o as Element of S;
       b is_a_root_of (PolyHom h).p by A2,POLYNOM5:def 10; then
       consider a being Element of R such that
A3:     a is_a_root_of p & h.a = b by Th36;
       a in Roots p by A3,POLYNOM5:def 10;
       hence o in {h.a where a is Element of R : a in Roots p} by A3;
     end;
     now let o be object;
       assume o in {h.a where a is Element of R : a in Roots p}; then
       consider a being Element of R such that
A4:     o = h.a & a in Roots p;
       a is_a_root_of p by A4,POLYNOM5:def 10; then
       h.a is_a_root_of (PolyHom h).p by Th36;
       hence o in Roots (PolyHom h).p by A4,POLYNOM5:def 10;
     end;
     hence thesis by A1,TARSKI:2;
   end;

begin :: Kronecker's Theorem

 reserve F for Field,
         p for irreducible Element of the carrier of Polynom-Ring F,
         f for Element of the carrier of Polynom-Ring F,
         a for Element of F;

definition
  let F,p;
  func KroneckerField(F,p) -> Field equals
  (Polynom-Ring F)/({p}-Ideal);
  coherence;
end;

definition
  let F, p;
  func emb p -> Function of F, KroneckerField(F,p) equals
  canHom({p}-Ideal) * canHom(F);
  coherence;
end;

registration
  let F, p;
  cluster emb p -> additive multiplicative unity-preserving;
  coherence;
end;

registration
  let F, p;
  cluster emb p -> monomorphism;
  coherence;
end;

registration
  let F, p;
  cluster KroneckerField(F,p) -> F-homomorphic F-monomorphic;
  coherence
  proof
    emb p is monomorphism;
    hence thesis by RING_3:def 3;
  end;
end;

definition
  let F, p, f;
  func emb(f,p) -> Element of the carrier of Polynom-Ring KroneckerField(F,p)
  equals
  (PolyHom (emb p)).f;
  coherence;
end;

definition
  let F, p;
  func KrRoot p -> Element of KroneckerField(F,p) equals
  Class(EqRel(Polynom-Ring F,{p}-Ideal),<%0.F,1.F%>);
  coherence
  proof
    set E = KroneckerField(F,p);
    reconsider q = <%0.F,1.F%> as Element of the carrier of Polynom-Ring F
      by POLYNOM3:def 10;
    Class(EqRel(Polynom-Ring F,{p}-Ideal),q) is Element of E by RING_1:12;
    hence thesis;
  end;
end;

theorem Th40:
  for F, p, a holds (emb p).a = Class(EqRel(Polynom-Ring F,{p}-Ideal),a|F)
   proof
     let F,p, a;
     reconsider pa = a|F as Element of Polynom-Ring F by POLYNOM3:def 10;
     dom(canHom F) = the carrier of F by FUNCT_2:def 1;
     hence (emb p).a = (canHom({p}-Ideal)).((canHom(F)).a) by FUNCT_1:13
           .= (canHom({p}-Ideal)).pa by RING_4:def 6
           .= Class(EqRel(Polynom-Ring F,{p}-Ideal),a|F) by RING_2:def 5;
   end;

theorem Th41:
   (emb(f,p)).n = Class(EqRel(Polynom-Ring F,{p}-Ideal),(f.n)|F)
   proof
      thus (emb(f,p)).n = (emb p).(f.n) by Def2
      .= Class(EqRel(Polynom-Ring F,{p}-Ideal),(f.n)|F) by Th40;
   end;

Lm5:
   eval(LM emb(f,p),KrRoot p) = Class(EqRel(Polynom-Ring F,{p}-Ideal),LM f)
   proof
     set LMf = Leading-Monomial(f), LMfe = Leading-Monomial(emb(f,p));
     set z = KrRoot p, E = KroneckerField(F,p);
     set efp = emb(f,p); set n = len efp -' 1;
     per cases;
       suppose A1: f = 0_.F; then
         emb(f,p) = 0_.E by Th23; then
         LMfe = 0_.E by POLYNOM4:13; then
A2:       eval(LMfe,KrRoot p) = 0.E by POLYNOM4:17
         .= Class(EqRel(Polynom-Ring F,{p}-Ideal),0.(Polynom-Ring F))
           by RING_1:def 6;
         0.(Polynom-Ring F) = 0_.F by POLYNOM3:def 10;
         hence thesis by A1,A2,POLYNOM4:13;
       end;
       suppose f <> 0_.F; then
         reconsider f1 = f as non zero Polynomial of F by UPROOTS:def 5;
         reconsider fnF = (f.n)|F as Element of the carrier of Polynom-Ring F
         by POLYNOM3:def 10;
         reconsider x = <%0.F,1.F%> as Element of the carrier of Polynom-Ring F
         by POLYNOM3:def 10;
A3:       efp.n = Class(EqRel(Polynom-Ring F,{p}-Ideal),(f.n)|F) by Th41;
A4:       (power E).(z,n) = z|^n by BINOM:def 2
         .= Class(EqRel(Polynom-Ring F,{p}-Ideal),x|^n) by Th3;
         set a = f.n;
A5:      deg f = deg efp by Th32 .= len efp - 1; then
A6:      n = deg f1 by XREAL_0:def 2;
         LC f1 is non zero; then
A7:      a is non zero by A5,RATFUNC1:def 6;
         x|^n = (power Polynom-Ring F).(<%0.F,1.F%>,n) by BINOM:def 2
         .= <%0.F,1.F%>`^n by POLYNOM5:def 3
         .= anpoly(1.F,n) by Th13; then
A8:       fnF * (x|^n) = anpoly(a,0) *' anpoly(1.F,n) by POLYNOM3:def 10
         .= anpoly(a * 1.F, 0 + n) by A7,Th11 .= LM f by A6,Th12;
        thus eval(LMfe,KrRoot p) = efp.n * (power E).(z,n) by POLYNOM4:22
        .= Class(EqRel(Polynom-Ring F,{p}-Ideal),LMf) by A8,A3,A4,RING_1:14;
      end;
    end;

theorem Th42:
   eval(emb(f,p),KrRoot p) = Class(EqRel(Polynom-Ring F,{p}-Ideal),f)
   proof
     set z = KrRoot p, E = KroneckerField(F,p), h = canHom (emb p);
     defpred P[Nat] means
     for f st len f = $1 holds eval(emb(f,p),z)
     = Class(EqRel(Polynom-Ring F,{p}-Ideal),f);
A1:  now let f be Element of the carrier of Polynom-Ring F;
       assume len f = 0; then
       f = 0_.F by POLYNOM4:5; then
A2:    f = 0.(Polynom-Ring F) by POLYNOM3:def 10;
       0_.E = 0.(Polynom-Ring E) by POLYNOM3:def 10
          .= emb(f,p) by A2,RING_2:6;
       hence eval(emb(f,p),z) = 0.E by POLYNOM4:17
       .= Class(EqRel(Polynom-Ring F,{p}-Ideal),f) by A2,RING_1:def 6;
     end;
A3:  now let k be Nat;
       assume A4: for m being Nat st m < k holds P[m];
       now let f be Element of the carrier of Polynom-Ring F;
         assume
A5:      len f = k;
         per cases;
            suppose k = 0;
            hence eval(emb(f,p),z) = Class(EqRel(Polynom-Ring F,{p}-Ideal),f)
            by A5,A1;
         end;
         suppose k > 0; then
         consider q being Polynomial of F such that
A6:       len q < len f & f = q + Leading-Monomial(f) &
         for n be Element of NAT st n < len f-1 holds q.n = f.n
         by A5,POLYNOM4:16;
         reconsider g = q as Element of the carrier of Polynom-Ring F
         by POLYNOM3:def 10;
         reconsider LMf = LM f as Element of the carrier of Polynom-Ring F
         by POLYNOM3:def 10;
         reconsider r1 = emb(LMf,p), r2 = emb(g,p) as Polynomial of E;
A7:       emb(LMf+g,p) = emb(LMf,p) + emb(g,p) by VECTSP_1:def 20
                     .= r1 + r2 by POLYNOM3:def 10;
         Leading-Monomial(emb(f,p)) = emb(LMf,p) by Th33; then
A8:       eval(emb(LMf,p),z)=Class(EqRel(Polynom-Ring F,{p}-Ideal),LMf)
         by Lm5;
A9:       eval(emb(g,p),z)=Class(EqRel(Polynom-Ring F,{p}-Ideal),g)
          by A6,A5,A4;
A10:       eval(emb(LMf,p),z) + eval(emb(g,p),z)
         = Class(EqRel(Polynom-Ring F,{p}-Ideal),LMf+g) by A9,A8,RING_1:13
         .= Class(EqRel(Polynom-Ring F,{p}-Ideal),f) by A6,POLYNOM3:def 10;
         thus eval(emb(f,p),z) = eval(r1+r2,z) by A7,A6,POLYNOM3:def 10
         .= Class(EqRel(Polynom-Ring F,{p}-Ideal),f) by A10,POLYNOM4:19;
       end;
     end;
     hence P[k];
   end;
A11: for k being Nat holds P[k] from NAT_1:sch 4(A3);
   ex n being Nat st len f = n;
   hence thesis by A11;
end;

theorem Th43:
   KrRoot p is_a_root_of emb(p,p)
   proof
A1:   p - 0.(Polynom-Ring F) in {p}-Ideal by IDEAL_1:66;
     eval(emb(p,p),KrRoot p)
     = Class(EqRel(Polynom-Ring F,{p}-Ideal),p) by Th42
     .= Class(EqRel(Polynom-Ring F,{p}-Ideal),0.(Polynom-Ring F))
       by A1,RING_1:6
     .= 0.KroneckerField(F,p) by RING_1:def 6;
     hence thesis by POLYNOM5:def 7;
   end;

theorem
   f is non constant implies ex p being irreducible Element of
   the carrier of Polynom-Ring F st emb(f,p) is with_roots
   proof
     assume f is non constant; then
     consider p being Element of the carrier of Polynom-Ring F such that
A2:   p is_a_irreducible_factor_of f by Th4;
     reconsider p as irreducible Element of the carrier of Polynom-Ring F
       by A2;
     take p;
     consider q being Element of the carrier of Polynom-Ring F such that
A3:   p * q = f by A2,GCD_1:def 1;
A4:   emb(f,p) = (PolyHom (emb p)).p * (PolyHom (emb p)).q by A3,GROUP_6:def 6
     .= emb(p,p) *' emb(q,p) by POLYNOM3:def 10;
     (KrRoot p) is_a_root_of emb(p,p) by Th43; then
     emb(p,p) is with_roots by POLYNOM5:def 8;
     hence thesis by A4;
   end;

theorem Th45:
   emb p is isomorphism implies p is with_roots
   proof
     set h = emb p;
     assume A1: emb p is isomorphism; then
     reconsider K = KroneckerField(F,p) as F-isomorphic F-homomorphic Ring
       by RING_3:def 4;
     reconsider h as Isomorphism of F,K by A1;
A2:   Roots (PolyHom h).p = {h.a where a is Element of F : a in Roots p}
       by Th39;
     KrRoot p is_a_root_of emb(p,p) by Th43; then
     KrRoot p in Roots (PolyHom h).p by POLYNOM5:def 10; then
     ex a being Element of F st (KrRoot p) = h.a & a in Roots p by A2;
     hence thesis;
   end;

theorem
   p is non with_roots implies emb p is non isomorphism by Th45;

subset_name: curated


TITLE: If magnetic monopoles exist would magnetic charge contribute to weak hypercharge similar to how electric charge does?
QUESTION [4 upvotes]: Electromagnetism and the weak force are intertwined as two parts of the electroweak force and some links still exist even at low energy levels one of the being weak hypercharge which is determined by a combination of electric charge and weak isospin in the form $$Y_w=2(Q-T_3) $$ Where $Q$ is electric charge and $T_3$ is weak isospin. Magnetic monopoles are not known to exist but I understand that predictions about their properties if they do exist have been made and that both the electromagnetic and weak force as well as their unification as the electroweak force are very well understood. If monopoles and magnetic charge do exist would they have a similar link to the weak force that electrons and electric charge do?

REPLY [3 votes]: The standard model predicts the existence of particles that are not represented directly by any individual quantum field in the lagrangian. As an example, it predicts the existence of protons, even though there is no proton field in the lagrangian. The standard standard model also predicts magnetic monopoles, even though there is no magnetic-monopole field in the lagrangian.
Here's some background to explain what I mean by standard standard model:

The gauge group of the standard model is often written $SU(3)_c\times SU(2)_L\times U(1)_Y$. Weak isospin $T_3$ is like a "charge" with respect to the $SU(2)_L$ part of the gauge group, and hypercharge $Y$ is the "charge" with respect to the $U(1)_Y$ part of the gauge group. The usual charge $Q$ is associated with the $U(1)_\text{EM}$ electromagnetic gauge group, which is a mixture of the $SU(2)_L$ and $U(1)_Y$ factors. The model looks simplest when written in terms of $SU(2)_L$ and $U(1)_Y$ instead of $U(1)_\text{EM}$, so in hindsight we usually consider $T_3$ and $Y$ to be inputs and $Q$ an output, even though $Q$ is the thing we measure more directly.

Actually, the gauge group $SU(3)_c\times SU(2)_L\times U(1)_Y$ is just one of a few possibilities that cannot be distinguished from each other in a small-coupling expansion (Feynman diagrams). A few of the possible variations are reviewed in arXiv:hep-ph/0609029. The possibility relevant to this question is that the $U(1)_Y$ factor (and therefore the resulting electromagnetic gauge group) could be noncompact — in other words, it could be $\mathbb{R}$ instead of $U(1)$. We're confident that it's really the compact group $U(1)$, though, because this explains why the electric charges of electrons and protons have precisely the same magnitude.$^\dagger$

By standard standard model, I mean the standard model using the compact group $U(1)_Y$ for the gauge interaction associated with hypercharge. In this version of the model, magnetic monopoles automatically exist, even though there is no magnetic-monopole field in the lagrangian. This is reviewed by Polchinski in arXiv:hep-th/0304042. It's relatively easy to see in lattice QED, and it plays a prominent role in Polyakov's classic book Gauge Fields and Strings.
Based on that, asking whether magnetic charge would contribute to weak hypercharge is like asking whether rocks would contribute to weak hypercharge. Weak hypercharge is an input to the theory. Rocks are an output: they are phenomena that the theory predicts. Similarly, magnetic monopols are an output: they are something that the theory predicts, using inputs like weak hypercharge.

Footnotes:
$^\dagger$ On page 76 in arXiv:1810.05338, Harlow and Ooguri mention that the electric charges of electrons and protons have the same magnitude to within one part in $10^{21}$, with this comment: "By far the most plausible explanation of this remarkable agreement is that the gauge group of electrodynamics is indeed $U(1)$, which presumably is why this is the terminology most people use." (In the context of the standard model, assuming the compact group $U(1)_Y$ for weak hypercharge is equivalent to assuming the compact group $U(1)$ for electrodynamics.)
By the way, the coexistence of quantum physics and gravity may give us another reason to be confident that the gauge group is compact, and therefore that magnetic monopoles exist. This connection is reviewed at length in Harlow and Ooguri's paper, which states the connection as conjecture 3 on page 1: If a quantum gravity theory at low energies includes a gauge theory with gauge group $G$, then $G$ must be compact.


TITLE: Is $\{(1,0),(0,0)\}\cup\bigcup_{n\neq1}\{(x,\frac{1}{n}):x\in\Bbb{R}\}$ locally connected?
QUESTION [1 upvotes]: Let
  $X=\{(1,0),(0,0)\}\cup\bigcup_{n\neq1}\{(x,\frac{1}{n}):x\in\Bbb{R}\}$.
  Determine whether or not $X$ is locally connected and find its
  components.

Well, I know that a space $X$ is said to be locally connected at x if for every neighborhood $U\subset X$ of $x$, there is a connected neighborhood $V$ of $x$ such that $V\subset U$. And the components  of $X$ are the equivalence classes of the relation $x\sim y$ if and only if there is a connected subspace of $X$ containing both $x$ and $y$.
Though the definitions of local connectness and components seem clear, this would be the first time I need to deal with a problem like this one, and I'm more interesting to know if there's a strategy to follow in this kind of problems. So where should I look in the first place to prove or disprove the local connectednes of this space? Any hint that can point me in the right direction would be highly appreciated. Thanks in advance!

REPLY [0 votes]: Unfortunately, around $(0, 0)$ there does not exist a connected neighbourhood. This is because if $\epsilon > 0$ is arbitrary, then $(X \setminus \{(0,0)\}) \cap B_\epsilon((0,0)) \neq \emptyset$, and because the connected components are given by
$$
\{(x, 1/n)|x \in \mathbb R\}, n \in \mathbb N \setminus \{1\} \text{ and } \{(1, 0)\} \text{ and } \{(0, 0)\};
$$
for, each is path-connected and if one contains a point of the other, we already have a partition into two disjoint open subsets.
The space looks roughly like this:

.                   .
The lines are supposed to be closer together the lower they are, but I can't type that, and I also can't type infinitely many lines.


TITLE: How do I evaluate this function?
QUESTION [1 upvotes]: I have the following problem

$$f(x)=\frac{(x+4)^{\frac12}(2x-x^2)(-\frac12(x+4)-^\frac{1}{2})}{x+4}, x>-4$$

Here's how far I got. I actually went a little farther, but after a couple extra steps I wasn't going anywhere.

Rewording the problem and including a constraint
$$\frac{\sqrt{x+4}(2x-x^2)-\frac12(\sqrt{x+4})}{x+4}, x>-4$$
Creating an equality, multiplying both sides with the denominator, then subtracting $(2x-x^2)$ to the other side to square both sides $$(\sqrt{x+4}-\frac12\sqrt{x+4})^2=(-(2x-x^2))^2$$
Ending up with this, unable to continue
$$\frac52x+10=(5x^3+4x^2-\frac32x+6)^2$$

I'm guessing I probably made some mistake from the start, and I'm guessing I need to work on simplifying roots and exponents better, like, instead of writing $x^2$ I write $xx$, I know things like that makes factoring, for example, easier. I'm still working on that.
Anyway, I'd appreciate some help here.
UPDATE: My mistake, I overlooked the directions. Apparently, I am to "write the expression as a single quotient in which only positive exponents and/or radicals appear"

REPLY [1 votes]: $$\sqrt{x+4}\cdot\sqrt{x+4}=x+4,$$ which for your previous problem gives $$f(x)=\frac{\sqrt{x+4}(2x-x^2)\left(-\frac{1}{2}\sqrt{x+4}\right)}{x+4}=\frac{x^2-2x}{2}$$ and for your new problem gives:
$$f(x)=\frac{\sqrt{x+4}(2x-x^2)\left(-\frac{1}{2}\cdot\frac{1}{\sqrt{x+4}}\right)}{x+4}=\frac{x^2-2x}{2(x+4)}.$$


TITLE: Prove that $X^\ast$ separable implies $X$ separable
QUESTION [21 upvotes]: Can someone tell me if I got the following right:
Assume $X$ to be a normed vector space over $\mathbb{R}$. Prove that if the dual space $X^\ast$ is separable then $X$ is separable as well.
I'm supposed to use the following hint: First show that for each $x_n^\ast$ we may choose a unit vector $x_n \in X$ such that $x_n^\ast (x_n) \geq \frac{\| x_n^\ast \|}{2}$. Then show that $\overline{Y} = \overline{span_\mathbb{Q} \{ x_n\}} = X$.
My answer:
(i) (by contradiction)
Assume for all $x_n \in X$ with $\| x_n \|_X = 1$ that
$$x_n^\ast (x_n) < \frac{\| x_n^\ast \|}{2} \iff 2 x_n^\ast (x_n) < \sup_{x_n; \| x_n \|_X = 1 } \{ | x_n^\ast(x_n) | \}$$
Claim: Then $\exists r \in \mathbb{R}: x_n^\ast(x_n) < r < \sup_{\dots}\{\dots \}$:
(i) $x_n^\ast (x_n) \neq 0$: because $\| x_n \| = 1$ and $x_n^\ast$ linear
(ii) if $x_n^\ast (x_n) < 0$ then
$2 x_n^\ast (x_n) < x_n^\ast (x_n) < x_n^\ast(- x_n) < 2 x_n^\ast(-x_n) < \sup_{\dots} \{ \dots \}$
(iii) $x_n^\ast(x_n) > 0$ then $\forall x_n: x_n^\ast (x_n) < 2 x_n^\ast (x_n) < \sup$
$\implies $ the $\sup$ is not the l.u.b., contradiction, so the claim $x_n^\ast (x_n) \geq \frac{\| x_n^\ast \|}{2}$ is true.
(ii) Using:
$ x \in \overline{Y} \iff \lnot \exists $ bounded linear functional $f^\ast$ such that $f^\ast (y ) = 0 \forall y \in Y$ and $f^\ast (x) \neq 0$
Let $f^\ast \in X^\ast$. Then $\{ x_n^\ast \}$ dense in $X^\ast \implies$
$$ \forall \varepsilon > 0 \exists x_n^\ast : \| x_n^\ast - f^\ast \| = \sup_{x \in X: \| x \| \leq 1} \{ |x_n^\ast (x) - f^\ast(x)| \} < \varepsilon$$
But for $x_n \in Y \subset X (\| x_n \| = 1)$ we know
$$| x_n^\ast (x_n)| \geq x_n^\ast (x_n) \geq \frac{\| x_n \|}{2} > 0$$
so if $f^\ast (y) = 0 \forall y \in Y$ then
$$ 0 < \frac{\| x_n \|}{2} \leq |x_n^\ast (x_n)| = |x_n^\ast (x_n) - f^\ast(x_n)|$$
$$ \implies \exists \varepsilon: \sup |x_n^\ast (x_n) - f^\ast(x_n)| > \varepsilon$$
$$ \implies \lnot \exists f^\ast \in X^\ast : \forall y \in Y: f^\ast (y) = 0$$
$$ x \in \overline{Y}$$
Thanks for your help.

REPLY [16 votes]: I’m going to comment only on what you wrote for (i):

Assume for all $x_n \in X$ with $\| x_n \|_X = 1$ that
$$x_n^\ast (x_n) \lt \frac{\| x_n^\ast \|}{2} \iff 2 x_n^\ast (x_n) \lt \sup_{x_n; \| x_n \|_X = 1 } \{| x_n^\ast(x_n)|\}$$
Claim: Then $\exists r \in \mathbb{R}: x_n^\ast(x_n) \lt r \lt \sup_{\dots}\{\dots \}$:
(i) $x_n^\ast (x_n) \neq 0$: because $\| x_n \| = 1$ and $x_n^\ast$ linear
(ii) if $x_n^\ast (x_n) \lt 0$ then $2 x_n^\ast (x_n) \lt x_n^\ast (x_n) \lt x_n^\ast(- x_n) \lt 2 x_n^\ast(-x_n) \lt \sup_{\dots} \{ \dots \}$
(iii) $x_n^\ast(x_n) \gt 0$ then $\forall x_n: x_n^\ast (x_n) \lt 2 x_n^\ast (x_n) \lt \sup$
$\implies $ the $\sup$ is not the l.u.b., contradiction, so the claim $x_n^\ast (x_n) \geq \frac{\| x_n^\ast \|}{2}$ is true.

The first problem, and it’s a major one, is that right off the bat you’re using $n$ for two completely different things. On the one hand it’s apparently supposed to be the index of a particular, fixed member of some countable norm-dense subset of $X^*$, though you never actually said that. On the other hand it’s a dummy index picking out members of $X$ of norm $1$; this would be a bad idea even if you weren’t already using $n$ for something else, since there’s no reason to suppose that there are only countably many elements of $X$ of norm $1$. You should have begun something like this:

Let $D=\{x_n^*:n\in\mathbb{N}\}$ be a countable norm-dense subset of $X^*$. Fix $x_n^*\in D$, and assume for each $x\in X$ with $\|x\|=1$ that $$x_n^*(x)<\frac{\|x_n^*\|}2.$$

Note that I stopped before your $\iff$ symbol: that’s because what follows it is not part of your assumption, but rather an inference from your assumption, so it does not belong in the same clause with assume that. Once you’ve clearly stated your assumption, then you can go on and draw conclusions:

This implies that $$2x_n^*(x)<\sup_{\|y\;\|=1}\|x_n^*(y)\|$$ for each $x\in X$ with $\|x\|=1$.

Note that I had to use a different letter for the dummy variable ($y$) in the supremum from the one used for the specific $x$ of norm $1$ in the surrounding statement: they refer to different objects.
The line that begins Claim makes no sense even after the ellipsis at the end is properly filled in. (Note, by the way, that this is something that you should have done yourself, so that the reader needn’t guess; with cut-and-paste it’s completely trivial.) You still have $n$ meaning two different things, and it’s not clear whether you’re talking talking about a specific $x$ of norm $1$ or all of them together. I suspect that you meant this:

Claim: There is an $r\in\mathbb{R}$ such that $$x_n^*(x)<r<\sup_{\|y\;\|=1}|x_n^*(y)|$$ for each $x\in X$ of norm $1$.

Presumably what follows is supposed to be a proof of the claim. Say so.

Proof of Claim: Fix $x\in X$ of norm $1$. Since $\|x_n^*\|$ is linear, $x_n^*(x)\ne 0$.

This doesn’t appear to follow. In fact, there seems to be nothing in your argument to here to preclude the possibility that $x_n^*$ is the zero functional.

If $x_n^*(x)>0$, then $$x_n^*(x)<2x_n^*(x)<\sup_{\|y\;\|=1}|x_n^*(y)|\;,$$ and if $x_n^*(x)<0$, then $$2x_n^*(x)<x_n^*(x)<x_n^*(-x)<2x_n^*(-x)<\sup_{\|y\;\|=1}|x_n^*(y)|\;.$$

This does not in fact prove the claim; you’ve merely shown that for each $x\in X$ of norm $1$, $$x_n^*(x)<\|x_n^*\|=\sup_{\|y\;\|=1}|x_n^*(y)|\;,$$ i.e., that $x_n^*$ does not attain its norm on $\{y\in X:\|y\|=1\}$.
Had you made the effort to write it intelligibly, thinking about what you were actually saying, you might have noticed that much of it makes no sense and that it does not in fact do what you wanted it to do. At the very least you would have made it possible for others to spot the problems and help with them much more easily.
Remember: A proof is just a particular kind of expository prose. It should consist of paragraphs of sentences. Yes, it will often contain special symbols, but DON’T use symbols just for the sake of using them. The object is to convince the reader that something is true, and you can’t do that if you can’t make yourself understood.


TITLE: Vectorizing Regularization in Linear Regression
QUESTION [1 upvotes]: I am wondering if someone could elaborate on the vectorized partial derivative of the MSE cost function. When writing code, I noticed that there seemed to be something wrong with the partial derivative terms that the class was outputting. I used the following formulas:
$$\frac{\partial J(\theta)}{\partial \theta}=\frac{1}{m}X^T(X\theta-y) \in R^{n+1}$$
$$\theta := \theta-\alpha (\frac{\partial J(\theta)}{\partial \theta})$$
Below, I have attached my work through the first iteration, where $\theta_0$ increases despite already being at an ideal value (0). If someone could explain to me where my error is, either in the assumption that $J(\theta)$ always decreases or in my math/formulas. Thanks.

REPLY [1 votes]: The first coordinate need not stay at $0$ and in this case, will not stay at $0$ since the coordinate of the gradient is non-zero. It will still converge back to $0$ if the step size is chosen carefully.
We have $\theta_0 = \begin{bmatrix} 0 \\ 0 \end{bmatrix}$.
$\theta_1 = \theta_0 - \alpha\begin{bmatrix} -\frac52 \\ -\frac{15}2 \end{bmatrix}$
In general,
\begin{align}\theta_{k+1} &= \theta_k -\alpha X^T(X\theta_k - y) \\
&=(I-\alpha X^TX)\theta_k + \alpha X^Ty \\
&= \begin{bmatrix} 1-4\alpha  & -10\alpha \\ -10\alpha & 1-30\alpha  \end{bmatrix} \theta_k +\alpha \begin{bmatrix} 10 \\ 30\end{bmatrix}\end{align}
We have to choose the step size carefully such that it converges. Let me pick $\alpha =0.01$ since the spectral radius is less than $1$.
octave:1> alpha = 0.01
alpha =  0.010000
octave:2> eig([1-4*alpha, -10*alpha; -10*alpha, 1-30*alpha])
ans =

   0.66599
   0.99401

Using the following Python code, we can see the progress:
import numpy as np

alpha = 0.01
A = np.array([[1-4*alpha, -10*alpha], [-10*alpha, 1-30*alpha]])
b = np.array([10*alpha, 30*alpha])
theta = np.array([0,0])

for i in range(1000):
    theta = np.matmul(A,theta) + b
    if i % 100 == 0:
        print(theta)

and we get the following output:
[0.1 0.3]
[0.16620987 0.94346837]
[0.09116498 0.96899279]
[0.05000337 0.98299276]
[0.02742651 0.99067164]
[0.01504325 0.99488346]
[0.00825112 0.99719361]
[0.00452568 0.99846072]
[0.00248231 0.99915571]
[0.00136153 0.99953691]