A tensor B is an A-algebra and a B-algebra

Stream: mathlib4

[Kevin Buzzard]

OK so Lean has this thing where for $A$ and $B$ commutative $R$-algebras, we have $A\otimes_R B$ is an $A$-algebra as an instance, but we're not allowed to have $A\otimes_R B$ being a $B$-algebra because of the stupid objection "if $A=B$ then there will be a diamond" which is (a) true and also (b) kind of dumb because 99% of the time $A$ is manifestly not equal to $B$ and rfl fails quickly.

But things are what they are, and the right algebra structure ($A\otimes B$ being a $B$-algebra) exists as a def but not as an instance. Except that sometimes you really do want it to exist. For example if $L$ is a $K$-algebra then you might want to make $\mathbb{A}_L$ into an $\mathbb{A}_K$-algebra (it doesn't matter if you don't know what the adeles $\mathbb{A}_K$ of $K$ is, all you need to know is that it's a commutative $K$-algebra and its construction is functorial in $K$), and then if it turns out that you're trying to prove that $L\otimes_K\mathbb{A}_K\cong\mathbb{A}_L$ (which we are) then you might want them to be isomorphic as $L$-algebras or as $\mathbb{A}_K$-algebras because these statements have different content and are both useful. For me this example is a concrete proof that @Eric Wieser 's suggestion "just try to write your tensor products the right way around to ensure that you only need the left algebra instance" is not viable in practice, at least in the kind of mathematics we're doing over in FLT.

So what I find I'm doing in FLT is that I've basically fixed an order for things ("adeles on the right", as is traditional in the literature) and when I want $L\otimes_K \mathbb{A}_K$ to be an $\mathbb{A}_K$-algebra I just make docs#Algebra.TensorProduct.rightAlgebra a local instance, or I make $A\otimes B$ into a $B$-algebra explicitly using this definition. I've been working fine with this until recently.

Recently I've realised that actually we want things like "if $A$ is a finite $R$-algebra then $A\otimes_R B$ is a finite $B$-algebra". For left algebra instances this is all in typeclass inference. For the right algebra theorem they're not instances because they can't be -- typeclass inference can't find the right algebra structure. So I'm having to not just remember Algebra.TensorProduct.rightAlgebra, I'm having to start remembering a list of declarations e.g. the FLT-specific Module.Finite.base_change_right which I need to make commutative algebra work painlessly.

Is there a way I can package everything up? So I can just type one line and all of a sudden $A\otimes_R B$ is a $B$-algebra, the system knows that if $A$ is finite as an $R$-module then $A\otimes_R B$ is finite as a $B$-module, and maybe the system also even forgets that $A\otimes_R B$ is an $A$-algebra? Can I do this with a...erm...scope, for example? Or is this likely to explode in my face? Is switching off instances in the middle of a file a safe thing to do?

[Yaël Dillies]

Kevin Buzzard said:

For the right algebra theorem they're not instances because they can't be -- typeclass inference can't find the right algebra structure. So I'm having to not just remember Algebra.TensorProduct.rightAlgebra, I'm having to start remembering a list of declarations e.g. the FLT-specific Module.Finite.base_change_right which I need to make commutative algebra work painlessly.

They can, actually. Instances of Prop-valued mixins over referring to non-instances are not a problem

[Eric Wieser]

That was true in Lean 3, but it's no longer entirely clear to me if it's true in Lean 4. I think I remember this coming up in one of @Anne Baanen's PRs

[Andrew Yang]

The only concern is performace I think. And the only place we have $A \otimes_R A$ in mathlib where this might be a problem is near the treacherous jacobi zariski.

[Eric Wieser]

Kevin Buzzard said:

if it turns out that you're trying to prove that $L\otimes_K\mathbb{A}_K\cong\mathbb{A}_L$ (which we are) then you might want them to be isomorphic as $L$-algebras or as $\mathbb{A}_K$-algebras because these statements have different content and are both useful. For me this example is a concrete proof that Eric Wieser 's suggestion "just try to write your tensor products the right way around to ensure that you only need the left algebra instance" is not viable in practice, at least in the kind of mathematics we're doing over in FLT.

I guess the extension of my suggestion is "passing through TensorProduct.comm repeatedly is better than fighting typeclass search", though that conjecture is unproven

[Eric Wieser]

Perhaps worth splitting this thread? (edit: done)

[Junyan Xu]

We could make rightAlgebra a scoped instance and put all instances referring to it within the same scope. I've adopted this approach here and here.

[Notification Bot]

13 messages were moved from this topic to #mathlib4 > Prop-valued instances in terms of non-canonical instances by Eric Wieser.