how to avoid `int_algebra` diamond

Stream: maths

[Kevin Buzzard]

The following instance

import algebra.algebra.basic

instance foo (A B C : Type*) [comm_ring A] [comm_ring B] [comm_ring C]
  [algebra A B] [algebra B C] : algebra A C :=
((algebra_map B C).comp (algebra_map A B)).to_algebra

causes problems, because algebra_int R : algebra ℤ R is an instance, so if R and S are comm_rings and [algebra R S] then foo and algebra_int give two non-defeq instances of algebra ℤ S. I don't see a way around this right now. This came up in #FLT regular .

[Riccardo Brasca]

It's probably an insane amount of work, but maybe the long term solution is to make the N action part of the definition of a semiring, and similarly for rings.

[Kevin Buzzard]

This still might not solve the problem though, because you can't have foo saying "if A is the integers then do it this way, else do it the obvious way".

[Kevin Buzzard]

As subscribers to #FLT regular will know, we're probably going to switch to a weaker version of foo which will suffice for the cases we're interested in. Johan suggested that there might already be a diamond in mathlib with rat.algebra_rat because there's some variant of foo which does exist for intermediate fields.

[Riccardo Brasca]

This what happened to monoids and groups, right? Now it's literally impossible to have two non defeq Z actions on a group if I understand what has been done

[Johan Commelin]

No, I don't think it's impossible. It got a bit harder to do it wrong though.

[Johan Commelin]

More importantly, it became possible to do it right.

[Kevin Buzzard]

Somehow it's not quite the same. We put an action of the integers on every group, but given a group homomorphism G -> H and an action of X on G you don't get an induced action of X on H.

[Riccardo Brasca]

Better than nothing :sweat_smile:

[Kevin Buzzard]

Here even if we make every ring a Z-algebra as part of the definition, we still can't have foo because it says precisely that A-algebra structures can be pushed along homomorphisms, and we don't want to push it in this one specific case when A=Z

[Yury G. Kudryashov]

I'm trying to redefine algebra in branch#redefine-algebra so that algebra_map is no longer part of the typeclass.

[Yury G. Kudryashov]

The only downside is that we loose nice definitional equalities for algebra_map but I think that we can live without them.

[Eric Wieser]

foo should never be an instance in the first place

[Eric Wieser]

Even if you remove algebra_map it creates diamonds in smul

[Kevin Buzzard]

Yury G. Kudryashov said:

I'm trying to redefine algebra in branch#redefine-algebra so that algebra_map is no longer part of the typeclass.

Oh wow, this seems to delete a bunch of code, which is a good sign. Do you think this solves the problem?

[Eric Wieser]

To be clear, "the problem" is not really anything to do with the thing at the top of this thread, but is instead:

import algebra.algebra.basic

example : algebra.id ℕ = algebra_nat := rfl -- fails, because...

example : @algebra.to_has_scalar _ _ _ _ (algebra.id ℕ) = @algebra.to_has_scalar _ _ _ _ algebra_nat :=
rfl -- while this works thanks to the nat-module refactor

example : @algebra.to_ring_hom _ _ _ _ (algebra.id ℕ) = @algebra.to_ring_hom _ _ _ _ algebra_nat :=
rfl -- this does not

Our choice are either:

• Declare we don't care about algebra_map having a convenient definition, and replace it with 1 • as Yury does in their branch.
• Decide we still do care about algebra_map having a convenient definition, and add semiring.of_nat / ring.of_int etc, as suggested in my scalar actions talk, which I made a feeble attempt to start in #9525.

[Yury G. Kudryashov]

With my approach we get a definition of algebra that works for non-associative algebras.

[Eric Wieser]

We already can express non-associative algebras as [module R A] [smul_comm_class R A A] [is_scalar_tower R A A], and indeed many of the instances for that already exist

[Eric Wieser]

