Algebraic functions

Stream: new members

[Yakov Pechersky]

I'm trying to play around with defining algebraic functions. Here's my attempt. What's going on with the dead-end-wrong simp in the bottom example? And do these algebra instances make sense?

import analysis.complex.polynomial

open polynomial

variables {R S : Type*}

instance polynomial.has_scalar_pi [semiring R] [has_scalar R S] :
  has_scalar (polynomial R) (R → S) :=
⟨λ p f x, eval x p • f x⟩

@[simp] lemma polynomial_smul_apply [semiring R] [has_scalar R S]
  (p : polynomial R) (f : R → S) (x : R) :
  (p • f) x = eval x p • f x := rfl

noncomputable instance polynomial.algebra_pi [comm_semiring R] :
  algebra (polynomial R) (R → R) :=
{ to_fun := λ p z, eval z p,
  map_one' := funext $ λ z, by simp,
  map_mul' := λ f g, funext $ λ z, by simp,
  map_zero' := funext $ λ z, by simp,
  map_add' := λ f g, funext $ λ z, by simp,
  commutes' := λ p f, funext $ λ z, mul_comm _ _,
  smul_def' := λ p f, funext $ λ z, by simp,
  ..polynomial.has_scalar_pi }

@[simp] lemma polynomial.algebra_map_pi_eq_eval [comm_semiring R] :
  (algebra_map (polynomial R) (R → R) : polynomial R → (R → R)) = λ p z, eval z p := rfl

lemma right (f : ℂ → ℂ) :
  aeval f (X - C ((2 : ℂ) • X) : polynomial (polynomial ℂ)) =
  aeval f (X - C ((2 : ℕ) • X) : polynomial (polynomial ℂ)) :=
begin
  ext1 x,
  rw nsmul_eq_mul,
  congr,
  ext1,
  simp [coeff_bit0_mul]
end

lemma wrong (f : ℂ → ℂ) :
  aeval f (X - C ((2 : ℂ) • X) : polynomial (polynomial ℂ)) =
  aeval f (X - C ((2 : ℕ) • X) : polynomial (polynomial ℂ)) :=
begin
  ext1 x,
  simp,
  -- 2 = 2 x ∨ x = 0
  sorry
end

[Kevin Buzzard]

lemma not_wrong (f : ℂ → ℂ) :
  aeval f (X - C ((2 : ℂ) • X) : polynomial (polynomial ℂ)) =
  aeval f (X - C ((2 : ℕ) • X) : polynomial (polynomial ℂ)) :=
begin
  ext1 x,
  simp,
  left, -- ⊢ 2 = 2 x
  refl, -- goals accomplished
end

[Yakov Pechersky]

Eric helped me understand that I was wrong about thinking that I was at a dead-end2 : ℂ → ℂ, its the constant function, not a scaling function.