trivial submodules

Stream: maths

[Thomas Browning]

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)-/)

[Chris Hughes]

\bot and \top

[Thomas Browning]

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

[Chris Hughes]

I think import linear_algebra.basic should be enough.

[Nico Courts]

Yup! That did it for me. Thanks!

[Kevin Buzzard]

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