## Stream: new members

### Topic: Algebraic functions

#### Yakov Pechersky (Dec 27 2021 at 20:16):

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 (Dec 27 2021 at 21:58):

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 (Dec 27 2021 at 23:15):

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.

Last updated: Dec 20 2023 at 11:08 UTC