is_scalar_tower

Stream: general

[Johan Commelin]

Suppose that A is an R-algebra. Would is_scalar_tower R A A be an evil instance?
(We already have is_scalar_tower R R A.)

[Kevin Buzzard]

The point was to try and implement commutative triangles and that's certainly a commutative triangle...

[Kevin Buzzard]

What about when R=A?

[Johan Commelin]

Yup, that's exactly the case I'm worried about

[Heather Macbeth]

@Yury G. Kudryashov taught me today that when dealing with Prop, it doesn't matter to have duplicate instances.

[Johan Commelin]

Right, but I'm fearing that things might start to loop at some point

[Heather Macbeth]

Do you mean, if Lean is trying to find an instance of is_scalar_tower, knows about transitivity so is trying to fill in a gap using transitivity, but gets stuck on the self-instance of is_scalar_tower?

[Johan Commelin]

Maybe... I just get confused when thinking about these issues. They ought not to exist :confused:

[Yury G. Kudryashov]

This is ok as long as we don't define transitive insurance at the same time.

[Yury G. Kudryashov]

Otherwise we need to do something like docs#has_coe_t

[Reid Barton]

If we think of R as fixed then we can reuse the method of has_coe_t and R A A is the base case.

[Reid Barton]

If we let R vary as well... then it looks like some 2-dimensional version and I don't know what happens.

[Filippo A. E. Nuccio]

How did this discussion end up? I have lean complaining that it is missing is_scalar_tower α β β and I wonder if I should add it explicitely as an assumption.

[Eric Wieser]

I think we already have an instance for is_scalar_tower R A A, but it might need an import

[Eric Wieser]

Recently @Oliver Nash and I have been using is_scalar_tower α β β and smul_comm_class α β β to mean a weaker version of algebra α β

[Filippo A. E. Nuccio]

Can you point out at where you used it, so that I can check what to import?

[Eric Wieser]

No import needed, its docs#is_scalar_tower.right which is in the same file as the one that defines algebra.