Pulling class instances through "complicated" computations

Stream: new members

[Robert Spencer]

Good morning all.

I wonder if anyone could help me understand how best to tackle the following. In a nutshell, I am performing some computations on types (taking quotients of submodules) and lean is struggling to find an instance I need for the result (that a quotient of a submodule is indeed a module).

Here is my minimal code. Mathematically I am defining a filtration of a module, and then finding its subquotients.

import linear_algebra.basic

import data.list

universes U₁ U₂

namespace list
  variables {α : Type U₁} {β : Type U₂}
  variables {R : α → α → Prop} {x y : α} {L : list α}

  -- Much like head,
  @[simp] def head'': Π  (L : list α), L ≠ [] → α
  | []        h := absurd rfl h
  | (x :: xs) h := x

  @[simp]
  lemma chain'_desc_left : chain' R (x :: L) → chain' R L := by cases L; simp[chain']

  def chain'_apply_between (f : Π(a b : α), (R a b) → β) : Π (L : list α), list.chain' R L → list β
  | [] h := []
  | [x] h := []
  | (x :: y :: xs) h := (f x y (rel_of_chain_cons h)) ::
                       (chain'_apply_between (y :: xs) (chain'_desc_left h) )

end list

variables (R : Type) [ring R]
variables (M : Type) [add_comm_group M] [module R M]