(I'm sure you knew that, but maybe not every reader of your message did)

[Yury G. Kudryashov]

extends ... is exactly the definition in branch#redefine-algebra. I think that we should try to minimize the amount of data in typeclasses (unless we really have to introduce it to avoid diamonds).

[Johan Commelin]

I think I'm willing to give up defeq properties of algebra_map.

[Sebastien Gouezel]

The less data there is, the less risk of diamonds, so I'd also go for the dataless definition. Defeqness properties are just an implementation detail that we shouldn't rely on too much in any case.

[Yury G. Kudryashov]

I'll try to fix compilation of branch#redefine-algebra next week.

[Yury G. Kudryashov]

BTW, is docs#subalgebra.under a particular case of docs#subalgebra.restrict_scalars?

[Kevin Buzzard]

I only learnt about the "extend smul_comm_class and is_scalar_tower" approach from looking at Yury's branch. Wow! Is this the way forward? It removes data from the typeclass system so that's surely a good thing

[Eric Wieser]

It was in my FMM2021 presentation too ;), months ago

[Eric Wieser]

If we do go in Yury's direction, do we want to copy the recent change from [integral_domain X] to [comm_ring X] [is_domain X] by replacing [algebra R A] with [module R A] [is_algebra R A]?

[Kevin Buzzard]

What I like about this is that it shows that an R-algebra A is just a non-homogeneous multiplication R x A -> A satisfying some axioms

[Kevin Buzzard]

I had never really internalised this

[Eric Wieser]

Either way, the reality is that we end up with instances that almost ubiquitously look like

instance : algebra R my_type :=
{ ..my_type.smul_comm_class,
  ..my_type.is_scalar_tower,
  ..my_type.module }

like they already do for docs#is_domain.

[Kevin Buzzard]

Wait though, my current model is that it's just a map R -> A satisfying some axioms

[Kevin Buzzard]

How come the new model is better?

[Eric Wieser]

The old model is properties of (• 1) = algebra_map, the new one is properties of (•). You need 1 : A to talk about the first one

[Eric Wieser]

But I emphasize again that we already have the tools to talk about the situation without 1 : A, so really this is an argument about how we want to spell things and if anyone cares about algebra_map

[Eric Wieser]

In particular I suspect the key benefit to algebra_map is that algebra_map R R = id is (intended to be, and in most cases other than the one titling this thread already is) true definitionally. As another example, algebra_map ℝ ℂ r = ⟨r, 0⟩ is true definitionally right now. In Yury's branch, it becomes algebra_map ℝ ℂ r = ⟨r*1 - 0*0, r*0 + 0*1⟩ (see src#complex.has_scalar to see why).

[Johan Commelin]

@Eric Wieser Do you think it makes sense to remove algebra completely?

[Eric Wieser]

Only if we decide we no longer want to control algebra_map definitionally, as Yury has already done on their branch

[Eric Wieser]

My rough order of preference (ignoring the "what mathetaticians want to read" aspect) is:

1. Leave typeclasses as they are, add ring.of_int etc to fix the diamonds
2. Remove algebra with no replacement, use [smul_comm_class R A A] [is_scalar_tower R A A] as we already can today
3. Remove algebra, introduce class is_algebra R A extends smul_comm_class R A A, is_scalar_tower R A A for convenience
4. Remove algebra.to_ring_hom from the definition of algebra as Yury does in the branch above.

Note that in Lean 4, we can (probably) have instance [smul_comm_class R A A] [is_scalar_tower R A A] : is_algebra R A without forming a loop, which removes all the downsides of option 3 over option 2.

[Johan Commelin]

I really want Lean 4. Those loops will be so extremely useful!

[Eric Wieser]

I'm a little scared they might not work quite as well as described in the case of dependent typeclasses like module, but I guess we'll find out eventually and this isn't the thread to speculate about that.

[Kevin Buzzard]

I don't understand how ring.of_int would solve the problem of being able to construct the algebra A C instance from algebra A B and algebra B C in a safe way

[Johan Commelin]

@Kevin Buzzard But that can't be an instance anyway, because how can Lean find B if it only knows algebra A C. It won't know where to look (at least with the current algorithm).

[Eric Wieser]

I'm pretty sure requiring that to not form a diamond is the same as requiring a • (1 : B) • c = a • c definitionally for all choices of B

[Eric Wieser]

Which seems like a pretty outrageous requirement

[Patrick Massot]

Kevin Buzzard said:

What I like about this is that it shows that an R-algebra A is just a non-homogeneous multiplication R x A -> A satisfying some axioms
I had never really internalised this

This is really funny. I never heard of algebras seen as maps from R to A before mathlib. I was taught about the non-homogeneous multiplication version.

[Sebastien Gouezel]

Eric Wieser said:

