finitely generated

Stream: condensed mathematics

[Johan Commelin]

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]

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]

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]

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]

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

[Kevin Buzzard]

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]

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

[Kevin Buzzard]

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]

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]

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]

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

[Aaron Anderson]

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

[Johan Commelin]

@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]

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