Zulip Chat Archive

Stream: maths

Topic: trivial submodules


view this post on Zulip Thomas Browning (Jun 23 2020 at 23:28):

If I understand things correctly, submodule R M is a type consisting of submodules of M. Is there a name for the zero submodule and the whole submodule? For example, how you would make this code work?

import algebra.module

definition simple (𝕜 : Type*) [field 𝕜] (V : Type*) [add_comm_group V] [module 𝕜 V] :=
( W : submodule 𝕜 V, /-(W=0) ∨ (W=V)-/)

view this post on Zulip Chris Hughes (Jun 23 2020 at 23:29):

\bot and \top

view this post on Zulip Thomas Browning (Jun 23 2020 at 23:32):

Maybe I need to import some mathlib file, but lean doesn't know that submodule 𝕜 V has \bot and \top.

definition simple (𝕜 : Type*) [field 𝕜] (V : Type*) [add_comm_group V] [module 𝕜 V] :=
( W : submodule 𝕜 V, (W=)  (W=))

view this post on Zulip Chris Hughes (Jun 23 2020 at 23:32):

I think import linear_algebra.basic should be enough.

view this post on Zulip Nico Courts (Jun 23 2020 at 23:33):

Yup! That did it for me. Thanks!

view this post on Zulip Kevin Buzzard (Jun 24 2020 at 06:16):

The decision was made to use lattice notation for bundled types like this and initially I was concerned that it would make it hard for newcomers, but given that mathematicians have so many different notations for the lattice operations in different circumstances I eventually ended up realising that teaching mathematicians about lattice notation might actually be a better idea. Sum of submodules is \lub and intersection is\glb and these are the simp normal forms


Last updated: May 18 2021 at 08:14 UTC