Skip to content
This repository has been archived by the owner on Dec 6, 2024. It is now read-only.

Pi-Base for abstract algebra #116

Open
FernandoChu opened this issue Oct 8, 2021 · 9 comments
Open

Pi-Base for abstract algebra #116

FernandoChu opened this issue Oct 8, 2021 · 9 comments

Comments

@FernandoChu
Copy link

Hello!
I've been a huge fan of this project for a while, and was thinking on implementing something like this for undergraduate abstract algebra. Since all your code is open source (great!) I was wondering if it was alright to fork it and use it as a base. Since there is no license in the repos, I was unsure if this is fine, hence I'm asking first.

@StevenClontz
Copy link
Member

We definitely would love to see the platform used for other areas of mathematics. The code is 99% @jamesdabbs so the choice of license is ultimately his. But we got the domain pi-base.org with the intention of having subdomains for various categories: https://topology.pi-base.org would pair nicely with e.g. https://algebra.pi-base.org

I guess in this implementation, we'd have groups instead of spaces (with the state of being a ring, field, etc. being possible properties of a group?).

@FernandoChu
Copy link
Author

Oh I didn't even think of being subdomain, I think that would be cool!

In terms of the implementation, I was thinking of having at least three "types of spaces". Group-like (structures with only one binary operation), ring-like (structures with two binary operations), and module-like (you get it). The problem of considering "being a ring" as a property of groups, is that it could be a ring in many ways, i.e. there are multiple "multiplications" that satisfy the axioms. Also, you can always make a group into a ring without unity, by making a * b = 0 which may look like the property is trivial, when it's not.

Another thing that is very important in algebra is "constructions", these take a given structure and gives you a new one; e.g. quotient groups, polynomial rings, ring of fractions, etc. Obviously there are constructions in topology too, but I think they play a smaller role, and I think pi-base is not covering them as of now (correct me if I'm wrong, but I couldn't find definitions for "product topology" or "quotient topology", for example).

I have not read the code yet, but I think two capabilities (supporting multiple "types of spaces", and "constructions") are a must have for algebra so I would have to add those if they are not there already. If you want pi-base to be used for other areas of math I think having these capabilities in the code would make an implementation easier in general.


But yeah I'm getting a bit ahead of myself, I have to hear what James has to say. If he gives it a green light I'd be happy to collaborate on the code! However, in case he says yes, I'd also like to talk a bit more about licenses and such as this would be a huge investment of time from me so I want to make sure everything is in order.

@StevenClontz
Copy link
Member

Yeah I think you're getting at #13 - we definitely do want things like for every space X there's a space C_p(X), and theorems like if X is Menger then C_p(X) is selectively separable. Likewise for every ring R there's a field of fractions...

We're not there yet though. I've applied for sabbatical in 2022-23 which will hopefully give me a chance to make big swings like this...

@jamesdabbs
Copy link
Member

Hey @Ryunaq, thanks for reaching out!

alright to fork it and use it as a base ... no license ...

Thanks for pointing that out; that was definitely an oversight. Our intention is definitely to encourage open collaboration - we've licensed the core logic as mit and the data as cc-by-4.0. Let me circle up w/ Steven real quick, but it probably makes sense to mit license this package as well.

two capabilities (supporting multiple "types of spaces", and "constructions")

This makes a lot of sense to me. As Steven said, we'd love to be able to spin up multiple versions of the pi-base at different subdomains, each of them running more-or-less the same code (modulo some language changes) but with different sets of underlying objects. I haven't spent a ton of time thinking through what that looks like in practice (or how feasible it actually is) ... but I'd personally be interested in exploring reworking the logic in category-theoretical terms: replacing "spaces" with "objects", and starting to look at e.g. deductions of the form "this object is the product of these two objects, and this property is preserved by products".

If he gives it a green light I'd be happy to collaborate on the code!

I'm all for contributions. What's your timeframe / availability like? Would it help to brainstorm / plan together a little bit, or would you prefer to just jump in and spike out some code first?

