siddhartha-gadgil on main
removed unused variables (in co… (compare)
siddhartha-gadgil on main
no nodejs in docker (compare)
siddhartha-gadgil on main
trying codespaces (compare)
siddhartha-gadgil on main
Definitions of `Quiver` and `Se… Define additional structures Define 2-complexes and 35 more (compare)
0art0 on lean-update
0art0 on main
partial, broken update update for free groups Fix remaining upgrade errors and 1 more (compare)
0art0 on lean-update
Fix remaining upgrade errors (compare)
siddhartha-gadgil on lean-update
partial, broken update update for free groups (compare)
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.
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.Array
and use results such as Array.size_pop
.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.
push
, pop
and size_push
, size_pop
.Fin n
is painful.