Algebra.FinitePresentation

Stream: mathlib4

[Christian Merten]

Why is docs#Algebra.FinitePresentation a def and not a class? Follow up question on naming conventions: For me FinitePresentation sounds like it contains data (i.e. a finite presentation of the algebra). Should it be called FinitelyPresented?

[Kevin Buzzard]

I think IsFinitelyPresented would be even better!

[Christian Merten]

I was somehow expecting you to suggest that :-)

[Kevin Buzzard]

And I agree that it could be a class. I guess the argument for is that then you could imagine typeclass inference could supply instances automatically, and the argument against is that what is the point of cluttering up the typeclass system even more when you can just have (h : IsFinitelyPresented R A) and use dot notation etc.

[Christian Merten]

To be consistent, FiniteType needs to be IsFiniteType then (and of course many more)

[Kevin Buzzard]

Well @Johan Commelin wrote that stuff in 2020 and perhaps conventions were less established back then. Note that for topology you have IsCompact for subspaces and CompactSpace for spaces, but here there doesn't seem to be such a dichotomy so I don't really see why we can't use Is for everything. I find that my students find it easier to navigate with the Is convention.

[Markus Schmaus]

What is the rule here? When should it start with Is?

[Christian Merten]

If it is a Prop.

[Kevin Buzzard]

The exception are predicates which we have in Lean both for topological spaces and for subspaces of topological spaces (like CompactSpace, which I would happily rename IsCompactSpace to be honest, but that's not how it is right now).

[Markus Schmaus]

To be precise, I think this means Prop valued function.

What about docs#LawfulMonad ? Should this be IsLawfulMonad? Or maybe Monad.IsLawful? Is this just legacy, or is there a rule exception which covers this case?

[Kevin Buzzard]

Well there you're in core, so this is beyond the community's jurisdiction.

[Markus Schmaus]

Ah, I understand. If it were in Mathlib, what would be its name?

[Kevin Buzzard]

Well Is zealots like me would be keen for IsLawful, but golfy people might argue for Lawful. There isn't an algorithm, it's whatever the community converges on :-) I'm not entirely sure why Monad is in there at all, given that it's not extending Monad

[Timo Carlin-Burns]

It takes [Monad m] as a parameter though

[Kevin Buzzard]

Sure, I mean why there's Monad in the name, I agree that it's pretty important that it takes a monad as parameter :-) For example we have IsDomain which doesn't mention Ring.

[Eric Wieser]

Well, if we had a Ring in core that contained only the data, then presumably you wouldn't argue against including Ring in a downstream IsLawfulRing...

[Eric Wieser]

We only get to use the name IsLawful once unless we suffix it!

[Christian Merten]

To come back to the original topic of this thread: Does anyone have objections to making docs#Algebra.FinitePresentation a class? Maybe @Johan Commelin has an opinion as the author of that file?

[Johan Commelin]

I have no objection.

[Anne Baanen]

Christian Merten said:

Should it be called FinitelyPresented?

Note that @Riccardo Brasca did the opposite rename in mathlib3#6382, for similarity to docs#Algebra.FiniteType.

[Anne Baanen]

Christian Merten said:

Does anyone have objections to making docs#Algebra.FinitePresentation a class?

Similarly, Riccardo initially made this a class in mathlib3#5407, but @Reid Barton preferred a plain def. The Lean 4 developers have radically improved the typeclass machinery since then, so IMO this warrants a re-evaluation.

[Christian Merten]

I get 404s on these links.

[Anne Baanen]

Sorry, fixed!

[Anne Baanen]

As a rule of thumb, making FinitePresentation R A a class is going to be useful if you can look at R and A and immediately say "yes, that looks finitely presented". If in practice showing it's finitely presented requires some proof steps first (even simple ones), in particular when it holds because A is actually equal to something else, then the typeclass system won't help you with this.

[Anne Baanen]

That is for instance why we don't have a typeclass for saying a number is prime: you can't look at it and immediately see that. You need some sort of computation first, and the typeclass system doesn't do computation in that way.

[Christian Merten]

