Zulip Chat Archive

Stream: general

Topic: open_locale tensor_product issue

Kevin Buzzard (Aug 02 2021 at 19:46):

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) :=

-- 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 (Aug 02 2021 at 20:05):

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

Adam Topaz (Aug 02 2021 at 20:07):

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

Kevin Buzzard (Aug 02 2021 at 20:08):

Because I was experimenting?

Eric Wieser (Aug 02 2021 at 20:09):

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

Eric Wieser (Aug 02 2021 at 20:09):

Or use the non-notation spelling for one of them

Adam Topaz (Aug 02 2021 at 20:10):

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

Kevin Buzzard (Aug 02 2021 at 20:12):

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

Last updated: Aug 03 2023 at 10:10 UTC