Zulip Chat Archive

Stream: new members

Topic: Pulling class instances through "complicated" computations


view this post on Zulip Robert Spencer (Aug 08 2019 at 08:43):

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!

view this post on Zulip Mario Carneiro (Aug 08 2019 at 09:03):

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

view this post on Zulip Mario Carneiro (Aug 08 2019 at 09:04):

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)

view this post on Zulip Mario Carneiro (Aug 08 2019 at 09:05):

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

view this post on Zulip Mario Carneiro (Aug 08 2019 at 09:14):

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.

view this post on Zulip Robert Spencer (Aug 08 2019 at 09:36):

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.

view this post on Zulip Kevin Buzzard (Aug 08 2019 at 09:36):

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.

view this post on Zulip Robert Spencer (Aug 08 2019 at 09:39):

"Bundling" such as the above structure?

view this post on Zulip Kevin Buzzard (Aug 08 2019 at 09:41):

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.

view this post on Zulip Kevin Buzzard (Aug 08 2019 at 09:43):

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.

view this post on Zulip Kevin Buzzard (Aug 08 2019 at 09:49):

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.

view this post on Zulip Chris Hughes (Aug 08 2019 at 10:06):

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.

view this post on Zulip Kevin Buzzard (Aug 08 2019 at 10:34):

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?

view this post on Zulip Robert Spencer (Aug 08 2019 at 11:07):

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

view this post on Zulip Chris Hughes (Aug 08 2019 at 11:24):

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)) _ _

view this post on Zulip Robert Spencer (Aug 08 2019 at 11:44):

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?

view this post on Zulip Kevin Buzzard (Aug 08 2019 at 11:57):

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.

view this post on Zulip Chris Hughes (Aug 08 2019 at 11:58):

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)

view this post on Zulip Chris Hughes (Aug 08 2019 at 12:00):

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.

view this post on Zulip Kevin Buzzard (Aug 08 2019 at 12:02):

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.

view this post on Zulip Kevin Buzzard (Aug 08 2019 at 12:03):

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.

view this post on Zulip Mario Carneiro (Aug 08 2019 at 12:32):

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?

view this post on Zulip Kevin Buzzard (Aug 08 2019 at 12:32):

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

view this post on Zulip Kevin Buzzard (Aug 08 2019 at 12:33):

A subquotient of MM is equivalently a subset of a quotient of MM, or a quotient of a subset of MM.

view this post on Zulip Mario Carneiro (Aug 08 2019 at 12:33):

but you have to equate isomorphic subquotients I assume?

view this post on Zulip Kevin Buzzard (Aug 08 2019 at 12:33):

I think it's better than that.

view this post on Zulip Kevin Buzzard (Aug 08 2019 at 12:34):

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

view this post on Zulip Mario Carneiro (Aug 08 2019 at 12:34):

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

view this post on Zulip Kevin Buzzard (Aug 08 2019 at 12:34):

Quotienting B/AB/A is just making AA bigger, and submoduling it is making BB smaller.

view this post on Zulip Kevin Buzzard (Aug 08 2019 at 12:34):

You mean a product of submodules I suspect. Yes.

view this post on Zulip Mario Carneiro (Aug 08 2019 at 12:34):

I mean a subquotient is encoded as a pair of submodules

view this post on Zulip Kevin Buzzard (Aug 08 2019 at 12:34):

Right.

view this post on Zulip Mario Carneiro (Aug 08 2019 at 12:35):

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

view this post on Zulip Mario Carneiro (Aug 08 2019 at 12:35):

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

view this post on Zulip Kevin Buzzard (Aug 08 2019 at 12:35):

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.

view this post on Zulip Mario Carneiro (Aug 08 2019 at 12:37):

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

view this post on Zulip Kevin Buzzard (Aug 08 2019 at 12:37):

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 Z\mathbb{Z}-module is just the same as an abelian group. The Z\mathbb{Z}-module Z/4Z\mathbb{Z}/4\mathbb{Z} is not simple, and even worse, it's not even isomorphic to a product of simple modules.

view this post on Zulip Kevin Buzzard (Aug 08 2019 at 12:38):

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

view this post on Zulip Kevin Buzzard (Aug 08 2019 at 12:38):

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

view this post on Zulip Mario Carneiro (Aug 08 2019 at 12:39):

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

view this post on Zulip Kevin Buzzard (Aug 08 2019 at 12:40):

For example, for the cyclic groups C4C_4 and C2×C2C_2\times C_2 the multisets are C2C_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).

view this post on Zulip Mario Carneiro (Aug 08 2019 at 12:42):

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

view this post on Zulip Kevin Buzzard (Aug 08 2019 at 12:44):

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.

view this post on Zulip Mario Carneiro (Aug 08 2019 at 12:45):

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

view this post on Zulip Kevin Buzzard (Aug 08 2019 at 12:46):

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

