Zulip Chat Archive

Stream: general

Topic: tensor product notation issue

view this post on Zulip 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]
[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 R) : Prop :=
 B, nonempty (A  B  𝟙_ (Module R))

view this post on Zulip 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


view this post on Zulip 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