Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

General Linear group #2006

Open
Alizter opened this issue Jul 1, 2024 · 1 comment
Open

General Linear group #2006

Alizter opened this issue Jul 1, 2024 · 1 comment

Comments

@Alizter
Copy link
Collaborator

Alizter commented Jul 1, 2024

#2005 adds notions of invertibility for rings. It also defines the group of units of a ring. This should allow us to define $\mathrm{GL}_n(R)$ over an arbitrary ring.

I'm not sure what else we can prove about $\mathrm{GL}_n(R)$ for an arbitrary ring $R$, once we have determinants it would be possible to define $\mathrm{SL}_n(R)$ and show we have an exact sequence of groups:

$$ 1 \to \mathrm{SL}_n(R) \to \mathrm{GL}_n(R) \to R^\times \to 1 $$

@Alizter
Copy link
Collaborator Author

Alizter commented Jul 1, 2024

@ThomatoTomato Would you like to have a go at defining the general linear group once #2005 is merged? It should be in theories/Algebra/Groups/GL.v and depend on Algebra.Rings.Ring.

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

No branches or pull requests

1 participant