Topic: trivial submodules
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)-/)
Chris Hughes (Jun 23 2020 at 23:29):
\bot and \top
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=⊤))
Chris Hughes (Jun 23 2020 at 23:32):
import linear_algebra.basic should be enough.
Nico Courts (Jun 23 2020 at 23:33):
Yup! That did it for me. Thanks!
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