My rough order of preference (ignoring the "what mathetaticians want to read" aspect) is:

1. Leave typeclasses as they are, add ring.of_int etc to fix the diamonds
2. Remove algebra with no replacement, use [smul_comm_class R A A] [is_scalar_tower R A A] as we already can today
3. Remove algebra, introduce class is_algebra R A extends smul_comm_class R A A, is_scalar_tower R A A for convenience
4. Remove algebra.to_ring_hom from the definition of algebra as Yury does in the branch above.

Note that in Lean 4, we can (probably) have instance [smul_comm_class R A A] [is_scalar_tower R A A] : is_algebra R A without forming a loop, which removes all the downsides of option 3 over option 2.

I'd vote for 3, and then 4. I don't really like 2 because of the "what mathematicians want to read" aspect, and I don't like 1 because it feels like opening the possibility to shoot oneself in the knee when there is no need for it.

[Kevin Buzzard]

What does 1 mean? You mean change the definition of ring to give it a canonical map from the integers? I don't understand how this fixes things. I like the look of 3 as well.

[Eric Wieser]

I suspect you don't understand how it fixes things because "things" to you is the example at the top of this thread that is not really possible at all. It fixes the examples I post above for the same reason that the smul ones are already fixed.

[Kevin Buzzard]

I guess the fix for my original issue is to make algebra_int not an instance

[Eric Wieser]

Your original issue will almost always make diamonds if algebra A C already exists, and it usually does. And the instance is illegal anyway as B can't be inferred

[Sebastien Gouezel]

Just to be clear: the instance in the first message of this thread is:

Kevin Buzzard said:

The following instance

import algebra.algebra.basic

instance foo (A B C : Type*) [comm_ring A] [comm_ring B] [comm_ring C]
  [algebra A B] [algebra B C] : algebra A C :=
((algebra_map B C).comp (algebra_map A B)).to_algebra

causes problems, because algebra_int R : algebra ℤ R is an instance, so if R and S are comm_rings and [algebra R S] then foo and algebra_int give two non-defeq instances of algebra ℤ S. I don't see a way around this right now. This came up in #FLT regular .

This can not be an instance, because there is no way to guess B from the goal algebra A C.

[Kevin Buzzard]

I see, so one just has to make the instance manually in the original setting where we know B

[Eric Wieser]