Thanks for the explanation, now that I think of it, there are probably not so many cases where typeclass inference can immediatly see that some algebra is finitely presented. Mostly base change (which is actually missing currently) and polynomial rings probably.

For me the reason for wanting this to be a class is that I want to say (e.g.) an unramified ring homomorphism is FormallyUnramified and of FinitePresentation. If I have Unramified R A in my assumptions, I want to have FinitePresentation R A automatically without passing the extra argument around.

[Riccardo Brasca]

I am in favor of making it a class, unless it creates serious performance issues.I don't see a lot of differences between finitely presented and of finite type, and docs#Module.Finite is a class.

[Riccardo Brasca]

I am very bad in choosing names, so fell free to rename if you think it is better.

[Christian Merten]

Suggestion: I'll make it a class later today and get a benchmark. Then we have some numbers to work with.

[Christian Merten]

Christian Merten said:

Suggestion: I'll make it a class later today and get a benchmark. Then we have some numbers to work with.

#12057, benchmark is on its way.

[Kevin Buzzard]

You won't get a benchmark until the entire library compiles again...

[Christian Merten]

It says "no significant changes".

[Antoine Chambert-Loir]

I don't see why you want FinitePresentation to be a class. It is rare that the actual structure beneath it is actually used in an important way. Most of the time, you can — an sometimes do — adjust the finite présentation so that it fits your present needs.

[Christian Merten]

Antoine Chambert-Loir said:

I don't see why you want FinitePresentation to be a class. It is rare that the actual structure beneath it is actually used in an important way. Most of the time, you can — an sometimes do — adjust the finite présentation so that it fits your present needs.

I think I don't understand. Note that Algebra.FinitePresentation is a Prop and remains a Prop after making it a class.

[Johan Commelin]

It should probably be renamed to FinitelyPresentable.

[Riccardo Brasca]

I tried to follow standard terminology, it seems to me people say "let M be of finite presentation", but of course they don't fix the actual presentation.

[Johan Commelin]

Yeah, I think in mathlib we might want to have both notions

[Antoine Chambert-Loir]

Christian Merten said:

Antoine Chambert-Loir said:

I don't see why you want FinitePresentation to be a class. It is rare that the actual structure beneath it is actually used in an important way. Most of the time, you can — an sometimes do — adjust the finite présentation so that it fits your present needs.

I think I don't understand. Note that Algebra.FinitePresentation is a Prop and remains a Prop after making it a class.

It was me that didn't understand. (When I read in mathlib Algebra.FinitePresentation, I expect a presentation, not simply the existence of one.) Regarding terminology, I believe mathlib should take the opportunity to systematize it, especially in theses cases where there is no ambiguity and where specialists see the point. (It will be more difficult to argue for things like “graphs” that exist in many guises, all inconsistent, and where mathlib has to make an ur-choice — the one of Serre is of course the best one — and all others should derive from it, in particular docs#SimpleGraph.)

[Antoine Chambert-Loir]

Johan Commelin said:

It should probably be renamed to FinitelyPresentable.

Or even IsFinitelyPresentable.

[Adam Topaz]

Here's a thought. What if we introduce the type of all finite presentations of an algebra, and put some structure on it (like a poset structure, or even a category structure). Then make FinitelyPresentable simply assert that this is nonempty. Then if you want to work with finite presentations, and modify them as needed by your argument, you can work with this additional structure of all finite presentations.

[Adam Topaz]

Something like this:

import Mathlib

open Lean

variable (A B : Type*) [CommRing A] [CommRing B] [Algebra A B]

structure FinitePresentation where
  n : Nat
  p : MvPolynomial (Fin n) A →ₐ[A] B
  hp : Function.Surjective p
  fg : p.toRingHom.ker.FG

variable {A B}

structure FinitePresentation.Hom (F G : FinitePresentation A B) where
  e : MvPolynomial (Fin F.n) A →+* MvPolynomial (Fin G.n) A
  he : G.p.toRingHom.comp e = F.p.toRingHom

