equiv for polynomial ring over opposite ring

Stream: Is there code for X?

[Yakov Pechersky]

I am not very familiar with the polynomial API. Is there code for the following?

import data.polynomial.monic

variables {R : Type*} [semiring R]

open polynomial

lemma sum_monomial_sum_monomial {S T : Type*} [semiring S] [semiring T] (p : polynomial R)
  (f : R → S) (g : S → T) (hg : g 0 = 0) :
  (p.sum (λ n r, monomial n (f r))).sum (λ n s, monomial n (g s)) =
  p.sum (λ n r, monomial n (g (f r))) :=
begin
  ext,
  simp only [coeff_sum, coeff_monomial, exists_prop, finset_sum_coeff, mem_support_iff,
             finset.sum_ite_eq', ite_eq_right_iff, ne.def, not_forall, sum_def],
  split_ifs with h h' h' h,
  { exact hg },
  { refl },
  { refl },
  { simp only [h', true_and, not_not, not_false_iff] at h,
    simp [h, hg] }
end

noncomputable example : (polynomial R)ᵒᵖ ≃+* polynomial Rᵒᵖ :=
{ to_fun := λ p, p.unop.sum (λ n r, monomial n (opposite.op r)),
  inv_fun := λ p, opposite.op (p.sum (λ n r, monomial n r.unop)),
  left_inv := λ p, by simp [sum_monomial_sum_monomial, opposite.unop_zero Rᵒᵖ, sum_monomial_eq],
  right_inv := λ p, by simp [sum_monomial_sum_monomial, opposite.op_zero R, sum_monomial_eq],
  map_add' := λ p q, by simp [sum_add_index],
  map_mul' := λ p q, begin
    induction p using opposite.op_induction,
    induction q using opposite.op_induction,
    dsimp,
    sorry
  end }

[Eric Wieser]

Is it any easier to prove this for add_monoid_algebra first?

[Eric Wieser]

The strategy here will be to use docs#add_monoid_hom.map_mul_iff and ext I think

[Eric Wieser]

In particular, this ext lemma helps:

/-- Add_monoid homs from the opposite type are equal if they are equal when composed with the regular type.

This allows further ext lemmas to chain. -/
@[ext]
lemma add_monoid_hom.op_ext {A B : Type*} [add_zero_class A] [add_zero_class B]
  (f g : Aᵒᵖ →+ B)
  (h : f.comp (op_add_equiv : A ≃+ Aᵒᵖ).to_add_monoid_hom =
       g.comp (op_add_equiv : A ≃+ Aᵒᵖ).to_add_monoid_hom) : f = g :=
add_monoid_hom.ext $ λ x, (add_monoid_hom.congr_fun h : _) x.unop

[Eric Wieser]

Full solution for add_monoid_algebra:

import algebra.monoid_algebra

variables {R : Type*} {I : Type*} [semiring R]

open finsupp opposite

-- simps doesn't do well here, but we could add some lemmas about `support` and `coe_fn` that are true by rfl
noncomputable def add_monoid_algebra.op_add_equiv :
  (add_monoid_algebra R I)ᵒᵖ ≃+ add_monoid_algebra Rᵒᵖ I :=
opposite.op_add_equiv.symm.trans
{ to_fun := λ p, ⟨p.support, op ∘ (p : I → R), λ i, mem_support_iff.trans (op_ne_zero_iff _).symm⟩,
  inv_fun := λ p, ⟨p.support, unop ∘ p, λ i, mem_support_iff.trans (unop_ne_zero_iff _).symm⟩,
  left_inv := λ p, finsupp.ext $ λ i, rfl,
  right_inv := λ p, finsupp.ext $ λ i, rfl,
  map_add' := λ p q, finsupp.ext $ λ i, rfl }

@[simp]
lemma add_monoid_algebra.op_add_equiv_single (i : I) (r : R):
  add_monoid_algebra.op_add_equiv (op (single i r)) = single i (op r) :=
begin
  ext j,
  classical,
  simp [add_monoid_algebra.op_add_equiv, single_apply, apply_ite op],
end

@[ext]
lemma add_monoid_hom.op_ext {A B : Type*} [add_zero_class A] [add_zero_class B]
  (f g : Aᵒᵖ →+ B)
  (h : f.comp (op_add_equiv : A ≃+ Aᵒᵖ).to_add_monoid_hom =
       g.comp (op_add_equiv : A ≃+ Aᵒᵖ).to_add_monoid_hom) : f = g :=
add_monoid_hom.ext $ λ x, (add_monoid_hom.congr_fun h : _) x.unop

noncomputable def add_monoid_algebra.op_ring_equiv [add_comm_monoid I] :
  (add_monoid_algebra R I)ᵒᵖ ≃+* add_monoid_algebra Rᵒᵖ I :=
{ map_mul' := λ p q, begin
    dsimp only [add_equiv.to_fun_eq_coe, ←add_equiv.coe_to_add_monoid_hom],
    revert p q,
    rw add_monoid_hom.map_mul_iff,
    ext,
    dsimp,
    rw ←op_mul,
    simp only [add_monoid_algebra.single_mul_single, add_monoid_algebra.op_add_equiv_single,
      ←op_mul, add_comm],
  end,
  ..add_monoid_algebra.op_add_equiv }

[Yakov Pechersky]

Will you PR this?

[Eric Wieser]

Probably not - are you happy to do so?

[Yakov Pechersky]

I'll try to understand how this works and how to specialize it to polynomial.

[Eric Wieser]

I'm also curious how hard it is to take that definition and apply it to polynomial; in the past they're defeq, but there's now a structure constructor to get slightly in the way. At any rate, it would be nice to have the def there for both (as then you get it for mv_polynomial too)

[Eric Wieser]

For monoid_algebra you can do a similar trick but additionally map I through op, to avoid needing commutativity. We don't have an additive_op which is why we can't do that for add_monoid_algebra , but it's not relevant to polynomials where I is nat anyway.

[Yakov Pechersky]

If I understand correctly, one should be able to fill the holes here?

noncomputable example : (polynomial R)ᵒᵖ ≃+* polynomial Rᵒᵖ :=
(ring_equiv.trans _
(add_monoid_algebra.op_ring_equiv :
  (add_monoid_algebra R (polynomial R))ᵒᵖ ≃+* _)).trans _

[Eric Wieser]

Ah, good point!

[Eric Wieser]

I think theres docs#polynomial.to_finsupp_iso_alg

[Yakov Pechersky]

docs#polynomial.to_finsupp_iso_alg

[Eric Wieser]

docs#polynomial.to_finsupp_iso is enough here

[Eric Wieser]

I guess it should be an alg_equiv not just a ring_equiv

[Eric Wieser]

add_monoid_hom.op_ext probably ought to be repeated for linear_map.op_ext, if that makes sense there. Maybe right actions screw with it.

[Yakov Pechersky]

#8537

[Yakov Pechersky]

alg_equivs require commutativity iiuc