Exactly, and in most places we do just that (eg, see docs#algebra.prod.algebra, which provides all algebra structures not just the A (prod A A) one). The instance is missing for spitting_field which is what started this problem, but I have a local branch that starts fixing it.

[Eric Wieser]

Regarding @Sebastien Gouezel's objection to 1, I'd argue since ring already has three foot-guns (nsmul, zsmul, npow), adding two more (of_nat and of_int) is not all that much worse. I guess the counterargument is we had no other choice but to add the existing 3, but we do have a choice here.

[Yury G. Kudryashov]

:+1: for the counterargument.

[Eric Wieser]

Losing rfl : algebra_map ℝ ℂ r = ⟨r, 0⟩ and rfl : algebra_map α (α × α) a = (a, a) seems like the most visible annoyance with options 2, 3, and 4

[Yury G. Kudryashov]

We don't have rfl : a / b = a * b⁻¹!

[Johan Commelin]

How is that related?

[Eric Wieser]

Yury G. Kudryashov, That almost makes the opposite argument; div,inv, and div_eq_mul_inv are analogous to algebra_map, smul, and algebra.smul_def

[Kevin Buzzard]

I am coming to terms with (a) losing readability of internal definitions of things like groups and (b) losing rfl. I wouldn't like to claim that lists in [insert your favourite language here] are implemented as [insert your naive idea about how to implement lists in this langauge], so maybe other people shouldn't assume that groups are implemented in the obvious way. And rfl is overrated.

[Johan Commelin]

Yury G. Kudryashov said:

We don't have rfl : a / b = a * b⁻¹!

It's funny. Here we added extra data to tear the rfl apart. But with algebra_map we are removing data.

[Yury G. Kudryashov]

I meant that we can live without some very natural rfls.

[Eric Wieser]

Here we added extra data to tear the rfl apart.

More accurately, we added extra data in order to allow us to choose which things were rfl in concrete cases, and remove things that were rfl from abstract cases

[Yury G. Kudryashov]

(I'll be away for the next 2 hours)

[Eric Wieser]

So adding div_eq_mul_inv did not quite remove "very natural rfls", but it said "the choice of what is natural might depend on the type", and indeed was motivated by "very natural rfls" on ideals that didn't match the generic "very natural rfl".

[Eric Wieser]

In the same way, the natural rfl on a general (unitary) algebra is algebra_map R A r = r • (1 : A), but in a specific one there are almost always more natural choices

[Johan Commelin]

That's true.

[Eric Wieser]

But of course, the difference is that the cost of mistakenly keeping the default div is usually just some annoying non-rfl lemmas (usually things like coe_div not being rfl), whereas the cost of mistakenly keeping the default of_nat would be diamonds, just like it is for nsmul.

[Riccardo Brasca]

Someone has surely already said this, but at some point we will want that sequences converging to zero form a real algebra. And in this case algebra_map really does not exist.

[Sebastien Gouezel]

Eric Wieser said:

Here we added extra data to tear the rfl apart.

More accurately, we added extra data in order to allow us to choose which things were rfl in concrete cases, and remove things that were rfl from abstract cases

Even more accurately, we added extra data here to kill a non-defeq diamond in typeclass inference. Which, to me, is the only situation where we should fight for defeqness. In the algebra situation, I agree that adding fields for nat and int embedding would solve the nat and int algebra diamond, but I fear there may be other algebra-related diamonds elsewhere (yet to be seen). Just removing the data from the definition is a nice way to kill all of them, once and for all.

[Kevin Buzzard]

But we are not removing the data, right? Instead of giving R -> A we're giving R -> A -> A

[Johan Commelin]

Currently we are giving both

[Sebastien Gouezel]

We're using a module structure which, supposedly, is already there. So, we avoid adding more data on top of a module structure.

[Kevin Buzzard]

Oh so we are!

[Kevin Buzzard]

Regarding whether the definition of an A-algebra is a ring hom or a module with a multiplication, I think Atiyah--Macdonald say it all:

Let f:A->B be a ring homomorphism. If a in A and b in B, define a product ab:=f(a)b. This definition makes the ring B into an A-module...Thus B has an A-module structure as well as a ring structure, and these two structures are compatible in a sense which the reader will be able to formulate for himself. The ring B equipped with this A-module structure is said to be an A-algebra [in italics, so this is the definition]. Thus an A-algebra is, by definition, a ring B together with a ring homomorphism f : A -> B

In other words, both definitions are "the definition", by definition.

[Julian Külshammer]

They don't quite "say it all" as they have this strange standing assumption that B is commutative, so they are missing the condition that the image of the ring homomorphism is in the centre of B. :-)

[Johan Commelin]

All noncommutative rings are central simple algebras, right?

[Johan Commelin]

Anyway, I'm more and more starting to like (3). Should we have a vote?

[Eric Wieser]

@Sebastien Gouezel, my message you quote was about div_inv_monoid where AFAIR there was no diamond

[Eric Wieser]

Perhaps @Anne Baanen can recall the motivation there

[Eric Wieser]

(I think they're on vacation right now?)

[Johan Commelin]

I think the issue was that you can always define I * J for ideals. And then, for suitable rings, you can define I⁻¹ and I / J. These definitions are only compatible for Dedekind rings, or so. But they are useful in a more general setting.

[Anne Baanen]

I am indeed on vacation, but it's raining so I decided to check my notifications, apparently exactly at the right moment :)

The motivation behind div_inv_monoid was types like docs#fractional_ideal that have a well-defined (/) operator in general, and form a group (with 0) in some special cases. So you would get a non-defeq group -> has_div instance.

[Johan Commelin]

Right, I should have mentioned fractional ideals.

[Eric Wieser]

Ok, so the original div_inv_monoid motivation doesn't quite apply here as there is no separate has_algebra_map instance that exists independently of has_scalar - thanks for the explanation.

[Eric Wieser]

Sebastien Gouezel said:

but I fear there may be other algebra-related diamonds elsewhere (yet to be seen)

My hunch is that in the likely event these do exist, they will have corresponding scalar diamond problems anyway; by the time we've fixed those (assuming they're even fixable), it's probably not too much harder to fix the algebra_map problems at the same time. Of course it does still create more work, so I'm sympathetic to the avoid-the-risk viewpoint.