Zulip Chat Archive

Stream: maths

Topic: Can't find algebra instance


view this post on Zulip 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 }

view this post on Zulip 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...

view this post on Zulip 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

view this post on Zulip Adam Topaz (Oct 16 2020 at 14:31):

Okay, if I cheat and use local attribute [reducible] tensor_algebra then lean is indeed happy.

view this post on Zulip 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?

view this post on Zulip Adam Topaz (Oct 16 2020 at 14:36):

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

view this post on Zulip Reid Barton (Oct 16 2020 at 14:36):

nope, still a mystery

view this post on Zulip Adam Topaz (Oct 16 2020 at 14:37):

I'll just cheat with reducibility for now then.

view this post on Zulip 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