Zulip Chat Archive

Stream: Is there code for X?

Topic: N ⊓ P as a submodule of N

Fabian Glöckle (Feb 14 2022 at 18:02):

Given an R-module M and N P : submodule R M, is there a way to view N ⊓ P as a submodule of N (or P, respectively)?

I am thinking of something like the following:

def submodule.inter
  {R : Type*} [comm_ring R]
  {M : Type*} [add_comm_group M] [module R M]
  (N : submodule R M)
  (P : submodule R M) :
  submodule R N :=
  begin
    refine ⟨set.restrict P.1 N.1, _, _, _⟩,
    {rw set.restrict_eq, exact P.2},
    {intros a b ha hb, rw set.restrict_eq at ha, rw set.restrict_eq at hb,
    rw set.restrict_eq, exact P.3 ha hb },
    {intros c x hx, rw set.restrict_eq at hx, rw set.restrict_eq, exact P.4 c hx}
  end

I'd assume something similar is already in mathlib, or the problem can be resolved without such a definition, but I didn't find the correct statement in the submodule section / couldn't really figure out how to do it with what there is. Of course, there should then also be lemmas relating submodule.inter N P with N ⊓ P.