Internal Direct Sum

Stream: maths

[Aaron Anderson]

Following a conversation on semisimple modules, I've started drafting what I think we need for the direct sum of two subgroups of acomm_group at branch#direct_sum2

[Aaron Anderson]

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]

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]

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_groups.

[Kevin Buzzard]

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]

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

[Kevin Buzzard]

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]

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]

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]

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]

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]

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]

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

[Kevin Buzzard]

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]

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]

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 disjointness

[Aaron Anderson]

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

[Kevin Buzzard]

yes, it's more than pairwise disjointness.

[Kevin Buzzard]

Are you indexing the subobjects by an an arbitrary type?

[Kevin Buzzard]

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]

Oh here's another way.

[Kevin Buzzard]

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

[Kevin Buzzard]

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

[Adam Topaz]

docs#dfinsupp

[Kevin Buzzard]

who would have thought it would be called that

[Kevin Buzzard]

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]

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

[Eric Wieser]

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

[Kevin Buzzard]

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

[Kevin Buzzard]

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]

I’ve recently merged complete_lattice.independent, which should give the direct sum condition for abelian groups and modules

[Eric Wieser]

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

[Eric Wieser]

docs#complete_lattice.independent for reference

[Eric Wieser]

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?