## Where communities thrive

• Join over 1.5M+ people
• Join over 100K+ communities
• Free without limits
##### Activity
• Dec 06 07:03

Removed unproven propositions Merge branch 'siddhartha-gadgil… Defined fundamental group up to… and 5 more (compare)

• Dec 06 07:03
• Nov 14 15:51

removed unused variables (in co… (compare)

• Nov 14 14:45

no nodejs in docker (compare)

• Nov 14 14:41

trying codespaces (compare)

• Nov 10 19:19
Appelcider synchronize #16
• Nov 10 18:52
Appelcider synchronize #16
• Nov 09 14:14

Definitions of Quiver and `Se… Define additional structures Define 2-complexes and 35 more (compare)

• Nov 09 14:14
• Nov 09 08:27
0art0 review_requested #20
• Nov 09 08:27
0art0 opened #20
• Nov 09 07:12

0art0 on lean-update

• Nov 09 07:12

0art0 on main

• Nov 09 07:12
0art0 closed #19
• Nov 09 06:59
• Nov 09 06:57
• Nov 09 06:18
0art0 commented #17
• Nov 09 06:16

0art0 on lean-update

• Nov 08 17:35
0art0 commented #17
• Nov 08 15:04
I see it. I don't think my earlier simp idea is a good way. The present approach seems better. We just need some implementation of free abelian groups.
As you commented earlier, a similar method works for any free object. One may want to use variants of this: for example, for a commutative ring, assuming full simplification using distributivity, we can make a single list of symbols for the product terms and use the correspoding free groups. Then a * b - b * a should cancel.
But we can do this step by step.
Anand
@0art0
I too was thinking of something similar for the case of rings. I am hoping that ring will not be too difficult after simplifying in Abelian groups.
Incidentally, as we will care for efficiency here, the fastest structure to use is Array, and one can define a vector as a subtype of an Array with given length.
It is a little harder to prove theorems about Arrays, but there is an extensionality result, i.e., Array determined by its indices, if I am not mistaken. So any needed theorem should be derivable.
I will experiment a little (probably tomorrow) with meta stuff starting with a term in an abelian group and trying to generate an array of symbols used and the tree corresponding to this relative to the symbols.
Anand
@0art0
That makes sense. I think the main bottleneck will be in the reduction of the expression in the free Abelian group; I have modelled the free group on n elements as Z ^ n (an iterated product), but I will try switching over to a different definition in terms of arrays after finishing the prototype that I am working on.
It makes sense to have one prototype first - no need for premature optimization. For the meta part arrays are convenient since they have methods to use with indices.
Anand
@0art0
I have made some more progress on the prototype, but some of the proofs are not complete yet since typeclass inference seems to be stuck at a few places.
My next steps are independent anway as I realized. Plus there are a couple of other things I have to do.
So there is no hurry and I am not blocked.
Anand
@0art0
I have finished setting up the basic machinery for constructing homomorphisms from Z^n to an additive group A, given a vector of elements of A of length n
I have also proved that the standard basis of Z^n maps to this vector of elements under the homomorphism (this is the lemma that I was stuck on; factoring out a few lemmas and using rewrites sorted it out).
I will next try out a concrete example and show that it holds in all Abelian groups by computing in Z^n.
Meanwhile I have made an additive tree structure. It seemed easiest to make the tree with elements in a type, and then make indices and an array. Will add methods in a few minutes to fold index trees.
This has been added too. Now the main step remaining is a theorem that shows the equality of the composition of two maps is the same as a third map.
• Assume we are given an array basis of positive size in the type α and a tree t.
• Assume that α has an additive commutative group structure (parallel for multiplicative).
• The function foldMap applied to t and the basisImages gives an element x of α.
• On the other hand, foldMap applied to t and the standard basis of the free group with generators the size of basisImages gives an element a of the free group.
• By freeness, there is a homomorphism taking the basis elements to basisElements. This maps a to an element y.
• The theorem is that x = y.
Since you are more familiar with the free group stuff, I am not trying to state or prove this. But I am happy to discuss whenever it is helpful.
Anand
@0art0
I am going through the code now. If I understand correctly, the array in the output of the indexTree function is mapping numbers occurring in the leaves of the IndexAddTree to the corresponding elements of \alpha.
Yes, that is correct (at least should be if there are no bugs).
Anand
@0art0
Thanks. I think I understand the code and what is left to be proved.
My current code is in terms of Vectors. However, I think I can try to create an "isomorphism" between the Array a and Vector a _ types, so that I can avoid reproving that the basis maps to the chosen elements of the additive group A.
With the more complicated setup that the generated tree maps to a given group element may not be reflexively true. But simpwith specific theorems should work.
By the way, if arrays are used via other slower structures one may not get efficiency.
Anand
@0art0
Thanks, I will keep that in mind. I was planning to only switch between structures for the proof that the basis elements map to the chosen group elements, and work entirely with arrays for the computation part.
That sounds good.
Anand
@0art0
The proof of soundness of the map is almost done. The remaining parts are either theorems about List.toArray or Array.get, which I will work on by looking at the definitions of these functions.
To reduce the complexity of the code, I am thinking of removing Vectors and sticking to only Lists and Arrays. Once I do this, the remaining obstacles in the proof due to indexed inductive type will disappear.
I will do this in a separate branch since I will be adding a new simp lemma about AddCommGroup.Homomorphism that may break existing code.
Anand
@0art0
That is nice to see.
Anand
@0art0
I am almost done with the proof of the soundness of compositions, but I am stuck because a rewrite that was working in the Vector formulation is now producing an error motive is not type correct.
I think it has something to do with the propositional equality that I introduced into the proofs. I will dig into it further.
Anand
@0art0
The expressions are the same even after using set_option pp.all true, which is strange.
Anand
@0art0
I found a Zulip thread which recommends using get? instead of get. I will try that.
The get method may be using a coercion which comes in the way of proofs.
Anand
@0art0
Yes, and I think a part of the problem may be Fin too (the proofs have to be specified at type level).
When working with quotients I have sometimes had to specify the motive using @fn (motive := ...). That may work here too.
Anand
@0art0
Okay, I will try that.
Anand
@0art0
I now strongly suspect that the issue is with Fin. I will also try working with a modified get' definition that uses propositional equality:
def Array.get' {α : Type _} (a : Array α) {n : ℕ} (h : a.size = n) (i : ℕ) (hi : i < n) : α :=
Array.get a ⟨i, Eq.substr h hi⟩
I was looking at your code briefly. I agree that it is the usual Fin tangle. But I had a question: is it necessary to use List at all? What stops us from using Array right through?
I see that there will be difficulties earlier. I will think through this a bit.
I am looking at the code again, and I do feel:
• unit_pow_list should first of all be camelcase as it is a definition, but also the name is cryptic. I take it this gives an element of the unit power sum from a list.
• more seriously, this is where you are using lists and this cascades; the function here should just take an Array and use results such as Array.size_pop.
I will think a little more about how to work with arrays here.
Related to this, to work with arrays one can define pow_sum to append a copy of T (though this goes against the usual right associativity). Alternatively work with vectors.
I am currently in the middle of a couple of other things, but should get to trying to modify your code later (maybe tomorrow).
One of the things is to try to work on using prompting with large language models to autoformalize. I am making notes (to double as slides) in a private Github repository which I am sharing with you. Do let me know any comments or further ideas you have.
Anand
@0art0
One reason I did not use Arrays throughout was because it is harder to prove theorems about them (such as mapcomp).
But it looks like this is causing issues in the proofs in Fin here.
unit_pow_list takes in a list of elements of the target Abelian group and gives a function from pow_sum Unit n (the direct sum of Unit with itself n times - the basis of \Z^n) to the Abelian group where each element of pow_sum Unit n maps to the corresponding entry in the list.
I will clean up the code a bit more soon and add documentation (it is currently mainly experimental).
Anand
@0art0
I am going through the notes now. I will think a bit more about some possible prompts and let you know soon.