algebraMap of sub-algebras with `.mk`

Stream: mathlib4

[Xavier Généreux]

Given [Algebra R A] [Algebra A B] {S : Subalgebra R A} (a : A) (ha : a ∈ S),
At the moment when I need to do the following rewrites:

algebraMap S B (⟨a, ha⟩ : S) = algebraMap A B a

and

⟨(algebraMap A B) a, ha⟩ = (algebraMap A S) a

I need to use rw [show ... by rfl] to close the goal in my proof. Would it be desirable to have these as simp lemmas so that the original goals would get closed by simp?

Something like,

@[simp]
theorem Subalgebra.algebraMap_apply_mk {B : Type*} [CommRing B] [Algebra A B]
    {S : Subalgebra R A} (a : A) (ha : a ∈ S) :
  algebraMap S B (⟨a, ha⟩ : S) = algebraMap A B a := rfl


@[simp]
theorem Subalgebra.mk_algebraMap_apply {B : Type*} [CommRing B] [Algebra A B]
    {S : Subalgebra A B} (a : A) (ha : algebraMap A B a ∈ S) :
  ⟨(algebraMap A B) a, ha⟩ = (algebraMap A S) a := rfl

If so, I have looked a little bit the Subalgebra.basic file and I didn't find a good place for it. Does someone know where would these be a good fit?

Thanks a lot!

[Yaël Dillies]

Those two lemmas look a priori very reasonable! Maybe try PRing to see whether CI agrees?

[Aaron Liu]

How about

import Mathlib

@[simp]
theorem Subalgebra.algebraMap_apply {R A B : Type*} [CommSemiring R] [CommSemiring A] [Semiring B]
    [Algebra R A] [Algebra A B] {S : Subalgebra R A} (a : S) :
  algebraMap S B a = algebraMap A B a := rfl

is that also reasonable?

[Yaël Dillies]

I doubt so, because on the LHS you have an alg hom applied to a free variable, while on the RHS you do not

[Aaron Liu]

is that bad?

[Yaël Dillies]

I'm thinking that it could prevent lemmas like docs#MonoidAlgebra.algHom_ext, but clearly that's not a great example :thinking:

[Andrew Yang]

I think this lemma is a good idea, but @Eric Wieser might have other opinions.

[Xavier Généreux]

Yaël Dillies said:

Those two lemmas look a priori very reasonable! Maybe try PRing to see whether CI agrees?

See #27637.

[Yakov Pechersky]

Looks similar to treating Subring smul as smul of the ambient type, in #26912

[Xavier Généreux]

Really not sure where to put these as I don't see an obvious spot for it, if someone has a better idea let me know. Currently waiting for the checks.

[Eric Wieser]

Aaron's version looks better to me (if not simp)

[Eric Wieser]

Though it should be algebraMap_def and the coercion would be clearer written explicitly

[Xavier Généreux]

But it doesn't cover the case ⟨(algebraMap A B) a, ha⟩ = (algebraMap A S) a or am I missing something?

[Xavier Généreux]

And for the first case is the play to:

• Keep my version as a simp lemma and also add Aaron's lemma. (not tagged as simp)
• Or, simply always unfold the def? (So kill my lemma and simp Aaron's version.)