Zulip Chat Archive

Stream: general

Topic: ring algebras


view this post on Zulip Kenny Lau (Sep 04 2018 at 08:51):

This problem has come up several times in this year, and I decided it's time to face it instead of to avoid it. This is the definition of an algebra over a commutative ring:

class algebra (R : out_param $ Type*) [comm_ring R] (A : Type*) extends ring A :=
(f : R  A) [hom : is_ring_hom f]
(commutes :  r s, s * f r = f r * s)

Mathematically there are no problems, but somehow every time I try to introduce this class, the class inferences become a mess, consistently. So, my question is: what is the best way to introduce this whole algebra thing to Lean?

view this post on Zulip Johan Commelin (Sep 04 2018 at 08:53):

Yeah! Go for it! I recognize the troubles, and I don't know the answer...

view this post on Zulip Johan Commelin (Sep 04 2018 at 08:53):

Concerning terminology... I think Bourbaki has a more general notion of algebra.

view this post on Zulip Johan Commelin (Sep 04 2018 at 08:54):

For example, a Lie algebra is an algebra.

view this post on Zulip Kenny Lau (Sep 04 2018 at 08:54):

MWE:

import data.polynomial

class algebra (R : out_param $ Type*) [comm_ring R] (A : Type*) extends ring A :=
(f : R  A) [hom : is_ring_hom f]
(commutes :  r s, s * f r = f r * s)

variables (R : Type*) [ring R]

instance ring.to_ℤ_algebra : algebra  R :=
{ f := coe,
  hom := by constructor; intros; simp,
  commutes := λ n r, int.induction_on n (by simp)
    (λ i ih, by simp [mul_add, add_mul, ih])
    (λ i ih, by simp [mul_add, add_mul, ih]), }

set_option trace.class_instances true
#check (by apply_instance : ring (polynomial ))

view this post on Zulip Johan Commelin (Sep 04 2018 at 08:55):

Don't you get diamonds this way?

view this post on Zulip Kenny Lau (Sep 04 2018 at 08:56):

What do you mean?

view this post on Zulip Johan Commelin (Sep 04 2018 at 08:56):

every algebra is already a ring, and now you are turning rings into algebras, so you are getting loops, not?

view this post on Zulip Johan Commelin (Sep 04 2018 at 08:56):

Maybe diamond is not the right word, but certainly loops.

view this post on Zulip Kenny Lau (Sep 04 2018 at 08:57):

I see

view this post on Zulip Kenny Lau (Sep 04 2018 at 08:57):

but it's an important fact that every ring is a Z-algebra, no?

view this post on Zulip Johan Commelin (Sep 04 2018 at 08:58):

Just as important as the fact that every abelian group is a Z-module.

view this post on Zulip Kevin Buzzard (Sep 04 2018 at 09:01):

Maybe that's the place to start this discussion. For example, my correspondence theorem is written for R-modules. How does one deduce the correspondence theorem for abelian groups? For mathematicians, the answer is easy -- "set R=Z; done". How do we do it in Lean?

view this post on Zulip Kevin Buzzard (Dec 08 2018 at 20:34):

At the time, the answer to this question was "just wait until the module refactor hits and then try again". Did you try again after the module refactor? What is still problematic?

view this post on Zulip Kenny Lau (Dec 08 2018 at 20:43):

@Kevin Buzzard the original MWE I posted above still works (in the sense that it still fails)

view this post on Zulip Kenny Lau (Dec 08 2018 at 20:43):

and if you define algebra differently, you run into another typeclass problem:

import data.polynomial

universes u v

class algebra (R : out_param $ Type u) (A : Type v) [out_param $ comm_ring R] [ring A] :=
(f : R  A) [hom : is_ring_hom f]
(commutes :  r s, s * f r = f r * s)

attribute [instance] algebra.hom

namespace algebra

variables (R : Type u) (A : Type v)
variables [comm_ring R] [ring A] [algebra R A]

instance to_module : module R A := module.of_core
{ smul := λ r x, f A r * x,
  smul_add := by intros; simp [mul_add],
  add_smul := sorry,
  mul_smul := sorry,
  one_smul := sorry }

@[simp] lemma mul_smul (s : R) (x y : A) :
  x * (s  y) = s  (x * y) :=
