## Where communities thrive

• Join over 1.5M+ people
• Join over 100K+ communities
• Free without limits
##### Activity
• Jan 29 04:41

• Jan 25 15:28

0art0 on main

• Jan 25 15:11

0art0 on main

Turning instances with K x Q … (compare)

• Jan 23 16:50

0art0 on main

Type declaration for the invers… (compare)

• Jan 23 16:40

0art0 on main

Minor changes in TorsionFree (compare)

• Jan 23 10:08

0art0 on main

Golf proof of exactness using … (compare)

• Jan 17 16:21

0art0 on main

Indentation fixes (compare)

• Jan 17 16:18

0art0 on main

Metabelian group is in an exact… (compare)

• Jan 17 15:00

0art0 on main

Better docs for files (compare)

• Jan 17 10:44

image in docs removed (not work… (compare)

• Jan 17 10:39

png image (compare)

• Jan 17 10:28

graph including in README but n… (compare)

• Jan 17 08:37

corrected imports (compare)

• Jan 17 08:19

corrected imports (compare)

• Jan 17 07:30

0art0 on main

Update to current folder name (compare)

• Jan 17 07:24

0art0 on main

Commenting out UniversalCover… (Failed) attempt at decideFora… Revert "(Failed) attempt at de… and 7 more (compare)

• Jan 17 06:09

ConjInvLength to top level complexes, experiments at top l… docs in Polylean file (compare)

• Jan 17 06:09

docs in Polylean file (compare)

• Jan 17 05:50

complexes, experiments at top l… (compare)

• Jan 17 05:39

ConjInvLength to top level (compare)

Within the Free Abelian group I to feel that the approach as above is fine. I am thinking of the bridge viewing an element as the image some homomorphism from this.
Anand
@0art0
Yes, I too think we might need trees for describing the element of the group
I am trying to work out a sketch of the lifting process. We should have maps between trees, which provably commute with folds. This will let us transport equality between elements in free abelian groups to equality in arbitrary abelian groups.
One step - that fold and treeM are inverses will have to have a proof by reflexivity at meta level for each instance though.
Anand
@0art0
Okay. I am now trying to implement this idea for a concrete example to see how it can be generalised. I also have an idea based on trees, which I will try to develop further after this.
Sounds good. As I said, I don't have a setup for programming today. I will try things (complementary to what you are doing) over the weekend or early next week.
Anand
@0art0
Sure. I will keep you updated and keep pushing to the Experiments folder.
Anand
@0art0
I have added an example of using coordinates to the experiments folder
In principle, I think it should be possible to write meta-level code that takes a particular equality and generates all the Lean code required to prove it using free groups the universal property.
Anand
@0art0
I have generalised the code slightly now to work uniformly for any formula on Abelian groups in 3 variables. I will try to experiment with Fin and Vector in some time to see if I can also generalise 3 to an arbitrary n.
Vector seems like a good option. I had forgotten this.
Anand
@0art0
Vector seems to be working fine so far, and I think it may be possible to get a general proof for all n using this approach (with some effort in the rewrite parts). I will continue working on this tomorrow.
Here is a sketch of reducing (e.g. to identity) that I feel is efficient.
• Represent Free Abelian groups using Vector.
• Use a BinTree with leaves Fin n × Bool to represent words in generators and their inverses.
• Define q mapping such a tree to the vector in the free abelian group.
• Represent data for a map to the additive group A by a Vector n A.
• Define function φ mapping the data and a tree to an element of A.
• Define ψ mapping a vector to an element in A.
• At meta level, associate to an element g in A a tree t (actually n and the data are chosen after associating the element).
• g is definitionally equal to φ(t) which we use to prove equality.
• Theorem: For a tree t and fixed data, φ(t) = ψ(q(t))
• this is a theorem at term level, so can be proved with types, using tactics etc. ; we need to prove such a theorem, as this is where the hypothesis that A is Abelian is used.
• The reduced form h of g is h = ψ(q(t)) and the above theorem shows g = h (due to reflexive equality). Both the reduction and the theorem have to be returned at meta level.
• The main part of the proof of the above theorem is exactly the statement that the standard map from the free abelian group to A is a homomorphism.
• So the main part of the work is just constructing free abelian groups and showing that functions on the basis extend to homomorphisms.
By the way, a periodic reminder that you are welcome to take a break from (this) work whenever you want. This is more so now that we do not have an immediate important target like Gardam's theorem.
Anand
@0art0
Thanks.
I don't mind continuing with work at the moment and trying out a few of these ideas. I may take a break sometime next week.
I have pushed a file containing some general functions and theorems for defining the map from the free group to a given Abelian group. It is slightly different from the approach that you suggested, but it is along similar lines (I have tried to use the existing FreeAbelianGroup machinery).
Anand
@0art0
I think the sketch seems good. We can perhaps run a simp before converting to the tree so that terms like -(x + y) get converted to -x + -y so that every leaf of the tree is a positive or negative literal.
Anand
@0art0
On a related note, I found a tactic in mathlib3 called assoc_rewrite, which rewrites using associativity implicitly. I haven't looked into this yet, but if this is easy to implement, we can alternatively use the idea you mentioned of fixing an order on the elements and swapping using simp.
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.
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.