## Stream: Is there code for X?

### Topic: generators smul generators generate

#### 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!

(deleted)

Fixed!

#### 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 :=


#### Kenny Lau (Mar 06 2021 at 15:59):

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

#### Damiano Testa (Mar 06 2021 at 15:59):

Great, thanks Kenny!

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

#### Damiano Testa (Mar 06 2021 at 16:00):

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

#### 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!

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

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

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

#### Kevin Buzzard (Mar 06 2021 at 18:59):

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

Ok, I will try!

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


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

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

#### 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_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 (Mar 06 2021 at 20:45):

Does letI work better than haveI?

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


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

#### 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_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 (Mar 06 2021 at 20:52):

Well add two new haveIs for those instances then!

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


#### Damiano Testa (Mar 06 2021 at 20:53):

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

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


#### Damiano Testa (Mar 06 2021 at 20:53):

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

#### Kevin Buzzard (Mar 06 2021 at 21:00):

The whole point is to avoid finset and fintype completely

#### Kevin Buzzard (Mar 06 2021 at 21:00):

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

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

#### Eric Wieser (Mar 06 2021 at 21:09):

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

#### Eric Wieser (Mar 06 2021 at 21:09):

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

#### 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!

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

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

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

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

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

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

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

#### 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!

#### 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!

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

#### Mario Carneiro (Mar 07 2021 at 08:28):

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

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

</pedantic>

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

#### 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!

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

#### 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!

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

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

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

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

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

#### Eric Wieser (Mar 07 2021 at 09:34):

Perhaps docs#tfae uses it?

#### Eric Wieser (Mar 07 2021 at 09:35):

Or whatever the full name is...

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

#### Damiano Testa (Mar 07 2021 at 09:37):

Ironic how list was in the name! :smile:

#### Damiano Testa (Mar 07 2021 at 09:38):

I did not know about tfae.

#### Mario Carneiro (Mar 07 2021 at 09:44):

tfae is the only example I know

#### Mario Carneiro (Mar 07 2021 at 09:44):

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

#### Mario Carneiro (Mar 07 2021 at 09:44):

it may as well be list unit

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

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

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

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

#### Eric Wieser (Mar 07 2021 at 13:30):

Surely it would be list (sym2 V)?

#### Yakov Pechersky (Mar 07 2021 at 13:31):

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

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

#### Mario Carneiro (Mar 07 2021 at 15:06):

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

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

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