class filtration :=
  (mods : list (submodule R M))
  (is_fil : list.chain' (has_le.le) mods)

def mk_quotient (U V : submodule R (M : Type)) (l : U ≤ V) : Type :=
  submodule.quotient ((submodule.map_subtype.order_iso V).inv_fun ⟨U, l⟩)


def factors (F : filtration R M) : list Type :=
  list.chain'_apply_between (mk_quotient R M) F.mods F.is_fil

variables (F : filtration R M) (h : factors R M F ≠ [])

#check M                                          /- M : Type -/
#check ((factors R M F).head'' h)                 /- list.head'' (factors R M F) h : Type -/
#check @neg_smul R M _ _ _                        /- neg_smul : ∀ (r : R) (x : M), -r • x = -(r • x) -/
#check @neg_smul R ((factors R M F).head'' h) _ _

The last line fails,

failed to synthesize type class instance for
R : Type,
_inst_1 : ring R,
M : Type,
_inst_2 : add_comm_group M,
_inst_3 : module R M,
F : filtration R M,
h : factors R M F ≠ list.nil
⊢ add_comm_group (list.head'' (factors R M F) h)

Now, there is an instance defined in mathlib for instance : add_comm_group (quotient p) , which, once you unpack head'' and chain'_apply_between is really what we are looking at.

How would be the best way to help lean find this instance? I have two ideas: either a bunch of lemmas that carry the instances over each step or bundling the type with its instance data (in a similar manner to submodule) so that it is all in one place. Are either of these good lean practice?

Hope I am not missing something obvious and stupid!

[Mario Carneiro]

I would first point out that your use of list Type is rather unidiomatic and can lead to this kind of issues

[Mario Carneiro]

It's almost useless to have a list Type because you don't know where the types came from so you don't know what structure they carry (like add_comm_group structure here)

[Mario Carneiro]

and you can't use the usual list lemmas because that leads to an equality of types which is problematic (aka "evil")

[Mario Carneiro]

One possibility is to use fin n -> Type instead, which has better characteristics. But you need to know n, which here is something like mods.length - 1 which is not so nice, especially in a rigid position like the n in fin n. You can remove the dependency by extending the list by some suitable default value past the end, for example if modn n := if h : n < mods.length then mods.nth_le n h else \top, then you can prove is_filn n : modn n <= modn (n+1) and then write factors n := mk_quotient (is_filn n) and now everything unfolds nicely.

[Robert Spencer]

I understand that list Type is a problem, exactly for the reasons stated.

I had thought that fin n -> A was almost interchangeable with list A, as there are suitable coercions between them (I think). As you say, though, fin n requires you to know n. This is not the end of the world for me I don't think. I'd much rather not extend the filtration past the top, as I would like to distinguish between 0 < U_1 < U_2 < M and 0 < U_1 < U_2 < M < M as filtrations.

This problem completely goes away if we have a list (submodule R M) for example because submodule R M is itself a structure and carries instances associated to that structure. In an earlier draft of this I redefined a modules structure along the lines of

structure modules (R : Type) [ring R] :=
  (carrier : Type)
  (add_comm_group : add_comm_group carrier)
  (module : module R carrier)

and then defined suitable coercions to Type, and instances of add_comm_group on that coercion etc. etc. This felt very dirty though, and not at all in the spirit of lean, but did let me have a list (modules R) very easily.

[Kevin Buzzard]

The problem seems to be that each of the subquotients has type Type, but type class inference isn't smart enough to spot that it can put a module structure on the subquotients. I suspect this problem could be solved by bundling. If you had a type whose terms were R-modules, rather than the current set-up where M is a parameter for the R-module set-up, then perhaps things would go better.

[Robert Spencer]

"Bundling" such as the above structure?

[Kevin Buzzard]

At the minute you have terms of type Type and it's not generally true that a random term of this type is a module, so Lean's typeclass system can't deal with what you are trying to do. I guess another possibility would be to make your own structure consisting of a list and an R-module structure of each element of the list, and then work with these structures.

[Kevin Buzzard]

Sorry, I'm on the London underground and I only have sporadic reception [messages are being sent before I see earlier messages you sent]. Yes, you're making the bundled category of R-modules. I am sure @Scott Morrison would thoroughly approve and would argue that it was, or perhaps should be, in the spirit of Lean. Different people seem to have different opinions on the matter.

[Kevin Buzzard]

Currently people believe that submodules of a given module should be a type, but that rings should not be a type (R should be a type and then the ring structure should be handled by the typeclass systems). Modules over a given ring are somewhere in the middle. Currently we're letting the typeclass system try and handle them -- but it's not clear to me whether this is "right" -- there will be advantages and disadvantages to each approach I guess. I will remark that we had real problems trying to make the typeclass system work with modules, there were a couple of failed attempts. The mathlib code

class module (α : Type u) (β : Type v) [ring α] [add_comm_group β] extends semimodule α β

structure module.core (α β) [ring α] [add_comm_group β] extends has_scalar α β :=
(smul_add : ∀(r : α) (x y : β), r • (x + y) = r • x + r • y)
(add_smul : ∀(r s : α) (x : β), (r + s) • x = r • x + s • x)
(mul_smul : ∀(r s : α) (x : β), (r * s) • x = r • s • x)
(one_smul : ∀x : β, (1 : α) • x = x)

def module.of_core {α β} [ring α] [add_comm_group β] (M : module.core α β) : module α β :=
by letI := M.to_has_scalar; exact
{ zero_smul := λ x,
    have (0 : α) • x + (0 : α) • x = (0 : α) • x + 0, by rw ← M.add_smul; simp,
    add_left_cancel this,
  smul_zero := λ r,
    have r • (0:β) + r • 0 = r • 0 + 0, by rw ← M.smul_add; simp,
    add_left_cancel this,
  ..M }

already seems to indicate that something funny is going on.

[Chris Hughes]

The best way would be to stick to submodules in your list, and then only quotient by them at the end. A fin n -> Type would also be better, because you can easily get the instance, by just unfolding the function, and you will have the right definitional equalities.

[Kevin Buzzard]

But if the entire R-module structure is bundled then he can just use lists, right? There is a category of R-modules. Was this ever created? Do these help to solve the problem?

[Robert Spencer]

@Chris Hughes Not quite understanding what you mean by "only quotient by them at the end". If you mean that (U : submodule R M) encodes the same information as M / U, then this is true, but I'd have to have a list where each member is a submodule of the next, which seems messy.

[Chris Hughes]

Something like this (not sure if this Type checks, but hopefully you get the idea)

def mk_quotient (U V : submodule R (M : Type)) (l : U ≤ V) : Type :=
(submodule.map_subtype.order_iso V).inv_fun ⟨U, l⟩

def factors (F : filtration R M) : list (submodule R M) :=
  list.chain'_apply_between (mk_quotient R M) F.mods F.is_fil

#check @neg_smul R (submodule.quotient ((factors R M F).head'' h)) _ _

[Robert Spencer]

Hmm. So if, for example, I wanted to check some filtration were a composition series I'd have to do

∀ (N : list.map submodule.quotient (factors R M F)), is_simple N

I feel like it would be neater if I could write

(factors R M F) ⊆ { N // is_simple N }

which I think I could get with a bundled object.

Is the consensus that this is currently a stylistic choice: bundle or not?

[Kevin Buzzard]

Chris and Mario have suggested sticking with unbundled modules, and they have written a lot more Lean code than I have. But submodules are bundled and subgroups are not bundled, which in my mind is evidence that the community is still learning what the best way to go about things is. I don't see anything wrong with bundling modules. Perhaps if you try it you'll see the problems which I cannot.

[Chris Hughes]

You can still write

(factors R M F) ⊆ { N | is_simple (submodule.quotient N) }

(you'd have to coerce the list into a set for this to work)

[Chris Hughes]

This is nicer from a category theoretic perspective, because if your objects are submodules, your category is small. This might be useful at some point.

[Kevin Buzzard]

The problem with using submodule is that if you are taking subquotients of a chain of submodules then everything is a submodule of everything above it and there is not one canonical module for which the submodules are the answer.

Perhaps another approach is bundled subquotients of a module. I think this would be a very interesting way of going about things. You carry around A and B, submodules of some fixed module M, with A a subset of B, and this represents the quotient module B/A. You'd have to write an API for this but if the community think that submodules are worth bundling, surely bundling subquotients is also a natural idea.

[Kevin Buzzard]

Assia Mahboubi wrote a paper called "the rooster and the butterfly" where she talks about subquotients of groups in Coq. This might have some relevant ideas. The more CS-minded people in this conversation seem to be against the idea of bundling modules, but perhaps they would be more open to the idea of bundling subquotients of a given module.

[Mario Carneiro]

I'm open to the idea of bundling subquotients, but first I would like to know what that is exactly. It doesn't quite line up with our current definitions; is there a single set of all subquotients of a module?

[Kevin Buzzard]

Yes. A subquotient of a module $M$ is just $B/A$, where $A\subseteq B\subseteq M$ are submodules.

[Kevin Buzzard]

A subquotient of $M$ is equivalently a subset of a quotient of $M$, or a quotient of a subset of $M$.

[Mario Carneiro]

but you have to equate isomorphic subquotients I assume?

[Kevin Buzzard]

I think it's better than that.

[Kevin Buzzard]

If you're dealing with subquotients then you can literally keep track of just the two submodules.

[Mario Carneiro]

Is the set simply a subset of the product of subquotients then?

[Kevin Buzzard]

Quotienting $B/A$ is just making $A$ bigger, and submoduling it is making $B$ smaller.

[Kevin Buzzard]

You mean a product of submodules I suspect. Yes.

[Mario Carneiro]

I mean a subquotient is encoded as a pair of submodules

[Kevin Buzzard]

Right.

[Mario Carneiro]

It's not obvious to me that this has nice algebraic properties like submodules do though

[Mario Carneiro]

That is, the collection of submodules is a "space", not just a "set"

[Kevin Buzzard]

There is such a thing as a simple subquotient -- a subquotient which is simple as a module. A simple module is a module which has precisely two submoules, bot and top.

[Mario Carneiro]

That, to me, is the compelling justification for bundling. If we are only claiming that subquotients are determined by this data (a pair A <= B), then you could just as well do that with a function mk_quotient (A B) (h: A <= B): Type

[Kevin Buzzard]

Simple modules are the analogue of prime numbers. Every positive integer is a uniquely a product of primes. For modules life isn't so simple. Recall that a $\mathbb{Z}$-module is just the same as an abelian group. The $\mathbb{Z}$-module $\mathbb{Z}/4\mathbb{Z}$ is not simple, and even worse, it's not even isomorphic to a product of simple modules.

[Kevin Buzzard]

However given a module with certain finiteness properties (e.g. a finite abelian group) one can produce a "saturated chain" of submodules $0=M_0\subset M_1\subset M_2\subset\cdots\subset M_n=M$, with each subquotient $M_{i+1}/M_i$ simple.

[Kevin Buzzard]

And the theorem is that the multiset of isomorphism classes of simple factors is an invariant of the module.

[Mario Carneiro]

I understand that list Type is a problem, exactly for the reasons stated.

I had thought that fin n -> A was almost interchangeable with list A, as there are suitable coercions between them (I think). As you say, though, fin n requires you to know n. This is not the end of the world for me I don't think. I'd much rather not extend the filtration past the top, as I would like to distinguish between 0 < U_1 < U_2 < M and 0 < U_1 < U_2 < M < M as filtrations.

To be clear, I'm not saying that the filtration actually extends past the top. This is only an encoding trick - the list (submodule R M) is still just as it was

[Kevin Buzzard]

For example, for the cyclic groups $C_4$ and $C_2\times C_2$ the multisets are $C_2$ with multiplicity 2 (in both cases), so you can't reconstruct a module from its irreducible subquotients. However the multiset is still useful -- for example in algebraic geometry one often does induction on the size of the multiset (with the inductive step typically being straightforward and the base case being the interesting one).

[Mario Carneiro]

That is, the filtrations 0 < U_1 < U_2 < M and 0 < U_1 < U_2 < M < M are distinct, but the function factors F : nat -> Type is the same for both filtrations. You just remember that they have different lengths and the function is "garbage" past the end

[Kevin Buzzard]

That is, the collection of submodules is a "space", not just a "set"

I find it hard to imagine a definition of "space" where the submodules form a space and the subquotients do not. The subquotients are a subspace of the product of two copies of the space of submodules.

[Mario Carneiro]

My question is mostly directed at whether that encoding is reflecting some real structure that we care about or if it's just the usual "a group is a 4-tuple" business

[Kevin Buzzard]

In some cases (for example subspaces of a finite-dimensional real vector space) the "space" of submodules really do naturally form a topological space, with one connected component for each dimension. But similarly the subquotients do too, they're a topological space with one connected component for each pair (dim A, dim B).

[Mario Carneiro]

Are they a lattice?

[Mario Carneiro]

Or at least, is there an ordering

[Kevin Buzzard]

You can visualise the space of $d$-dimensional submodules of $\mathbb{R}^n$ as a quotient $GL_n(\mathbb{R})/P$ where $P$ is a subgroup of "block upper triangular matrices" consisting of a $d\times d$ block at the top and an $(n-d)\times (n-d)$ block at the bottom. You can get more general subquotients (or even chains of submodules) by using other choices of "parabolic subgroup" P with more blocks on the diagonal.

[Kevin Buzzard]

I don't think I can intersect two subquotients, but I am more confident about an ordering. I think I would suggest that $B/A$ and $B'/A'$ were incomparable unless $A=A'$ in which case it goes on the subset ordering on the $$B$$s.

[Kevin Buzzard]

One could risk $(B\cap B')/(A\cap A')$ but it might not be a great idea. It looks a bit odd to me in the sense that I've not seen it before.

[Mario Carneiro]

Oh, I was going to guess $B_1/A_1 \le B_2/A_2$ iff $B_1\le B_2$ and $A_2\le A_1$

[Kevin Buzzard]

It might work but not be useful, or it might work and be a really cool way of thinking about things, or it might just not work.

[Kevin Buzzard]

One could I guess also say $B_1/A_1\leq B_2/A_2$ iff there was a "natural map" from one to the other, like for submodules.

[Kevin Buzzard]

If you did that you'd get $A_1\subseteq A_2$ and $B_1\subseteq B_2$

[Mario Carneiro]

Your point about considering subquotients as generalizations of submodules by inserting an additional block, and filtrations as a further generalization to multiple blocks, suggests a way to encode this as an inductive type, which might work out nicer

[Kevin Buzzard]

Grassmannians are the topological spaces which one gets by considering filtrations on a finite-dimensional vector space. Because they can be computed as quotients of general linear groups by subgroups there is also a purely algebraic way of thinking about them, where your base field is now arbitrary and the quotients are (non-affine) schemes.

[Kevin Buzzard]

Projective 1-space is the space of 1-dimensional subspaces of a 2-dimensional vector space. These are the first natural examples of non-affine schemes. @Kenny Lau how is gluing?

[Kevin Buzzard]

Do we have Grassmannians yet? ;-)

[Mario Carneiro]

universe u
open lattice
inductive transit {α : Type u} [preorder α] : α → α → Type u
| one (a b) : a ≤ b → transit a b
| trans (a b c) : transit a b → transit b c → transit a c

def filtration (α) [bounded_lattice α] := transit (⊥ : α) ⊤

The downside of this encoding is that it distinguishes reassociated sequences, i.e. 0 < (A < (B < M)) vs (0 < A) < (B < M)

[Mario Carneiro]

Here's how you can say that a filtration is simple:

import linear_algebra.basic

universe u
open lattice
inductive transit {α : Type u} [preorder α] : α → α → Type u
| one (a b) : a ≤ b → transit a b
| trans (a b c) : transit a b → transit b c → transit a c

def filtration (α) [bounded_lattice α] := transit (⊥ : α) ⊤

structure le_pair (α : Type u) [preorder α] := (a b : α) (a_le_b : a ≤ b)

def transit.factors {α} [preorder α] : ∀ {a b : α}, transit a b → list (le_pair α)
| _ _ (transit.one a b h) := [⟨a, b, h⟩]
| _ _ (transit.trans a b c t1 t2) := t1.factors ++ t2.factors

def subquotient {α β} [ring α] [add_comm_group β] [module α β]
  (p : le_pair (submodule α β)) := (submodule.comap p.b.subtype p.a).quotient

instance {α β} [ring α] [add_comm_group β] [module α β] (p : le_pair (submodule α β)) :
  add_comm_group (subquotient p) := submodule.quotient.add_comm_group _
instance {α β} [ring α] [add_comm_group β] [module α β] (p : le_pair (submodule α β)) :
  module α (subquotient p) := submodule.quotient.module _

def module.is_simple (α β) [ring α] [add_comm_group β] [module α β] : Prop := sorry

def filtration.is_simple (α β) [ring α] [add_comm_group β] [module α β]
  (F : filtration (submodule α β)) : Prop :=
∀ p ∈ F.factors, module.is_simple α (subquotient p)

[Robert Spencer]

I'll have to take some time to look at that solution and wrap my head around it, and how transit is really different from a list with a chain' (in particular, I think one could replace transit.factors with some sort of chain'_factors (l : list \a) [chain' <= l] : list (le_pair \a) and get a similar result.

[Robert Spencer]

Thanks for the pointers though

[Robert Spencer]

I think for now I'll just treat sub quotients as these le_pairs until something better comes around

[Mario Carneiro]

You can still use list and chain; the key point here is that you don't put types in a list, you put the data from which you generate the types

[Mario Carneiro]

But I think it would be better to use structures that encode the relevant invariants, so that for example it's not possible to have an empty factors list, rather than having a predicate on the side to assert this

[Mario Carneiro]

You can also avoid the reassociation problem by structuring the inductive type a little differently so that it's all associated one way (this is basically what the list representation gives you), but this has different defeq simplifications and introduces a bias for one kind of association over the other. Whether this matters one way or another depends on details of the application

[Robert Spencer]

When I said use a list I meant something more along the lines of

import linear_algebra.basic

universe u
open lattice

class filtration (α) [preorder α] := (modules : list α) (c : list.chain' (≤) modules)

structure le_pair (α : Type u) [preorder α] := (a b : α) (a_le_b : a ≤ b)

variables {α : Type} {R : α → α → Prop} {x y : α} {L L₁ L₂ : list α}
lemma chain'_of_first_two : list.chain' R (x :: y :: L) → R x y := by dunfold list.chain'; simp; exact λ a b, a
lemma chain'_desc_left : list.chain' R (x :: L) → list.chain' R L := by cases L; simp[list.chain']

def filtration.factors {α} [bounded_lattice α] : filtration α → list (le_pair α)
| ⟨ [],       _ ⟩ := []
| ⟨ [x],      _ ⟩ := []
| ⟨ (x::y::l),h ⟩ := ⟨ x, y , chain'_of_first_two h⟩ :: (filtration.factors ⟨ (y::l), (chain'_desc_left h)⟩ )

