Transitivity of Algebra instances

Stream: Is there code for X?

[Weiyi Wang]

I couldn't find the following in Mathlib

import Mathlib
def Algebra.trans (A B C : Type*) [CommSemiring A] [CommSemiring B] [Semiring C]
    [Algebra A B] [Algebra B C] :
  Algebra A C := Algebra.compHom C (algebraMap A B)

and I have got two questions

• Is this the right way to say this, or there is a better way in Mathlib?
• When I attempt to turn this into an instance, I got the following error. Why is it?

cannot find synthesization order for instance trans with type
  (A : Type u_1) →
    (B : Type u_2) →
      (C : Type u_3) →
        [inst : CommSemiring A] →
          [inst_1 : CommSemiring B] → [inst_2 : Semiring C] → [Algebra A B] → [Algebra B C] → Algebra A C
all remaining arguments have metavariables:
  CommSemiring ?B
  @Algebra A ?B inst✝⁴ CommSemiring.toSemiring
  @Algebra ?B C ?inst✝ inst✝²

[Kenny Lau]

If you need an instance of Algebra A C, Lean would need to guess the B out of thin-air, which is impossible. Remember that instances work backwards from how you state them.

[Kenny Lau]

Therefore the standard way to assume this in the statement of a theorem is by [Algebra A B] [Algebra B C] [Algebra A C] [IsScalarTower A B C], and if you actually construct the algebra instances then you use compHom or some other way

[Weiyi Wang]

I see. I am not super familiar with the usage of IsScalarTower yet, but good to learn an example of its usage! I'll try formulating my statements in that way

[Riccardo Brasca]

Note that it took us quite a lot of time to realize that the good design choice is IsScalarTower, this is a beautiful piece of formalization.

[Kenny Lau]

@Weiyi Wang https://loogle.lean-lang.org/?q=%E2%8A%A2+IsScalarTower+_+_+_+%E2%86%92+%28_+%3A+Prop%29

[Kevin Buzzard]

There is a subtlety here, which shows up in lots of different places. Here's another one: if you have a topological space and you want to say "now put the Borel sigma algebra on it" you don't just magically construct a sigma algebra in the middle of your proof, you put the extra assumptions [MeasurableSpace X] [BorelSpace X] -- the first is a "random" sigma algebra and the second is the assumption that it's the Borel sigma algebra. Similarly here you don't want to make Algebra A C, you want to assume C has a random A-algebra structure and then put the hypothesis that the triangle commutes into the typeclass system. This way you're getting the typeclass system to work for you, instead of fighting against it. The problem with your def is that it can't be an instance, because if C is already an A-algebra then you just made a second A-algebra structure on it, and it's equal to the one you already had but, crucially, the proof might not be rfl so now typeclass inference is going to break. By asking typeclass inference to supply the A-algebra structure you avoid this problem.

[Aaron Liu]

I think it's fine to magically construct the new structure in the middle of your proof, you just don't want to do that in the middle of your statement

[Junyan Xu]

By the same token as [TopologicalSpace X] [MeasurableSpace X] [BorelSpace X],
we should have [UniformSpace X] [TopologicalSpace X] [UniformityInducesTopology X]

[Eric Wieser]

Things start to get out of hand if we also have NormInducesDist and DistInducesTopology as well

[Sébastien Gouëzel]

I'm not sure what you mean. A topological space and a measurable space are orthogonal structures in general, and then BorelSpace X says they are related. While a uniform structure always gives rise to a topology, so it would be very weird to have them separately. It would be a little bit like having [Ring R] [AddCommGroup R] [RingInducesAddCommGroup R].

[Artie Khovanov]

Is Algebra.compHom C (algebraMap A B) the idiomatic way to stitch together two Algebras in the middle of a proof? Is there nothing like def Algebra.comp [Algebra A B] [Algebra B C] : Algebra A C?

[Snir Broshi]

Why are some instances orthogonal (topology and measure) but some aren't (ring and group, topology and uniformity)? IIUC this is only based on what people want to do with it right? If there were interesting maths to be done where the same type is a ring and a group that aren't related, we would have RingInducesGroup?
Also, thoughts on #32891? (a metric unrelated to the topology)

[Andrew Yang]

Artie Khovanov said:

Is Algebra.compHom C (algebraMap A B) the idiomatic way to stitch together two Algebras in the middle of a proof? Is there nothing like def Algebra.comp [Algebra A B] [Algebra B C] : Algebra A C?

Maybe algebraize [(algebraMap B C).comp (algebraMap A B)]. It might give you IsScalarTower A B C for free if you are lucky.

[Violeta Hernández]

Snir Broshi said:

Why are some instances orthogonal (topology and measure) but some aren't (ring and group, topology and uniformity)? IIUC this is only based on what people want to do with it right? If there were interesting maths to be done where the same type is a ring and a group that aren't related, we would have RingInducesGroup?
Also, thoughts on #32891? (a metric unrelated to the topology)

A ring is mathematically defined as a group with extra structure. Meanwhile topologies and measures are just different kinds of structures, where it so happens you can sometimes create one using the other.

[Snir Broshi]

I agree but I think these are the extremes, whereas the inner-product/norm/metric/uniformity/topology chain seems a bit more fluid to me.
Also I once wanted to have the CommMonoid on Int where the operation is max, and at the same time have the usual Ring structure.
Can we not have something like DistInducesTopology and the rest, and add some fancy macros to make them easier to handle?
(slightly tangential: made me think of having a @to_classes that converts every FooHom in a statement to FooHomClass)

[Artie Khovanov]

Andrew Yang said:

Maybe algebraize [(algebraMap B C).comp (algebraMap A B)]. It might give you IsScalarTower A B C for free if you are lucky.

Thank you this worked! It even game me the scalar tower in 1/2 cases.