## Stream: general

### Topic: tensor product notation issue

#### Kevin Buzzard (Aug 09 2020 at 02:30):

I was writing down a definition of Picard groups in Lean and I ran into the below notation issue. How am I supposed to be working here?

import linear_algebra.tensor_product
import ring_theory.noetherian
import algebra.category.Module.abelian
import algebra.category.Module.monoidal

--open_locale tensor_product -- comment this line out fixes something
-- and breaks something else

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

-- 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 R) : Prop :=
∃ B, nonempty (A ⊗ B ≅ 𝟙_ (Module R))


#### Alex J. Best (Aug 09 2020 at 02:45):

In sections? Looks like the notations for tensor product of unbundled modules clashes with that for bundled modules (as a monoidal category) right so just stick to one within a section.
Alternatively opening the locale and then doing

infixr  ⊗ :70 := category_theory.monoidal_category.tensor_obj
infixr  ⊗ :70 := category_theory.monoidal_category.tensor_hom


works

#### Eric Wieser (Aug 09 2020 at 09:15):

Are those the same symbol or different symbols?

Last updated: May 16 2021 at 05:21 UTC