# Zulip Chat Archive

## Stream: maths

### Topic: Can't find algebra instance

#### Adam Topaz (Oct 16 2020 at 14:24):

Can someone explain what's going on here?

```
import linear_algebra.tensor_algebra
import algebra.category.Algebra.basic
variables {R : Type*} [comm_ring R]
example {M : Module R} : algebra R (tensor_algebra R M) := by apply_instance -- WORKS
def free_of_module : Module R ⥤ Algebra R :=
{ obj := λ M,
{ carrier := tensor_algebra R M,
is_ring := algebra.semiring_to_ring R,
is_algebra := by apply_instance }, -- FAILS
map := sorry,
map_id' := sorry,
map_comp' := sorry }
```

#### Adam Topaz (Oct 16 2020 at 14:25):

Note that `algebra.semiring_to_ring`

also requires the algebra instance, so the fact that the `is_ring`

field works adds to the strangeness...

#### Reid Barton (Oct 16 2020 at 14:30):

Possibly related to https://leanprover.zulipchat.com/#narrow/stream/113488-general/topic/algebra.2Esemiring_to_ring.20breaks.20semimodule.20typeclass.20lookup/near/212584556

#### Adam Topaz (Oct 16 2020 at 14:31):

Okay, if I cheat and use `local attribute [reducible] tensor_algebra`

then lean is indeed happy.

#### Adam Topaz (Oct 16 2020 at 14:32):

The algebra instance for the tensor algebra is obtained by a `derive`

declaration. Is it possible there's some conflict with the fact that it's also tagged `irreducible`

?

#### Adam Topaz (Oct 16 2020 at 14:36):

Did that conversation ever lead to a satisfactory conclusion @Eric Wieser @Reid Barton ?

#### Reid Barton (Oct 16 2020 at 14:36):

nope, still a mystery

#### Adam Topaz (Oct 16 2020 at 14:37):

I'll just cheat with reducibility for now then.

#### Adam Topaz (Oct 16 2020 at 15:09):

Okay, I have the algebra/module adjunction here:

https://github.com/leanprover-community/mathlib/compare/tensor_algebra_adjunction

But this involves cheating with semireducibility :(

Last updated: May 14 2021 at 20:13 UTC