Zulip Chat Archive

Stream: Is there code for X?

Topic: generators smul generators generate


view this post on Zulip Damiano Testa (Mar 06 2021 at 15:55):

Dear All,

let S be an R-algebra and M an S-module. Suppose that gs : set S is a set of generators of Sas an R-module and gm : set M is a set of generators of M as an S-module. Is it already in Lean the statement that the products s • m, for s ∈ gs and m ∈ gmgenerate M as an R-module?

Thank you!

view this post on Zulip Eric Wieser (Mar 06 2021 at 15:55):

(deleted)

view this post on Zulip Damiano Testa (Mar 06 2021 at 15:56):

Fixed!

view this post on Zulip Kenny Lau (Mar 06 2021 at 15:59):

theorem span_smul {s : set S} (hs : span R s = ) (t : set A) :
  span R (s  t) = (span S t).restrict_scalars R :=

view this post on Zulip Kenny Lau (Mar 06 2021 at 15:59):

https://github.com/leanprover-community/mathlib/blob/b04aeb5e19faa21c2ae76158fc8454bb236f5f4f/src/algebra/algebra/tower.lean#L266

view this post on Zulip Damiano Testa (Mar 06 2021 at 15:59):

Great, thanks Kenny!

view this post on Zulip Eric Wieser (Mar 06 2021 at 16:00):

Is your statement something like [algebra R S] [module S M] (hs : subalgebra.adjoin gs = \top) (hm : submodule.span S gm =\top) : submodule.span R {...} = \top?

view this post on Zulip Damiano Testa (Mar 06 2021 at 16:00):

Eric, yes, with some is_scalar_tower scattered around as well.

view this post on Zulip Damiano Testa (Mar 06 2021 at 16:01):

I will try to see if what Kenny sent works, but it looks like it is exactly what I need!

view this post on Zulip Eric Wieser (Mar 06 2021 at 16:03):

Unrelatedly, the docs#submodule.smul_mem_span_smul' next to Kenny's lemma looks like a special case of docs#submodule.smul_mem?

view this post on Zulip Damiano Testa (Mar 06 2021 at 18:34):

Continuing in this thread, I like the \smul notation for multiplying set ??, but it seems that I cannot smultiply finset ?? by finset ??.

Since I am a little worried of finset, before embarking in proving that the smultiplication of finsets is a finset, I wanted to make sure that this is really not in mathlib yet.

So... are finsets smultiplicable in mathlib?

view this post on Zulip Damiano Testa (Mar 06 2021 at 18:35):

(For those who are curious about why I care about this, I am trying to prove that in the "generator tower" mentioned at the beginning of the thread, if I start with finite generating sets for the two parts, then I get a finite generating set over the whole tower.)

view this post on Zulip Kevin Buzzard (Mar 06 2021 at 18:59):

Why not just use sets with a finite hypothesis? I think this makes things easier.

view this post on Zulip Damiano Testa (Mar 06 2021 at 19:56):

Ok, I will try!

view this post on Zulip Damiano Testa (Mar 06 2021 at 20:06):

Kevin, your suggestion reduces my problem to the lemma below. If you have any suggestions of what I can try to remove the sorry, I will be happy to hear it!

import algebra.algebra.tower

lemma finite.smul_of_finite {S M : Type*} [semiring S] [add_comm_monoid M] [semimodule S M]
  {G : set S} {v : set M} (fG : G.finite) (fv : v.finite) :
  (G  v).finite :=
begin
  sorry
end

view this post on Zulip Kevin Buzzard (Mar 06 2021 at 20:09):

The library will know that the product of G and v (a subset of S x M) is finite, and that the image of a finite set is finite.

view this post on Zulip Damiano Testa (Mar 06 2021 at 20:18):

So, I should first prove that (G • v) is a fintype? Sorry about the silly questions, but I am not really able to make much progress on this.

view this post on Zulip Damiano Testa (Mar 06 2021 at 20:34):

I managed to construct a function from the cartesian product to the smul-product, but even assuming a fintype instance on the product, Lean would not allow me to prove fintype from a surjection:

lemma finite.smul_of_finite {S M : Type*} [semiring S] [add_comm_monoid M] [semimodule S M]
  {G : set S} {v : set M} (fG : G.finite) (fv : v.finite) :
  (G  v).finite :=
begin
  let f : G × v  G  v := λ ⟨⟨g, gG⟩, v, vM⟩⟩, g  v, _, v, gG, vM, rfl⟩⟩⟩,
  haveI : fintype G × v := sorry,
  have : fintype (G  v : set M),
  refine fintype.of_surjective f _,
