Using `Algebra.cast`

Stream: mathlib4

[Kevin Buzzard]

import Mathlib.Algebra.Algebra.Basic

/- mathlib has this:

````
/-- Coercion from a commutative semiring to an algebra over this semiring. -/
@[coe] def Algebra.cast {R A : Type*} [CommSemiring R] [Semiring A] [Algebra R A] : R → A :=
  algebraMap R A
````
-/

example (A B : Type) [CommSemiring A] [CommSemiring B] [Algebra A B] (a : A) : B := a -- fails

What am I doing wrong?

[Oliver Nash]

Are you expecting the coe attribute to mean that Lean will silently apply that function? AFAIK coe only affects behaviour of docs#Coe instances.

[Kevin Buzzard]

I don't understand coercions at all and don't really know where to look to read about them.

[Oliver Nash]

There's plenty I don't understand but I believe you need a docs#Coe (or docs#CoeOut etc.) instance for them to fire and the @[coe] decorator just affects whether the result expands or stays like a little up arrow.

[Oliver Nash]

(So in this case, you need to invoke docs#algebraMap manually.)

[Kevin Buzzard]

So this is the intention?

def fooexample (A B : Type) [CommSemiring A] [CommSemiring B] [Algebra A B] (a : A) : B := Algebra.cast a
def barexample (A B : Type) [CommSemiring A] [CommSemiring B] [Algebra A B] (a : A) : B := algebraMap A B a

example : @fooexample = @barexample := rfl

#print fooexample -- ↑a

#print barexample -- (algebraMap A B) a

Which of these is the simp normal form?

example (A B : Type) [CommSemiring A] [CommSemiring B] [Algebra A B] (a : A) (b : B) :
    Algebra.cast a = b := by
  -- ⊢ ↑a = b
  simp -- no progress
  sorry

example (A B : Type) [CommSemiring A] [CommSemiring B] [Algebra A B] (a : A) (b : B) :
    algebraMap A B a = b := by
  -- ⊢ (algebraMap A B) a = b
  simp -- no progress
  sorry

[Jireh Loreaux]

@Kevin Buzzard the Coe instances exist to allow Lean to find coercions. The @[coe] attributes exist to leave a trail of breadcrumbs after they've been inserted so that Lean can tell a coercion was applied. That is, how would Lean know something is a coercion after it inserts the corresponding function? Because that function has the attribute. This is how the delaborator knows to print an up arrow. It's also how norm_cast figures out how many coercions there are and where they are.

So, with just the attribute, the function will display as an up arrow in the infoview, but you have to write algebraMap in the source. With just the instance, you could coerce in the source, but in the infoview it would show up as algebraMap

[Kevin Buzzard]

The attribute is not on algebraMap, it's on Algebra.cast, which is the same as algebraMap except that it explicitly asks for source and target rings. Is this something to do with the design decision?

[Oliver Nash]

It looks like the reason for this attribute on docs#Algebra.cast is because of docs#algebraMap.coeHTCT

[Oliver Nash]

That doesn't answer your question (and in fact raises others). I'd like to know why we have docs#algebraMap.coeHTCT

[Kevin Buzzard]

(sorry -- a message got lost on the Eurostar: this was supposed be about #10125) Oh ha ha now we get this ⊢ (↑R A) 0 = 0 because the coercion is asking for R and A explicitly :-)