Finitely Presented Things

Stream: Is there code for X?

[Adam Topaz]

Do we have a consistent way to talk about finitely-presented algebraic objects?

[Riccardo Brasca]

I don't know, but the theory for modules is completely done by hand.

[Adam Topaz]

What is the name of the condition saying that a module is finitely-presented?

[Adam Topaz]

I'm mostly looking for consistent names

[Riccardo Brasca]

I am on mobile, but iirc is FinitelyPresented

[Adam Topaz]

oh I found docs#RingHom.FinitePresentation et al.

[Adam Topaz]

docs#Module.FinitelyPresented and docs#Module.FinitePresentation come up short though

[Riccardo Brasca]

Ah sorry, I meant finitely presented algebras, not modules

[Riccardo Brasca]

I don't think we have those

[Adam Topaz]

Right now I'm mostly interested in finitely-presented rings anyway :)

[Adam Topaz]

FWIW, I think it would be worthwhile to introduce a "small" model for finitely-presented rings (and other algebraic objects), and show that any ring is a colimit of suitable finitely-presented rings. In the case of rings, one approach would be:

structure CommRingCat₀ where
  n : ℕ
  I : Ideal <| MvPolynomial (Fin n) ℤ

Thoughts?

[Adam Topaz]

Note the key property that CommRingCat₀ : Type and that it's a small category

[Antoine Chambert-Loir]

It could be “compact”, because they are the compact objects on the category of modules.

[Adam Topaz]

Yes I agree but the type of all compact objects is still “large” from the pov of universe parameters

[Andrew Yang]

I think we should instead use docs#CategoryTheory.EssentiallySmall and hide the CommRingCat₀ you mentioned as an implementation detail.

[Adam Topaz]

yeah, probably. How good is the api for essentially small cats? I've never really used it.

[Adam Topaz]

In fact, I wonder if it makes sense to develop an API for an "essentially small subcategory" coming from a fully faithful functor S \func C where S is small. Once thing that comes up quite often is representing objects of C as filtered colimits of compact objects, and having to deal with just one functor, as opposed to an equivalence followed by a fully faithful inclusion of some subcategory, is probably easier to manage.

[Eric Wieser]

Does Algebra.FinitePresentation generalize to non-commutative rings by using the tensor algebra instead of multivariate polynomials, or does that not then yield the right meaning when specialize to the commutative case?

[Matthew Ballard]

I think finitely presented should be admits an epi from a free functor applied to a finite set. But I don’t see as much use for either notion in non commutative algebra.

[Adam Topaz]

There’s a general notion of finitelypresented/compactobject from universal algebra. It’s a finitely generated free thing modulo a finitely generated congruence relation IIRC. So for noncomm rings, it should indeed be the tensor algebra modulo a f.g. two-sided ideal

[Eric Wieser]

So I guess for that definition to work we need some notion of RingCon.FG?

[Adam Topaz]

Yeah I suppose. The categorical notion of compactness is much more general of course

[Adam Topaz]

In these algebraic cases it’s equivalent to being finitely presented

[Adam Topaz]

Matthew Ballard said:

I think finitely presented should be admits an epi from a free functor applied to a finite set. But I don’t see as much use for either notion in non commutative algebra.

I don’t think this is the right notion in general

[Adam Topaz]

The “correct” categorical notion is that X is f.p. if Hom(X,-) commutes with filtered colimits.

[Matthew Ballard]

Right. I was thinking finitely generated