algebra ℕ[X] R[X]

Stream: Is there code for X?

[Damiano Testa]

Dear All,

After having amply demonstrated my inability to find results in mathlib, I am now struggling to find if there is already and instance/def of the algebra in the title: if R is a semiring, is there and algebra instance algebra ℕ[X] R[X]?

Thanks!

[Heather Macbeth]

@Damiano Testa How about docs#polynomial.map_ring_hom for a start? Perhaps we have a way of turning a (semi)ring homomorphism into a scalar action.

[Heather Macbeth]

Ah yes, docs#ring_hom.to_algebra

[Adam Topaz]

docs#ring_hom.to_algebra I think?

[Damiano Testa]

Great, thank you both!

[Heather Macbeth]

And the last piece is docs#nat.cast_ring_hom

[Adam Topaz]

I think rings might have a $\mathbb{N}$-algebra instance?

[Heather Macbeth]

But to use docs#polynomial.map_ring_hom it needs to be in ring-hom form, not in algebra form.

[Damiano Testa]

The nat.cast_ring_hom I had via algebra ℕ R. Does it make a difference?

[Adam Topaz]

Well, you would have had to use algebra_map anyway... it makes no difference :)

[Damiano Testa]

Ok, thanks!

[Damiano Testa]

This reminds me of a different question. For a different thread, though!

Thank you so much!

[Damiano Testa]

Trying this out in my case, I specifically wanted to not assume that the target ring R was commutative. docs#polynomial.map_ring_hom docs#ring_hom.to_algebra has this assumption. So, instead, I prove it myself -- note the awkwardness in the field commutes where all the action takes place.

Is the instance below in mathlib?

Thanks!

import data.polynomial.eval

open_locale polynomial big_operators
open polynomial

