## Stream: new members

### Topic: Expressing a sum with finitely many nonzero terms

#### Eric Wieser (Jul 01 2020 at 16:20):

I'm trying to state the following in lean:

every A  G may be expressed one and only one way as A = _r Ar where Ar  Gr and all but finitely many Ar vanish.

I've attempted to write that as

(A :   Type u) (G: Type u)
[module (A 0) G] :=
(to_fun : {r}, A r [A 0] G)
(from_fun : r, G [A 0] A r)
(to_inj:  r,  (v: A r), v = from_fun r (to_fun v)) -- to_fun is injective
(from_iso :  g : G, g = ( r in , to_fun (from_fun r g))) -- the domain of from_fun r covers all of G

but the is unhappy because is not a finset. I think the issue is my definition does not account for the " all but finitely many Ar vanish" part.

#### Eric Wieser (Jul 01 2020 at 16:50):

Solved!

(from_iso :  g : G,  (rs : finset ),
( r  rs, from_fun r g = 0)
(g =  r in rs, to_fun (from_fun r g))

#### Bryan Gin-ge Chen (Jul 01 2020 at 16:52):

We also have finsupps, which might be useful here.

#### Eric Wieser (Jul 01 2020 at 16:57):

It's not immediately clear to me how to apply that

#### Bryan Gin-ge Chen (Jul 01 2020 at 17:06):

Yes, it will definitely take some wrangling. Maybe looking at how it's used in linear_algebra.basis will help, particularly e.g. docs#is_basis.repr and other theorems around there.

#### Utensil Song (Jul 02 2020 at 05:49):

Defining an infinite-dimensional geometric algebra is that it is essential to the treatment of manifolds in Chapter 4 of Clifford Algebra to Geometric Calculus.

#### Utensil Song (Jul 02 2020 at 05:50):

Is there code to do this for infinitely many Ar? We'll eventually need it.

#### Utensil Song (Jul 02 2020 at 05:55):

As David Sheets is working on this in Agda.

#### Utensil Song (Jul 02 2020 at 05:56):

It's better if we can assume nothing of the finiteness of the dimension at the outset and have a finite version later.

#### Utensil Song (Jul 02 2020 at 05:57):

linear algebra in mathlib seems to be doing exactly this.

#### Johan Commelin (Jul 02 2020 at 05:57):

Utensil Song said:

Is there code to do this for infinitely many Ar? We'll eventually need it.

What is Ar?

#### Utensil Song (Jul 02 2020 at 05:58):

A r as in (A : ℕ → Type u)

#### Utensil Song (Jul 02 2020 at 06:02):

It doesn't matter what it is concretely here. The question is only about summing (multiplying) infinitely with the familiar big_operators in Lean.

#### Johan Commelin (Jul 02 2020 at 06:05):

Aha, as opposed to A : (fin n) → Type?

Yes

#### Johan Commelin (Jul 02 2020 at 06:06):

I think it's nontrivial to allow for both nat and fin n as indexing types. But it can be done.

#### Johan Commelin (Jul 02 2020 at 06:07):

@Mario Carneiro Would it be safe to take A : nat → Type as a field of a structure, and an axiom \for k, n < k → A k = empty?

#### Johan Commelin (Jul 02 2020 at 06:08):

Yup... guessed that...

#### Mario Carneiro (Jul 02 2020 at 06:08):

\for k, n < k, \not nonempty (A k) is better

#### Mario Carneiro (Jul 02 2020 at 06:08):

or A k -> false if you prefer

#### Johan Commelin (Jul 02 2020 at 06:09):

@Utensil Song And now you could do this for n : enat, and then you would have merged nat and fin n.

#### Mario Carneiro (Jul 02 2020 at 06:10):

if you use nat, then why is the sum finite?

#### Johan Commelin (Jul 02 2020 at 06:13):

I guess because you are looking at the direct sum of the A i

#### Mario Carneiro (Jul 02 2020 at 06:17):

One way to write from_iso using dfinsupp is

(from_iso :  g : G,  (f : Π r, A r),
( r, f r = from_fun r g)
(g = f.sum (λ _, to_fun))

#### Mario Carneiro (Jul 02 2020 at 06:20):

alternatively you can bake this into from_fun by reordering the arguments to

(from_fun : G [A 0] (Π r, A r))

#### Mario Carneiro (Jul 02 2020 at 06:22):

(A :   Type u) (G: Type u)
[module (A 0) G] :=
(to_fun : {r}, A r [A 0] G)
(from_fun : G [A 0] (Π r, A r))
(to_inj :  r,  (v: A r), v = from_fun (to_fun v) r)
(from_iso :  g : G, g = (from_fun g).sum (λ r, to_fun))

(untested)

#### Utensil Song (Jul 02 2020 at 06:34):

To be sure, Π₀ r allows optional fin r and it can also work like the ordinary Π r which assumes no finiteness?

#### Johan Commelin (Jul 02 2020 at 06:37):

I'm confused by what you mean/want.

#### Utensil Song (Jul 02 2020 at 06:46):

I was thinking about an approach that we first do everything about assuming no finiteness, then do things about fin n assuming the finiteness. But the enat and Π₀ gave me the impressions that I can merge two steps into one but I can't see how lemmas only apply to the finite version interact with the infinite version (could be more general (so every lemma in the infinite version apply to the finite version)or could have its own special lemmas).

But I won't know whether this impression is correct until I try some proofs with the defs with enat and Π₀. (I'm guessing I'm wrong)

#### Johan Commelin (Jul 02 2020 at 06:50):

I think you can merge the definitions.

#### Johan Commelin (Jul 02 2020 at 06:50):

Q: what is this number called, the maximal r such that A r is non-trivial?

#### Mario Carneiro (Jul 02 2020 at 07:01):

with this approach, you only ever use nat, and the Π₀ ensures that the A r are eventually trivial

#### Utensil Song (Jul 02 2020 at 07:02):

I don't get what's the triviality being talked about here.

A r = {0}

#### Utensil Song (Jul 02 2020 at 07:04):

I see. But it can also be non-trivial even for A \inf, right?

#### Mario Carneiro (Jul 02 2020 at 07:04):

Actually I think the version I wrote allows for this to not happen

#### Mario Carneiro (Jul 02 2020 at 07:05):

there is no A inf in the version I wrote, or the version you wrote at the beginning

#### Johan Commelin (Jul 02 2020 at 07:06):

@Utensil Song We are mixing A : nat → Type and n : enat.

#### Mario Carneiro (Jul 02 2020 at 07:06):

I think Johan thinks that these conditions imply that there are only finitely many nonzero A r sets, but the finiteness is different for each g : G so I think that's not necessarily the case

#### Mario Carneiro (Jul 02 2020 at 07:07):

I could be wrong though, this is an unusual definition that I don't know much about

#### Johan Commelin (Jul 02 2020 at 07:09):

No, there can be infinitely many nonzero A r, if I understand Utensil correctly

#### Utensil Song (Jul 02 2020 at 07:10):

Yes, there can be infinitely many nonzero A r

#### Johan Commelin (Jul 02 2020 at 07:10):

@Utensil Song Is there a name for the maximal degree (possibly inf) for which A r is nonzero?

#### Mario Carneiro (Jul 02 2020 at 07:13):

I think the original text description given by Eric at the start of this thread doesn't match the statement of to_inj

#### Mario Carneiro (Jul 02 2020 at 07:14):

I think the uniqueness should be something like

(to_fun : {r}, A r [A 0] G)
(from_fun : G [A 0] (Π r, A r))
(from_iso :  g : G,  f, f = from_fun g  g = f.sum (λ r, to_fun))

#### Mario Carneiro (Jul 02 2020 at 07:19):

That is also enough to prove that \all r (v : A r), from_fun (to_fun v) = single r v

#### Mario Carneiro (Jul 02 2020 at 07:19):

also the names of from_fun and to_fun seem to be swapped

#### Utensil Song (Jul 02 2020 at 07:30):

Johan Commelin said:

Utensil Song Is there a name for the maximal degree (possibly inf) for which A r is nonzero?

I don't see explicitly naming it in literature. But it's equal to the dimension of the vector space that Clifford Algebra is extending. If one begins with a real countably infinite-dimensional vector space and assumes sufficient structure on this space, a Clifford algebra will be generated, the same for the finite-dimensional case. The infinite-dimensional Clifford algebra contains all finite-dimensional Clifford algebras.

#### Johan Commelin (Jul 02 2020 at 07:40):

So in the infinite dimensional case you don't want indexing by nat by some ordinal or something?

#### Kevin Buzzard (Jul 02 2020 at 07:46):

Is enat enough? How about fin' n for n : enat?

#### Mario Carneiro (Jul 02 2020 at 07:50):

The dfinsupp definition doesn't require anything for the type of r except that it have a 0 so that A 0 makes sense

#### Mario Carneiro (Jul 02 2020 at 07:50):

in fact A 0 could just be some other ring here

#### Utensil Song (Jul 02 2020 at 08:06):

Johan Commelin said:

So in the infinite dimensional case you don't want indexing by nat by some ordinal or something?

In the relevant proofs, it seems it's always lazily and relatively indexed. Like assuming A p and A q then later there would be A p+qin the proof.

#### Utensil Song (Jul 02 2020 at 08:09):

I could not find fin'

#### Johan Commelin (Jul 02 2020 at 08:09):

It doesn't exist.

#### Johan Commelin (Jul 02 2020 at 08:09):

Kevin was proposing if it should be defined

#### Utensil Song (Jul 02 2020 at 08:22):

I've seen a few sth' or sth2 in mathlib. Shouldn't this be discouraged?

#### Kevin Buzzard (Jul 02 2020 at 08:27):

It could be enat.fin if you like

#### Eric Wieser (Jul 02 2020 at 08:58):

Mario Carneiro said:

I think the uniqueness should be something like

(to_fun : {r}, A r [A 0] G)
(from_fun : G [A 0] (Π r, A r))
(from_iso :  g : G,  f, f = from_fun g  g = f.sum (λ r, to_fun))

Thanks for this. Unfortunately, that example fails for me due to inability to synthesize a type class instance for Π (i : ℕ) (x : A i), decidable (x ≠ 0)

#### Mario Carneiro (Jul 02 2020 at 09:09):

open_locale classical

#### Eric Wieser (Jul 02 2020 at 09:11):

Now I'm left with the problem of synthesizing semimodule (A 0) (Π₀ (r : ℕ), A r) from∀ r, module (A 0) (A r) - which is presumably because I need something captureing both →ₗ and Π₀

#### Mario Carneiro (Jul 02 2020 at 09:12):

that should be in mathlib

#### Eric Wieser (Jul 02 2020 at 09:13):

"I think its there already" or "it should be there if it isn't"?

both

#### Eric Wieser (Jul 02 2020 at 09:13):

Maybe I need to update

#### Mario Carneiro (Jul 02 2020 at 09:13):

it is there, but it's not an instance. Try attribute [instance] dfinsupp.to_semimodule

#### Eric Wieser (Jul 02 2020 at 09:14):

Sure enough, that does the trick

#### Eric Wieser (Jul 02 2020 at 09:14):

Should that be an instance?

I think so

#### Mario Carneiro (Jul 02 2020 at 09:14):

it's probably leftover from a change to module before which it could not safely be an instance

#### Utensil Song (Jul 02 2020 at 09:39):

I'm confused about the effect of attribute [instance]

#### Eric Wieser (Jul 02 2020 at 09:40):

It marks the bundled field as elegible for type class lookup, I think

#### Mario Carneiro (Jul 02 2020 at 09:40):

@[instance] def is the same as instance

#### Utensil Song (Jul 02 2020 at 09:40):

What's its natural form

#### Kevin Buzzard (Jul 02 2020 at 09:40):

It's just a tag on definitions saying "hey type class inference system, look at me"

#### Mario Carneiro (Jul 02 2020 at 09:41):

and you can mark a def as an instance after the fact using attribute [instance] or more commonly local attribute [instance]

#### Utensil Song (Jul 02 2020 at 09:41):

instance (with a proof) v.s. @[instance] v.s. attribute [instance]

#### Mario Carneiro (Jul 02 2020 at 09:42):

[instance] is an attribute that you can stick on definitions just like @[simp] and others

#### Utensil Song (Jul 02 2020 at 09:42):

Can @[instance] be used in this case?

#### Kevin Buzzard (Jul 02 2020 at 09:42):

You use @[instance] at the moment you're making the def

#### Mario Carneiro (Jul 02 2020 at 09:42):

instance foo is the same as @[instance] def foo

#### Utensil Song (Jul 02 2020 at 09:42):

and only at the moment?

#### Mario Carneiro (Jul 02 2020 at 09:42):

Mario Carneiro said:

and you can mark a def as an instance after the fact using attribute [instance] or more commonly local attribute [instance]

#### Utensil Song (Jul 02 2020 at 09:43):

I mean: is it that@ can only be used at the moment of definition and attribute can only be used after the definition?

#### Mario Carneiro (Jul 02 2020 at 09:46):

class foo (α : Type) := (a : α)

#check (foo.a : nat) -- fails

-- Option 1 --
instance : foo nat := 37
#check (foo.a : nat) -- works

-- Option 2 --
@[instance] def nat.foo : foo nat := 37
#check (foo.a : nat) -- works

-- Option 3 --
def nat.foo : foo nat := 37
#check (foo.a : nat) -- fails
section
local attribute [instance] nat.foo
#check (foo.a : nat) -- works
end
#check (foo.a : nat) -- fails
attribute [instance] nat.foo
#check (foo.a : nat) -- works

#### Mario Carneiro (Jul 02 2020 at 09:47):

You can also write attribute [instance] def nat.foo : foo nat := ⟨37⟩ instead but this is usually not used

#### Mario Carneiro (Jul 02 2020 at 09:48):

The @[attr] form only works immediately before a keyword like def or theorem

#### Mario Carneiro (Jul 02 2020 at 09:49):

The attribute [attr] nat.foo form works as a standalone command but requires the name of the definition(s) being marked

#### Eric Wieser (Jul 02 2020 at 09:52):

Mario Carneiro said:

That is also enough to prove that \all r (v : A r), from_fun (to_fun v) = single r v

Any tips for that proof?

#### Mario Carneiro (Jul 02 2020 at 09:54):

Applying from_iso, you have to prove to_fun v = (single r v).sum (λ r, to_fun), which follows from sum_single_index

#### Eric Wieser (Jul 02 2020 at 09:55):

Thanks, will see what I can come up with, then ask how to simplify my proof :)

#### Eric Wieser (Jul 02 2020 at 10:01):

lemma from_zulip (r : ) (v : A r) : select (to_fun v : G) = dfinsupp.single r v := begin
symmetry,
rw from_iso (to_fun v : G) (dfinsupp.single r v),
symmetry,
apply dfinsupp.sum_single_index,
exact linear_map.map_zero _,
end

#### Mario Carneiro (Jul 02 2020 at 10:05):

you can write that in term mode if you want, probably something like ((from_iso _ _).2 (dfinsupp.sum_single_index _ (linear_map.map_zero _)).symm).symm although I can't say for sure without an #mwe

#### Eric Wieser (Jul 02 2020 at 10:06):

Would it be sensible to define my from_iso with the both equalities reversed to avoid needing the symm?

#### Mario Carneiro (Jul 02 2020 at 10:07):

I would wait to see 5 or 6 uses of the theorem before taking a guess on which direction is more common

#### Eric Wieser (Jul 02 2020 at 10:21):

One final question before I write all this up - is this a suitable set of precedences for notation?

notation ⟨g⟩_:0 r:100 := graded_algebra_iso.from_fun g r

The problem I'm having is that for v : A r, I can't seem to write ⟨v : G⟩_r but have to add parentheses for the syntax to be understood as ⟨(v : G)⟩_r

#### Utensil Song (Jul 02 2020 at 10:30):

I guess in the spirit of the tail recursion, it's usually better to add the "new" thing to the right and proofs usually start cracking it from the right. But I don't know how to apply this principle to this case...

#### Eric Wieser (Jul 02 2020 at 13:58):

Wrapped this up at https://github.com/pygae/lean-ga/pull/5 for anyone interested.

#### Utensil Song (Jul 03 2020 at 12:29):

A related question: how to express "generated by" in Lean?

## Main definitions

Let R be a ring and let M and P be R-modules. Let N be an R-submodule of M.

• fg N : Prop is the assertion that N is finitely generated as an R-module.
• is_noetherian R M is the proposition that M is a Noetherian R-module. It is a class,
implemented as the predicate that all R-submodules of M are finitely generated.

#### Jalex Stark (Jul 03 2020 at 12:40):

Did you look at the implementation of fg or is_noetherian?

#### Kevin Buzzard (Jul 03 2020 at 12:44):

The subobject generated by X is typically called span X, and "X generates A" is typically just written span X = \top

#### Utensil Song (Jul 03 2020 at 12:50):

I don't understand it when the implementation reaches the part about complete lattices.

#### Utensil Song (Jul 03 2020 at 12:54):

Complete lattices by itself look well defined, but I don't understand the necessity of using it to express/implement a pretty elementary concept span.

image.png

#### Eric Wieser (Jul 03 2020 at 12:55):

Where is that image from?

Mathlib paper

#### Kevin Buzzard (Jul 03 2020 at 12:56):

There is a "bottom-up" and a "top-down" way to define span

#### Kevin Buzzard (Jul 03 2020 at 12:57):

The "top-down" way is to define the foo-span of the set X as the intersection of all the foos which contain X

#### Kevin Buzzard (Jul 03 2020 at 12:58):

The bottom-up way is to make some new set recursively, which contains X and is closed under all the foo axioms

#### Utensil Song (Jul 03 2020 at 13:08):

Ah, I see how this applies to linear algebra.

#### Utensil Song (Jul 03 2020 at 13:08):

But the question at our hand seems to be:

If we think of Grassmann Algebra as a vector space generated by its subspaces, this seems to be sufficient. But the subspaces, in turn, are generated by vectors. So how to express the concept of Grassmann Algebra is "generated" by vectors via wedge product?

#### Utensil Song (Jul 03 2020 at 13:09):

(using Grassmann Algebra for a simpler analogy of Clifford Algebra)

#### Reid Barton (Jul 03 2020 at 13:13):

You can apply the same method to subalgebras.

#### Utensil Song (Jul 03 2020 at 13:13):

So in this case, I was kind of thinking about things like generators in group theory.

#### Utensil Song (Jul 03 2020 at 13:13):

Reid Barton said:

You can apply the same method to subalgebras.

So do I have to use a two-level span here?

#### Utensil Song (Jul 03 2020 at 13:15):

Also, I don't get the remark of the "tension" here.

#### Patrick Massot (Jul 03 2020 at 13:19):

I need more help to help you here. Which part you don't get?

#### Patrick Massot (Jul 03 2020 at 13:20):

Is it the non-zero characteristic thing?

#### Utensil Song (Jul 03 2020 at 13:21):

"the fact (seen as the subspace of multilinear maps) is clearly wrong in positive characteristic where (seen as a quotient of the tensor algebra)"

#### Utensil Song (Jul 03 2020 at 13:22):

I understand what's in the parentheses and not the sentence connecting them.

#### Patrick Massot (Jul 03 2020 at 13:23):

Where do you see this quote?

#### Patrick Massot (Jul 03 2020 at 13:24):

I see

There is a tension between having $\Lambda^k V^*$ seen as the subspace of multilinear maps from $V^k$ to the base field which happen to be antisymmetric, which is nice and concrete, and the fact this is clearly wrong in positive characteristic where there is no other choice than seeing it as a quotient of the tensor algebra.

#### Patrick Massot (Jul 03 2020 at 13:26):

Let me try again. In any case, there is a very concrete elementary thing which is the subspace of multilinear forms made of antisymmetric forms. And there is a slightly more abstract thing which is a quotient of the space of multilinear forms by some subspace. In characteristic zero, there is an isomorphism between those things, so there is not much loss in forgetting about the abstract one. In positive characteristic you can't.

I see

#### Utensil Song (Jul 03 2020 at 13:31):

So the approach might be using the latter as a general definition, and prove the former is isomorphic to the latter in characteristic zero?

#### Patrick Massot (Jul 03 2020 at 13:35):

Probably yes, but this kind of question is hard to answer with total confidence without trying. Note that there is an additional complication: in the positive characteristic world, characteristic 2 is a world of its own. In characteristic 2, you'll also have to be careful that alternating and antisymmetric are not the same thing.

#### Utensil Song (Jul 03 2020 at 13:51):

image.png

from Clifford Algebras and Spinor Structures.

It elaborates on the issue here and there seems possible to have some reasonable solutions to this. But, yeah, hard to answer without trying.

#### Utensil Song (Jul 03 2020 at 14:02):

Back to "generated by". @Eric Wieser used a pretty elementary way to "generate" subobjects (i.e. r-blade) by orthogonal vectors, but I don't know how can that be connected to the abstract way(complete lattices) of expressing span.

def is_rblade (r : ) (b : G) : Prop :=
-- a product of orthogonal vectors an a scalar
( (k: G₀) (v : pairwise_ortho_vector r),
b = fₛ k * list.prod (v.val.val.map f))

#### Eric Wieser (Jul 03 2020 at 14:05):

I had a variant of the definition on https://github.com/pygae/lean-ga/blob/master/src/geometric_algebra/nursery/chisolm.lean#L228 that used lattices via def Mᵣ (r : ℕ) := ⨆ s <= r, Gᵣ s, if that helps

#### Utensil Song (Jul 03 2020 at 14:08):

I think I accidentally merged your two PRs with parallel designs in mind into one file which happens to have no conflict

#### Eric Wieser (Jul 03 2020 at 14:13):

You 100% did I thought so too, but can't see any evidence of the second one

I see

#### Utensil Song (Jul 03 2020 at 14:20):

The branch in pygae/lean-ga#4 is based on pygae/lean-ga#3 (which deleted the whole pygae/lean-ga#3 in https://github.com/pygae/lean-ga/commit/9235ca262b12b4e7f8861a7dfcfd0cdc401069de ) .

#### Utensil Song (Jul 03 2020 at 14:21):

The meta-question here might be how to connect the more elementary presentation of a subject with the mathematical rigorous and abstract treatment. Both can be done in Lean, but it's difficult to establish a link. Geometric Algebra, as reformulated by Hestenes and many from Clifford Algebra, is meant to be more elementary and application-oriented. This more elementary formalism (which is meant to do "application" level reasoning) is unlikely to be PRed into mathlib, but mathlib would certainly have a general version of Clifford Algebra, which would be of little interest of the intended audience here. But it would be nice to show the elementary version is isomorphic to the general version under certain conditions.

#### Utensil Song (Jul 10 2020 at 06:26):

Free module seems to be related, see also free.lean discussed here, seems that it hasn't made into mathlib yet.

Last updated: May 10 2021 at 17:39 UTC