help debugging lemma

Stream: new members

[Vasily Ilin]

EDIT 2: this fails: #check map (Δ K), so map (Δ K) is the issue. But why?

EDIT: it looks like there was an extra parenthesis at the end of the definition. Once I removed it, it stopped complaining but now is giving me a deterministic timeout.

This gives me invalid definition, '|' or ':=' expected. What's wrong with it?

noncomputable lemma coassoc :
(tensor_product.assoc K K[X] K[X] K[X]) ∘ (map (Δ K) (alg_hom.id K K[X])) ∘ (Δ K)
= (map (alg_hom.id K K[X]) (Δ K)) ∘ (Δ K))
:= sorry

[Vasily Ilin]

For context, these are the definitions above:

notation K`[X]`:9000 := polynomial K

noncomputable def comul : K[X] →ₐ[K] K[X] ⊗[K] K[X] := polynomial.aeval ((polynomial.X ⊗ₜ 1) + (1 ⊗ₜ polynomial.X))

notation `Δ` :9000 := comul

noncomputable def counit : K[X] →ₐ[K] K := polynomial.aeval 0

[Yakov Pechersky]

We have the polynomial notation in the polynomial locale

[Vasily Ilin]

Thanks! I changed it. Do you have any ideas for why algebra.tensor_product.map (Δ K) might not work?

[Yaël Dillies]

As a rule of thumb, letters should not be notation. This bit me very recently: #13217