# Zulip Chat Archive

## Stream: condensed mathematics

### Topic: finitely generated

#### 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

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

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

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

#### Johan Commelin (Feb 25 2021 at 21:16):

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

#### Kevin Buzzard (Feb 25 2021 at 21:23):

For $R$-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$-modules, but then there's the usual song and dance to translate this into questions about abelian groups.

#### Kevin Buzzard (Feb 25 2021 at 21:27):

How do you want to do this? Define `add_comm_group.fg`

or resist doing this?

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

#### 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:

#### 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...
```

#### Aaron Anderson (Feb 26 2021 at 01:58):

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

#### 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`

#### 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

#### 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