Extending algebra with a coproduct

Stream: new members

[Ali Ramsey]

Hi! I'm trying to play around a bit with coalgebras and algebras in Lean, but I'm having some trouble combining them. The minimal non-working example I have is

class Test₁ (F : Type u) (H : Type v) [Field F] [Ring H] extends Module F H where
  d : H →ₗ[F] H ⊗[F] H

class Test₂ (F : Type u) (H : Type v) [Field F] [Ring H] extends Algebra F H, Test₁ F H where
  m : H ⊗[F] H →ₗ[F] H := TensorProduct.lift (LinearMap.mk₂ F (· * ·) add_mul smul_mul_assoc mul_add mul_smul_comm)

which gives the error: unsupported dependent field in d : H →ₗ[F] H ⊗[F] H. When I swap Test₁ F H and Algebra F H after extends, I can use the coproduct d, but I get the error failed to synthesize instance IsScalarTower F H H on smul_mul_assoc and mul_smul_comm. This makes me think that Test₁ F H and Algebra F H are interfering with each other somehow - changing the element of Test₁ F H to be an F-linear map (without any tensor products) also fails, but changing it to be just any map H -> H works fine. So it seems to be some problem with the field F (also tried changing it to be a commutative ring or a commutative semiring, with no effect), but I can't think what it would be. Any help would be greatly appreciated.

[Eric Wieser]

What are you trying to do with m there?

[Eric Wieser]

Note that that says "m is some arbitrary bilinear map, which by default is multiplication, but may be something else"

[Eric Wieser]

Do you really not want it to always be multiplication?

[Eric Wieser]

This seems to work:

import Mathlib.Algebra.Algebra.Bilinear

open scoped TensorProduct

-- `Module` is no longer after the `extends`
class HasCoproduct (F : Type u) (H : Type v) [Field F] [Ring H] [Module F H] where
  d : H →ₗ[F] H ⊗[F] H

class CoAlgebra (F : Type u) (H : Type v) [Field F] [Ring H] extends Algebra F H, HasCoproduct F H

[Eric Wieser]

The problem with your original is that you are asking Lean to merge the Algebra.toSMul instance with Test₁.toModule, and it doesn't know how to do that without making a mess of the type of d

[Eric Wieser]

My version above avoids that issue because Test₁ doesn't actually contain the module structure, it assumes it.

[Ali Ramsey]

Eric Wieser said:

Do you really not want it to always be multiplication?

Ah yep! I've gotten into the habit of writing my maps as arbitrary before specifying them because the second part so often breaks, and I want to check everything else works before fixing it. Now that it seems to be working, I should delete that.

[Eric Wieser]

In fact, the map in question already exists as docs#LinearMap.mul'

[Ali Ramsey]

Eric Wieser said:

This seems to work:

-- `Module` is no longer after the `extends`
class HasCoproduct (F : Type u) (H : Type v) [Field F] [Ring H] [Module F H] where
  d : H →ₗ[F] H ⊗[F] H

class CoAlgebra (F : Type u) (H : Type v) [Field F] [Ring H] extends Algebra F H, HasCoproduct F H

Thank you! Do you have any advice on when to use extends, and when to use the square brackets? I've mostly been guessing based on what's already in mathlib. Also, I'm not quite sure why the order in which things are specified after extends matters?

[Ali Ramsey]

Eric Wieser said:

In fact, the map in question already exists as docs#LinearMap.mul'

I was trying to use that, but I kept getting a strange error message about types, so I went to the source and just copied the definition and that seemed to work

[Kevin Buzzard]

If you're interested in understanding the strange error message about types, then feel free to post a #mwe .

[Ali Ramsey]

(the error message was invalid field notation, type is not of the form (C ...) where C is a constant)

[Kevin Buzzard]

That means "you typed something wrong", it's not helpful unless we see the code as well.

[Ali Ramsey]

Kevin Buzzard said:

If you're interested in understanding the strange error message about types, then feel free to post a #mwe .

Ah ok, thank you

[Eric Wieser]

It probably means you forgot to write import Mathlib.Algebra.Algebra.Bilinear

[Eric Wieser]

Ali Ramsey said:

Ah yep! I've gotten into the habit of writing my maps as arbitrary before specifying them because the second part so often breaks, and I want to check everything else works before fixing it. Now that it seems to be working, I should delete that.

Just to be clear, := does not specify the map at all, and it's probably almost never what you want to use inside a class or structure.

[Ali Ramsey]

Eric Wieser said:

Ali Ramsey said:

Ah yep! I've gotten into the habit of writing my maps as arbitrary before specifying them because the second part so often breaks, and I want to check everything else works before fixing it. Now that it seems to be working, I should delete that.

