deterministic timeout on definition of structure

Stream: new members

[Vasily Ilin]

I have the following file, which gives me deterministic timeout both on the structure and the notation. I can't figure out why.

import ring_theory.tensor_product
import algebra.monoid_algebra.basic
import data.polynomial.algebra_map

open_locale tensor_product

open algebra.tensor_product

variables (K : Type) [field K]
variables (V : Type) [semiring V] [algebra K V]

structure hopf_algebra extends algebra K V :=
(comul : V →ₐ[K] V ⊗ V)
(counit : V →ₐ[K] K)
(coassoc : (tensor_product.assoc K V V V) ∘ (map comul (alg_hom.id K V)) ∘ comul = map (alg_hom.id K V) comul ∘ comul)
(counit_left : (tensor_product.lid K V) ∘ (map counit (alg_hom.id K V)) ∘ comul = (alg_hom.id K V))
(counit_right : (tensor_product.rid K V) ∘ (map (alg_hom.id K V) counit) ∘ comul = (alg_hom.id K V))
(coinv : V →ₗ[K] V)

When I delete all but the comul line in the definition, it says "Loading" for 3 minutes and says "don't know how to synthesize placeholder" for $\otimes$. Is anything wrong with the imports? Here is the link to the file on Github: https://github.com/leomayer1/Hopf/blob/master/src/Hopf.lean

[Vasily Ilin]

Update: it looks like extends algebra K V was the culprit...

[Adam Topaz]

Vasily Ilin said:

Update: it looks like extends algebra K V was the culprit...

I think it makes sense to assume [algebra K V] as a typeclass parameter as opposed to extending it anyway

[Adam Topaz]

I.e.

import ring_theory.tensor_product
import algebra.monoid_algebra.basic
import data.polynomial.algebra_map

open_locale tensor_product

open algebra.tensor_product

variables (K : Type) [field K]
variables (V : Type) [semiring V] [algebra K V]

structure hopf_algebra :=
(comul : V →ₐ[K] V ⊗ V)
(counit : V →ₐ[K] K)
(coassoc : (tensor_product.assoc K V V V) ∘ (map comul (alg_hom.id K V)) ∘ comul = map (alg_hom.id K V) comul ∘ comul)
(counit_left : (tensor_product.lid K V) ∘ (map counit (alg_hom.id K V)) ∘ comul = (alg_hom.id K V))
(counit_right : (tensor_product.rid K V) ∘ (map (alg_hom.id K V) counit) ∘ comul = (alg_hom.id K V))
(coinv : V →ₗ[K] V)

[Vasily Ilin]

Thanks!