def subquotient {α β} [ring α] [add_comm_group β] [module α β]
  (p : le_pair (submodule α β)) := (submodule.comap p.b.subtype p.a).quotient

instance {α β} [ring α] [add_comm_group β] [module α β] (p : le_pair (submodule α β)) :
  add_comm_group (subquotient p) := submodule.quotient.add_comm_group _
instance {α β} [ring α] [add_comm_group β] [module α β] (p : le_pair (submodule α β)) :
  module α (subquotient p) := submodule.quotient.module _

def module.is_simple (α β) [ring α] [add_comm_group β] [module α β] : Prop := sorry

def filtration.is_simple (α β) [ring α] [add_comm_group β] [module α β]
  (F : filtration (submodule α β)) : Prop :=
∀ p ∈ F.factors, module.is_simple α (subquotient p)

which I am pretty sure never has a list of types?

[Robert Spencer]

To return to the bundling issue, am I going to run into problems when I try to define equivalence classes of modules? From a (very brief) reading of setoid and quot, you aren't allowed to tack classes onto the types. In particular this

import data.set.function
import algebra.module

variables {R : Type} [ring R] (M : Type) [add_comm_group M] [module R M] (N : Type) [add_comm_group N] [module R N]

def are_isomorphic := ∃ (f : M →ₗ[R] N), function.bijective f ∧ ...

