a • ↑b = ↑(a • b)

Stream: general

[Daniel Weber]

I need to prove

import Mathlib

set_option autoImplicit false

open Polynomial algebraMap

variable (R : Type*) [CommRing R]
variable (K : Type*) [Field K] [Module R K] [Algebra R[X] K]

example (a : R) (b : R[X]) : a • (b : K) = (a • b : R[X]) := by
  exact?

I think my typeclasses might be off and I need more/different ones. What are the correct typeclasses for this? I need K both as an algebra over R[X] and as a module over R, and they should be compatible.

I thought IsScalarTower R R[X] K is what I need but exact? still doesn't work.

[Kevin Buzzard]

You're right about IsScalarTower -- this says exactly that the two R-module structures you've put on K (one via R[X], the other direct) coincide. I'm not at lean right now and am slightly surprised that the coercions work -- I thought that for technical reasons there wasn't a coercion from A to B if B is an A-algebra; perhaps I'm behind the times.

To make progress I would use the fact that the IsScalarTower instance tells you that (a dot b) dot 1 = a dot (b dot 1) where this 1 is in K.

[Daniel Weber]

The coercions are due to open algebraMap, docs#algebraMap.coeHTCT. I'll try what you said, thanks

[Kevin Buzzard]

Oh nice!

There should be a theorem saying that \u a = a bub 1 and then maybe exact? will get you home after you've rewritten it on both sides

[Daniel Weber]

I managed to get it as

import Mathlib

set_option autoImplicit false

open algebraMap

variable (A B C : Type*) [Semiring A] [CommSemiring B] [Semiring C] [Module A C] [Module A B] [Algebra B C] [inst : IsScalarTower A B C]

