[Merged by Bors] - feat(algebra/monoid_algebra): Add an equivalence between add_monoid_algebra and monoid_algebra in terms of multiplicative

[eric-wieser]

---

• depends on: [Merged by Bors] - feat(data/finsupp): Make finsupp.dom_congr a ≃+ #4398

Note this ran into two bits of weirdness:

• Needing exact in conv mode: https://leanprover.zulipchat.com/#narrow/stream/113488-general/topic/Closing.20.60.E2.8A.A2.60.20goals.20in.20.60conv.60.20mode/near/212181256
• Proving p + q = p * q with rfl: https://leanprover.zulipchat.com/#narrow/stream/113488-general/topic/p.20.2B.20q.20.3D.20p.20*.20q.20solves.20by.20refl!/near/212218929

[eric-wieser]

https://leanprover.zulipchat.com/#narrow/stream/113488-general/topic/p.20.2B.20q.20.3D.20p.20*.20q.20solves.20by.20refl!/near/212218929

[eric-wieser]

Note that this line is the only reason map_domain_mul' exists - I can't work out any way to invoke the bundled map_domain_mul version here (apply monoid_algebra.map_domain_mul times out!).

[kbuzzard]

I believe that applying this mul' version is causing you problems. I think you are abusing type equality somewhere here. One of the inputs of add_monoid_algebra.map_domain_mul is supposed to be an add_hom, and you want to feed it to_add which is neither an add_hom nor a mul_hom. Your mul' hack has the same problem -- what can f be, if it is to satisfy the axioms of the proposition?

[kbuzzard]

I believe that applying this mul' version is causing you problems. I think you are abusing type equality somewhere here. One of the inputs of add_monoid_algebra.map_domain_mul is supposed to be an add_hom, and you want to feed it to_add which is neither an add_hom nor a mul_hom. Your mul' hack has the same problem -- what can f be, if it is to satisfy the axioms of the proposition?

[kbuzzard]

This is because you abused type equality when you applied map_domain_mul' -- it was an act of desperation by the unifier. If multiplicative was irreducible, which it should be in my opinion, then people would find this much harder to do and they would be forced to write better (in the sense of type correct) code.

[kbuzzard]

Aah! If you make multiplicative irreducible, we see that this line is also abusing type equality.

type mismatch at field 'to_fun'
  (finsupp.dom_congr multiplicative.to_add).to_fun
has type
  (multiplicative ?m_1 →₀ ?m_2) → ?m_1 →₀ ?m_2 : Type (max ? ?)
but is expected to have type
  add_monoid_algebra k G → monoid_algebra k (multiplicative G) : Type (max (max u₂ u₁) u₁ u₂)

This is the problem -- multiplicative is on the wrong side.

[kbuzzard]

protected def add_monoid_algebra.of_multiplicative [semiring k] [add_monoid G] :
  monoid_algebra k (multiplicative G) ≃+* add_monoid_algebra k G :=
{ map_mul' := λ x y, by {
    simp only [finsupp.dom_congr],
    sorry
  },
  ..finsupp.dom_congr multiplicative.to_add }

This typechecks even if multiplicative is irreducible. Note that I switched the order of the equiv! (and hence changed the name).

But now you need a result which applies to to_add so it can't have the hypotheses of your f in the mul' lemma.

[kbuzzard]

BTW making multiplicative irreducible shows that there is also type abuse going on in lift (which is already in mathlib) -- for example

type mismatch at application
  ⇑F a
term
  a
has type
  G
but is expected to have type
  multiplicative G

error in definition of lift.to_fun. Type abuse like this creates problems down the line (e.g. the earlier problem about p*q=p+q) and I've found that making stuff like multiplicative irreducible stops this sort of thing happening.

[eric-wieser]

This is the problem -- multiplicative is on the wrong side.

Thanks for catching this - but this was a mistake in just one of the two definitions.

[eric-wieser]

I think this is a case of two wrong make a right. After the simp only [finsupp.dom_congr], line, the goal is:

--                                 VVVVV add_monoid_algebra k G
map_domain ⇑multiplicative.of_add (x * y) =
-- ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^ monoid_algebra k multiplicative(G)
  map_domain ⇑multiplicative.of_add x * map_domain ⇑multiplicative.of_add y

map_domain doesn't know about *_monoid_algebra, so has signature (G →₀ k) → (multiplicative G →₀ k). At this point, we've done our first sneaky step in type abuse - we're considering the input an add_monoid_algebra, and the output a monoid_algebra - even though map_domain_mul' implies that both input and output are of the same type.

The second wrong is the tricks we already see in (f).

This would all be a lot easier if we could do away with add_*, and have monoid_algebra k G (+) and monoid_algebra k G (*) as our two versions...

[kbuzzard]

I think that sneaky steps in type abuse should be avoided if at all possible. Can't we also use to_add and of_add etc to work around this?

[eric-wieser]

I'd argue that type abuse is only a problem in definitions. In proofs, it shouldn't matter - as long as the theorem statement plays no tricks, then proof irrelevance means that abuse in the proof doesn't matter, right?

[eric-wieser]

Now, I could replace the proof

apply monoid_algebra.map_domain_mul',
intros p q,
simp only [of_mul_mul],
refl

with

    simp only [finsupp.dom_congr],
    rw monoid_algebra.mul_def,
    rw add_monoid_algebra.mul_def,
    simp_rw [map_domain_sum, map_domain_single, of_mul_mul],
    rw finsupp.sum_map_domain_index,
    { congr,
      ext a b,
      rw finsupp.sum_map_domain_index,
      { simp },
      { simp [mul_add] } },
    { simp },
    { simp [add_mul] },

but that amounts to a copy-paste of monoid_algebra.map_domain_mul, with:

• One monoid_algebra.mul_def replaced with add_monoid_algebra.mul_def
• f.map_mul replaced with of_mul_mul

Given the whole point of the multiplicative type tag is to avoid duplicate lemmas, is this really worth it?

[kim-em]

Is there a summary somewhere of what help you want with this PR? Perhaps you could create a thread on zulip explaining what's going on.

[eric-wieser]

At this point, @kbuzzard has provided most of the help I needed. All that remains is to decide if the weird intermediate goal state and dependence on unfolding multiplicative is ok.

[kbuzzard]

My understanding from Eric's comment is that this should be awaiting-author?

[kbuzzard]

I think that sneaky steps in type abuse should be avoided if at all possible. Can't we also use to_add and of_add etc to work around this?

[eric-wieser]

My understanding from Eric's comment is that this should be awaiting-author?

That wasn't what I meant by my comment. I'm looking for a reviewer to say "yes, there's no obvious way to avoid the type abuse" and/or "the type abuse is inevitable because this code operates on the boundary between type tags"

[jcommelin]

@eric-wieser I pushed a golf. I didn't make similar changes in the rest of the file, but I hope you can use this.

[eric-wieser]

Thanks for the golf @jcommelin, much simpler now. The nasty type abuse is now nicely hidden by convert

[jcommelin]

Thanks 🎉

bors merge

[bors]

Pull request successfully merged into master.

Build succeeded:

• Build mathlib
• Lint mathlib
• Lint style
• Run tests