--- here is the error:
failed to synthesize type class instance for
S : Type u_1,
M : Type u_2,
_inst_2 : semiring S,
_inst_3 : add_comm_monoid M,
_inst_4 : semimodule S M,
G : set S,
v : set M,
fG : G.finite,
fv : v.finite,
f : G × v  (G  v) :=
  λ (_x : G × v),
    (λ (_a : G × v),
       _a.cases_on
         (λ (fst : G) (snd : v),
            subtype.cases_on fst
              (λ (fst_val : S) (fst_property : fst_val  G),
                 subtype.cases_on snd
                   (λ (snd_val : M) (snd_property : snd_val  v),
                      id_rhs {x // x  G  v} fst_val  snd_val, _⟩))))
      _x,
_inst : fintype G × v
 fintype (G × v)

end

view this post on Zulip Eric Wieser (Mar 06 2021 at 20:45):

Does letI work better than haveI?

view this post on Zulip Damiano Testa (Mar 06 2021 at 20:46):

Eric, I got it down to just the product instance:

lemma finite.smul_of_finite {S M : Type*} [semiring S] [add_comm_monoid M] [semimodule S M]
  {G : set S} {v : set M} (fG : G.finite) (fv : v.finite) :
  (G  v).finite :=
begin
  let f : G × v  G  v := λ ⟨⟨g, gG⟩, v, vM⟩⟩, g  v, _, v, gG, vM, rfl⟩⟩⟩,
  haveI : fintype (G × v) := begin
  {
    sorry,
  }
  end,
  have : fintype (G  v : set M),
  { refine fintype.of_surjective f _,
    rintro j_val, g, m, gG, mv, rfl⟩,
    use g,
    { exact gG },
    { use m,
      exact mv },
    { exact subtype.mk_eq_mk.mpr rfl } },
  { exact finite.smul_of_finite fG fv }
end

view this post on Zulip Eric Wieser (Mar 06 2021 at 20:48):

docs#prod.fintype?

view this post on Zulip Damiano Testa (Mar 06 2021 at 20:50):

I think that the issue is that when I write G, it is no longer a set, but a weird type and Lean does not seem to know that G.fintype means that this weird type is also a fintype...

view this post on Zulip Damiano Testa (Mar 06 2021 at 20:51):

so when I apply prod.fintype, Lean tells me that there is no fintype instance on G:

failed to synthesize type class instance for
S : Type u_1,
M : Type u_2,
_inst_2 : semiring S,
_inst_3 : add_comm_monoid M,
_inst_4 : semimodule S M,
G : set S,
v : set M,
fG : G.finite,
fv : v.finite,
f : G × v  (G  v) :=
  λ (_x : G × v),
    (λ (_a : G × v),
       _a.cases_on
         (λ (fst : G) (snd : v),
            subtype.cases_on fst
              (λ (fst_val : S) (fst_property : fst_val  G),
                 subtype.cases_on snd
                   (λ (snd_val : M) (snd_property : snd_val  v),
                      id_rhs {x // x  G  v} fst_val  snd_val, _⟩))))
      _x
 fintype G

view this post on Zulip Eric Wieser (Mar 06 2021 at 20:52):

Well add two new haveIs for those instances then!

view this post on Zulip Damiano Testa (Mar 06 2021 at 20:52):

Indeed! This is where I am now:

lemma finite.smul_of_finite {S M : Type*} [semiring S] [add_comm_monoid M] [semimodule S M]
  {G : set S} {v : set M} (fG : G.finite) (fv : v.finite) :
  (G  v).finite :=
begin
  let f : G × v  G  v := λ ⟨⟨g, gG⟩, v, vM⟩⟩, g  v, _, v, gG, vM, rfl⟩⟩⟩,
  haveI : fintype G := sorry,
  haveI : fintype v := sorry,
  haveI : fintype (G × v) := prod.fintype G v,
  have : fintype (G  v : set M),
  { refine fintype.of_surjective f _,
    rintro j_val, g, m, gG, mv, rfl⟩,
    use g,
    { exact gG },
    { use m,
      exact mv },
    { exact subtype.mk_eq_mk.mpr rfl } },
  { exact finite.smul_of_finite fG fv }
end

view this post on Zulip Damiano Testa (Mar 06 2021 at 20:53):

library_search: haveI : fintype G := set.finite.fintype fG!

view this post on Zulip Damiano Testa (Mar 06 2021 at 20:53):

This works!

lemma finite.smul_of_finite {S M : Type*} [semiring S] [add_comm_monoid M] [semimodule S M]
  {G : set S} {v : set M} (fG : G.finite) (fv : v.finite) :
  (G  v).finite :=
begin
  let f : G × v  G  v := λ ⟨⟨g, gG⟩, v, vM⟩⟩, g  v, _, v, gG, vM, rfl⟩⟩⟩,
  haveI : fintype G := set.finite.fintype fG,
  haveI : fintype v := set.finite.fintype fv,
  haveI : fintype (G × v) := prod.fintype G v,
  have : fintype (G  v : set M),
  { refine fintype.of_surjective f _,
    rintro j_val, g, m, gG, mv, rfl⟩,
    use g,
    { exact gG },
    { use m,
      exact mv },
    { exact subtype.mk_eq_mk.mpr rfl } },
  { exact finite.smul_of_finite fG fv }
end

view this post on Zulip Damiano Testa (Mar 06 2021 at 20:53):

It feels unnecessarily complicated, but I am happy to have it now!

view this post on Zulip Kevin Buzzard (Mar 06 2021 at 21:00):

The whole point is to avoid finset and fintype completely

view this post on Zulip Kevin Buzzard (Mar 06 2021 at 21:00):

You do everything with sets and then show that everything is finite.

view this post on Zulip Damiano Testa (Mar 06 2021 at 21:05):

I tried to use sets, but when I write G × v, Lean converts this to something that is not a set. Is there a way of getting the cartesian product without making it into a strange type?

view this post on Zulip Eric Wieser (Mar 06 2021 at 21:09):

set.finite.fintype fg is fg.fintype I think

view this post on Zulip Eric Wieser (Mar 06 2021 at 21:09):

And you should be able to get away without the third haveI

view this post on Zulip Eric Wieser (Mar 06 2021 at 21:13):

docs#set.prod?

view this post on Zulip Damiano Testa (Mar 06 2021 at 21:38):

Well, I give up for today.

I also realized that my "proof" above does not actually work!

Hopefully it will all seem simpler when I get back to this!

view this post on Zulip Kevin Buzzard (Mar 07 2021 at 00:10):

@Damiano Testa

import algebra.algebra.tower

lemma finite.smul_of_finite {S M : Type*} [semiring S] [add_comm_monoid M] [semimodule S M]
  {G : set S} {v : set M} (fG : G.finite) (fv : v.finite) :
  (G  v).finite :=
fG.image2 () fv

Sorry I didn't get to this earlier -- I was having family time. The set.finite API should be, IMNSHO, the go-to way for mathematicians to deal with finiteness. finset and fintype are these type-valued finiteness things which experts seem to be able to use and can't see what the fuss is all about when us regular people whinge about instance problems because they understand all the details of what's going on. The advantage of finset over finite is that it's computable, but computability is worth absolutely nothing to me, and I find Prop-valued finiteness much easier to use.

view this post on Zulip Damiano Testa (Mar 07 2021 at 06:04):

Kevin, thank you so much for the proof and also for the information about finset vs finite. I did not realize that one of them was easier to work with and was using finset simply because that was what I had seen in mathlib.

Even though I had problems working with finite, it did appear easier to navigate than finset.

I certainly tried library_search on the lemma above. Why did it fail? Is it because of the fact that one of the inputs is a function?

view this post on Zulip Kevin Buzzard (Mar 07 2021 at 08:04):

I don't know. I just looked at the definition of G bub v, saw it used set.image2, so knew that the answer was going to be set.finite.image2 . I agree that library_search could have found this.

view this post on Zulip Damiano Testa (Mar 07 2021 at 08:17):

I tried looking at the definition of the \smul, but what I clicked took me to has_scalar, which was probably not what you found.

view this post on Zulip Kevin Buzzard (Mar 07 2021 at 08:18):

But this is the pattern in general, eg in my sketch above I went via set.prod and the proof that a product of two finite sets is finite is set.finite.prod . The "weird type" you're talking about above is just the coercion to Type. This is what happens when you bundle subobjects. Because things like set X and subgroup G ( if G is a group) are types, this means that things like H : subgroup G are terms, which is not how we mathematicians usually think about them -- we would usually think of a subgroup as being a group itself. This is why we have the notation g \in H, to remind us that the type of g is still G and the relationship between g and H is something else. This is fine sometimes, but if you actually want to think about H as a type itself rather than a term (eg if you really want to define a function with source H and cannot or will not think about it as the restriction of a function defined on G, or you want to talk about a subgroup of H and cannot or will not think of it as a subgroup of G contained in H) then you need to have a way to promote H to a type. This is done via has_coe_to_sort and as I've implied it's often something I try to avoid because it looks a bit inelegant, but it's not hard to understand: the promotion of the subset {x | p x} is the subtype {x // p x} and a term of this type is just a pair consisting of x : G and a proof that x \in H so you can do cases on it and use pointy bracket notation etc.

view this post on Zulip Damiano Testa (Mar 07 2021 at 08:18):

I just assumed that it was set up in such a way that once you set up smul for types, then it automatically picks up what to do with subsets of those types.

view this post on Zulip Kevin Buzzard (Mar 07 2021 at 08:20):

Re definition: you need to use the infoview correctly. You looked at the definition of the notation in general. If you inspect the bub in G bub v you can see it's something like set.has_scalar (I think -- not at lean right now) and this is where you can see it's image2.

view this post on Zulip Damiano Testa (Mar 07 2021 at 08:24):

Thanks, Kevin! The stuff on coercions is very helpful! It is something that I am starting to understand, but I still struggle with. For instance, I would like to avoid these coercions, but sometimes I feel that Lean corners me into using them and I am rarely able to exit the resulting mess. However, it is not always clear to me what it is that I did wrong that took me to such an undesirable place!

view this post on Zulip Damiano Testa (Mar 07 2021 at 08:25):

I indeed Ctrl-clicked the bullet in the code side, and did not think of clicking on the infoview and then specializing to the correct bullet to go to the correct definition! Now I found it! Thanks again!

view this post on Zulip Kevin Buzzard (Mar 07 2021 at 08:27):

You treated a term as a type, that's what makes has_coe_to_sort kick in. We're taught that everything is a term and some terms are types but this is a bad way of thinking about things. If you think of everything as precisely one of a term, a type and a universe then you get a much better model of how type theory is used in mathematics in general.

view this post on Zulip Mario Carneiro (Mar 07 2021 at 08:28):

well, some terms are types: nat is a type and also a term of type Type

view this post on Zulip Mario Carneiro (Mar 07 2021 at 08:29):

of course when we talk about terms used as types we usually mean terms whose type is not Type or Prop but something like finset A, in which case you need a coercion

view this post on Zulip Mario Carneiro (Mar 07 2021 at 08:29):

</pedantic>

view this post on Zulip Kevin Buzzard (Mar 07 2021 at 08:33):

The fact that nat is a term is for me deemed harmful. I don't see any use of this and I would accept a model of type theory where there were two different colons, one of the form term : type and one of the form type :: universe.

view this post on Zulip Damiano Testa (Mar 07 2021 at 08:35):

Ok, while I knew this, I am glad that Kevin also finds it a little bit of a coincidence that nat is a term!

I view this as the type-theory analogue of the fact that you can wonder about whether ℕ is an element of π in set-theory, but you really shouldn't!

view this post on Zulip Kevin Buzzard (Mar 07 2021 at 08:36):

I remember as a beginner trying to draw a map of Lean's type theory and starting with Prop : Type which is in some sense the most harmful of all the "random" term : type relations. It took me a long time to realise that Prop and Type were the same kind of thing and that this relation between them was of no use. We have a system where we can ask if nat = Prop and for me this is embarrassing, it's a junk question. I have constantly emphasised this universe/type/term viewpoint in my teaching and I think it makes it clearer to mathematicians

view this post on Zulip Damiano Testa (Mar 07 2021 at 08:41):

I certainly find it closer to my intuition to separate Props from non-Props. In fact, I sometimes have troubles applying inductions (Edit: in Lean!) and I think that the issue is often related to the fact that there is a blur between whether you are doing it on Prop or Type (or something like that).

Yet, I find it interesting that this distinction is not so strong and you can talk about Props on a similar footing as "usual mathematical objects". I guess that this is something that is no news to logicians, but I find charming these concepts!

view this post on Zulip Eric Wieser (Mar 07 2021 at 08:51):

Prop : Type and nat : Type make sense in the context of list Prop and list nat, respectively a list of statements and a list of integers

view this post on Zulip Mario Carneiro (Mar 07 2021 at 09:00):

Kevin Buzzard said:

The fact that nat is a term is for me deemed harmful. I don't see any use of this and I would accept a model of type theory where there were two different colons, one of the form term : type and one of the form type :: universe.

This kind of type theory exists; it's actually quite common outside DTT circles. For example Haskell's type theory distinguishes between "terms", "types" and "kinds"; so for example 1 : int and int : * where * is the kind of all types (what we would call Type). This is useful when talking about "higher kinded types" like list : * -> *, where * -> * is another "kind". (Of course this is no biggie for a DTT user, but if you are used to dealing with just types then these "types of types" are a little mind blowing.)

view this post on Zulip Mario Carneiro (Mar 07 2021 at 09:02):

I guess the DTT crowd saw this and said "well you're duplicating all the work now with a typehood relation that looks just like the other one. What if you need kinds of kinds? So let's make an infinite hierarchy of kinds of kinds of kinds and call them universes"

view this post on Zulip Mario Carneiro (Mar 07 2021 at 09:05):

This solves the problem of having many kinds of typehood judgment, at the cost of universe hierarchy management. Lean uses a little nat-like algebra of levels, while Coq uses a partial order of globally coherent universe constraints, and I think they are both lotsa complicated when we only really care about somewhere between 0 and 1 universes

view this post on Zulip Kevin Buzzard (Mar 07 2021 at 09:31):

@Eric Wieser I would be surprised if there were any lists of Props occurring anywhere in mathlib other than in meta code. I can fully believe that this is an important concept in tactic-writing but this is an abstraction layer i never go into in my teaching.

view this post on Zulip Eric Wieser (Mar 07 2021 at 09:34):

Perhaps docs#tfae uses it?

view this post on Zulip Eric Wieser (Mar 07 2021 at 09:35):

Or whatever the full name is...

view this post on Zulip Eric Wieser (Mar 07 2021 at 09:36):

I think that's a secret def that doc-gen doesn't want to tell me about?

view this post on Zulip Damiano Testa (Mar 07 2021 at 09:37):

docs#list.tfae ?

view this post on Zulip Damiano Testa (Mar 07 2021 at 09:37):

Ironic how list was in the name! :smile:

view this post on Zulip Damiano Testa (Mar 07 2021 at 09:38):

I did not know about tfae.

view this post on Zulip Mario Carneiro (Mar 07 2021 at 09:44):

tfae is the only example I know

view this post on Zulip Mario Carneiro (Mar 07 2021 at 09:44):

In fact list Prop is useless in meta code because Prop has no computational content

view this post on Zulip Mario Carneiro (Mar 07 2021 at 09:44):

it may as well be list unit

view this post on Zulip Mario Carneiro (Mar 07 2021 at 09:46):

I think a much more important use of types as terms is in things like ring A where the application of A to ring is the same as the application of f to x in any function application f x

view this post on Zulip Mario Carneiro (Mar 07 2021 at 09:48):

It's possible to get by with this being two different kinds of application but it's at best a notational headache

view this post on Zulip Yakov Pechersky (Mar 07 2021 at 13:28):

In the current definition of simple graphs in mathlib, edges are given by V -> V -> Prop, so a list of statements whether an edge is in the graph would also be list Prop

view this post on Zulip Yakov Pechersky (Mar 07 2021 at 13:30):

Kevin Buzzard said:

The fact that nat is a term is for me deemed harmful. I don't see any use of this

How would you then phrase statements like "the naturals are countable", "the reals are uncountable"?

view this post on Zulip Eric Wieser (Mar 07 2021 at 13:30):

Surely it would be list (sym2 V)?

view this post on Zulip Yakov Pechersky (Mar 07 2021 at 13:31):

You're right, I mean a list of edge \in graph

view this post on Zulip Yakov Pechersky (Mar 07 2021 at 13:33):

I think one of the smarter things that is in Lean syntax is differentiating cartesian products from the type level to the term level: term : (⬝,⬝) vs type (⬝ × ⬝), unlike Haskell which uses (,) for both.

view this post on Zulip Mario Carneiro (Mar 07 2021 at 15:06):

Well, in haskell you don't need to since types and terms are different

view this post on Zulip Mario Carneiro (Mar 07 2021 at 15:07):

You wouldn't really be able to unify them in lean because they have different (incompatible) types

view this post on Zulip Mario Carneiro (Mar 07 2021 at 15:08):

I once played around with unifying lambda and pi, which is just about doable (you just treat lambda as pi when it is used as a type)


Last updated: May 19 2021 at 03:22 UTC