ring_hom to algebra?

Stream: new members

[Jake Kesinger]

I'm having a bit of trouble showing that a structure is an algebra. I've got :

@[ext]
structure dual_algebra (R : Type*)[comm_ring R] (jj: R) :=
mk {} :: (re : R) (im : R)

and have proved a homomorphism incl : R →+* dual_algebra R jj with type Π (jj : ?M_1), ?M_1 →+* DUAL[?M_1,jj]

I'd like to do : instance : algebra R DUAL[R,jj] := by ring_hom.to_algebra incl
but it looks like the Π (jj : ?M_1) is causing a type mismatch

[Jake Kesinger]

I've generally been following Yuri Kudryashov's quaternion algebra : https://github.com/leanprover-community/mathlib/blob/7190444fb254067ff70b6c5942bd219261281cdd/src/data/quaternion.lean
but it looks like mathlib's changed out from under it.

I'm able to get it working up until "instance : algebra R ℍ[R, c₁, c₂]" but that's where I get stuck

[Adam Topaz]

#backticks would help

[Adam Topaz]

Could you provide a #mwe as well? In particular it's not clear how you define the ring structure on dual_algebra and/or incl.

[Jake Kesinger]

one sec ...

[Jake Kesinger]

https://gist.github.com/kesinger/ed7fb84bdcc78abce09db9c710527cb4

[Adam Topaz]

Thanks. It's just a syntax issue. Just replace the algebra R ... line with the following:

instance : algebra R DUAL[R,jj]  := ring_hom.to_algebra (incl _)

[Adam Topaz]

The point is that incl has an explicit variable (the jj) that was missing.

[Adam Topaz]

Also, when you write by ... you're entering tactic mode, which isn't needed here.

[Adam Topaz]

You could also write

instance : algebra R DUAL[R,jj] := ring_hom.to_algebra (incl jj)

if you want the sanity check that it's really the jj that's being used.

[Jake Kesinger]

ah heck I knew it had to be something simple
thanks!

[Adam Topaz]

No problem!