subalgebra coercion commutes with polynomial evaluation

Stream: new members

[Paul Nelson]

When the algebra is commutative, this is Subalgebra.aeval_coe. Is there a simple way to check this more generally? Something that would fill in the sorry here (note the difference in assumptions between the two examples, [CommRing A] vs. [Ring A]):

import Mathlib

open Polynomial

example
  (R : Type) [CommRing R]
  (A : Type) [CommRing A] [Algebra R A]
  (S : Subalgebra R A)
  (x : A)
  (hx : x ∈ S)
  (p : R[X])
  : (((aeval (R := R) x) p) : A) = ↑((aeval (R := R) (⟨ x, hx ⟩ : S)) p)
  := Subalgebra.aeval_coe S ⟨ x, hx ⟩ p

example
  (R : Type) [CommRing R]
  (A : Type) [Ring A] [Algebra R A]
  (S : Subalgebra R A)
  (x : A)
  (hx : x ∈ S)
  (p : R[X])
  : (((aeval (R := R) x) p) : A) = ↑((aeval (R := R) (⟨ x, hx ⟩ : S)) p)
  := by sorry

#check Subalgebra.aeval_coe
-- ∀ {R : Type u_1} {A : Type u_2} [inst : CommSemiring R] [inst_1 : CommSemiring A] [inst_2 : Algebra R A]
--   (S : Subalgebra R A) (x : ↥S) (p : R[X]), (aeval ↑x) p = ↑((aeval x) p)

(In everyday mathematical discourse, one would say "just replace S with the commutative subalgebra generated by x" to reduce from the second example to the first, but implementing that would seem to require many further checks along the lines of the above example.)

[Junyan Xu]

docs#Polynomial.aeval_subalgebra_coe should work, and docs#Subalgebra.aeval_coe should be generalized (or deprecated in favor of aeval_subalgebra_coe).

[Paul Nelson]

thanks! here's how I managed to massage that:

example
  (R : Type) [CommRing R]
  (A : Type) [Ring A] [Algebra R A]
  (S : Subalgebra R A)
  (x : A)
  (hx : x ∈ S)
  (p : R[X])
  : (((aeval (R := R) x) p) : A) = ↑((aeval (R := R) (⟨ x, hx ⟩ : S)) p)
  := by
  have h := Polynomial.aeval_subalgebra_coe p S ⟨ x, hx ⟩
  have : ↑(⟨ x, hx ⟩ : S) = x := rfl
  rw [this] at h
  exact symm h

[Junyan Xu]

You can just apply it directly:

import Mathlib
open Polynomial
example
  (R : Type) [CommRing R]
  (A : Type) [Ring A] [Algebra R A]
  (S : Subalgebra R A)
  (x : A)
  (hx : x ∈ S)
  (p : R[X])
  : (((aeval (R := R) x) p) : A) = ↑((aeval (R := R) (⟨ x, hx ⟩ : S)) p)
  := (aeval_subalgebra_coe p S ⟨x, hx⟩).symm