ring algebras

Stream: general

[Kenny Lau]

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?

[Johan Commelin]

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

[Johan Commelin]

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

[Johan Commelin]

For example, a Lie algebra is an algebra.

[Kenny Lau]

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 ℤ))

[Johan Commelin]

Don't you get diamonds this way?

[Kenny Lau]

What do you mean?

[Johan Commelin]

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

[Johan Commelin]

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

[Kenny Lau]

I see

[Kenny Lau]

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

[Johan Commelin]

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

[Kevin Buzzard]

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?

[Kevin Buzzard]

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?

[Kenny Lau]

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

[Kenny Lau]

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

[Kenny Lau]

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

[Kevin Buzzard]

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

[Johan Commelin]

@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?

[Johan Commelin]

I hope that should just work.

[Kenny Lau]

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

[Johan Commelin]

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

[Kenny Lau]

I haven't

[Johan Commelin]

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

[Johan Commelin]

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

[Kenny Lau]

oh well I didn't use the category theory language

[Johan Commelin]

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

[Johan Commelin]

So, there is something there.

[Johan Commelin]

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

[Johan Commelin]

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

[Kenny Lau]

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

[Johan Commelin]

You only need that 1 line.

[Johan Commelin]

Comma categories are already in mathlib.

[Johan Commelin]

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

[Johan Commelin]

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.

[Johan Commelin]

@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.

[Kenny Lau]

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

[Johan Commelin]

@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.

[Kenny Lau]

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

[Johan Commelin]

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.

[Johan Commelin]

@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?

[Kenny Lau]

sure

[Johan Commelin]

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

[Kevin Buzzard]

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".

[Kevin Buzzard]

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?

[Chris Hughes]

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.

[Kenny Lau]

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 }

[Chris Hughes]

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

[Kenny Lau]

I made it a structure

[Kevin Buzzard]

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

[Chris Hughes]

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

[Kenny Lau]

(non-MWE incoming)

[Kenny Lau]

2018-12-09-2.png

[Kenny Lau]

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

[Kenny Lau]

so what is happening"

[Kenny Lau]

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

[Kenny Lau]

The two module structures are not definitionally equal

[Kenny Lau]

can we get rid of the latter structure?

[Reid Barton]

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

[Kenny Lau]

right

[Reid Barton]

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 ℕ α?

[Reid Barton]

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

[Kenny Lau]

yes

[Reid Barton]

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...

[Kenny Lau]

@Mario Carneiro what do you think about this?

[Mario Carneiro]

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

[Kenny Lau]

right, so I am not using this now

[Kenny Lau]

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

[Kenny Lau]

I've been using this

[Kenny Lau]

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

[Kenny Lau]

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

[Mario Carneiro]

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

[Mario Carneiro]

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

[Kenny Lau]

I thought we like definitional equalities

[Kenny Lau]

hmm, I see that can be a solution

[Kevin Buzzard]

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 $R$-algebra is a ring which is also an $R$-module, and an $R$-algebra is the codomain of a ring homomorphism from $R$ -- the two notions are completely interchangeable. In Lean things seem to be much more delicate.

[Kevin Buzzard]

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.

[Kevin Buzzard]

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.

[Kevin Buzzard]

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.

[Kenny Lau]

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

[Kevin Buzzard]

So Lean 7 does do magic after all.

[Kevin Buzzard]

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?

[Kevin Buzzard]

There is a fundamental issue unrelated to algorithms.

[Kevin Buzzard]

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".

[Kevin Buzzard]

@Sebastian Ullrich am I living in a dream world?

[Kevin Buzzard]

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.

[Kevin Buzzard]

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.

[Kevin Buzzard]

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

[Sebastian Ullrich]

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.

[Sebastian Ullrich]

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

[Kevin Buzzard]

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.

[Sebastian Ullrich]

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.

[Patrick Massot]

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.

[Sebastian Ullrich]

@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.

[Kevin Buzzard]

Can one locally mark a def as reducible?

[Patrick Massot]

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

[Patrick Massot]

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

[Kevin Buzzard]

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

[Patrick Massot]

Excluding maxdepth error

[Patrick Massot]

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

[Patrick Massot]

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 ℕ)?

[Sebastian Ullrich]

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.

[Kenny Lau]

how is the Lean 4 system better?

[Sebastian Ullrich]

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