Internal sum of two submodules

Stream: Is there code for X?

[Patrick Massot]

We have docs#DirectSum.IsInternal to say that a family of submodules is in direct sum. Do we have the analogue for two submodules? Should we have it? It seems a pretty common special case.

[Patrick Massot]

Also, what am I missing when I write the super complicated:

import Mathlib


variable {K : Type*} [Field K] {V : Type*} [AddCommGroup V] [Module K V]


example {ι : Type*} [DecidableEq ι] (U : ι → Submodule K V) (h : DirectSum.IsInternal U)
    {i j : ι} (hij : i ≠ j) : U i ⊓ U j = ⊥ :=
  disjoint_iff.mp <| h.submodule_independent.pairwiseDisjoint hij

[Eric Wieser]

Is it docs#IsCompl ? I guess this doesn't work for subsemimodules

[Eric Wieser]

example {ι : Type*} [DecidableEq ι] (U : ι → Submodule K V) (h : DirectSum.IsInternal U)
    {i j : ι} (hij : i ≠ j) : U i ⊓ U j = ⊥ :=
  h.submodule_independent.pairwiseDisjoint hij |>.eq_bot

is a little better

[Eric Wieser]

Arguably something to teach is to avoid U i ⊓ U j = ⊥ and stick with Disjoint, which removes the last bit

[Patrick Massot]

Eric Wieser said:

Is it docs#IsCompl ? I guess this doesn't work for subsemimodules

Oh yes, I was silly, I didn’t think of looking for a purely lattice-theoretic spelling. I guess I was misled by the existence of docs#DirectSum.IsInternal which is specific to linear algebra.

[Eric Wieser]

The lattice and algebraic spellings don't coincide for additive submonoids!

[Eric Wieser]

That's probably not a point to dwell on in MIL though!

[Patrick Massot]

What do you mean by the algebraic spelling here? Writing things uniquely as a product?

[Patrick Massot]

Indeed I’m currently writing the linear algebra chapter only in the classical context of vector spaces, although I will probably include a short section on modules over rings.

[Eric Wieser]

Patrick Massot said:

What do you mean by the algebraic spelling here? Writing things uniquely as a product?

I think I mean that U.subtype.coprod V.subtype is bijective (docs#LinearMap.coprod), so yes

[Patrick Massot]

Yes, that’s the same thing.

[Eric Wieser]

although I will probably include a short section on modules over rings.

but not semimodules over semirings, I assume!

[Patrick Massot]

I wanted to mention briefly those, simply to explain why we have this generality in Mathlib. My plan was to point out the case of monoids and

instance Submodule.moduleSubmodule {R : Type u} {M : Type v} [CommSemiring R] [AddCommMonoid M] [Module R M] :
Module (Ideal R) (Submodule R M)

[Patrick Massot]

Maybe we should have a binary version of docs#DirectSum.IsInternal then.

[Eric Wieser]

And presumably also a lattice version of it