by rw [smul_def, smul_def,  mul_assoc, commutes, mul_assoc]

end algebra

view this post on Zulip Kenny Lau (Dec 08 2018 at 20:43):

in any case I'm quite tired of Lean's typeclass inference

view this post on Zulip Kevin Buzzard (Dec 08 2018 at 20:44):

@Mario Carneiro Help! Is this sort of thing still a problem?

view this post on Zulip Johan Commelin (Dec 08 2018 at 21:02):

@Kenny Lau I know I'm just commenting without having tried anything out. But I have been working with over-categories a bit. And there has been some work with CommRing, I understand. So couldn't we define algebra R as under R?

view this post on Zulip Johan Commelin (Dec 08 2018 at 21:02):

I hope that should just work.

view this post on Zulip Kenny Lau (Dec 08 2018 at 21:07):

@Johan Commelin could you show me what the code I just posted would become?

view this post on Zulip Johan Commelin (Dec 08 2018 at 22:01):

@Kenny Lau Sorry, I was distracted for a while. You have worked on colimits in CommRing haven't you?

view this post on Zulip Kenny Lau (Dec 08 2018 at 22:01):

I haven't

view this post on Zulip Johan Commelin (Dec 08 2018 at 22:01):

Aah, I thought you did, together with Ramon and Kevin.

view this post on Zulip Johan Commelin (Dec 08 2018 at 22:01):

Anyway, I think CommRing is currently being PR'd or about to be PR'd.

view this post on Zulip Kenny Lau (Dec 08 2018 at 22:02):

oh well I didn't use the category theory language

view this post on Zulip Johan Commelin (Dec 08 2018 at 22:02):

https://github.com/leanprover/mathlib/blob/master/category_theory/examples/rings.lean

view this post on Zulip Johan Commelin (Dec 08 2018 at 22:02):

So, there is something there.

view this post on Zulip Johan Commelin (Dec 08 2018 at 22:03):

Next, you could define under categories, as in https://github.com/leanprover-community/mathlib/blob/sheaf/category_theory/sheafy_preamble.lean#L180

view this post on Zulip Johan Commelin (Dec 08 2018 at 22:03):

And combining those, you would have commutative algebras over a commring.

view this post on Zulip Kenny Lau (Dec 08 2018 at 22:04):

yes, yes, yes, you could, provided that your URL doesn't contain "leanprover-community"

view this post on Zulip Johan Commelin (Dec 08 2018 at 22:04):

You only need that 1 line.

view this post on Zulip Johan Commelin (Dec 08 2018 at 22:04):

Comma categories are already in mathlib.

view this post on Zulip Johan Commelin (Dec 08 2018 at 22:05):

The functor.of.obj is currently being PR'd to replace functor.of_obj

view this post on Zulip Johan Commelin (Dec 09 2018 at 08:02):

