open_locale tensor_product issue

Stream: general

[Kevin Buzzard]

Can I not have tensor products in ring theory and tensor products in monoidal categories at the same time?

import ring_theory.noetherian
import algebra.category.Module.monoidal

-- uncommenting the next line fixes something and breaks something else
-- open_locale tensor_product

variables (R M N : Type) [comm_ring R] [add_comm_group M] [module R M]
[add_comm_group N] [module R N]

-- works iff locale open
theorem fg_of_pseudoinvertible :
  nonempty (linear_equiv R (M ⊗[R] N) R) → submodule.fg (⊤ : submodule R M) :=
sorry

-- works iff locale not open
def pseudoinvertible (A : Module.{0} R) : Prop :=
∃ B, nonempty (A ⊗ B ≅ 𝟙_ (Module R))

I can live without not being allowed both, I was just a bit surprised.

[Eric Rodriguez]

category_theory.monoidal.category redefines the notation, which is probably the issue

[Adam Topaz]

@Kevin Buzzard why do you need both? The (monoidal) tensor product in Module R is the usual tensor product.

[Kevin Buzzard]

Because I was experimenting?

[Eric Wieser]

You can always create a tiny section around each lemma and open the locale within than section

[Eric Wieser]

Or use the non-notation spelling for one of them

[Adam Topaz]

Notation overloading is supposed to be better in lean4, right?

[Kevin Buzzard]

There is no locale for the monoidal one, and they have different binding powers too!