Zulip Chat Archive

Stream: condensed mathematics

Topic: finitely generated


view this post on Zulip Johan Commelin (Feb 24 2021 at 15:30):

A little project: develop some API for module.finite. Mathlib knows the definition.

  • Do we also want a predicate for finitely generated (mul/add) groups? And glue with the module version in the additive case?
  • Do we care about the noncommutative case?

For LTE we will need

  • finite direct sums of fin.gen modules (or add_groups) are fin.gen
  • an add_subgroup of a fin.gen add_group is again finitely generated

view this post on Zulip Julian Külshammer (Feb 24 2021 at 18:23):

Which proof of the third bullet point do you have in mind that would use commutativity? Finitely generated modules are definitely also studied in the noncommutative setting.

view this post on Zulip Johan Commelin (Feb 24 2021 at 18:31):

I didn't think carefully at all about the noncommutative case. There are actually two kinds of noncommutativity here. The base ring, in the module case, but also the group itself in the case of fin.gen. groups.

view this post on Zulip Kevin Buzzard (Feb 25 2021 at 21:13):

Re LTE needs: when Mario did Noetherian modules years ago I'm pretty sure he did that a submodule of a Noetherian module was Noetherian. Do we have finite direct sums? This feels like one of those things where there are about four ways of formalising it.

view this post on Zulip Johan Commelin (Feb 25 2021 at 21:16):

I have no idea what's there... :oops:

view this post on Zulip Kevin Buzzard (Feb 25 2021 at 21:23):

For RR-modules we have the is_noetherian predicate, a proof that a f.g. module over a Noetherian ring is Noetherian, a submodule of a Noetherian module is Noetherian, and a Noetherian module is finitely-generated. That gives us the second bullet point for Z\Z-modules, but then there's the usual song and dance to translate this into questions about abelian groups.

view this post on Zulip Kevin Buzzard (Feb 25 2021 at 21:27):

How do you want to do this? Define add_comm_group.fg or resist doing this?

view this post on Zulip Kevin Buzzard (Feb 25 2021 at 21:58):

Aah, I see you ask the same question! I don't see why we shouldn't have is_fg a predicate on add_comm_group, it could maybe be a class but maybe not, I think there's some lemma that Z-module structure on an add_comm_group is unique so there shouldn't be problems just pulling results over. The third bullet point is certainly fine in the case where the ring is noncommutative. I think finitely generated groups are a different thing to this.

view this post on Zulip Riccardo Brasca (Feb 25 2021 at 22:04):

I am playing with finitely generated modules to develop the API for finitely presented morphisms, so I can very well work on finitely generated groups... but as usual I leave the design decisions to you the experts :smile:

view this post on Zulip Adam Topaz (Feb 25 2021 at 22:45):

import algebra
import linear_algebra
import group_theory.subgroup
import data.finset.basic
import order.galois_connection

variables {α β : Type*} [preorder β] [has_top β]
  {f : β  set α} {g : set α  β} (gi : galois_insertion g f)

include gi
def is_fg : Prop :=  (F : finset α), g F = 

def group.is_fg (G : Type*) [group G] := is_fg (subgroup.gi G)
def module.is_fg (A M : Type*) [ring A] [add_comm_group M] [module A M] := is_fg (submodule.gi A M)

-- etc...

view this post on Zulip Aaron Anderson (Feb 26 2021 at 01:58):

FWIW, a subwidget being fg is should be equivalent to complete_lattice.is_compact_element

view this post on Zulip Aaron Anderson (Feb 26 2021 at 01:59):

We should prove some theorems about that and galois insertions that connect this to the above definition of is_fg

view this post on Zulip Johan Commelin (Feb 26 2021 at 05:40):

@Aaron Anderson I like that idea of generalisation. A good API for compact elements can probably be easily specialised to different forms of is_fg. Thanks for the suggestion

view this post on Zulip Aaron Anderson (Feb 26 2021 at 05:58):

The theory I've had in mind for a while but haven't fully put into practice is classifying all of these examples of galois insertions as "finitary" or "algebraic" (terms usually used for closure operators, but Galois insertions are basically the same). That should be enough specificity to prove that being the closure of a finset is equivalent to being a compact element (as well as lots of other good things, this is nearly the definition of matroids/pregeometries).


Last updated: May 09 2021 at 15:11 UTC