# Zulip Chat Archive

## Stream: maths

### Topic: Internal Direct Sum

#### Aaron Anderson (Dec 31 2020 at 20:57):

Following a conversation on semisimple modules, I've started drafting what I think we need for the direct sum of two `subgroup`

s of a`comm_group`

at branch#direct_sum2

#### Aaron Anderson (Dec 31 2020 at 20:59):

This can logically be extrapolated to additive subgroups, submodules, etc., and eventually to internal direct sums of families, but before I try to do that, does anyone have any feedback on whether this is the right way to code the isomorphisms involved.

#### Kevin Buzzard (Dec 31 2020 at 20:59):

Aren't you going to want all this for add_comm_groups too? e.g. in your application the group law was addition. Probably `to_additive`

will magically do it all for you.

#### Aaron Anderson (Dec 31 2020 at 21:01):

Yes, I figure `to_additive`

will take care of that. I'm not super-well-versed in `to_additive`

, so if someone else wants to try adding that to the branch, they can. Otherwise I'll get to it once I'm confident we have the right API for `comm_group`

s.

#### Kevin Buzzard (Dec 31 2020 at 21:01):

I'm not really clear why you need this stuff at the minute. If s and t are subgroups of G, then you have their external product which you can make, and their internal product which you can make.

#### Kevin Buzzard (Dec 31 2020 at 21:01):

"I have a complement" just means "there exists t such that s meet t is bot and s join t is top"

#### Kevin Buzzard (Dec 31 2020 at 21:02):

I guess at some point though you might have to move from top to s x t and that's what you're setting up here.

#### Aaron Anderson (Dec 31 2020 at 21:04):

I don't think this is necessary for working with semisimple modules or any other case where I care about direct summands, but I think it's useful for justifying that my definitions match up with the literature.

#### Aaron Anderson (Dec 31 2020 at 21:06):

I think the correct way in Lean to say that something's a direct summand is totally order-theoretic, just that it has a complement, but that's not as familiar as saying that something's isomorphic to the direct product of two subobjects.

#### Aaron Anderson (Dec 31 2020 at 21:08):

It'd probably also be nice to use the isomorphism between an internal direct sum of a family and the direct sum of families that we've already developed, e.g. to concretely realize a representation as a sum of irreps, and this is basically a warmup for that.

#### Kevin Buzzard (Dec 31 2020 at 21:15):

Right now I am a bit unclear about what you need here. I mean the definition "I'm a direct summand" is easy using the lattice structure. The statement tha a rep is a finite sum of irreps is just the statement that it's Noetherian and semisimple.

#### Kevin Buzzard (Dec 31 2020 at 21:15):

But I'm not at all clear on how to say "I'm a finite sum of irreps" explicitly. How is this fact used? Is it ever used or do people just use Noeth plus semisimple?

#### Heather Macbeth (Dec 31 2020 at 21:17):

Can you use Yury's definition of a complemented submodule? docs#submodule.closed_complemented

#### Kevin Buzzard (Dec 31 2020 at 21:19):

Yes that works in this generality. What I am unclear about right now is whether one now needs to go into the details of the fact that the abstract direct sum $P\oplus Q$ is isomorphic to the module you started with. I guess one will not be able to avoid this...

#### Aaron Anderson (Dec 31 2020 at 21:26):

Heather Macbeth said:

Can you use Yury's definition of a complemented submodule? docs#submodule.closed_complemented

I was basically going to use what appears in that file as `closed_complemented.has_closed_complement`

, but without the closed part. Essentially the conclusion to docs#monoid_algebra.submodule.exists_is_compl

#### Aaron Anderson (Dec 31 2020 at 21:27):

Another question is how else would we define whether a `Sup`

of subobjects is an internal direct sum, because it's not as simple as with two, where we can use `disjoint`

ness

#### Aaron Anderson (Dec 31 2020 at 21:30):

I see also that this ties in a lot to `linear_algebra.projection`

.

#### Kevin Buzzard (Dec 31 2020 at 21:30):

yes, it's more than pairwise disjointness.

#### Kevin Buzzard (Dec 31 2020 at 21:31):

Are you indexing the subobjects by an an arbitrary type?

#### Kevin Buzzard (Dec 31 2020 at 21:33):

It's the predicate on F : I -> subs X that for all i, F i is compl to the sup of the obvious function F' : I-[i} -> X.

#### Kevin Buzzard (Dec 31 2020 at 21:34):

Oh here's another way.

#### Kevin Buzzard (Dec 31 2020 at 21:36):

`is_direct (F : I -> subs X) := \forall w : I \to_0 F I....`

...wait a minute

#### Kevin Buzzard (Dec 31 2020 at 21:37):

I want some kind of dependent finitely supported type. Is that a thing?

#### Adam Topaz (Dec 31 2020 at 21:37):

#### Kevin Buzzard (Dec 31 2020 at 21:37):

who would have thought it would be called that

#### Kevin Buzzard (Dec 31 2020 at 21:58):

meh I can't quite get it to work and I need to go and be with my family now. It' something like this

```
def is_direct (F : I → add_subgroup X) := Π (w : I →₀ X) (hw : ∀ i, w i ∈ F i)
(sw : w.sum = 0), w = 0
```

#### Kevin Buzzard (Dec 31 2020 at 21:59):

X an add_comm_group. I needed finite support so I had to use 0 and as the identity.

#### Eric Wieser (Jan 01 2021 at 00:23):

Worth noting that `dfinsupp`

is very defeq to docs#direct_sum, in that the latter is the former with a smaller API

#### Kevin Buzzard (Jan 01 2021 at 01:08):

It's something like `injective (finsupp.sum F)`

#### Kevin Buzzard (Jan 01 2021 at 10:03):

Sorry, NYE intervened. Isn't it this?

```
import tactic
import data.finsupp.basic
variables (X : Type) [add_comm_group X] (I : Type)
def is_direct (F : I → add_subgroup X) := ∀ (w : I →₀ X) (hw : ∀ i, w i ∈ F i)
(sw : w.sum (λ i x, x) = 0), w = 0
```

#### Aaron Anderson (Feb 07 2021 at 06:40):

I’ve recently merged `complete_lattice.independent`

, which should give the direct sum condition for abelian groups and modules

#### Eric Wieser (Feb 07 2021 at 09:05):

Meanwhile, #6053 will put a ring structure on internal direct sums of rings

#### Eric Wieser (Feb 07 2021 at 09:58):

docs#complete_lattice.independent for reference

#### Eric Wieser (Feb 25 2021 at 09:56):

The statement to show is:

```
import linear_algebra.direct_sum_module
open_locale direct_sum
variables {R M ι : Type*} [decidable_eq ι] [semiring R] [add_comm_monoid M] [semimodule R M] (S : ι → submodule R M)
def direct_sum.to_Sup_carrier : (⨁ i, S i) →ₗ[R] ↥(⨆ i, S i) :=
direct_sum.to_module R ι _ $ λ i, submodule.of_le (le_supr S i)
/-- This makes `S` an internal direct sum. -/
lemma direct_sum.to_Sup_carrier_bijective (hs : complete_lattice.independent $ set.range S) :
function.bijective (direct_sum.to_Sup_carrier S) := sorry
```

right?

Last updated: May 14 2021 at 20:13 UTC