generalizing `monoid_hom`

Stream: general

[Scott Morrison]

I wanted to try generalizing monoid_hom in src/algebra/group/hom.lean to look like:

@[ancestor one_hom mul_hom, to_additive]
structure monoid_hom (M : Type*) (N : Type*) [has_one M] [has_mul M] [has_one N] [has_mul N] extends one_hom M N, mul_hom M N

(rather than [monoid M] [monoid N])

[Scott Morrison]

and that line works, but in

@[to_additive]
instance monoid_hom.has_coe_to_one_hom {mM : monoid M} {mN : monoid N} :
  has_coe (M →* N) (one_hom M N) := ⟨monoid_hom.to_one_hom⟩

just a few lines later I get an error message from to_additive that I don't understand:

[Scott Morrison]

type mismatch at application
  M →+ N
term
  @add_monoid.to_has_zero M mM
has type
  has_zero M
but is expected to have type
  add_monoid M

Does anyone see what is going on?

[Yakov Pechersky]

Does it work if you rephrase it as

@[ancestor one_hom mul_hom, to_additive]
structure monoid_hom (M : Type*) [has_one M] [has_mul M] (N : Type*)  [has_one N] [has_mul N] extends one_hom M N, mul_hom M N

[Yakov Pechersky]

No reason that that should fix it unless there's some weird variable order in the to_additive code

[Scott Morrison]

The error message changes to

type mismatch at application
  M →+ add_monoid.to_has_zero M
term
  add_monoid.to_has_zero M
has type
  has_zero M
but is expected to have type
  Type u_2

[Yakov Pechersky]

Did you also change add_monoid_hom above?

[Yakov Pechersky]

Because that fixes it for me

[Yakov Pechersky]

(deleted)

[Yakov Pechersky]

@[ancestor zero_hom add_hom]
structure add_monoid_hom (M : Type*) (N : Type*) [has_zero M] [has_zero N] [has_add M] [has_add N]
  extends zero_hom M N, add_hom M N

[...]

@[ancestor one_hom mul_hom, to_additive]
structure monoid_hom (M : Type*) (N : Type*) [has_one M] [has_one N] [has_mul M] [has_mul N] extends one_hom M N, mul_hom M N

and just eval_apply needs to be fixed

[Yakov Pechersky]

eval_apply needs help inferring which eval is being discussed:

lemma eval_apply [monoid M] [comm_monoid N] (x : M) (f : M →* N) :
  (eval : M →* (M →* N) →* N) x f = f x := rfl

And that makes the file error free for me.

[Scott Morrison]

Ah!!! I didn't realise add_monoid_hom had already been defined above, and thought it was being generated, rather than just matched, by the to_additive on monoid_hom.

[Yakov Pechersky]

That sort of double-definition thing is so tricksy, I still don't really understand why it needs to be that way

[Yakov Pechersky]

For the record (if anyone has similar issues), I debugged this by comparing

#check @add_monoid_hom
#check @monoid_hom

after changing just monoid_hom and not add_monoid_hom. I saw that add_monoid_hom still had add_monoid constraints, and I couldn't imagine that to_additive was creating them out of thin air. Then I just did a F12 to go to definition.

[Scott Morrison]

I made a bit further progress, but the concrete categories are really upset. They expect the morphisms to need a single typeclass on source and target, and it looks a bit grungy to make it more flexible...

[Scott Morrison]

I could presumably generalize to mul_one_class :-)

[Scott Morrison]

That at least would relax caring about associativity.

[Yakov Pechersky]

Should we just fill out this diagram? https://en.wikipedia.org/wiki/Semigroup#/media/File:Magma_to_group4.svg

[Scott Morrison]

Possibly... gosh it would be nice to automate. :-)

[Yakov Pechersky]

I'm looking forward to what Yasmine is able to generate in that rosy future

[Damiano Testa]

While Kevin might have been joking about it, I really think that there is a (possibly small) use for additive structures with_one, just like there are multiplicative ones with_zero.

[Damiano Testa]

In most applications, they are merged by assuming semiring, but it is nice to be able to develop a little bit of theory without assuming the other operation

[Eric Wieser]

Note that the cost in terms of number of typeclasses of having a different typeclass for the presence or absence of each axiom is effectively exponential in number of axioms

[Eric Wieser]

So arguably there needs to be a stronger argument than "it is nice", Damiano!

[Scott Morrison]

Yes. I think the current motivation is trying to unify Lie algebras with other algebras to the extent possible, but this would require a lot of flexibility about units and associativity.

[Eric Wieser]

Doesn't that also require the lie stuff to start using * instead of the lie brackets?

[Eric Wieser]

I suppose we could have a to_lie like to_additive

[Oliver Nash]

Scott Morrison said:

Yes. I think the current motivation is trying to unify Lie algebras with other algebras to the extent possible, but this would require a lot of flexibility about units and associativity.

Speaking for myself, I wouldn't say "to the extent possible" but rather "to the extent that is immediately useful" and adopting a wait and see approach about some sort of possible future grand unification.

[Oliver Nash]

Eric Wieser said:

Doesn't that also require the lie stuff to start using * instead of the lie brackets?

Notation aside, we need to be able to talk about algebras that carry both associative and Lie products. I claim this need justifies the special Lie bracket product instead of *. For what it's worth, here's an example (in a messy branch which I will tidy up if/when a bunch of other stuff is resolved) where I do cross the boundary and usefully turn a Lie product into a *: https://github.com/leanprover-community/mathlib/pull/6723/files#diff-53e86155c95b35de6847327b3a7a3abac9132834bcab9e06644828a38aced107R67

[Eric Wieser]

Oliver Nash said:

Notation aside, we need to be able to talk about algebras that carry both associative and Lie products

Do you mean carry both at the same time with different notation, or a generalization that treats the two as synonyms?

[Oliver Nash]

I mean, they have two product operations (that are compatible). The standard example would be a (non-commutative) ring, thus carrying has_mul, where we define a second has_bracket product as ⁅x, y⁆ = x*y - y*x.

[Yury G. Kudryashov]

to_additive can't generate structures because Lean 3 meta programming doesn't let us (easily) define structures in meta code.

[Johan Commelin]

Can't we build a bit of API around emit_code_here that would allow us to define structures in meta code?