noncomputable instance {R : Type*} [semiring R] : algebra ℕ[X] R[X] :=
{ smul := λ p q, polynomial.map_ring_hom (nat.cast_ring_hom R) p * q,
  to_fun := polynomial.map_ring_hom (nat.cast_ring_hom R),
  map_one' := map_one (map_ring_hom (nat.cast_ring_hom R)),
  map_mul' := map_mul (map_ring_hom (nat.cast_ring_hom R)),
  map_zero' := map_zero (map_ring_hom (nat.cast_ring_hom R)),
  map_add' := map_add (map_ring_hom (nat.cast_ring_hom R)),
  commutes' := λ p q, begin
    simp_rw [coe_map_ring_hom],
    refine polynomial.induction_on' p (λ f g fq gq, by simp [add_mul, mul_add, fq, gq]) _,
    intros n c,
    rw [monomial_eq_C_mul_X, polynomial.map_mul, polynomial.map_pow, polynomial.map_X, mul_assoc,
      X_pow_mul, ← mul_assoc, ← mul_assoc, eq_nat_cast, polynomial.map_nat_cast, nat.cast_comm]
  smul_def' := λ p q, rfl }

For some further context: I am trying to prove facts about docs#pochhammer by proving it with the commutative assumption on the semiring and then transporting them using docs#pochhammer_map.

[Damiano Testa]

I found docs#ring_hom.to_algebra' that gets me closer and isolates exactly the commutativity requirement:

noncomputable instance {R : Type*} [semiring R] : algebra ℕ[X] R[X] :=
begin
  refine ring_hom.to_algebra' (polynomial.map_ring_hom (nat.cast_ring_hom R)) (λ p q, _),
  simp_rw [coe_map_ring_hom],
  refine polynomial.induction_on' p (λ f g fq gq, by simp [add_mul, mul_add, fq, gq]) _,
  intros n c,
  rw [monomial_eq_C_mul_X, polynomial.map_mul, polynomial.map_pow, polynomial.map_X, mul_assoc,
    X_pow_mul, ← mul_assoc, ← mul_assoc, eq_nat_cast, polynomial.map_nat_cast, nat.cast_comm]
end

From a maths point of view, this is the statement that X commutes with everything and nat also commutes with everything.

[Eric Wieser]

Note that ring_hom.to_algebra rarely has the right definitional properties, as it defines algabra.to_has_scalar badly

[Eric Wieser]

Does your proposed instance create a diamond when R = ℕ[X]?

[Damiano Testa]

Eric, how can I test whether this instance creates a diamond? Is it just by playing around or is there a more systematic way of checking?

[Eric Rodriguez]

try check whether your instance is equal to algebra.refl N[X] by refl; if it is not, it will make a diamond

[Damiano Testa]

I am not understanding something. I tried

-- I have this instance, with proof, in my file
noncomputable instance new_instance (R : Type*) [semiring R] : algebra ℕ[X] R[X] := sorry

example : new_instance ℕ = algebra.refl ℕ[X] :=
-- error says: unknown identifier 'algebra.refl'

[Anne Baanen]

It should be docs#algebra.id

[Damiano Testa]

Thanks Anne!

The answer appears to be that they are not defeq:

example : new_instance ℕ = algebra.id ℕ[X] := rfl
type mismatch, term
  rfl
has type
  ?m_2 = ?m_2
but is expected to have type
  new_instance ℕ = algebra.id ℕ[X]

[Alex J. Best]

Are they even mathematically eq?

[Alex J. Best]

If R = nat[X] then nat[X][X] has two algebra structures depending on which X you look at.

[Damiano Testa]

Alex, I would imagine so [EDIT: I think that they are equivalent mathematically]. This means that if I unfold enough the previous non-rfl proof, I can actually prove it, right?

[Damiano Testa]

Alex, wrt to the second question, it can get confusing, but I imagine that there will be some book-keeping to see which X represents the new and which the old variable.

[Eric Wieser]

I think this is a similar discussion to the one we've had in the context of monoid_algebraelsewhere, although perhaps it's not the same

[Eric Wieser]

Well, it's at least true mathematically:

@[simp] lemma nat.cast_ring_hom_nat : nat.cast_ring_hom ℕ = ring_hom.id ℕ :=
ring_hom.ext nat.cast_id

example : new_instance = algebra.id ℕ[X] :=
begin
  ext : 1,
  change  polynomial.map_ring_hom (nat.cast_ring_hom _) r = r,
  simp,
end

[Anne Baanen]

(You can also prove the first one by docs#ring_hom.eq_nat_cast) Wait, we only have that for eq_int_cast and eq_rat_cast?

[Eric Wieser]

I'm going to PR the set all of three simp lemmas for that first bit in a second

[Damiano Testa]

I found out that, for my specific application to pochhammer, there is also a docs#pochhammer_map lemma that does essentially what I want and I do not need the instance for this.

Indeed, this lemma takes a ring_hom and produces the corresponding polynomial.map only for pochhammer.

[Damiano Testa]

Thanks Eric!

[Anne Baanen]

Eric Wieser said:

I'm going to PR the set all of three simp lemmas for that first bit in a second

Could you also add a generic ring_hom.eq_nat_cast (f : ℕ →+* R) : f = nat.cast_ring_hom?

[Damiano Testa]

This presumably means that, once Eric's PR goes through, the proof of docs#pochhammer_map can be shortened, right? Or possibly may not even be needed anymore?

[Eric Wieser]

To match docs#ring_hom.eq_int_cast'?

[Anne Baanen]

And while we're at it, docs#nat.subsingleton_ring_hom should really say unique (ℕ →+* R)

[Anne Baanen]

Eric Wieser said:

To match docs#ring_hom.eq_int_cast'?

Yes please! Or even both variants, since I'm so busy making up work to do :)

[Eric Wieser]

We already have docs#eq_nat_cast for the other variant

[Eric Wieser]

#13001

[Eric Wieser]

Damiano Testa said:

This presumably means that, once Eric's PR goes through, the proof of docs#pochhammer_map can be shortened, right? Or possibly may not even be needed anymore?

I'm struggling to follow what you're suggesting here

[Eric Wieser]

This looks like the more general case of the instance you were asking for:

noncomputable instance {R S : Type*} [comm_semiring R] [semiring S] [algebra R S] :
  algebra R[X] S[X] :=
{ smul := λ p q, polynomial.map_ring_hom (algebra_map R S) p * q,  -- this probably could be better
  to_ring_hom := polynomial.map_ring_hom (algebra_map R S),
  commutes' := λ p q, begin
    simp_rw [ring_hom.to_fun_eq_coe, coe_map_ring_hom],
    refine polynomial.induction_on' p (λ f g fq gq, by simp [add_mul, mul_add, fq, gq]) _,
    intros n c,
    rw [monomial_eq_C_mul_X, polynomial.map_mul, polynomial.map_pow, polynomial.map_X, mul_assoc,
      X_pow_mul, map_C, C_mul', C_mul', algebra_map_smul, algebra_map_smul, mul_smul_comm],
  end,
  smul_def' := λ p q, rfl }

but again, it creates at least a non-defeq diamond

[Damiano Testa]

Eric Wieser said:

Damiano Testa said:

This presumably means that, once Eric's PR goes through, the proof of docs#pochhammer_map can be shortened, right? Or possibly may not even be needed anymore?

I'm struggling to follow what you're suggesting here

My comment was non-sense. I think that I got carried away and hoped that simp would have done miracles.