Zulip Chat Archive

Stream: maths

Topic: Internal Direct Sum


view this post on Zulip 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 subgroups of acomm_group at branch#direct_sum2

view this post on Zulip 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.

view this post on Zulip 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.

view this post on Zulip 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_groups.

view this post on Zulip 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.

view this post on Zulip 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"

view this post on Zulip 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.

view this post on Zulip 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.

view this post on Zulip 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.

view this post on Zulip 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.

view this post on Zulip 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.

view this post on Zulip 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?

view this post on Zulip Heather Macbeth (Dec 31 2020 at 21:17):

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

view this post on Zulip 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 PQP\oplus Q is isomorphic to the module you started with. I guess one will not be able to avoid this...

view this post on Zulip 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

view this post on Zulip 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 disjointness

view this post on Zulip Aaron Anderson (Dec 31 2020 at 21:30):

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

view this post on Zulip Kevin Buzzard (Dec 31 2020 at 21:30):

yes, it's more than pairwise disjointness.

view this post on Zulip Kevin Buzzard (Dec 31 2020 at 21:31):

Are you indexing the subobjects by an an arbitrary type?

view this post on Zulip 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.

view this post on Zulip Kevin Buzzard (Dec 31 2020 at 21:34):

Oh here's another way.

view this post on Zulip Kevin Buzzard (Dec 31 2020 at 21:36):

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

view this post on Zulip Kevin Buzzard (Dec 31 2020 at 21:37):

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

view this post on Zulip Adam Topaz (Dec 31 2020 at 21:37):

docs#dfinsupp

view this post on Zulip Kevin Buzzard (Dec 31 2020 at 21:37):

who would have thought it would be called that

view this post on Zulip 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

view this post on Zulip 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.

view this post on Zulip 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

view this post on Zulip Kevin Buzzard (Jan 01 2021 at 01:08):

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

view this post on Zulip 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

view this post on Zulip 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

view this post on Zulip Eric Wieser (Feb 07 2021 at 09:05):

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

view this post on Zulip Eric Wieser (Feb 07 2021 at 09:58):

docs#complete_lattice.independent for reference

view this post on Zulip 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