Zulip Chat Archive

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