view this post on Zulip Mario Carneiro (Aug 08 2019 at 12:47):

Are they a lattice?

view this post on Zulip Mario Carneiro (Aug 08 2019 at 12:48):

Or at least, is there an ordering

view this post on Zulip Kevin Buzzard (Aug 08 2019 at 12:49):

You can visualise the space of dd-dimensional submodules of Rn\mathbb{R}^n as a quotient GLn(R)/PGL_n(\mathbb{R})/P where PP is a subgroup of "block upper triangular matrices" consisting of a d×dd\times d block at the top and an (nd)×(nd)(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.

view this post on Zulip Kevin Buzzard (Aug 08 2019 at 12:50):

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

view this post on Zulip Kevin Buzzard (Aug 08 2019 at 12:51):

One could risk (BB)/(AA)(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.

view this post on Zulip Mario Carneiro (Aug 08 2019 at 12:51):

Oh, I was going to guess B1/A1B2/A2B_1/A_1 \le B_2/A_2 iff B1B2B_1\le B_2 and A2A1A_2\le A_1

view this post on Zulip Kevin Buzzard (Aug 08 2019 at 12:51):

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.

view this post on Zulip Kevin Buzzard (Aug 08 2019 at 12:52):

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

view this post on Zulip Kevin Buzzard (Aug 08 2019 at 12:53):

If you did that you'd get A1A2A_1\subseteq A_2 and B1B2B_1\subseteq B_2

view this post on Zulip Mario Carneiro (Aug 08 2019 at 12:53):

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

view this post on Zulip Kevin Buzzard (Aug 08 2019 at 12:54):

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.

view this post on Zulip Kevin Buzzard (Aug 08 2019 at 12:58):

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?

view this post on Zulip Kevin Buzzard (Aug 08 2019 at 12:59):

Do we have Grassmannians yet? ;-)

view this post on Zulip Mario Carneiro (Aug 08 2019 at 13:03):

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)

view this post on Zulip Mario Carneiro (Aug 08 2019 at 13:28):

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)

view this post on Zulip Robert Spencer (Aug 08 2019 at 15:14):

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.

view this post on Zulip Robert Spencer (Aug 08 2019 at 15:14):

Thanks for the pointers though

view this post on Zulip Robert Spencer (Aug 08 2019 at 15:15):

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

view this post on Zulip Mario Carneiro (Aug 08 2019 at 15:46):

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

view this post on Zulip Mario Carneiro (Aug 08 2019 at 15:47):

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

view this post on Zulip Mario Carneiro (Aug 08 2019 at 15:49):

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

view this post on Zulip Robert Spencer (Aug 08 2019 at 16:15):

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?

view this post on Zulip Robert Spencer (Aug 09 2019 at 07:15):

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

view this post on Zulip Kevin Buzzard (Aug 09 2019 at 07:33):

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)

view this post on Zulip Kevin Buzzard (Aug 09 2019 at 07:36):

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

view this post on Zulip Robert Spencer (Aug 09 2019 at 08:36):

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.

view this post on Zulip Robert Spencer (Aug 09 2019 at 08:37):

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

view this post on Zulip Kevin Buzzard (Aug 09 2019 at 08:42):

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

view this post on Zulip Kevin Buzzard (Aug 09 2019 at 08:44):

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.

view this post on Zulip Robert Spencer (Aug 09 2019 at 08:48):

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.

view this post on Zulip Kevin Buzzard (Aug 09 2019 at 09:01):

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 GHG\cong H and HKH\cong K then GKG\cong K, and are introducing new notation for each kind of isomorphism. With the category theory approach we get all these for free.

view this post on Zulip Robert Spencer (Aug 10 2019 at 11:22):

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

view this post on Zulip Mario Carneiro (Aug 10 2019 at 12:08):

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

view this post on Zulip Mario Carneiro (Aug 10 2019 at 12:09):

I think the issue might be in the definition of Module

view this post on Zulip Mario Carneiro (Aug 10 2019 at 12:10):

r_mod is a bad idea

view this post on Zulip Robert Spencer (Aug 10 2019 at 12:12):

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

view this post on Zulip Mario Carneiro (Aug 10 2019 at 12:12):

You should probably define Module directly rather than using bundled

view this post on Zulip Mario Carneiro (Aug 10 2019 at 12:13):

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

view this post on Zulip Mario Carneiro (Aug 10 2019 at 12:13):

and don't make it reducible

view this post on Zulip Robert Spencer (Aug 10 2019 at 12:14):

Ah.

I was basically copying mathlib's group_theory.category

view this post on Zulip Robert Spencer (Aug 10 2019 at 12:21):

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.

view this post on Zulip Robert Spencer (Aug 10 2019 at 12:29):

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

view this post on Zulip Robert Spencer (Aug 10 2019 at 12:45):

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


Last updated: May 14 2021 at 06:16 UTC