example (a : A) (b : B) : a • (b : C) = (a • b : B) := calc
  a • (b : C) = a • (b • 1) := by congr 1; rw [Algebra.smul_def', mul_one]; rfl
  _ = (a • b) • 1 := (inst.smul_assoc ..).symm
  _ = (a • b : B) := by rw [Algebra.smul_def', mul_one]; rfl

Is this something which could be added to Mathlib?

[Kevin Buzzard]

You should relax the module condition to SMul R K in a PR. The symm indicates that you've stated it backwards. And is the proof definitely not just inst.smul_assoc? Equivalently are the first and third proofs not rfl?

[Kevin Buzzard]

(I'm still getting the hang of the coercion. My guess is that it's not rfl, in which case this looks good for a PR)

[Daniel Weber]

Kevin Buzzard said:

You should relax the module condition to SMul R K in a PR. The symm indicates that you've stated it backwards. And is the proof definitely not just inst.smul_assoc? Equivalently are the first and third proofs not rfl?

No, as docs#Algebra.algebraMap_eq_smul_one is not true by definition. Golfed it a bit to

import Mathlib.Algebra.Algebra.Defs

set_option autoImplicit false

open algebraMap

variable (A B C : Type*) [Semiring A] [CommSemiring B] [Semiring C] [SMul A C] [SMul A B] [Algebra B C] [inst : IsScalarTower A B C]

example (a : A) (b : B) : a • (b : C) = (a • b : B) := calc
  a • (b : C) = a • (b • 1) := congrArg _ (Algebra.algebraMap_eq_smul_one b)
  _ = (a • b) • 1 := (inst.smul_assoc ..).symm
  _ = (a • b : B) := (Algebra.algebraMap_eq_smul_one _).symm

How should this be called? algebraMap.coe_smul, maybe?

[Daniel Weber]

Looking at other coe_smul lemmas, it should be reversed

example (a : A) (b : B) : (a • b : B) = a • (b : C) := calc
  ((a • b : B) : C) = (a • b) • 1 := Algebra.algebraMap_eq_smul_one _
  _ = a • (b • 1) := inst.smul_assoc ..
  _ = a • (b : C) := congrArg _ (Algebra.algebraMap_eq_smul_one b).symm

[Kevin Buzzard]

I still think the equality should be the other way around (edit: sorry! You just reversed it), but it's always difficult with coercion lemmas because these are results which people genuinely want to apply in both directions. Yes that sounds like a good name. Try tagging it @[norm_cast] and then see if in your application you can just use norm_cast or push_cast instead of applying the lemma directly. If the stars are aligned you might be able to apply the lemma in both directions with those tactics.

[Daniel Weber]

Where in file#Mathlib/Algebra/Algebra/Defs should it be located? It has to be after algebraMap_eq_smul_one, so it can't be next to the other algebraMap.coe_

[Eric Wieser]

Doesn't this exist as docs#algebraMap_smul ?

[Eric Wieser]

It helps to write these statements without the implicit coercions when trying to find the lemma

[Daniel Weber]

Eric Wieser said:

Doesn't this exist as docs#algebraMap_smul ?

No, because the cast is on the RHS of the multiplication, and in docs#algebraMap_smul it's on the LHS

[Kevin Buzzard]

Yeah, in the notation of docs#algebraMap_smul with [IsScalarTower R A M] here we have A -> M being the algebra map, whereas in mathlib it's R -> A

[Kevin Buzzard]

Stick it just after algebraMap_eq_smul_one if it can't go before. Indeed it makes norm_cast work in your use case. Note: you don't have to name the IsScalarTower instance:

import Mathlib

@[norm_cast]
lemma algebraMap.coe_smul (A B C : Type*) [SMul A B] [CommSemiring B] [Semiring C] [Algebra B C]
    [SMul A C] [IsScalarTower A B C] (a : A) (b : B) : (a • b : B) = a • (b : C) := calc
  ((a • b : B) : C) = (a • b) • 1 := Algebra.algebraMap_eq_smul_one _
  _ = a • (b • 1) := smul_assoc ..
  _ = a • (b : C) := congrArg _ (Algebra.algebraMap_eq_smul_one b).symm

open Polynomial algebraMap

variable (R : Type*) [CommRing R]
variable (K : Type*) [Field K] [Module R K] [Algebra R[X] K] [IsScalarTower R R[X] K]

example (a : R) (b : R[X]) : a • (b : K) = (a • b : R[X]) := by
  norm_cast -- now works

[Kevin Buzzard]

PS the coercions don't need algebraMap open, they Just Work. This wasn't the case a few months ago IIRC, and is a very nice development. Edit: no I'm wrong! It's the name of the lemma which is opening the namespace.

[Daniel Weber]

Maybe this should also be stated as a lemma for algebraMap, not just for coercions

[Kevin Buzzard]

Now that algebraMap is a coercion there should be some decision about what the simp normal form is, and this is what should be used. But I only learnt that it was a coercion this morning, so I don't know what design decision was made.

[Kevin Buzzard]

Although given that the coercion is scoped, maybe this logic doesn't apply? You could try PRing both :-)

[Kevin Buzzard]

Can you move algebraMap_eq_smul_one earlier? That's another possibility I guess, if you want it by the other coercion lemmas.

[Daniel Weber]

Kevin Buzzard said:

Now that algebraMap is a coercion there should be some decision about what the simp normal form is, and this is what should be used. But I only learnt that it was a coercion this morning, so I don't know what design decision was made.

Even though the coercion is scoped I think there should be some kind of normal form. Currently simp can't prove algebraMap B C b = (b : C), even though rfl can, which is a bit annoying.

[Kevin Buzzard]

I'm not really competent to make design decisions like this, hopefully an expert will weigh in again.

[Eric Wieser]

There is no simp-normal form issue here, right? Coercions are just a pretty-printing concern, right?

[Eric Wieser]

Oh, the coercion is docs#Algebra.cast

[Daniel Weber]

Perhaps docs#Algebra.cast could be made an abbrev? Although I must admit I don't fully understand the consequences of that