Expressing a sum with finitely many nonzero terms

Stream: new members

[Eric Wieser]

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

class graded_algebra_iso
  (A : ℕ → Type u) (G: Type u)
  [graded_algebra_components A]
  [add_comm_group G]
  [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]

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]

We also have finsupps, which might be useful here.

[Eric Wieser]

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

[Bryan Gin-ge Chen]

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]

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]

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

[Utensil Song]

As David Sheets is working on this in Agda.

[Utensil Song]

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]

linear algebra in mathlib seems to be doing exactly this.

[Johan Commelin]

Utensil Song said:

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

What is Ar?

[Utensil Song]

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

[Utensil Song]

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]

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

[Utensil Song]

Yes

[Johan Commelin]

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

[Johan Commelin]

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

[Mario Carneiro]

type equality bad

[Johan Commelin]

Yup... guessed that...

[Mario Carneiro]

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

[Mario Carneiro]

or A k -> false if you prefer

[Johan Commelin]

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

[Mario Carneiro]

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

[Johan Commelin]

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

[Mario Carneiro]

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]

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

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

[Mario Carneiro]

class graded_algebra_iso
  (A : ℕ → Type u) (G: Type u)
  [graded_algebra_components A]
  [add_comm_group G]
  [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]

It's much more readable now!

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

[Johan Commelin]

I'm confused by what you mean/want.

[Utensil Song]

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]

I think you can merge the definitions.

[Johan Commelin]

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

[Mario Carneiro]

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

[Utensil Song]

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

[Mario Carneiro]

A r = {0}

[Utensil Song]

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

[Mario Carneiro]

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

[Mario Carneiro]

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

[Johan Commelin]

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

[Mario Carneiro]

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]

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

[Johan Commelin]

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

[Utensil Song]

Yes, there can be infinitely many nonzero A r

[Johan Commelin]

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

[Mario Carneiro]

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]

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]

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

[Mario Carneiro]

also the names of from_fun and to_fun seem to be swapped

[Utensil Song]

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]

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

[Kevin Buzzard]

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

[Mario Carneiro]

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]

in fact A 0 could just be some other ring here

[Utensil Song]

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]

I could not find fin'

[Johan Commelin]

It doesn't exist.

[Johan Commelin]

Kevin was proposing if it should be defined

[Utensil Song]

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

[Kevin Buzzard]

It could be enat.fin if you like

[Eric Wieser]

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]

open_locale classical

[Eric Wieser]

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]

that should be in mathlib

[Eric Wieser]

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

[Mario Carneiro]

both

[Eric Wieser]

Maybe I need to update

[Mario Carneiro]

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

[Eric Wieser]

Sure enough, that does the trick

[Eric Wieser]

Should that be an instance?

[Mario Carneiro]

I think so

[Mario Carneiro]

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

[Utensil Song]

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

[Eric Wieser]

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

[Mario Carneiro]

@[instance] def is the same as instance

[Utensil Song]

What's its natural form

[Kevin Buzzard]

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

[Mario Carneiro]

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

[Utensil Song]

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

[Mario Carneiro]

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

[Utensil Song]

Can @[instance] be used in this case?

[Kevin Buzzard]

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

[Mario Carneiro]

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

[Utensil Song]

and only at the moment?

[Mario Carneiro]

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]

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]

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]

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

[Mario Carneiro]

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

[Mario Carneiro]

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

[Eric Wieser]

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]

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]

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

[Eric Wieser]

  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]

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]

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

[Mario Carneiro]

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

[Eric Wieser]

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]

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]

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

[Utensil Song]

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

[Utensil Song]

What I can find is in https://github.com/leanprover-community/mathlib/blob/master/src/ring_theory/noetherian.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]

Did you look at the implementation of fg or is_noetherian?

[Kevin Buzzard]

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

[Utensil Song]

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

[Utensil Song]

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.

[Utensil Song]

image.png

[Eric Wieser]

Where is that image from?

[Utensil Song]

Mathlib paper

[Kevin Buzzard]

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

[Kevin Buzzard]

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]

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

[Utensil Song]

Ah, I see how this applies to linear algebra.

[Utensil Song]

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]

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

[Reid Barton]

You can apply the same method to subalgebras.

[Utensil Song]

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

[Utensil Song]

Reid Barton said:

You can apply the same method to subalgebras.

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

[Utensil Song]

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

[Patrick Massot]

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

[Patrick Massot]

Is it the non-zero characteristic thing?

[Utensil Song]

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

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

[Patrick Massot]

Where do you see this quote?

[Patrick Massot]

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]

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.

[Utensil Song]

I see

[Utensil Song]

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]

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]

image.png

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]

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

as in https://github.com/pygae/lean-ga/blob/master/src/geometric_algebra/nursery/chisolm.lean#L108

[Eric Wieser]

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]

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

[Eric Wieser]

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

[Utensil Song]

I see

[Utensil Song]

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]

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]

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