siddhartha-gadgil on main
module docs for free groups, gr… (compare)
0art0 on main
Fix README (compare)
0art0 on main
Turning instances with `K x Q` … (compare)
0art0 on main
Type declaration for the invers… (compare)
0art0 on main
Minor changes in `TorsionFree` (compare)
0art0 on main
Golf proof of exactness using `… (compare)
0art0 on main
Indentation fixes (compare)
0art0 on main
Metabelian group is in an exact… (compare)
0art0 on main
Better docs for files (compare)
siddhartha-gadgil on main
image in docs removed (not work… (compare)
siddhartha-gadgil on main
png image (compare)
siddhartha-gadgil on main
graph including in README but n… (compare)
siddhartha-gadgil on main
corrected imports (compare)
siddhartha-gadgil on main
corrected imports (compare)
0art0 on main
Update to current folder name (compare)
0art0 on main
Commenting out `UniversalCover`… (Failed) attempt at `decideFora… Revert "(Failed) attempt at `de… and 7 more (compare)
siddhartha-gadgil on main
ConjInvLength to top level complexes, experiments at top l… docs in Polylean file (compare)
siddhartha-gadgil on toplevel
docs in Polylean file (compare)
siddhartha-gadgil on toplevel
complexes, experiments at top l… (compare)
siddhartha-gadgil on toplevel
ConjInvLength to top level (compare)
Vector
.BinTree
with leaves Fin n × Bool
to represent words in generators and their inverses.q
mapping such a tree to the vector in the free abelian group.A
by a Vector n A
.φ
mapping the data and a tree to an element of A
.ψ
mapping a vector to an element in A
.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.t
and fixed data, φ(t) = ψ(q(t))
A
is Abelian is used.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.A
is a homomorphism.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
.
simp
idea is a good way. The present approach seems better. We just need some implementation of free abelian groups.a * b - b * a
should cancel.
Array
s, 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.
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.
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.
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).
Z^n
.
basis
of positive size in the type α
and a tree t
.α
has an additive commutative group structure (parallel for multiplicative).foldMap
applied to t
and the basisImages
gives an element x
of α
.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.basisElements
. This maps a
to an element y
.x = y
.Vector
s. 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
.
Vector
s and sticking to only List
s and Array
s. Once I do this, the remaining obstacles in the proof due to indexed inductive type will disappear.
simp
lemma about AddCommGroup.Homomorphism
that may break existing code.