Zulip Chat Archive

Stream: new members

Topic: Expressing a sum with finitely many nonzero terms


view this post on Zulip 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

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.

view this post on Zulip 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))

view this post on Zulip Bryan Gin-ge Chen (Jul 01 2020 at 16:52):

We also have finsupps, which might be useful here.

view this post on Zulip Eric Wieser (Jul 01 2020 at 16:57):

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

view this post on Zulip 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.

view this post on Zulip 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.

view this post on Zulip Utensil Song (Jul 02 2020 at 05:50):

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

view this post on Zulip Utensil Song (Jul 02 2020 at 05:55):

As David Sheets is working on this in Agda.

view this post on Zulip 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.

view this post on Zulip Utensil Song (Jul 02 2020 at 05:57):

linear algebra in mathlib seems to be doing exactly this.

view this post on Zulip 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?

view this post on Zulip Utensil Song (Jul 02 2020 at 05:58):

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

view this post on Zulip 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.

view this post on Zulip Johan Commelin (Jul 02 2020 at 06:05):

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

view this post on Zulip Utensil Song (Jul 02 2020 at 06:05):

Yes

view this post on Zulip 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.

view this post on Zulip 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?

view this post on Zulip Mario Carneiro (Jul 02 2020 at 06:07):

type equality bad

view this post on Zulip Johan Commelin (Jul 02 2020 at 06:08):

Yup... guessed that...

view this post on Zulip Mario Carneiro (Jul 02 2020 at 06:08):

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

view this post on Zulip Mario Carneiro (Jul 02 2020 at 06:08):

or A k -> false if you prefer

view this post on Zulip 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.

view this post on Zulip Mario Carneiro (Jul 02 2020 at 06:10):

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

view this post on Zulip Johan Commelin (Jul 02 2020 at 06:13):

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

view this post on Zulip 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))

view this post on Zulip 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))

view this post on Zulip Mario Carneiro (Jul 02 2020 at 06:22):

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)

view this post on Zulip Utensil Song (Jul 02 2020 at 06:34):

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?

view this post on Zulip Johan Commelin (Jul 02 2020 at 06:37):

I'm confused by what you mean/want.

view this post on Zulip 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)

view this post on Zulip Johan Commelin (Jul 02 2020 at 06:50):

I think you can merge the definitions.

view this post on Zulip Johan Commelin (Jul 02 2020 at 06:50):

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

view this post on Zulip 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

view this post on Zulip Utensil Song (Jul 02 2020 at 07:02):

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

view this post on Zulip Mario Carneiro (Jul 02 2020 at 07:02):

A r = {0}

view this post on Zulip Utensil Song (Jul 02 2020 at 07:04):

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

view this post on Zulip Mario Carneiro (Jul 02 2020 at 07:04):

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

view this post on Zulip 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

view this post on Zulip Johan Commelin (Jul 02 2020 at 07:06):

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

view this post on Zulip 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

view this post on Zulip 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

view this post on Zulip Johan Commelin (Jul 02 2020 at 07:09):

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

view this post on Zulip Utensil Song (Jul 02 2020 at 07:10):

Yes, there can be infinitely many nonzero A r

view this post on Zulip 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?

view this post on Zulip 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

view this post on Zulip 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))

view this post on Zulip 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

view this post on Zulip Mario Carneiro (Jul 02 2020 at 07:19):

also the names of from_fun and to_fun seem to be swapped

view this post on Zulip 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.

view this post on Zulip 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?

view this post on Zulip Kevin Buzzard (Jul 02 2020 at 07:46):

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

view this post on Zulip 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

view this post on Zulip Mario Carneiro (Jul 02 2020 at 07:50):

in fact A 0 could just be some other ring here

view this post on Zulip 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.

view this post on Zulip Utensil Song (Jul 02 2020 at 08:09):

I could not find fin'

view this post on Zulip Johan Commelin (Jul 02 2020 at 08:09):

It doesn't exist.

view this post on Zulip Johan Commelin (Jul 02 2020 at 08:09):

Kevin was proposing if it should be defined

view this post on Zulip Utensil Song (Jul 02 2020 at 08:22):

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

view this post on Zulip Kevin Buzzard (Jul 02 2020 at 08:27):

It could be enat.fin if you like

view this post on Zulip 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)

view this post on Zulip Mario Carneiro (Jul 02 2020 at 09:09):

open_locale classical

view this post on Zulip 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 Π₀

view this post on Zulip Mario Carneiro (Jul 02 2020 at 09:12):

that should be in mathlib

view this post on Zulip Eric Wieser (Jul 02 2020 at 09:13):

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

view this post on Zulip Mario Carneiro (Jul 02 2020 at 09:13):

both

view this post on Zulip Eric Wieser (Jul 02 2020 at 09:13):