@StevenClontz
Copy link
Member

I'm very much a novice category theorist, but maybe this is the pattern:

  • objects (currently spaces)
  • properties
  • theorems
  • functors
    • defines "meta" objects from basic objects, e.g. a product functor defines X×Y for each pair of objects X,Y
    • should have its own theorems, e.g. if X,Y are compact, then X×Y is compact

The functors can't be iterated indefinitely of course, so maybe there should be a way to "save" interesting constructions as static objects.

@StevenClontz
Copy link
Member

MIT license makes sense to me

@FernandoChu
Copy link
Author

Hey @jamesdabbs, great!

I've been thinking about how to structure it since yesterday and it definitely gets very complicated haha so sure! I'd like to brainstorm / plan together. My timezone is UTC-5, and my schedule is pretty flexible so I'm available every day except 6-9pm on weekdays, and 2:30-4:30pm this weekend.


For a small preview of what I was thinking of, is having a this mix of "topic", "structures", "properties", and "constructions". For algebra, here are some examples

  • The topics would be "Group-like, Ring-like, and Module-like".
  • "Structures" are relative to a given topic, so relative to ring-like, the structures are "Rings", "Rngs", "Fields", (not so sure about this actually), but also "ideals" and "ring elements". This is so the "Properties" work.
  • "Properties" are relative to a given structure, so relative to "Ring" we have the "commutative", "noetherian", etc. But we also have properties like "two-sided", "prime", "maximal" of an ideal of an specific ring, and properties like "nilpotent", "irreducible" of a given ring element of a given ring.
  • "Constructions" are what I talked earlier, things like Quotient rings, group products, ring of fractions etc. But there's actually more important constructions on the other two "structures", we have sum, product, intersection of ideals, and things like gcd, mcm, on ring elements, for example.

Knitting all of these are obviously theorems and counterexamples, but since the relation between "structures", "properties", and "constructions" is not so clear cut as before, I thing a tag system is needed. For example, I don't see any really ordered way of presenting "R/Ker(Phi) \cong Phi(R)" other than just tagging it with "Quotient ring, kernel, image under homomorphism". Still, the nice if x then y model does hold well for a lot of things. This could help for connecting multiple subdomains too! E.g. talking about the Zariski topology construction.

A simpler alternative to category theory for automate some "obvious" reasoning is modelling the transitivity of certain properties, and checking what properties are preserved under certain construction. I think this may be better since one, it is (probably) more comprehensible for undergraduates, and two, a lot of constructions are not categoric in nature (or are in a somewhat awkward way). Still, this gives a powerful way of proving properties of specific objects, like if you prove that X is isomorphic to Pi(Y) and you know that Y is a field and Pi preserves multiplicative inverses, then X is a field too.

Hope this was interesting at least, tell me whenever you want to meet!

jamesdabbs added a commit that referenced this issue Oct 17, 2021
Per discussion in #116, I believe the intent was always for the
viewer code to match license with @pi-base/core, and that the
lack of license in this repo was just an oversight.
jamesdabbs added a commit that referenced this issue Oct 17, 2021
Per discussion in #116, I believe the intent was always for the
viewer code to match license with @pi-base/core, and that the
lack of license in this repo was just an oversight.
jamesdabbs added a commit that referenced this issue Oct 17, 2021
Per discussion in #116, I believe the intent was always for the
viewer code to match license with @pi-base/core, and that the
lack of license in this repo was just an oversight.
@StevenClontz
Copy link
Member

Having really looked at it yet, but I stumbled across https://ringtheory.herokuapp.com/ via random Twitter recommendation. I'm excited to see what similarities/differences our projects have...

@pqnelson
Copy link

What's the current status of this endeavour? I'd like to help with the group theory side of things...since the start of the pandemic, I started studying the classification theorem of finite simple groups, and organized my notes on slips of paper (like an analogue version of the pi-base).

Sign up for free to subscribe to this conversation on GitHub. Already have an account? Sign in.
Labels
None yet
Projects
None yet
Development

No branches or pull requests

4 participants