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)
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.
@fn (motive := ...)
. That may work here too.
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.
Unit^n
as a basis as we have done in the case of \Z^n
. The iterated direct sum will probably not affect the efficiency since all the computations happen with the elements of the free Abelian group, and the basis type is only used in proving that the basis elements of \Z^n
map to the chosen elements of the target Abelian group under the induced homomorphism.
Vec
(the subtype of Array
s of a fixed length) with integer entries has the structure of a free Abelian group under pointwise addition
c : Vec \Z n -> \Z ^ n
be an identification of the two types by coordinates. Once we define addition pointwise on Vec \Z n
and show that c (v + v') = c(v) + c(v')
, we can directly get a group structure on Vec \Z n
and furthermore show that it is a free Abelian group. This bypasses proofs of associativity and so on, which might be difficult with just the Array
representation.