open CategoryTheory
instance : Category (FinitePresentation A B) where
  Hom := FinitePresentation.Hom
  id X := .mk (RingHom.id _) <| by simp
  comp := fun ⟨f,hf⟩ ⟨g,hg⟩ => ⟨g.comp f, by rw [← RingHom.comp_assoc, hg, hf]⟩

[Adam Topaz]

We could, for example, prove that FinitePresentation A B has finite coproducts.

[Matthew Ballard]

Yes this a good idea. There is a natural partial order also

[Adam Topaz]

Right. But for that we would have to identify the map from Fin n to B with its image which is categorically “evil”

[Adam Topaz]

But maybe only slightly evil in this case :)

[Matthew Ballard]

You need this for “factor through”?

[Adam Topaz]

No? I think the Homs in the category above would work as well

[Matthew Ballard]

Yeah. That’s more natural

[Adam Topaz]

I mean, the skeleton of that category is “just” the poset you’re referring to, so :shrug:

[Matthew Ballard]

People do care about minimal things quite a bit

[Adam Topaz]

Fixed it:

import Mathlib

open Lean

variable (A B : Type*) [CommRing A] [CommRing B] [Algebra A B]

structure FinitePresentation where
  n : Finset B
  hp : Function.Surjective (MvPolynomial.aeval (R := A) (S₁ := B) fun x : n => x)
  fg : ((MvPolynomial.aeval (R := A) (S₁ := B) fun x : n => x)).toRingHom.ker.FG

variable {A B}
instance : PartialOrder (FinitePresentation A B) where
  le A B := A.n ≤ B.n
  le_refl A := le_refl A.n
  le_trans {A B C} h1 h2 := le_trans (a := A.n) h1 h2
  le_antisymm := by
    rintro ⟨a,f,hf,h1⟩ ⟨b,g,hg,h2⟩ h1' h2'
    congr
    exact le_antisymm h1' h2'

[Matthew Ballard]

Did anyone complain about not using Finite yet?

[Adam Topaz]

Do we have the concept of a finitely generated equivalence relation in mathlib?

[Antoine Chambert-Loir]

The problem I see with the second definition is that it doesn't show that there is an algebra isomorphic to B which lives in the same universe as A

[Adam Topaz]

Antoine Chambert-Loir said:

The problem I see with the second definition is that it doesn't show that there is an algebra isomorphic to B which lives in the same universe as A

This could be done after the fact using, e.g. docs#Fintype.equivFin

[Eric Wieser]

I think you can use docs#PartialOrder.lift to golf the instance above

[Eric Wieser]

Another direction this could go is:

structure IsFinitePresentationOn {I : Type} [Finite I] (f : I → B) where
  hp : Function.Surjective (MvPolynomial.aeval (R := A) (S₁ := B) f)
  fg : ((MvPolynomial.aeval (R := A) (S₁ := B) f).toRingHom.ker.FG

and then recover FinitePresentation by making a subtype and specializing to I := (_ : Finset B) and f := coe

[Eric Wieser]

(this is a bit like the Module.Free vs Basis distinction)

[Antoine Chambert-Loir]

Adam Topaz said:

Antoine Chambert-Loir said:

The problem I see with the second definition is that it doesn't show that there is an algebra isomorphic to B which lives in the same universe as A

This could be done after the fact using, e.g. docs#Fintype.equivFin

Yes, but doing that in practice,I felt that it added one layer of burden.

[Adam Topaz]

I understand. We could of course introduce both approaches I mentioned above, and an equivalence of categories between them. This would be the "best of both worlds".

[Christian Merten]

How should we proceed? Should I close #12057 or can we merge #12057 as an intermediate step? (Naturally I prefer the latter, as I would like to have Algebra.FinitePresentation as a class as soon as possible).

[Adam Topaz]

Looks like Matt has merged this PR, which I completely agree with! We can think more about the design and refactor as needed

[Matthew Ballard]

Sorry. The merge was definitely not meant as the end of the conversation. Using a class instead is somewhat orthogonal to the excellent ideas discussed here. I hope there is an expansion of them!

[Andrew Yang]

#12518 is an attempt to develop an API for presentations of algebras. The presentations I need aren't necessarily finite so not everything in this thread is used.