#check quot are_isomorphic
#check (⟨ are_isomorphic, sorry ⟩ : setoid Type)

gives errors, and I feel very dirty defining setoid Type

[Kevin Buzzard]

If you want to deal with isomorphism classes of R-modules then this is another argument that says you should be bundling them. Independent of this, the usual way in Lean to express that two objects are isomorphic is not to ask for a bijection between them but to ask for functions in each direction whose composite is the identity -- see e.g. data.equiv.basic (which also provides notation \equiv)

[Kevin Buzzard]

The more you talk about the sort of things you are interested in, the more I am convinced you should just be working with a type representing the category of R-modules. I still don't know if such a type is in Lean (I was hoping that Scott would have chimed in by now) but even if it doesn't exist I would suspect that it wouldn't be too much trouble to make. Then you have all the category machinery available to you and in particular the notion of isomorphism would be available to you already together with all standard theorems you'll need about it (transitivity etc).

[Robert Spencer]

the usual way in Lean to express that two objects are isomorphic is not to ask for a bijection between them but to ask for functions in each direction whose composite is the identity -- see e.g. data.equiv.basic (which also provides notation \equiv)

yes, I think I've seen this, but wanted to throw together a MWE above.

[Robert Spencer]

I know next-to-nothing about categories in lean. Is there any documentation or sample code I could peruse?