Is there any chance that we will be able to use \Z notation as an object of Ring? Will we always have to type Ring.int? Somehow I wish that we can automatically coerce a type into an object of a category if the right type class instance is found... (maybe let's not worry if that is possible with modules, atm) It would be possible if that would at least be possible with the most basic examples, like nats, ints (modulo n), rats, reals, complexes.

view this post on Zulip Johan Commelin (Dec 09 2018 at 08:28):

@Kenny Lau This is what I came up with, after a little bit of hacking. https://github.com/leanprover-community/mathlib/blob/jmc-leftmod/category_theory/examples/left_module.lean
Need to go now. Of course there is lots to be done.

view this post on Zulip Kenny Lau (Dec 09 2018 at 09:00):

well... are you sure there will be no type-class issues?

view this post on Zulip Johan Commelin (Dec 09 2018 at 11:01):

@Kenny Lau Of course I can't be sure about that. But I think that the more you bundle, the less type class issues you will have. Otoh, the more you will have to be explicit about "coercions", and things like that.

view this post on Zulip Kenny Lau (Dec 09 2018 at 11:01):

so are you implying that the Lean typeclass system cannot be salvaged unless we bundle everything?

view this post on Zulip Johan Commelin (Dec 09 2018 at 11:03):

I don't know. The current type class system clearly isn't the most powerful thing imaginable. But for now I wouldn't mind trying more module stuff with less type class stuff.

view this post on Zulip Johan Commelin (Dec 09 2018 at 11:05):

@Kenny Lau Shall we try to define map f and comap f between R-Mod and S-Mod if f : R \hom S is a morphism of commutative rings?

view this post on Zulip Kenny Lau (Dec 09 2018 at 11:06):

sure

view this post on Zulip Johan Commelin (Dec 09 2018 at 11:08):

First complication: CommRing is not a full subcategory of Ring in the current setup. So we can't just speak of R-Mod.

view this post on Zulip Kevin Buzzard (Dec 09 2018 at 12:17):

Isn't Lean's type class system the most powerful thing you can imagine subject to the requirement that you promise that if you ever define two terms of a given typeclass then they will be defeq? The problem might be that mathematicians are expecting too much from it perhaps. One way of upgrading it is to weaken the promise from "defeq" to "either defeq, or the typeclass is provably a subsingleton".

view this post on Zulip Kevin Buzzard (Dec 09 2018 at 12:21):

Maybe there is an art to using priorities somehow? You could imagine that mathematicians could try to get better at this art. I've not seen this technique used before. @Chris Hughes you had problems with finsets or fintypes when you ended up with...something like two "different" empty lists representing the empty finset, right? Could you imagine carefully switching the priority of something to either very low or very high, to ensure that type class inference issues don't occur? Johan/Kenny, could you imagine doing the same thing here?

view this post on Zulip Chris Hughes (Dec 09 2018 at 12:47):

I don't think priority switching works. In the algebra example maybe who end up with the two different instances because you used a lemma that had to use the polynomial instance, because it was proved in more generality than just the integers, and likewise for the other instance.

view this post on Zulip Kenny Lau (Dec 09 2018 at 14:11):

will auxiliary types be the solution?

def to_module (i : algebra R A) : Type v := A

instance to_module.comm_ring : comm_ring (to_module i) :=
by dunfold to_module; apply_instance

instance to_module.module : module R (to_module i) := module.of_core
{ smul := λ r x, i r * x,
  smul_add := by intros; simp [mul_add],
  add_smul := by intros; simp [add_mul],
  mul_smul := by intros; simp [mul_assoc],
  one_smul := by intros; simp; exact one_mul x }

view this post on Zulip Chris Hughes (Dec 09 2018 at 14:12):

But you're still going to end up needing to prove the two instances are equal right? If you use lemmas about each of the different instances

view this post on Zulip Kenny Lau (Dec 09 2018 at 14:18):

I made it a structure

view this post on Zulip Kevin Buzzard (Dec 09 2018 at 14:20):

Maybe you can use convert cleverly at some point. Can you remove things from the type class inference machine? I can't help but think that it will somehow be possible to do all this, maybe we're not having the clearest ideas about how to do it

view this post on Zulip Chris Hughes (Dec 09 2018 at 17:43):

Maybe you can use convert cleverly at some point. Can you remove things from the type class inference machine? I can't help but think that it will somehow be possible to do all this, maybe we're not having the clearest ideas about how to do it

convert and congr are handy in these situations

view this post on Zulip Kenny Lau (Dec 09 2018 at 21:45):

(non-MWE incoming)

view this post on Zulip Kenny Lau (Dec 09 2018 at 21:45):

2018-12-09-2.png

view this post on Zulip Kenny Lau (Dec 09 2018 at 21:46):

"there's a type mismatch so I use convert which produces a proof by eq.mpr (eq.refl _)

view this post on Zulip Kenny Lau (Dec 09 2018 at 21:46):

so what is happening"

view this post on Zulip Kenny Lau (Dec 10 2018 at 02:41):

R[X] is an R-algebra so it has a module structure (where the scalar multiplication is C r * p). However R[X] is a finsupp so it also gets another module structure

view this post on Zulip Kenny Lau (Dec 10 2018 at 02:42):

The two module structures are not definitionally equal

view this post on Zulip Kenny Lau (Dec 10 2018 at 02:42):

can we get rid of the latter structure?

view this post on Zulip Reid Barton (Dec 10 2018 at 02:49):

Isn't the latter instance "the direct sum of R-modules is an R-module"?

view this post on Zulip Kenny Lau (Dec 10 2018 at 02:50):

right

view this post on Zulip Reid Barton (Dec 10 2018 at 02:59):

How does the second instance come up in practice? Are you manually unfolding to a finsupp?
Ah, do you mean the line instance : module α (polynomial α) := finsupp.to_module ℕ α?

view this post on Zulip Reid Barton (Dec 10 2018 at 03:00):

(does R[X] refer to data.polynomial?)

view this post on Zulip Kenny Lau (Dec 10 2018 at 03:04):

yes

view this post on Zulip Reid Barton (Dec 10 2018 at 03:06):

I think I mostly caught up on this thread. Deleting that instance makes sense, though I wouldn't be too surprised if you end up with new problems...

view this post on Zulip Kenny Lau (Dec 10 2018 at 08:15):

@Mario Carneiro what do you think about this?

view this post on Zulip Mario Carneiro (Dec 10 2018 at 08:17):

class algebra (R : out_param $ Type*) [comm_ring R] (A : Type*) extends ring A :=

this is trouble, because this will make ring A typeclass problems go looking for instances of algebra ? A

view this post on Zulip Kenny Lau (Dec 10 2018 at 08:18):

right, so I am not using this now

view this post on Zulip Kenny Lau (Dec 10 2018 at 08:18):

structure algebra (R : Type u) (A : Type v) [comm_ring R] [comm_ring A] :=
(to_fun : R  A) [hom : is_ring_hom to_fun]

view this post on Zulip Kenny Lau (Dec 10 2018 at 08:18):

I've been using this

view this post on Zulip Kenny Lau (Dec 10 2018 at 08:20):

@Mario Carneiro would there be any problem if we forgot about the module structure on R[X] induced by finsupp?

view this post on Zulip Kenny Lau (Dec 10 2018 at 08:21):

or maybe I should just prove that these two modules are isomorphic

view this post on Zulip Mario Carneiro (Dec 10 2018 at 08:22):

I thought an algebra was a ring that is also a module

view this post on Zulip Mario Carneiro (Dec 10 2018 at 08:22):

why not have it extend module, and assert that the function's induced smul matches the existing one

view this post on Zulip Kenny Lau (Dec 10 2018 at 08:24):

I thought we like definitional equalities

view this post on Zulip Kenny Lau (Dec 10 2018 at 08:25):

hmm, I see that can be a solution

view this post on Zulip Kevin Buzzard (Dec 10 2018 at 08:49):

I thought an algebra was a ring that is also a module

In CS you have to think really carefully about these sorts of things. In my mind, an RR-algebra is a ring which is also an RR-module, and an RR-algebra is the codomain of a ring homomorphism from RR -- the two notions are completely interchangeable. In Lean things seem to be much more delicate.

view this post on Zulip Kevin Buzzard (Dec 10 2018 at 08:50):

class algebra (R : out_param $ Type*) [comm_ring R] (A : Type*) extends ring A :=

this is trouble, because this will make ring A typeclass problems go looking for instances of algebra ? A

Can someone explain this to me? I don't know how the type class machine works at all and I would really like to know what its algorithm is.

view this post on Zulip Kevin Buzzard (Dec 10 2018 at 09:02):

Maybe what I need is some abstract examples of classes and instances and an explanation of what typeclass inference does to solve typeclass problems, and also an example of how type class inference can get into trouble and cause one of those huge log files which ends up in a max class instance resolution error.

view this post on Zulip Kevin Buzzard (Dec 10 2018 at 09:03):

If this isn't going to change in Lean 4 then perhaps it's worth documenting how all this works a bit better. Currently I just regard it as magic, but as Kenny once informed me, Lean does not do magic.

view this post on Zulip Kenny Lau (Dec 10 2018 at 09:09):

well in the future a neural network will resolve typeclass issues and none of us would know the algorithm

view this post on Zulip Kevin Buzzard (Dec 10 2018 at 09:10):

So Lean 7 does do magic after all.

view this post on Zulip Kevin Buzzard (Dec 10 2018 at 09:11):

But how does Lean 7 resolve the problem that it can find two non-defeq instances of topological_space X \times Y when X and Y are both metric spaces?

view this post on Zulip Kevin Buzzard (Dec 10 2018 at 09:11):

There is a fundamental issue unrelated to algorithms.

view this post on Zulip Kevin Buzzard (Dec 10 2018 at 09:13):

Can we feed useful theorems into the network and tell it to try applying them whenever it can't resolve type class issues? "If you can't prove that instance1 : foo A and instance2 : foo A are defeq, take look at the useful theorems about terms of type foo A which I told you about".

view this post on Zulip Kevin Buzzard (Dec 10 2018 at 09:13):

@Sebastian Ullrich am I living in a dream world?

view this post on Zulip Kevin Buzzard (Dec 10 2018 at 09:14):

This happens to mathematicians in practice, in particular in cases where foo A is a subsingleton and not a prop, and the two terms are not defeq but are trivially equal.

view this post on Zulip Kevin Buzzard (Dec 10 2018 at 09:15):

We want to do hard algebra in Lean but we cannot do it in a natural way and also use the typeclass system because our structures seem to be slightly too complex for it.

view this post on Zulip Kevin Buzzard (Dec 10 2018 at 09:16):

Well -- maybe we can use it -- maybe we just didn't figure out how to use it yet.

view this post on Zulip Sebastian Ullrich (Dec 10 2018 at 09:19):

Type classes only work well when all instances are unique. In other languages this property is enforced, but Lean's type class inference is too general to implement that in a sensible way.

view this post on Zulip Sebastian Ullrich (Dec 10 2018 at 09:20):

I haven't followed these threads closely enough to say what should be done about the examples that don't satisfy this property right now

view this post on Zulip Kevin Buzzard (Dec 10 2018 at 09:29):

By "unique" you mean that any two instances are defeq, I guess. Could you imagine a strengthening of the system which could handle non-defeq instances which are equal because of a theorem which the type class system "knows" ? Or is this just somehow completely computationally unfeasible? The simplest case is when the class is a subsingleton.

view this post on Zulip Sebastian Ullrich (Dec 10 2018 at 09:43):

The type class system doesn't even know anything about definitional equality, it just uses the same unification as any other part of Lean. I'm not sure if it would be weird to add some sense of definitional extensionality to just this one part of the system, or what that should look like.

view this post on Zulip Patrick Massot (Dec 10 2018 at 09:52):

What about the following modification: if the type class search terminally fails (not an intermediate fail during exploration), unfold the head symbol and try again? It seems to me this would make the type wrapping solution much more usable.

view this post on Zulip Sebastian Ullrich (Dec 10 2018 at 09:58):

@Patrick Massot The failed inference can involve many other classes, should they also be unfolded if possible? No, if you want a def to be unfolded by type class inference, it should be reducible.

view this post on Zulip Kevin Buzzard (Dec 10 2018 at 09:59):

Can one locally mark a def as reducible?

view this post on Zulip Patrick Massot (Dec 10 2018 at 09:59):

I don't want it to be reducible, I want is to be unfolded only in the situation I described

view this post on Zulip Patrick Massot (Dec 10 2018 at 10:00):

This is strictly an extension of the current algorithm, it takes over after everything else failed, and start again on a different problem

view this post on Zulip Kevin Buzzard (Dec 10 2018 at 10:01):

By "failure" you presumably do you not include "max type class instance resolution reached", which might just mean it's not trying hard enough.

view this post on Zulip Patrick Massot (Dec 10 2018 at 10:01):

Excluding maxdepth error

view this post on Zulip Patrick Massot (Dec 10 2018 at 10:02):

My vague understanding is that Coq canonical structure instance resolution does what I wrote

view this post on Zulip Patrick Massot (Dec 10 2018 at 10:04):

By the way, Sebastian, would it make sense to add shortcuts for the instance problems that Lean keeps solving for each proof (like has_bind tactic or has_one ℕ or has_add ℕ)?

view this post on Zulip Sebastian Ullrich (Dec 10 2018 at 11:33):

By the way, Sebastian, would it make sense to add shortcuts for the instance problems that Lean keeps solving for each proof (like has_bind tactic or has_one ℕ or has_add ℕ)?

Shortcut instances are a valid optimization, though they can also increase run time when the subproblem fails (whereas the full problem could still succeed) because there simply are more instances to check. In theory, better caching could also help there, which is the one part of the type class system that's likely to change in Lean 4.

view this post on Zulip Kenny Lau (Dec 10 2018 at 11:34):

how is the Lean 4 system better?

view this post on Zulip Sebastian Ullrich (Dec 10 2018 at 11:42):

I don't know, it hasn't changed yet


Last updated: May 18 2021 at 15:14 UTC