search

HoTT / Coq-HoTT

A Coq library for Homotopy Type Theory
http://homotopytypetheory.org/
Other
1.25k stars 191 forks source link

General Linear group #2006

Open Alizter opened 3 months ago

Alizter commented 3 months ago

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 commented 3 months ago

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