[Kevin Buzzard]

https://github.com/leanprover-community/mathlib/blob/master/docs/tutorial/category_theory/calculating_colimits_in_Top.lean

[Kevin Buzzard]

But another alternative is just to write the stuff yourself without categories. It will be a pleasant, but long, exercise. I don't know which will be easier. You bundle modules like earlier in the thread, bundle linear maps, and you can make your own kernels and cokernels. I'm really sorry -- it's the kind of thing I would just spend a couple of hours doing because I like that kind of thing, but I am really snowed under at the minute.

[Robert Spencer]

Ok. I'll take a look. I'm not so keen on the idea (in general) of writing custom bundlings for every algebraic structure (once modules are done, what about bimodules, comodules etc. etc.) so I'll look into categories first.

[Kevin Buzzard]

This has been Scott's argument too. In mathlib we are still figuring out the right way to do things, and several approaches have been tried (and I am partly to blame for this) . I am working with two summer students on group theory and we have been using unbundled groups but bundled subgroups and isomorphisms, so we're having to write our own theorems such as if $G\cong H$ and $H\cong K$ then $G\cong K$, and are introducing new notation for each kind of isomorphism. With the category theory approach we get all these for free.

[Robert Spencer]

Ok, I think I have a (very ugly) first pass at this, culminating in the line

