Replacing the definition of `algebra`

Stream: general

[Scott Morrison]

The current definition of an algebra has a severe problem: if you have type X with an existing module R X structure, it's impossible to put an algebra R X structure on it in such a way that the module R X structure derived from that algebra R X will be definitionally equal to the original one.

(I ran into this just now trying to prove Schur's lemma in an R-linear category with finite dimensional hom spaces: every X ⟶ Y has a module R (X ⟶ Y), but we also need to talk about the algebra R (X ⟶ X) structures.)

Oliver Nash and I were trying a few weeks ago to replace this definition, moving to

class algebra (R : Type u) [semiring R]
  (A : Type v) [semiring A] extends semimodule R A :=
(smul_mul_assoc' : ∀ (t : R) (a b : A), (t • a) * b = t • (a * b))
(mul_smul_comm' : ∀ (t : R) (a b : A), a * (t • b) = t • (a * b))

Unfortunately it was proving a lot of work. About three weeks ago we ground to a halt, and in the intervening time @Sebastien Gouezel's diamond refactoring PRs have arrived, and I'm not at all confident I can bring the existing half-working branch#replace_algebra_def up to master (I've just tried, and pushed, but who knows what state it is in... It's going to have further collisions with #7255.)

[Scott Morrison]

This alternative definition also has the nice feature that it generalises immediately to nonassociative and nonunital settings, unlike the current design.

[Scott Morrison]

I'm definitely game to work on this some more, but I thought it might be worth doing some coordination here first.

[Scott Morrison]

Perhaps the best strategy is actually to abandon the existing branch#replace_algebra_def (this makes me sad, and will probably make @Oliver Nash even sadder, as he'd done a lot of work here!), and start over, after both #7255 and @Anne Baanen's #7322.

[Scott Morrison]

Advice, complaints, or promises to contribute to the next attempt all welcome. :-)

[Eric Wieser]

I don't understand your first comment - surely smul := has_scalar.smul ensures definitional equality?

[Scott Morrison]

Hmm, okay, you're absolutely right, my problem in Schur's lemma is not about algebra. It is something even more basic, where I have an add_comm_group which is also a ring, and Lean can't see that it's only an add_comm_group in one way. :-(

[Scott Morrison]

If anyone feels like having a look at findim_endomorphism_simple_eq_one in schur.lean on branch#schur2, I am stumped. If I can just get the obtain line to work everything is fine.

[Sebastien Gouezel]

I had a look. The thing that creates problem is that

lemma findim_endomorphism_simple_eq_one
  [linear 𝕜 C] {X : C} [simple.{v} X] [I : finite_dimensional 𝕜 (X ⟶ X)] :

@finite_dimensional 𝕜 (@End C (@category.to_category_struct C _inst_1) X) _inst_4
    (@preadditive.category_theory.End.add_comm_group C _inst_1 _inst_2 X)
    (@linear.category_theory.End.module C _inst_1 _inst_2 𝕜
       (@euclidean_domain.to_comm_ring 𝕜 (@field.to_euclidean_domain 𝕜 _inst_4))
       _inst_6
       X)
  =
  @finite_dimensional 𝕜 (@End C (@category.to_category_struct C _inst_1) X) _inst_4
    (@ring.to_add_comm_group (@End C (@category.to_category_struct C _inst_1) X)
       (@preadditive.category_theory.End.ring C _inst_1 _inst_2 X))
    (@algebra.to_semimodule 𝕜 (@End C (@category.to_category_struct C _inst_1) X)
       (@comm_ring.to_comm_semiring 𝕜
          (@euclidean_domain.to_comm_ring 𝕜 (@field.to_euclidean_domain 𝕜 _inst_4)))
       (@ring.to_semiring (@End C (@category.to_category_struct C _inst_1) X)
          (@preadditive.category_theory.End.ring C _inst_1 _inst_2 X))
       (@linear.category_theory.End.algebra C _inst_1 _inst_2 𝕜
          (@euclidean_domain.to_comm_ring 𝕜 (@field.to_euclidean_domain 𝕜 _inst_4))
          _inst_6
          X)) :=
rfl

fails. If you try to congr it away, you see that the first problem it encounters is with two add_comm_group which are obvisouly the same, but where Lean can not see it. Probably for lack of beta-reduction (or whatever greek letter is meant here): two structures have the same fields which are all defeq, but the structures themselves are not defeq. A way out is to make sure that the first structure is also an assembly of stuff, and not a monolithic structure, by replacing the line 89 of preadditive/default.lean with

instance (X : C) : add_comm_group (End X) := { .. preadditive.hom_group X X }

Once this is done, Lean can see that both add_comm_groups are defeq. Then it runs into the second problem that

linear.category_theory.End.module X = algebra.to_semimodule

is not defeq either. I have not yet investigated this one.

[Scott Morrison]

Thanks very much @Sebastien Gouezel for having a look at this (I've been banging my head on this!!)

[Scott Morrison]

I found that

  obtain ⟨c, nu⟩ := @exists_spectrum_of_is_alg_closed_of_finite_dimensional 𝕜 _ _ (End X) _ _ _
    (by { convert I, ext; refl, ext; refl, }) (End.of f),

[Scott Morrison]

works, if I run

local attribute [ext] add_comm_group semimodule distrib_mul_action mul_action has_scalar

before embarking on the proof.

[Scott Morrison]

Then ext blasts through to the fields, and refl verifies they really do match up.

[Scott Morrison]

This exactly fits with your diagnosis.

[Scott Morrison]

I'll see if your { .. } trick (which I'm not sure whether I love or loath... :-) can solve the semimodule problem too.

[Oliver Nash]

Scott Morrison said:

Perhaps the best strategy is actually to abandon the existing branch#replace_algebra_def (this makes me sad, and will probably make Oliver Nash even sadder, as he'd done a lot of work here!), and start over, after both #7255 and Anne Baanen's #7322.

While I note that Eric has pointed out that we actually can solve the defeq problem by clobbering smul, I still plan to try to change the definition of algebra and I agree that we should probably just abandon branch#replace_algebra_def. I'm hoping to start again with a fresh branch in a week or so, hopefully after #7255 and #7322 have landed.

[Oliver Nash]

It's totally doable, just a matter of being persistent enough.

[Sebastien Gouezel]

I am really starting to wonder it we should ditch once and for all old style structures, and go for new style structures. It should solve this problem as the structures would not be a bunch of random fields, but nice functions to the substructures that the structure extends, that we could arrange for equality in this kind of situation. Of course, this would be a crazy refactor, but we will probably have to do it at some point (both to solve our performance problems, this kind of issue, and to port to Lean 4)...

[Scott Morrison]

:up: Oh boy. :-) We should have listened to Leo back in ... 2017?

[Oliver Nash]

I wonder if we could write some code to perform such a refactor. It would be an awesome validation of the value of digital formalisation if it could be done. Most of the effort for a human carrying out such a task would be pretty automatic and I bet that even when there is a choice to be made, it's usually from a smallish list so I could imagine some localised brute force approach would work.

[Eric Wieser]

Don't new style structures make this problem go away for only one "canonical" path through the algebra heirarchy DAG?

[Eric Wieser]

And leave exactly the same problem for non-canonical paths

[Sebastien Gouezel]

I still think most of it should be human-driven, since there are choices to be made (i.e., what is the most important path along which we will go down the instances -- this is what one should extend) and what is more accessory. But I think it wouldn't be that bad, in fact.

[Sebastien Gouezel]

Eric Wieser said:

Don't new style structures make this problem go away for only one "canonical" path through the algebra heirarchy DAG?

Yes, exactly, it only solves the problem along the canonical paths. Which we should choose wisely to minimize the number of issues.

[Eric Wieser]

My impression is that the problem we're seeing here is due to different paths being taken in different places

[Eric Wieser]

So making one or the other canonical won't help

[Sebastien Gouezel]

No, here it is really: define an add_comm_group instance foo on something, then defining a ring instance bar with { ..., .. foo}, and then bar.to_add_comm_group is not defeq to foo.

[Patrick Massot]

Sebastien Gouezel said:

I am really starting to wonder it we should ditch once and for all old style structures, and go for new style structures.

Really I'm not competent to judge. But Leo, who thought about the whole system more than anyone else by several order of magnitude, has a very strong opinion about this. I don't see how he could tell us more clearly that he thinks we should be using new structures.

[Kevin Buzzard]

One could imagine a "bit by bit" refactor where leaves are turned into new structures first.

What would a typical refactor look like, turning an old structure into a new structure? I personally don't know the difference between old structures and new structures, it's just some CS thing as far as I am concerned. One would delete the old_structure_cmd line, and then everything breaks, and then one redefines the structure causing the problem and/or adds a bunch of projection lemmas which used to be generated and now aren't?

[Kevin Buzzard]

Here's a concrete question. It seems to me that topology.algebra.open_subgroup is only imported by topology.algebra.nonarchimedean, which is not imported by anything. Does it make sense to see what happens if we delete set_option old_structure_cmd true in that file and refactor? Or does the whole thing have to be done in one go?

[Kevin Buzzard]

#7355 It wasn't that hard to change open_subgroup. What difficulties will one run into in general? Ones of the form I saw (cases U changed behaviour) or far nastier ones? One down, about 50 to go!

[Eric Wieser]

One type of the change that will come up - if you change comm_group to new style, you'll have to add a new mul_comm field.

[Kevin Buzzard]

OK so I just deleted all of them in one go (the vast majority are in src/algebra BTW) and the first thing that breaks is

/-- An `add_monoid` is an `add_semigroup` with an element `0` such that `0 + a = a + 0 = a`. -/
@[ancestor add_semigroup add_zero_class]
class add_monoid (M : Type u) extends add_semigroup M, add_zero_class M :=
(nsmul : ℕ → M → M := nsmul_rec)
(nsmul_zero' : ∀ x, nsmul 0 x = 0 . try_refl_tac)
(nsmul_succ' : ∀ (n : ℕ) x, nsmul n.succ x = x + nsmul n x . try_refl_tac)

I get an error on add_zero_class M in extends add_semigroup M, add_zero_class M and the error is

invalid 'structure' header, field 'to_has_add' from 'add_zero_class' has already been declared

So this means...what? add_semigroups and add_zero_classes both have an add, I guess, but the actual complaint is that add_semigroup.to_has_add and add_zero_class.to_has_add both exist.

Is one fix for this to literally not extend anything and just to write all the fields all over again and then just define the projections manually?

[Eric Wieser]

That's the only fix - you only get to extend things that don't overlap

[Eric Wieser]

So you have to decide which is most canonical

[Eric Wieser]

Eg, comm_ring can only extend one of ring, and comm_semiring

[Eric Wieser]

I suspect the correct choice is always the one with more data, in this case ring which has neg and sub

[Kevin Buzzard]

Right. So for example with add_monoid it seems the thing to extend is add_zero_class and then add assoc manually. I'm currently trying to figure out how to prove a monoid is a semigroup.

[Kevin Buzzard]

ooh suddenly loads of errors disappeared. This is quite satisfying. This is going to be a major but do-able refactor.

[Eric Wieser]

It might be worth agreeing on canonical paths before going too far with this

[Eric Wieser]

Eg, get a graphviz file with the instance heirarchy, and agree on the correct spanning tree and highlight it in a different color.

[Kevin Buzzard]

Yes this is why I started, to try and understand what the main issues were.

[Kevin Buzzard]

And to be quite honest the other reason I'm interested is that I trust Leo.

[Eric Wieser]

So I think the biggest impact of this change would be that we end up with tens of copies of (mul/add)_(assoc_comm)

[Eric Wieser]

A custom newish_structure command could generate those and the projections automatically though

[Kevin Buzzard]

Lol, we have to decide which of cancel_monoid -> left_cancel_monoid -> monoid and cancel_monoid -> right_cancel_monoid -> monoid is canonical

[Kevin Buzzard]

Yeah, it is difficult to do this in my head. I am now staring at cancel_comm_monoid and trying to figure out whether I should be going to left_cancel_monoid or comm_monoid. In fact I realise now I don't understand what is going on. Presumably we still need the four theorems that a cancel_monoid is a left/right_cancel_monoid and a left/right_cancel_monoid is a monoid? And presumably they all have to be instances? I'm just showing my ignorance of the problem.

[Kevin Buzzard]

OK so on the delete-old-structures branch I deleted all old_structure_cmds and I fixed what looked like one of the most challenging files -- algebra/group/defs (of course I'll have broken a lot of the files it depends on). You can see what the diff looks like here

[Eric Wieser]

Yes, anything you remove from extends has to be added as an instance

[Eric Wieser]

You could avoid tie breaking by saying neither left nor right is canonical, and have cancel_monoid extend monoid

[Julian Külshammer]

Given that mathlib (currently) seems to favour left modules, I would choose left_cancel_monoid.

[Sebastien Gouezel]

Anyway, there won't be a lot of things extending cancel_monoid, so this shouldn't really matter. There are essentially two kinds of classes: those that really play a role in the main hierarchy, and those that are merely gadgets to be able to state theorems in the right generality. The gadgets should probably never appear in the main hierarchy: there should be instances from the main classes to the gadgets, and theorems proved assuming the right gadget class.

[Mario Carneiro]

Eric Wieser said:

A custom newish_structure command could generate those and the projections automatically though

As one of the main proponents for old structures, I should probably say something about this. The main technical problem with new structures as currently implemented in lean 3 is that they outright reject diamond inheritance. What I think it should do instead is that given extends A, B, C it will classify the superclasses according to whether they contain any fields also present in any superclasses earlier in the list (in which case they are marked non-canonical). All canonical superclasses are embedded, and non-canonical superclasses get a pack/unpack parent instance. That way, this is the same as new structures when there are no diamonds, and the same as old structures when there are diamonds, and when there is a mix it just does the right thing

[Mario Carneiro]

This doesn't change the observation made up-thread that we should be careful to make sure we get the right spanning tree of canonical extensions

[Kevin Buzzard]

Eric Wieser said:

It might be worth agreeing on canonical paths before going too far with this

I don't understand what this means. If foo extends bar1 and bar2, and both bar1 and bar2 extend bar, then we still surely need all the theorems foo -> bar1, foo -> bar2, bar1 -> bar and bar2 -> bar, so surely a defeq diamond is inevitable? Are we talking about priorities? I am a complete amateur at type class inference, I have little understanding of how it works and little understanding of the difference between old and new structures and little understanding of the issues in this thread, but I am interested to learn, not least because I can now finally announce that Oliver Nash is going to be my post-doc for the next three years and I'd like to understand what he's doing!

[Mario Carneiro]

The issue isn't about defeq diamonds, but rather about minimizing the number of non-compositional(? - we need a name for this) instances, that is, instances where bar1 is not literally a member of foo and so we have to explode foo into fields and put them back together to produce an instance of bar1. These instances are large when foo has many fields and so we want to keep them to a minimum, but composition is necessarily diamond-free so they can't all be compositional instances

[Sebastien Gouezel]

An example: semiring could either extend monoid_with_zero and has_one, or it could extend add_comm_monoid and monoid. The second choice is clearly better than the first, since you will encounter much more often reductions of semirings to monoids and add_comm_monoids than to the more exotic monoid_with_zero.

[Kevin Buzzard]

PS this from the tabled typeclass resolution paper (the number is the number of routes to has_add, other than the 0 on has_add which is presumably an edge case)

routes_to_has_add.png

[Mario Carneiro]

Here's a simple demonstration of the difference between old style and new style. In both cases I'm simulating what extends would do if you didn't have the keyword:

class bar1 (α : Type) :=
(x : α)
(y : α)

class bar2 (α : Type) :=
(z : α)
(w : α)

-- new structure style inheritance
namespace new_structure
class foo (α : Type) :=
(to_bar1 : bar1 α)
(to_bar2 : bar2 α)

instance foo.bar1 {α} [foo α] : bar1 α := foo.to_bar1
instance foo.bar2 {α} [foo α] : bar2 α := foo.to_bar2
end new_structure

-- old structure style inheritance
namespace old_structure
class foo (α : Type) :=
(x : α)
(y : α)
(z : α)
(w : α)

instance foo.bar1 {α} [foo α] : bar1 α := {x := foo.x, y := foo.y}
instance foo.bar2 {α} [foo α] : bar2 α := {z := foo.z, w := foo.w}
end old_structure

[Mario Carneiro]

And here's an example where bar1 uses new style inheritance and bar2 uses old style inheritance (they can't both use new style in this case because of the shared field x):

class bar1 (α : Type) :=
(x : α)
(y : α)

class bar2 (α : Type) :=
(x : α)
(z : α)

namespace mixed_structure
class foo (α : Type) :=
(to_bar1 : bar1 α)
(z : α)

instance foo.bar1 {α} [foo α] : bar1 α := foo.to_bar1
instance foo.bar2 {α} [foo α] : bar2 α := {x := bar1.x, z := foo.z}
end mixed_structure

[Kevin Buzzard]

Oh! I thought that the interesting question was when you wanted to extend things which had overlapping fields. But here this is not the case(written before 2nd example). OK so now I understand the difference between old structures and new structures (indeed I was just re-reading the wiki page about this to try and get up to speed). Now why does this matter?

[Kevin Buzzard]

I should probably try to write a blog post about this, because it's the only way I will make any sense of it, and I have learnt from a lot of previous experience that if I learn something and then forget it again (something which happens all too often at my age) then I can re-learn it very efficiently if I've written it down in my own words.

[Mario Carneiro]

The achilles heel of new style structures is that you can't use them when there are overlapping fields (or rather you can still use the same method but you get the wrong result because you end up with two copies of the overlapped fields)

[Mario Carneiro]

in the first example there are no overlaps so new structures work fine

[Kevin Buzzard]

Right, but my understanding is that the argument is that we should now consider new style structures because it may or may not solve some problem or other.

[Mario Carneiro]

Right, so the question is how to be as new-structure-like as we can subject to the constraint that new style diamonds are impossible

[Kevin Buzzard]

I don't understand Scott's first claim at the top of this thread:

The current definition of an algebra has a severe problem: if you have type X with an existing module R X structure, it's impossible to put an algebra R X structure on it in such a way that the module R X structure derived from that algebra R X will be definitionally equal to the original one.

Maybe I should start by trying to do this exercise and understanding why this fails.

[Mario Carneiro]

In the mixed_structure example, I have broken the symmetry between the two parent structures by embedding bar1 as a field of foo and recombining fields for bar2. For lack of a better name I'm calling the bar1 kind "compositional inheritance" and bar2 non-compositional. We want as many compositional edges in the structure graph as possible, but the compositional edges have to be diamond free

[Kevin Buzzard]

I'm afraid I have this rather unfashionable trait in me whereby I like to understand stuff by seeing explicit examples, rather than just eating up the axioms and then becoming an expert :-/

[Mario Carneiro]

Ah, I haven't been talking about that issue, just new structures in general

[Kevin Buzzard]

Right but I'm keen to learn about everything right now

[Mario Carneiro]

src#algebra

[Mario Carneiro]

I'm not sure I see the problem either. Although you won't get the module structure itself to be the same, all the projections can still be defeq to the old ones, and this is all we generally expect (it's difficult to get defeq of the instances themselves in most cases)

[Kevin Buzzard]

but I thought we want defeq instances?

If every structure were completely flat, this would be impossible right, because eta reduction for structures is not definitional (if $z\in\mathbb{C}$ then {re := z.re, im := z.im} = z can't be proved by rfl). But surely it is going to be pretty much impossible to make everything definitional here?

[Mario Carneiro]

So here's an example of what I think scott is talking about

class bar1 (α : Type) := (x y : α)
class bar2 (α : Type) := (x z : α)
class foo (α : Type) := (x y z : α)

instance foo.bar1 (α) [foo α] : bar1 α := {x := foo.x, y := foo.y}
instance foo.bar2 (α) [foo α] : bar2 α := {x := foo.x, z := foo.z}

def bla (α : Type) := α
variables (α : Type) [B : bar1 (bla α)]
include B

instance bla.foo : foo (bla α) := {z := bar1.x, ..‹bar1 (bla α)›}
example : @foo.bar1 _ (@bla.foo α B) = B := rfl -- fails
example : @bar1.x _ (@foo.bar1 _ (@bla.foo α B)) = @bar1.x _ B := rfl
example : @bar1.y _ (@foo.bar1 _ (@bla.foo α B)) = @bar1.y _ B := rfl

[Mario Carneiro]

Now you might call this a non-defeq diamond, but this is actually fairly common in the hierarchy and mostly harmless. That is, we would classify this as a defeq diamond because all projections are defeq, even though the instances themselves are not

[Kevin Buzzard]

An example we have in mathlib is cancel_monoid extending both left_cancel_monoid and right_cancel_monoid as an old structure, both of which live over monoid. If we manage to make ourselves a monoid instance on a type, and then manage to extend it to a left_cancel_monoid and to a right_cancel_monoid, then type class inference might well be able to spit out the original monoid structure from the left_cancel_monoid. But if we then put the cancel_monoid instance into the type class inference machine, there is surely no way that both implications cancel_monoid -> left_cancel_monoid and cancel_monoid -> right_cancel_monoid can produce structures which are defeq to the ones we have already.

[Kevin Buzzard]

Oh so this is allowed? I thought that this was exactly what Scott was complaining about! This is not the issue we are trying to solve? As far as I can see it's surely provably unsolvable?

[Mario Carneiro]

Right, the issue is that we don't have eta for structures. It's basically impossible to make the first example work, unless bar1 happens to be a compositional superclass of foo. But as we've established it's not possible for everything to be compositional superclasses so new structures are going to end up making a new distinction that wasn't visible before matter

[Mario Carneiro]

To be sure it's a bit of a pain when you have non-defeq instances like this, because if you apply an unknown function on the instances (like nat.cast) then you have to unfold it enough to know that the function only uses the projections out of the instance, not the instances themselves

[Kevin Buzzard]

OK re-reading the thread and these comments have been very helpful -- thanks. So really this is not about diamonds, it's about something else, if "diamond" is being interpreted as "not even equal if you include eta reduction".

[Mario Carneiro]

The thing is, the more complicated definitions we pile on top of a structure the harder it becomes to prove that the function uses only projections, because all the higher level definitions will take an instance argument directly. In this case I think the definition in question is finite_dimensional