Just to be clear, := does not specify the map at all, and it's probably almost never what you want to use inside a class or structure.

What do you mean by it doesn't specify the map? Is it not setting the map I want as the default?

[Ali Ramsey]

Eric Wieser said:

It probably means you forgot to write import Mathlib.Algebra.Algebra.Bilinear

Ah that's embarrassing, that was the problem... I think I thought it was in LinearAlgebra.TensorProduct for some reason

[Eric Wieser]

structure Two where
  two := 2

#eval Two.two {}  -- 2
#eval Two.two { two := 3 }  -- 3

[Ali Ramsey]

Would I just use : instead of := if I wanted it to be immutable then?

[Eric Wieser]

No, you just want a regular def:

structure Two where

def Two.two (_t : Two) := 2

#eval Two.two {}  -- 2
#eval Two.two { two := 3 }  -- error, no `two` field exists

[Ali Ramsey]

How does that work when the structure needs inputs like Test₁? Also, what is the _t in the brackets doing? Sorry, I haven't really used def much so I don't know the syntax. Is this all happening outside of the structure too?

[Eric Wieser]

Ali Ramsey said:

How does that work when the structure needs inputs like Test₁?

You gives these inputs to the function too

Also, what is the _t in the brackets doing?

That's just another input. The _ is because lean complains at you if you call it t, but it doesn't actually make any difference

Is this all happening outside of the structure too?

Yes: the only things that go inside the structure are things the caller provides themselves

[Jireh Loreaux]

def name : type := term just assigns the name name to the term with type type. If the def takes arguments like def name (arg : argType) : type := term[arg], where term[arg] is some term with occurrences of arg throughout, then this just assigns the name name to a term fun arg ↦ term[arg] which has type argType → type.

[Jireh Loreaux]

So, def twoNat : Nat := 2 just gives us another way to refer to 2 (in a semireducible way; which you can ignore for the moment if you don't know what it means). You can then do #eval 1 + twoNat -- 3.

[Ali Ramsey]

Sorry, I'm still really confused. If I take the example I had earlier of

class Test₁ (F : Type u) (H : Type v) [Field F] [Ring H] [Module F H] where
  d : H →ₗ[F] H ⊗[F] H

class Test₂ (F : Type u) (H : Type v) [Field F] [Ring H] extends Algebra F H, Test₁ F H where
  m : H ⊗[F] H →ₗ[F] H := LinearMap.mul' F H

as I understand it I shouldn't use :=, because it's mutable. So I should have

class Test₁ (F : Type u) (H : Type v) [Field F] [Ring H] [Module F H] where
  d : H →ₗ[F] H ⊗[F] H

class Test₂ (F : Type u) (H : Type v) [Field F] [Ring H] extends Algebra F H, Test₁ F H where

and some def below it (outside the class). But then what should this be? I've tried

def Test₂.m (F : Type u) (H : Type v) : Test₂ F H := LinearMap.mul' F H

and

def Test₂.m (F : Type u) (H : Type v) [Field F] [Ring H] : Test₂ F H := LinearMap.mul' F H

neither of which work. Do I need to put more in square brackets, like [Module F H]? Shouldn't it pick that up from Test₂ F H? Am I going about this completely the wrong way? And I'm confused as to why it really matters, since I won't be doing anything that should change m anyway?

[Eric Wieser]

I think it might be worth looking for some basic exercises that use def before trying to work out how to use typeclasses!

[Eric Wieser]

But here, you want something more like

def Test₂.m (F : Type u) (H : Type v)
  [Field F] [Ring H] [Test₂ F H] : H ⊗[F] H →ₗ[F] H := LinearMap.mul' F H

[Eric Wieser]

Shouldn't it pick ([Module F H] up from Test₂ F H?

Yes, but you didn't give it Test₂ F H! You wrote that after the colon, which means "I am going to build a Test₂ F H". You need it before the colon, which means "I am going to assume a Test₂ F H".

[Ali Ramsey]

Eric Wieser said:

I think it might be worth looking for some basic exercises that use def before trying to work out how to use typeclasses!

Yeah, that's fair. I didn't think I'd be using def at all, I figured I'd just be defining structures so I went straight to reading about that. Thank you for your help!

[Ali Ramsey]

I also just wanted to ask: how do you know when to put an argument in square brackets, and when to use extends?

[Eric Wieser]

It sounds like the "Structures and classes" tutorial I gave at https://lftcm2023.github.io/tutorial/index.html might be of interest to you; there's a video recording there, and some exercises about working with structures (and def as needed to use them)

[Ali Ramsey]

Oh nice, I'll take a look - thank you!