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