generators smul generators generate

Stream: Is there code for X?

[Damiano Testa]

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!

[Eric Wieser]

(deleted)

[Damiano Testa]

Fixed!

[Kenny Lau]

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

[Kenny Lau]

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

[Damiano Testa]

Great, thanks Kenny!

[Eric Wieser]

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?

[Damiano Testa]

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

[Damiano Testa]

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

[Eric Wieser]

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

[Damiano Testa]

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?

[Damiano Testa]

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

[Kevin Buzzard]

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

[Damiano Testa]

Ok, I will try!

[Damiano Testa]

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

[Kevin Buzzard]

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.

[Damiano Testa]

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.

[Damiano Testa]

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

[Eric Wieser]

Does letI work better than haveI?

[Damiano Testa]

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

[Eric Wieser]

docs#prod.fintype?

[Damiano Testa]

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

[Damiano Testa]

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

[Eric Wieser]

Well add two new haveIs for those instances then!

[Damiano Testa]

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

[Damiano Testa]

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

[Damiano Testa]

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

[Damiano Testa]

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

[Kevin Buzzard]

The whole point is to avoid finset and fintype completely

[Kevin Buzzard]

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

[Damiano Testa]

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?

[Eric Wieser]

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

[Eric Wieser]

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

[Eric Wieser]

docs#set.prod?

[Damiano Testa]

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!

[Kevin Buzzard]

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

[Damiano Testa]

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?

[Kevin Buzzard]

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.

[Damiano Testa]

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.

[Kevin Buzzard]

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.

[Damiano Testa]

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.

[Kevin Buzzard]

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.

[Damiano Testa]

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!

[Damiano Testa]

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!

[Kevin Buzzard]

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.

[Mario Carneiro]

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

[Mario Carneiro]

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

[Mario Carneiro]

</pedantic>

[Kevin Buzzard]

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.

[Damiano Testa]

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!

[Kevin Buzzard]

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

[Damiano Testa]

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!

[Eric Wieser]

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

[Mario Carneiro]

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

[Mario Carneiro]

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"

[Mario Carneiro]

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

[Kevin Buzzard]

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

[Eric Wieser]

Perhaps docs#tfae uses it?

[Eric Wieser]

Or whatever the full name is...

[Eric Wieser]

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

[Damiano Testa]

docs#list.tfae ?

[Damiano Testa]

Ironic how list was in the name! :smile:

[Damiano Testa]

I did not know about tfae.

[Mario Carneiro]

tfae is the only example I know

[Mario Carneiro]

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

[Mario Carneiro]

it may as well be list unit

[Mario Carneiro]

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

[Mario Carneiro]

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

[Yakov Pechersky]

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

[Yakov Pechersky]

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"?

[Eric Wieser]

Surely it would be list (sym2 V)?

[Yakov Pechersky]

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

[Yakov Pechersky]

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.

[Mario Carneiro]

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

[Mario Carneiro]

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

[Mario Carneiro]

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)