Adds inverse limits of Modules, Rings, Groups and Representations

[javierlcontreras]

Needed for the formalization of existence of the Universal Deformation Ring (following Smit&Lenstra).

This is not Mathlib-grade code, I am guessing (and @YaelDillies agreed) that both Representation and InverseLimit should be done categorically, but at the moment the CategoryTheory API is hard (to me at least). I implemented this to unblock the R project.

[kbuzzard]

Are you sure you want it as a Submodule and not as a type by itself? See this comment from Mathlib.NumberTheory.NumberField.Basic:

/-- The ring of integers (or number ring) corresponding to a number field
is the integral closure of ℤ in the number field.

This is defined as its own type, rather than a `Subalgebra`, for performance reasons:
looking for instances of the form `SMul (RingOfIntegers _) (RingOfIntegers _)` makes
much more effective use of the discrimination tree than instances of the form
`SMul (Subtype _) (Subtype _)`.
The drawback is we have to copy over instances manually.
-/
def RingOfIntegers : Type _ :=
  integralClosure ℤ K

Without Type _ it would have type Subalgebra \Z K or something. The problem with leaving it as a subobject is that 9 times out of 10 with rings of integers, you want to treat them as a type not a term, so you write a : 𝓞 K and if you've defined it as a subalgebra then it comes out as weird up-arrow 𝓞 K, and whenever you write something like a • x typeclass inference is quick to think "hmm, a is in a subtype so if K acted on x then I could use this action" and we would be forever wasting out time looking for actions of K on things like fractional ideals, which don't exist.

I think basically I'm saying "are you using this as a submodule 9 times out of 10, or as a type? If a type, then you might want to consider

def InverseLimit : Type _ := (... : Submodule R (Π i : ι, obj i))

[javierlcontreras]

Oh I was unaware of this, but makes sense. I think making it a type makes more sense. Thank you for the detailed explanation :)