Maybe I need to update

view this post on Zulip Mario Carneiro (Jul 02 2020 at 09:13):

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

view this post on Zulip Eric Wieser (Jul 02 2020 at 09:14):

Sure enough, that does the trick

view this post on Zulip Eric Wieser (Jul 02 2020 at 09:14):

Should that be an instance?

view this post on Zulip Mario Carneiro (Jul 02 2020 at 09:14):

I think so

view this post on Zulip 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

view this post on Zulip Utensil Song (Jul 02 2020 at 09:39):

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

view this post on Zulip Eric Wieser (Jul 02 2020 at 09:40):

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

view this post on Zulip Mario Carneiro (Jul 02 2020 at 09:40):

@[instance] def is the same as instance

view this post on Zulip Utensil Song (Jul 02 2020 at 09:40):

What's its natural form

view this post on Zulip Kevin Buzzard (Jul 02 2020 at 09:40):

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

view this post on Zulip 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]

view this post on Zulip Utensil Song (Jul 02 2020 at 09:41):

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

view this post on Zulip Mario Carneiro (Jul 02 2020 at 09:42):

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

view this post on Zulip Utensil Song (Jul 02 2020 at 09:42):

Can @[instance] be used in this case?

view this post on Zulip Kevin Buzzard (Jul 02 2020 at 09:42):

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

view this post on Zulip Mario Carneiro (Jul 02 2020 at 09:42):

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

view this post on Zulip Utensil Song (Jul 02 2020 at 09:42):

and only at the moment?

view this post on Zulip 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]

view this post on Zulip 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?

view this post on Zulip 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

view this post on Zulip 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

view this post on Zulip Mario Carneiro (Jul 02 2020 at 09:48):

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

view this post on Zulip 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

view this post on Zulip 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?

view this post on Zulip 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

view this post on Zulip Eric Wieser (Jul 02 2020 at 09:55):

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

view this post on Zulip 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

view this post on Zulip 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

view this post on Zulip 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?

view this post on Zulip 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

view this post on Zulip 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

view this post on Zulip 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...

view this post on Zulip Eric Wieser (Jul 02 2020 at 13:58):

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

view this post on Zulip Utensil Song (Jul 03 2020 at 12:29):

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

view this post on Zulip Utensil Song (Jul 03 2020 at 12:33):

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.

view this post on Zulip Jalex Stark (Jul 03 2020 at 12:40):

Did you look at the implementation of fg or is_noetherian?

view this post on Zulip 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

view this post on Zulip Utensil Song (Jul 03 2020 at 12:50):

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

view this post on Zulip 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.

view this post on Zulip Utensil Song (Jul 03 2020 at 12:55):

image.png

view this post on Zulip Eric Wieser (Jul 03 2020 at 12:55):

Where is that image from?

view this post on Zulip Utensil Song (Jul 03 2020 at 12:56):

Mathlib paper

view this post on Zulip Kevin Buzzard (Jul 03 2020 at 12:56):

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

view this post on Zulip 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

view this post on Zulip 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

view this post on Zulip Utensil Song (Jul 03 2020 at 13:08):

Ah, I see how this applies to linear algebra.

view this post on Zulip 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?

view this post on Zulip Utensil Song (Jul 03 2020 at 13:09):

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

view this post on Zulip Reid Barton (Jul 03 2020 at 13:13):

You can apply the same method to subalgebras.

view this post on Zulip Utensil Song (Jul 03 2020 at 13:13):

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

view this post on Zulip 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?

view this post on Zulip Utensil Song (Jul 03 2020 at 13:15):

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

view this post on Zulip Patrick Massot (Jul 03 2020 at 13:19):

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

view this post on Zulip Patrick Massot (Jul 03 2020 at 13:20):

Is it the non-zero characteristic thing?

view this post on Zulip 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)"

view this post on Zulip Utensil Song (Jul 03 2020 at 13:22):

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

view this post on Zulip Patrick Massot (Jul 03 2020 at 13:23):

Where do you see this quote?

view this post on Zulip Patrick Massot (Jul 03 2020 at 13:24):

I see

There is a tension between having ΛkV\Lambda^k V^* seen as the subspace of multilinear maps from VkV^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.

view this post on Zulip 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.

view this post on Zulip Utensil Song (Jul 03 2020 at 13:29):

I see

view this post on Zulip 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?

view this post on Zulip 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.

view this post on Zulip Utensil Song (Jul 03 2020 at 13:51):

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.

view this post on Zulip 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))

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

view this post on Zulip 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

view this post on Zulip 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

view this post on Zulip 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

view this post on Zulip Utensil Song (Jul 03 2020 at 14:19):

I see

view this post on Zulip 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 ) .

view this post on Zulip 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.

view this post on Zulip 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