Algebra.TensorProduct.rid as isomorphism over the larger ...

Stream: mathlib4

[Antoine Chambert-Loir]

Here is a MWE. If anyone can fill the sorry better than I did, I'll be happy!

import Mathlib.RingTheory.TensorProduct


section

variable {A B R : Type _} [CommSemiring R] [Semiring A] [Semiring B]
  [Algebra R A] [Algebra R B]

lemma AlgEquiv.toFun_eq_coe (e : A ≃ₐ[R] B) : e.toFun = e := rfl

end

open scoped TensorProduct

variable (A : Type _) [CommSemiring A] (R : Type _) [CommSemiring R] [Algebra A R]

namespace Algebra.TensorProduct

-- The natural `R`-algebra map from `R ⊗[A] A` to `R`.
def rid' : R ⊗[A] A →ₐ[R] R := { Algebra.TensorProduct.rid A R with
  map_one' := by simp only [AlgEquiv.toFun_eq_coe, map_one]
  map_zero' := by simp only [AlgEquiv.toFun_eq_coe, map_zero]
  commutes' := fun r => by
    simp only [algebraMap_apply, AlgEquiv.toFun_eq_coe, rid_tmul, one_smul] }

example : R ⊗[A] A →ₐ[R] R :=
  { Algebra.TensorProduct.rid A R with
  map_one' := sorry
  map_zero' := sorry
  commutes' := sorry }

[Eric Wieser]

I implemented this the other day

[Eric Wieser]

Its in a local branch that is waiting for #6035

[Eric Wieser]

(also, Algebra A R is very backwards for mathlib conventions!)

[Eric Wieser]

Kevin Buzzard said:

yeah the two sides are displaying differently, maybe this is an error and the lemma shouldn't have been deleted? The linter seems happy.

Lots of people ported FunLike stuff wrongly, then the linter told them to delete a bunch of lemmas. By the time reviewers came along and fixed the FunLike stuff, they usually didn't notice the missing lemmas.

[Eric Wieser]

Which is to say, this lemma should definitely be restored

[Antoine Chambert-Loir]

Eric Wieser said:

(also, Algebra A R is very backwards for mathlib conventions!)

What do you mean?

[Jireh Loreaux]

We almost always write Algebra R A where A is an R-algebra.

[Jireh Loreaux]

R for "Ring", A for "Algebra"

[Eric Wieser]

As opposed to "A ring" and "algebRa"

[Eric Wieser]

Eric Wieser said:

Its in a local branch that is waiting for #6035

Note that in order to have a nice defeq, this branch also depends on #6209 which in turn depends on #6207 ()

[Antoine Chambert-Loir]

Jireh Loreaux said:

We almost always write Algebra R A where A is an R-algebra.

Understood! (In French, where A is for « anneau », it is often the first letter that comes to my mind…)

[Eric Wieser]

Eric Wieser said:

I implemented this the other day

The Lean 4 version is here

[Eric Wieser]

It's not quite clear to me whether we want rid (a ⊗ₜ r) = a * algebraMap _ _ r or rid (a ⊗ₜ r) = r • a as the defeq

[Eric Wieser]

Ideally it would be rid (a ⊗ₜ r) = MulOpposite.op r • a, but that requires !3#10716

[Eric Wieser]

Anyway, #6417 now changes rid to have the structure you wanted

[Eric Wieser]

Eric Wieser said:

It's not quite clear to me whether we want rid (a ⊗ₜ r) = a * algebraMap _ _ r or rid (a ⊗ₜ r) = r • a as the defeq

@Antoine Chambert-Loir, @Kevin Buzzard: do you have any strong opinions on which one of these is the "canonical" defeq, or do you not care at all? This will propagate downstream to whether the base change of Q has the defeq:

• Q (a ⊗ₜ v) = a^2 * algebra_map _ _ (Q v) or
• Q (a ⊗ₜ v) = Q v • a ^ 2.

(Github discussion here)

[Notification Bot]

17 messages were moved here from #mathlib4 > AlgEquiv.toFun_eq_coe by Eric Wieser.

[Kevin Buzzard]

My instinct is not to care about what is defeq. As long as there's a lemma saying Q (a ⊗ₜ v) = a^2 * algebra_map _ _ (Q v) I don't care if the proof is rfl or not.

[Eric Wieser]

Would you be unhappy if only the Q (a ⊗ₜ v) = Q v • a ^ 2 lemma existed?

[Eric Wieser]

(with a rationale like "oh, that's the mathlib-canonical spelling, if you want it to look different you can do further rewrites yourself")

[Eric Wieser]

FWIW, I am finding it extraordinarily useful that I modified defeqs a few months ago such that docs#TensorProduct.lift.tmul (_ : lift f (x ⊗ₜ[R] y) = f x y) is now defeq

[Eric Wieser]

It avoids slow proofs of the form dsimp, rw [lift.tmul], dsimp

[Kevin Buzzard]

docs#TensorProduct.rid

[Kevin Buzzard]

I would definitely be unhappy if the Q(av)=a^2*\u Q(v) lemma didn't exist at all! How can that possibly not be mathlib-canonical? BTW is algebra_map a coercion yet?

[Alex J. Best]

Kevin Buzzard said:

My instinct is not to care about what is defeq. As long as there's a lemma saying Q (a ⊗ₜ v) = a^2 * algebra_map _ _ (Q v) I don't care if the proof is rfl or not.

I think we found that we also need the lemma,

@[simp]
lemma QuadraticForm.baseChange_associated (F : QuadraticForm R₁ M) :
  (associated : _ →ₗ[A] _) (F.baseChange A) = ((associated : _ →ₗ[R₁] _) F).baseChange A :=

is that easy enough with your changes Eric?

[Eric Wieser]

Yeah, that one is easy

[Eric Wieser]

Note that I don't have the full picture for what other people wrote here: it sounds like people worked on this in some secret Leiden repo

[Alex J. Best]

Well its public but just a workshop project so it's not publicized if that makes sense, https://github.com/alexjbest/ant-lorentz, certainly no secrets here!

[Eric Wieser]

I've ended up going with rid (a ⊗ₜ r) = r • a since Antoine seemed to be in favor and it has the advantage of being defeq to docs#TensorProduct.rid

[Notification Bot]

9 messages were moved from this topic to #PR reviews > #6342 by Eric Wieser.