variables (R : Type) [ring R] (M : Module R)

variable (F : filtration (submodule R M))

def filtration.is_composition_series : Prop := ∀ p ∈ F.factors, is_simple (subquotient' R M p)

There are many ugly bits, mostly due to my ignorance (e.g. stating a object in a category is isomorphic to another), but it works. At last. I think.
https://github.com/rspencer01/lean_representation_theory/tree/master/src

[Mario Carneiro]

What's up with the remark on submodule not inferring add_comm_group?

[Mario Carneiro]

I think the issue might be in the definition of Module

[Mario Carneiro]

r_mod is a bad idea

[Robert Spencer]

I'm very happy to suggestions/corrections. I defined r_mod because bundled only works on a single class.

[Mario Carneiro]

You should probably define Module directly rather than using bundled

[Mario Carneiro]

I don't think it's actually saving you that much work, you still have to associate the right category structure

[Mario Carneiro]

and don't make it reducible

[Robert Spencer]

Ah.

I was basically copying mathlib's group_theory.category

[Robert Spencer]

I still am not certain what is up with submodule and add_comm_group. Here is an example:

variable (p : filtration.le_pair (submodule R M))
#check p.b
/- p.b : submodule R ↥M -/
#check @submodule.comap _ _ _ _ (submodule.add_comm_group p.b) _ _ _ p.b.subtype p.a
/- submodule.comap (submodule.subtype (p.b)) (p.a) : submodule R ↥(p.b) -/
#check @submodule.comap _ _ _ _ _                              _ _ _ p.b.subtype p.a
/- maximum class-instance resolution depth has been reached (the limit can be increased by setting option 'class.instance_max_depth') (the class-instance resolution trace can be visualized by setting option 'trace.class_instances')-/

which seems to indicate that it can't find an instance of add_comm_group for p.b, an honest submodule R ↥M.

To me this feels like a problem in submodule, rather than Module.

[Robert Spencer]

In fact, the same happens if I replace M : Module R with (N : Type) [add_comm_group N] [module R N]

[Robert Spencer]

Whoops. Nevermind. I retract that. Its only a problem when I import Module.