Jónathan Heras
email: jonathan.heras@unirioja.es

María Poza
email: maria.poza@unirioja.es

Maxime Dénès
email: maxime.denes@inria.fr

Laurence Rideau
email: laurence.rideau@inria.fr

Incidence simplicial matrices formalized in Coq/SSReflect *

Simplicial complexes are at the heart of Computational Algebraic Topology, since they give a concrete, combinatorial description of otherwise rather abstract objects which makes many important topological computations possible. The whole theory has many applications such as coding theory, robotics or digital image analysis. In this paper we present a formalization in the COQ theorem prover of simplicial complexes and their incidence matrices as well as the main theorem that gives meaning to the definition of homology groups and is a first step towards their computation.

Introduction

Algebraic Topology is a vast and complex subject, in particular mixing Algebra and (combinatorial) Topology. Algebraic Topology consists of trying to use as much as possible "algebraic" methods to attack topological problems. For instance, one can define some special groups associated with a topological space, in a way that respects the relation of homeomorphism of spaces. This allows one to study properties about topological spaces by means of statements about groups, which are often easier to prove.

However, in spite of being an abstract mathematical subject, Algebraic Topology methods can be implemented in software systems and then applied to different contexts such as coding theory [START_REF] Wood | Spinor groups and algebraic coding theory[END_REF], robotics [START_REF] Mackenzie | Topologists and Roboticists Explore and Inchoate World[END_REF] or digital image analysis [START_REF] Gonzalez-Diaz | Algebraic Topological Analysis of Time-Sequence of Digital Images[END_REF][START_REF] Gonzalez-Diaz | On the Cohomology of 3D Digital Images[END_REF] (in this last case, in particular in the study of medical images [START_REF] Ségonne | Topological Correction of Subcortical Segmentation[END_REF]). Nevertheless, if we want to use these systems in real life problems, we have to be completely sure that the systems are correct. Therefore, to increase the reliability of these methods and the systems that implement them, we can use Theorem Proving tools. In this paper we are going to focus on the verification of some results about a mathematical structure which can be useful, among others things, to study properties of digital images.

Simplicial complexes are topological abstract structures which provide a good framework to apply topological methods to analyse digital images. Intuitively, a simplicial complex is a generalization of the notion of graph to higher dimensions. Indeed, all the simplicial complexes of dimension less than two are graphs.

A central problem in this context consists of computing homology groups of simplicial complexes. Homology groups characterize both the number and the type of holes and the number of connected components of a simplicial complex. This type of information is used, for instance, to determine similarities between proteins in molecular biology [START_REF] Dey | Contemporary Mathematics[END_REF].

In the context of the computation of homology groups, we can highlight the Kenzo program [START_REF] Dousson | The Kenzo program[END_REF], a successful Computer Algebra system, implemented in Common Lisp, which has obtained some homology groups not confirmed nor refuted by any other means.

There are two different ways of computing homology groups in Kenzo depending on the type of the object. On the one hand, the task of calculating homology groups of a finite object is translated to a problem of diagonalizing certain matrices called incidence matrices, see [START_REF] Veblen | Analysis Situs[END_REF]. On the other hand, in the case of non-finite type objects, Sergeraert's effective homology [START_REF] Rubio | Constructive Homological Algebra and Applications[END_REF] theory, implemented in Kenzo, provides a framework where this question can be handled. Roughly speaking, the effective homology method links a non-finite type object, X , with a finite type object, Y , with the same homology groups; then the problem of computing the homology groups of X is reduced to the task of diagonalizing the incidence matrices of Y .

Sergeraert's ideas have been translated to theorem provers with the aim of not only formalizing the effective homology theory, but also applying formal methods to the study of Kenzo. Thus far, the main formalization efforts have been focused on theorems which provide the connection between non-finite type objects with finite type ones; here, we can distinguish the verification of the Basic Perturbation Lemma in the Isabelle/HOL proof assistant, see [START_REF] Aransay | A mechanized proof of the Basic Perturbation Lemma[END_REF], or the formalization in COQ of the Effective Homology of Bicomplexes, see [DR].

However, up to now, the question of formalizing the computation of homology groups of finite objects has not been undertaken. In this paper we discuss the formalization of simplicial complexes and their incidence matrices as well as the main theorem that gives meaning to the definition of homology groups. To this aim, we have used the proof assistant COQ [tdt10, BC04] as well as the SSREFLECT extension [START_REF] Gonthier | A Small Scale Reflection Extension for the Coq system[END_REF] and the libraries it provides.

The rest of the paper is organized as follows. Section 2 contains some preliminaries on Algebraic Topology. A sketch of the proof of the main theorem is presented in Section 3. A brief introduction to SSREFLECT is provided in Section 4. The main steps of the formalization are given in Section 5. The paper ends with a section of Conclusions and Further Work, and the bibliography.

Mathematical preliminaries

In this section, we briefly provide the minimal standard background needed in the rest of the paper. We mainly focus on definitions. Many good textbooks are available for these definitions and results about them, the main one being maybe [START_REF] Maclane | Homology[END_REF].

The notion of simplicial complex gives rise to the most elementary method to settle a connection between common Topology and Algebraic Topology. The notion of topological space is too abstract to perform computations. Simplicial complexes provide a purely combinatorial description of topological spaces which admit a triangulation. The computability of properties, such as homology groups, from a simplicial complex associated with a topological space is well-known and the algorithm uses simple linear algebra [START_REF] Veblen | Analysis Situs[END_REF]. Then, an algebraic topologist can decide every sensible space (that is to say, a topological space which admit a triangulation) is a simplicial complex, making computations easier.

Let us start with some basic terminology. Let V be an ordered set, called the vertex set. An (abstract) simplex over V is any finite subset of V . An (abstract) n-simplex over V is a simplex over V whose cardinality is equal to n + 1. Given a simplex α over V , we call subsets of α faces of α.

Definition 1 An (ordered abstract) simplicial complex over V is a set of simplices over V such that it is closed by taking faces (subsets); that is to say, if α ∈ all the faces of α are in , too. Let be a simplicial complex. Then the set S n ( ) of n-simplices of is the set made of the simplices of cardinality n + 1.

Example 1 Let us consider V = (0, 1, 2, 3, 4, 5, 6).

The small simplicial complex drawn in Figure 1 is mathematically defined as the object:

= , (0), (1), (2), (3), (4), (5), (6), (0, 1), (0, 2), (0, 3), (1, 2), (1, 3), (2, 3), (3, 4), (4, 5), (4, 6), (5, 6), (0, 1, 2), (4, 5, 6) It is worth noting that simplicial complexes can be infinite. For instance if V = and the simplicial complex is {(n)} n∈ ∪ {(0, n)} n≥1 , the simplicial complex obtained can be seen as an infinite bunch of segments.

Definition 2 A facet of a simplicial complex over V is a maximal simplex with respect to the subset order ⊆ among the simplexes of . {(0, 3), (1, 3), (2, 3), (3, 4), (0, 1, 2), (4, 5, 6)} To construct the simplicial complex associated with a sequence of facets, , we generate all the faces of the simplexes of . Subsequently, if we perform the set union of all the faces we obtain the simplicial complex associated with . Definition 3 Let be a simplicial complex over V . Let n and i be two integers such that n ≥ 1 and 0 ≤ i ≤ n. Then the face operator ∂ n i is the linear map ∂ n i : S n ( ) → S n-1 ( ) defined by:

∂ n i ((v 0 , . . . , v n )) = (v 0 , . . . , v i-1 , v i+1 , . . . , v n )
the i-th vertex of the simplex is removed, so that an (n -1)-simplex is obtained. Now, we are going to introduce a central notion in Algebraic Topology. We assume as known the notions of ring, module over a ring and module morphism (see [START_REF] Jacobson | Basic Algebra II[END_REF] for details).

Definition 4 Given a ring R, a graded module M is a family of left R-modules (M n ) n∈ .
Definition 5 Given a pair of graded modules M and M ′ , a graded module morphism f of degree k between them is a family of module morphisms

( f n ) n∈ such that f n : M n → M ′ n+k for all n ∈ . Definition 6 Given a graded module M , a differential (d n ) n∈ is a family of module endomorphisms of M of degree -1 such that d n-1 • d n = 0 for all n ∈ .
The previous definitions define a graded structure and a way of going from a level of the structure to the inferior one. From the previous definitions, the notion of chain complex is defined as follows.

Definition 7 A chain complex C * is a family of pairs (C n , d n ) n∈ where (C n ) n∈ is a graded module and (d n ) n∈ is a differential on (C n ) n∈ . The module C n is called the module of n-chains. The image B n = im d n+1 ⊆ C n is the (sub)module of n-boundaries. The kernel Z n = ker d n ⊆ C n is the (sub)module of n-cycles. Given a chain complex C * = (C n , d n ) n∈ , the identities d n-1 • d n = 0 are equivalent to the inclusion relations B n ⊆ Z n :
every boundary is a cycle but the converse is not generally true. Thus, the next definition makes sense.

Definition 8 Let C * = (C n , d n ) n∈ be a chain complex of R-modules. For each degree n ∈ , the n-homology module of C * is defined as the quotient module

H n (C * ) = Z n B n
Once we have defined the notions of simplicial complexes and chain complexes, we can define the link between them considering as the ring R; the most common case in Algebraic Topology. Definition 9 Let be a simplicial complex over V . Then the chain complex C * ( ) canonically associated with is defined as follows. The chain group C n ( ) is the free module generated by the n-simplices of . In addition, let (v 0 , . . . , v n ) be an n-simplex of , the differential of this simplex is defined as:

d n := n i=0 (-1) i ∂ n i
In order to clarify the notion of chain complex canonically associated with a simplicial complex, let us present an example. The chain complexes associated with simplicial complexes are good candidates for this purpose.

Example 3 Let be the simplicial complex defined in Figure 1. The chain complex C * ( ) canonically associated with is:

• • • → 0 → C 2 ( ) d 2 -→ C 1 ( ) d 1 -→ C 0 ( ) → 0 → • • •
where there are 3 associated chain groups:

• C 0 ( ), the free -module on the set of 0-simplexes (vertices) {(0), (1), ( 2), (3), (4), ( 5), (6)}.

• C 1 ( ), the free -module on the set of 1-simplexes (edges) {(0, 1), (0, 2), (0, 3), (1, 2), (1, 3), (2, 3), (3, 4), (4, 5), (4, 6), (5, 6)}.

• C 2 ( ), the free -module on the set of 2-simplexes (triangles) {(0, 1, 2), (4, 5, 6)}.

The elements of either of those groups C p are linear integer combinations of the corresponding basis (set of σ i 's), i.e. elements of the form

λ i σ i , λ i ∈ .
The differential homomorphism is in this case:

d n ((v 0 , . . . , v n )) := n i=0 (-1) i (v 0 , . . . , v i-1 , v i+1 , . . . , v n ) (1) For instance, d 2 ((0, 1, 2)) = (1, 2) -(0, 2) + (0, 1).
From the previous definition, we can introduce a very useful concept for the computation of homology groups of simplicial complexes.

Definition 10 Let be a simplicial complex over V and let n be an integer such that n ≥ 1. The n-th incidence matrix of over the ring , denoted by M n ( , ), represents the (n -1)-simplices of as rows and the n-simplices of as columns. Assuming an ordering on the simplices of the same dimension (in the rest of the paper we assume that the simplices of the same dimension will be ordered), M n ( , ) is [a j i ] where i ranges from 1 to the cardinality of S n-1 ( ), j ranges from 1 to the cardinality of S n ( ) and the value of a j i is the coefficient of the i-th (n -1)-simplex in the differential of the j-th n-simplex; then a j i is a value in {0, ±1}.

Example 4 If we impose a lexicographical order on the simplices of the same dimension of the simplicial complex depicted in Figure 1

(if v = (a 0 , . . . , a n ) and w = (b 0 , . . . , b n ) are n-simplices of the simplicial complex, then v < w if a 0 < b 0 , or a 0 = b 0 and a 1 < b 1 , or a 0 = b 0 and a 1 = b 1 and a 2 < b 2 ,. . . , or a 0 = b 0 , . . . a n-1 = b n-1 and a n < b n ), then its first incidence matrix is:           (0, 1) (0, 2) (0, 3) (1, 2) (1, 3) (2, 3) (3, 4) (4, 5) (4, 6) (5, 6) (0) -1 -1 -1 0 0 0 0 0 0 0 (1) 1 0 0 -1 -1 0 0 0 0 0 (2) 0 1 0 1 0 -1 0 0 0 0 (3) 0 0 1 0 1 1 -1 0 0 0 (4) 0 0 0 0 0 0 1 -1 -1 0 (5) 0 0 0 0 0 0 0 1 0 -1 (6) 0 0 0 0 0 0 0 0 1 1          
The relevance of the incidence matrices of simplicial complexes lies in the fact that they can be used to compute the homology groups of the simplicial complex by means of a diagonalization process, as explained for instance in [START_REF] Veblen | Analysis Situs[END_REF].

0 1 0 1 (1,2) (2,1) (2,2) (0,0) (0,1) (1,0) (1,1)
Figure 2: A digital image and its simplicial complex representation

The theorem formalized and its context

The definitions presented in the previous section are classical definitions from Algebraic Topology. However, since our final goal consists of working with mathematical objects coming from digital images, let us show how this machinery from algebraic topology may be used in this context.

It is worth noting that there are several methods to construct a simplicial complex from a digital image [START_REF] Ayala | Homotopy in digital spaces[END_REF]. We are going to explain one of these methods. Roughly speaking, the chosen method consists of obtaining a sequence of facets from a digital image. Then, as we have explained in the previous section, we can obtain the simplicial complex associated with the facets. So, we only need to explain how to get the facets from a digital image.

We are going to work with monochromatic two dimensional images. An image can be represented by a finite 2-dimensional array of 1's and 0's in which the black pixels are represented by 1's and white pixels are represented by 0's.

Let be an image codified as a 2-dimensional array of 1's and 0's. Let V = ( , ) be the vertex set, each vertex is a pair of natural numbers. Let p = (a, b) be the coordinates of a black pixel in . For each p we can obtain two 2-simplexes which are two facets of the simplicial complex associated with . Namely, for each p = (a, b) we obtain the following facets: ((a, b), (a +1, b), (a +1, b+1)) and ((a, b), (a, b+1), (a +1, b+1)). If we repeat the process for the coordinates of all the black pixels in , we obtain the facets of a simplicial complex associated with , let us called it .

Example 5 Consider the image depicted in Figure 2. This image, , can be codified by means of the 2dimensional array: ((1,0),(0,1)). Then, with the previously explained process we obtain the facets of . The coordinates of the black pixels are (0, 0) and (1, 1), so the facets that we obtain are:

(((0, 0), (1, 0), (1, 1)), ((0, 0), (0, 1), (1, 1)), ((1, 1), (2, 1), (2, 2)), ((1, 1), (1, 2), (2, 2)))

We have presented a method to obtain a simplicial complex associated with a 2D-image, this process can be generalized to higher-dimensional images [START_REF] Orden | Asymptotically efficient triangulations of the d-cube[END_REF].

It is worth noting that even the bigger digital images have always a finite number of components, hence a finite number of vertices and then our vertex set V consists of a finite number of vertices. Therefore, the simplicial complexes coming from digital images are always of finite type. This point will be important in our formalization.

Moreover, instead of working with the ring , we consider the ring /2 since the computation of homology groups is easier working with /2 . This approach is usually followed when algebraic topology methods are applied to the study of digital images, see [START_REF] Gonzalez-Diaz | Algebraic Topological Analysis of Time-Sequence of Digital Images[END_REF][START_REF] Gonzalez-Diaz | On the Cohomology of 3D Digital Images[END_REF].

Then, we are going to work with a different definition of the face operator and associated incidence matrices. Indeed, since coefficients (in /2 ) of opposite sign are identified, we do not have to deal with orientations of faces.

Thus, in the following will denote a simplicial complex over a finite set V and n an integer such that n ≥ 1. The incidence matrix is now defined by: Definition 11 The n-th incidence matrix of over the ring /2 , denoted by M n ( ), is a matrix of size m × p, where m is the cardinality of S n-1 ( ) and p is cardinality of S n ( ). Its coefficients [a j i ] are 1 if the i-th (n -1)-simplex is a face of the j-th n-simplex and 0 otherwise. Note that the n-th incidence matrix of over the ring /2 is the absolute value of the n-th incidence matrix of over the ring .

Using this definition of incidence matrices, it is not necessary to use chain complexes to compute homology groups of simplicial complexes, but just applying a diagonalization process, as described in [START_REF] Veblen | Analysis Situs[END_REF].

Example 6 If we impose a lexicographical order on the simplices of the same dimension of the simplicial complex depicted in Figure 1, then its first incidence matrix over the ring /2 is:

          (0, 1) (0, 2) (0, 3) (1, 2) (1, 3) (2, 3) (3, 4) (4, 5) (4, 6) (5, 6) (0) 1 1 1 0 0 0 0 0 0 0 (1) 1 0 0 1 1 0 0 0 0 0 (2) 0 1 0 1 0 1 0 0 0 0 (3) 0 0 1 0 1 1 1 0 0 0 (4) 0 0 0 0 0 0 1 1 1 0 (5) 0 0 0 0 0 0 0 1 0 1 (6) 0 0 0 0 0 0 0 0 1 1          
As we have said previously, incidence matrices of simplicial complexes come from the differentials of the chain complexes canonically associated with the simplicial complexes. Theses differentials satisfy a nilpotency condition

(d n-1 • d n = 0).
Then, we can state and proof the following theorem that is analogous to this nilpotency condition on the incidence matrices we have defined above. It should be noted that the statement below is the immediate transcription of the one we formalized and proved in Coq/SSReflect.

Theorem 1

The product of the n-th incidence matrix of over the ring /2 , M n ( ), and the (n + 1)incidence matrix of over the ring /2 , M n+1 ( ) is equal to the null matrix.

Sketch of the proof. Let S n-1 , S n , S n+1 be the set of (n -1)-simplices of , the set of n-simplices of and the set of (n + 1)-simplices of respectively. Then,

M n ( ) =        S n [1] • • • S n [r1] S n-1 [1] a 1,1 • • • a 1,r1 . . . . . . . . . . . . S n-1 [r2] a r2,1 • • • a r2,r1        , M n+1 ( ) =        S n+1 [1] • • • S n+1 [r3] S n [1] b 1,1 • • • b 1,r1 . . . . . . . . . . . . S n [r1] b r1,1 • • • b r1,r3        where r1 = ♯|S n |, r2 = ♯|S n-1 | and r3 = ♯|S n+1 |. Thus, M n ( ) × M n+1 ( ) =     c 1,1 • • • c 1,r3 . . . . . . . . . c r2,1 • • • c r2,r3     where c i, j = 1≤k≤r1 a i,k × b k, j
To prove that M n ×M n+1 is equal to the null matrix, it is enough to prove that ∀i, j such that 1 ≤ i ≤ ♯|S n-1 | and 1 ≤ j ≤ ♯|S n+1 |, then c i, j = 0. Each of these coefficients is written:

c i, j = 1≤k≤r1 a i,k × b k, j
Since k enumerates the indices of elements of S n , we may write:

c i, j = X ∈S n F (S n-1 [i], X ) × F (X , S n+1 [ j]) with F (Y, Z) = 1 if Y ∈ d Z 0 otherwise (2)
d Z is the analogous in our context of the differential operator defined by (1) and is equal to:

d Z = {Z \ {x} | x ∈ Z}
This summation can be split depending on whether

X ∈ ∂ S n+1 [ j] or X / ∈ ∂ S n+1 [ j]. c i, j = X ∈S n |X ∈∂ S n+1 [ j] F (S n-1 [i], X ) × 1 (3) + X ∈S n |X / ∈∂ S n+1 [ j] F (S n-1 [i], X ) × 0 = X ∈S n |X ∈∂ S n+1 [ j] F (S n-1 [i], X ) (4)
The last summation is expressed over the image of the face operator x → S n+1 [ j] \ {x} which, restricted to S n+1 [ j], is injective. Thus, we can reindex:

c i, j = x∈S n+1 [ j] F (S n-1 [i], S n+1 [ j] \ {x}) (5)
Subsequently, this summation can also be split depending on whether

x ∈ S n-1 [i] or x / ∈ S n-1 [i]. c i, j = x∈S n+1 [ j]|x∈S n-1 [i] F (S n-1 [i], S n+1 [ j] \ {x}) + x∈S n+1 [ j]|x / ∈S n-1 [i] F (S n-1 [i], S n+1 [ j] \ {x}) (6)
Let us note that if

x ∈ S n-1 [i] then S n-1 [i] ⊂ S n+1 [ j]
\ {x}, hence the first sum above is 0.

c i, j = x∈S n+1 [ j]|x / ∈S n-1 [i] F (S n-1 [i], S n+1 [ j] \ {x}) (7)
Here, we can split our proof considering two cases:

S n-1 [i] ⊂ S n+1 [ j] and S n-1 [i] ⊂ S n+1 [ j].
In the first case, we have:

∀x ∈ S n-1 [i], F (S n-1 [i], S n+1 [ j] \ {x}) = 0, hence the result holds. In the second case, S n-1 [i] ⊂ S n+1 [ j] implies that if x / ∈ S n-1 [i] then S n-1 [i] ∈ ∂ S n+1 [ j] \ {x}, so the terms are all 1. c i, j = x∈S n+1 [ j]|x / ∈S n-1 [i] 1 (8) = ♯|S n+1 [ j] \ S n-1 [i]| = n + 2 -n = 2 = 0 mod 2

SSReflect basics

To formalize Theorem 1, we have used SSREFLECT [START_REF] Gonthier | A Small Scale Reflection Extension for the Coq system[END_REF], an extension for the COQ proof assistant [START_REF] Bertot | Interactive Theorem Proving and Program Development, Coq'Art: the Calculus of Inductive Constructions[END_REF][START_REF]The COQ Proof Assistant Reference Manual[END_REF]. Its development was started by G. Gonthier during the formal proof of the Four Color Theorem [START_REF] Gonthier | Formal proof -The Four-Color Theorem[END_REF] and is now involved in the formalisation of the Feit-Thompson theorem [Mat]. SSREFLECT (for Small Scale Reflection) introduces a new language for tactics that eases the development of proof scripts. Another main feature is the generic reflection mechanism. More details on the SSREFLECT tactics language and reflection techniques are presented in its manual [START_REF] Gonthier | A Small Scale Reflection Extension for the Coq system[END_REF].

Moreover, SSREFLECT provides a set of libraries embedding definitions and properties for a variety of mathematical structures. In our formalization, it is worth mentioning the following libraries:

• matrix.v: this library formalizes matrix theory, determinant theory and matrix decompositions. In our problem, this library is used to define incidence matrices, and to state and prove Theorem 1.

• finset.v and fintype.v: theory of finite sets and finite types. We use these libraries to define the basic concepts about simplicial complexes.

• bigop.v: generic indexed "big" operations, like n i=0 f (i) or i∈I f (i) and their properties, which are useful to deal with the matricial product in Theorem 1.

• zmodp.v: additive group and ring p , together with field properties when p is a prime. As we work with elements of the field 2 , we need this library.

For more precise details on these libraries we refer to [BGBP08, GMR + 07] Then we have all the ingredients to state Theorem 1:

Theorem incidence_matrices_sc_product:
forall (V:finType) (n:nat) (sc: {set (simplex V)}), simplicial_complex sc -> (incidence_mx_n sc n) *m (incidence_mx_n sc (n.+1)) = .

In the statement above, *m denotes the matricial product. The type information of each matrix includes its size. When the product operator is applied, the typechecking ensures that the two arguments have compatible sizes. Then the system knows the expected size of the result matrix and reads 0 as the null matrix of this size.

The formal proof of Theorem 1 follows the schema presented in Section 3. A large part of the proof is devoted to the work with summations, for which the Coq/SSReflect library "bigop" has played a key role.

For instance, the first summation splitting (equation ( 3)) is realized by: rewrite (bigID (mem (boundary (enum_val j)))).

where j belongs to S n+1 . The lemma bigID states that an iterated operation using a commutative monoidal operator can be split:

i∈r|P i F i = i∈r|P i ∧a i F i + i∈r|P i ∧∼a i F i
It is also possible to split a summation (equation ( 6)) and at the same time rewrite the first resulting sum to 0 as in: rewrite (bigID (mem (enum_val i))) big1. big1 states that, when a monoidal operator is iterated over elements that are all equal to the neutral, then the result is also the neutral element:

i∈r|P i 0 = 0
Therefore, after the last tactic, the system will require a proof that all the terms of the first resulting summation are zero. big1 is applied to obtain equations 4 and 7 of Section 3.

Our proof relies on two main reindexations: from ordinals to n-simplices (2) and later on from simplices to vertices (5). To perform the first reindexation, the script has the following shape: rewrite (reindex_onto (enum_rank_in Hx ) enum_val) ; last first. by move=> x _ ; exact:enum_valK_in.

Where:

• Hx0 is a proof that there exists at least one n-simplex

• enum_rank_in enumerates the n-simplices since Hx0 ensures there is at least one • enum_val enumerates the ordinals over which the sum is expressed

• reindex_onto reindexes from ordinals to n-simplices, given a bijection between both sets. Indeed, the second line proves that enum_val • enum_rank_in = Id

The second reindexation is based on the injectivity of the face operator:

rewrite big_imset ; last exact:face_op_inj2.

Rewriting with the lemma big_imset triggers a check that the summation is expressed over the image of a set by a function. In our case, the system automatically infers that this function is the face operator face_op, and will then ask for a proof of its injectivity. The lemma eq_big and its variants eq_bigl and eq_bigr allow to rewrite the predicate or the operand of an iterated operation. It is applied in particular to obtain equation 8 of Section 3: rewrite (eq_bigr (fun _ => 1)).

The system will of course require a proof that the operand is equal to 1. Then it will rewrite the expression to a constant summation, allowing the use of the lemma big_const to replace it with a product (cardinal of the iterated set by the constant value).

Simple arithmetic arguments on cardinals will then complete the proof. The interested reader will find a snapshot of our development online [START_REF] Heras | Incidence simplicial matrices formalized in SSReflect[END_REF].

Conclusions and further work

In this paper we have presented the formalization of simplicial complexes and their incidence matrices as well as the main theorem that gives meaning to the definition of homology groups. The proof assistant used has been COQ as well as the SSREFLECT extension and the libraries it provides. The verified algorithm is related to a Computer Algebra system for Algebraic Topology called Kenzo [START_REF] Dousson | The Kenzo program[END_REF]. Therefore, our research is placed between the efforts to formalize mathematics and the application of formal methods in software systems.

Some parts of the future work are quite natural. The work presented here is solid enough to undertake the challenge of formalizing the construction of the Smith Normal Form [START_REF] Veblen | Analysis Situs[END_REF] of incidence matrices, that is the diagonalization process which obtains homology groups of finite type objects.

Moreover, if we want to apply our Algebraic Topology methods to real life problems, for instance the study of medical images, we must be completely sure that our programs are safe. Therefore, the process to construct a simplicial complex from a digital image, presented in Section 3, should be formalized, too.

In addition, our proof seems generic enough to achieve the case of working with -modules, instead of /2 -modules, quite easily.

Another topic is related to the executability of our proofs, that is the computational capabilities of the objects we have defined (like the incidence matrices). Two main approaches are possible: code extraction or internal computations. The first one delivers a certified program and takes advantage of the existing extraction machinery of the Coq system. However, technical limitations have to be dealt with to get a usable program in our context. The second approach is somewhat more challenging regarding efficiency. Indeed, reaching inside Coq an execution speed on par with the one obtained by extraction and compilation is difficult because proofs cannot safely be erased from the terms (what extraction does). However, compilation techniques and evaluation strategies mitigating the performance impact are currently being studied and implemented.

One advantage of this second approach lies in the fact that it would enable the reuse of computational results in further formal developments. For instance, the computation of the smith normal form of a matrix could be used for further deductions, in the same system, on the topological object under study. We are currently studying the use of both code extraction and efficient computational techniques in the Coq/SSReflect system, applied to the objects and theories we have presented above.

Example 2

 2 Figure 1: Butterfly Simplicial Complex

  Definition n_1_simplices := [set x \in c | #|x| == n]. Definition n_simplices := [set x \in c | #|x| == n+1]. Definition incidence_matrix_n := incidenceMatrix n_1_simplices n_simplices. End nth_incidence_matrix.

* Partially supported by Ministerio de Educación y Ciencia, project MTM2009-13842-C02-01, and by European Community FP7, STREP project ForMath.

Formal development

The SSREFLECT libraries include all the necessary ingredients to represent the mathematical structures of our formalization.

First of all, we define the notions related to simplicial complexes. The vertices are represented by a finite type V. A simplex is defined as a finite set of vertices. Then, the definition of a simplicial complex as a set of simplices closed under inclusion is straightforward:

Variable V : finType. Definition simplex := {set V}. Definition simplicial_complex (c : {set simplex}) := forall x, x \in c -> forall y : simplex, y \subset x -> y \in c.

Since we do not take into account the signs of the coefficients appearing in the incidence matrices, we define a face operator as a set difference (we remove a vertex from a simplex) and the boundary as the image of a simplex by the face operator. The statement reflect P b expresses an equivalence between a proposition P and a boolean expression b. This allows to take advantage of the decidability of some propositions by going back and forth from their logical expressions (useful for reasoning) to their boolean counterparts (well suited for computations).

A key argument for our proof is the injectivity of the face operator above, which we establish as a lemma:

Lemma face_op_inj2: forall (S : simplex), {in S &, injective (face_op S)}.

The notation {in S &, P} performs localization of predicates: if P is of the form forall x y, Qxy then { in S &, P} means forall x y, x \in S -> y \in S -> Qxy. In our case, injective f stands for forall x y, f x = f y -> x = y. Now, before giving the definition of the n-th incidence matrix of a simplicial complex, we can define the more generic notion of incidence matrix of two finite sets of simplices.

Representing a matrix requires an indexing of the simplices in Left (for the rows) and Top (for the columns). Since Left and Top are finite sets, they are equipped with a canonical enumeration: (enum_val Left i) returns the i-th element of the set Left. A coefficient a i j of the incidence matrix will be 1 if the i-th simplex of Left is a face (subset) of the j-th simplex of Top and 0 otherwise. Thus we can define the incidence matrix of two finite sets of simplices as follows:

Variables Left Top : {set simplex}. Definition incidenceMatrix := \matrix_(i < #|Left|, j < #|Top|) if enum_val i \in boundary (enum_val j) then 1 else :'F_2.

In the definition above, it can be noted that the first argument of enum_val is implicit and determined by the context. Indeed, the notation i < #|Left| means that the type of i is 'I_(#|Left|), that is i is an ordinal ranging from 0 to #|Left|-1, where #|X| denotes the cardinal of the set X. With this type information, the system expands enum_val i to enum_val Left i, thus resolving the ambiguity (and similarly for j).

The type annotation :'F_2 indicates that the 0 and 1 appearing as coefficients of the matrix are the two elements of 2 , that is /2 as a field.

We now define the n-th incidence matrix of a simplicial complex c, by instantiating Left to the set of n -1-simplices (of c) and Top to the set of n-simplices. Note that n should be nonzero.

Section nth_incidence_matrix.

Variable c: {set simplex}. Variable n:nat.


Paolo Bellingeri

Eddy Godelle

John Guaschi

Exact sequences, lower central series and representations of surface braid groups

Keywords: 2000 AMS Mathematics Subject Classification: 20F14, 20F36. Keywords: surface braid groups, linear representations of braid groups 1

We consider exact sequences and lower central series of (surface) braid groups and we explain how they can prove to be useful for obtaining representations for surface braid groups. In particular, using a completely algebraic framework, we describe the notion of extension of a representation introduced and studied recently by An and Ko and independently by Blanchet.

Introduction

The faithful linear representations of Bigelow-Krammer-Lawrence of the Artin braid groups B n are probably one of the most important recent discoveries in the theory of braid groups, and as such, have been intensively studied over the last few years. They have also been extended to other groups, such as Artin-Tits groups of spherical type (see for instance [START_REF] Cohen | Linearity of Artin groups of finite type[END_REF][START_REF] Digne | On the linearity of Artin braid groups[END_REF]). However, with the exception of a few results [START_REF] Bardakov | Linear representations of the braid groups of some manifolds[END_REF][START_REF] Bigelow | The mapping class group of a genus two surface is linear[END_REF][START_REF] Gonçalves | Embeddings of the braid groups of covering spaces, classification of the finite subgroups of the braid groups of the real projective plane, and linearity of braid groups of low-genus surfaces[END_REF], their generalisation in a more topological direction, to braid and mapping class groups of surfaces for example, as well as the linearity of these groups, are open problems in general.

The aim of this paper is twofold. The first is to underline the relevance of short exact sequences of braid groups and their generalisations to the study of representations of these groups. As we shall recall in Section 2, the Burau and Bigelow-Krammer-Lawrence representations appear when one studies certain 'mixed' extensions of B n arising from fibrations at the level of configuration spaces. This extension splits, and in the simplest case, its kernel is the fundamental group of the n-punctured disc D n . The Burau representation then occurs as the induced action of B n on the homology of the infinite cyclic covering D n of D n .

The Bigelow-Krammer-Lawrence representations may be obtained in a similar way in terms of the Borel-Moore middle homology group of a Z 2 -covering of D n (see Section 2.3 for more details). Motivated by these constructions, one possible strategy for obtaining linear representations of (surface) braid groups is to study exact sequences of these groups. With this in mind, we recall the definitions of surface braid groups and their short exact sequences in Section 3, as well as the known results concerning the splitting of these sequences (Lemma 3.2). In the case of the short exact sequence of 'mixed' Artin braid groups, the induced short exact sequence on the level of commutator subgroups brings into play groups and homomorphisms that appear in the construction of Bigelow-Krammer-Lawrence representations of B n (see the end of Section 2.3).

Before stating similar results for exact sequences of surface braid groups, in Section 4, we recall the basic definitions pertaining to the lower central series (Γ i (G)) i∈N of a group G, and we show that if G is the braid or mixed braid group (with a sufficiently large number of strings) of a compact orientable surface Σ g with a single boundary component, the quotient group G/Γ 3 (G) is a semi-direct product of free Abelian groups. We provide group presentations for such quotients (Lemma 4.9 and Corollary 4.10) that will play an important rôle in the rest of the paper.

In [START_REF] An | A family of representations of braid groups on surfaces[END_REF], An and Ko described an extension of the Bigelow-Krammer-Lawrence representations of B n to braid groups of orientable surfaces of positive genus and with non-empty boundary. However, it is not currently known whether these representations are faithful. The representation is based on the regular covering arising from a projection of the n-th braid group of a surface Σ with non-empty boundary onto a specific group G Σ , constructed in a technical manner in order to satisfy certain homological constraints (Section 3 and Definition 2.2 of [START_REF] An | A family of representations of braid groups on surfaces[END_REF]) and which turns out to be a Heisenberg group; more recently, the above projection has been independently studied by Christian Blanchet to obtain a representation of a large subgroup of the Torelli group of a surface with one boundary component containing the Johnson subgroup [START_REF] Blanchet | Non commutative representations of Torelli groups[END_REF].

The second aim of our paper is to show that technical construction proposed in [START_REF] An | A family of representations of braid groups on surfaces[END_REF] of the representations may be described in terms of lower central series and exact sequences of surface braid groups: this is the object of Section 5. As we mentioned above, in the case of Artin braid groups, the induced short exact sequence on the Γ 2 -level gives rise to elements used in the construction of the Bigelow-Krammer-Lawrence representations. In the case of surface braid groups, the corresponding construction on the same level does not work (Proposition 5.4), but if we take this construction a stage further, to the Γ 3 -level, we obtain the corresponding objects of the An-Ko representations. More precisely we show how to use the Γ 3 -level to extend Bigelow-Krammer-Lawrence representations and we prove that such extensions are unique up to isomorphism (Propositions 5.7 and 5.8), according to Definition 5.2.

We finish the main part of the paper with another possible application of the lower central series of surface braid groups by showing that the standard length function on B n admits a unique extension to a homomorphism whose source is the braid group of a surface of positive genus with one boundary component (Proposition 5.10), and that there is no such extension if the surface is closed and orientable (Proposition 5.11). In an Appendix, we discuss the relationship between the splitting of the 'mixed' surface braid group sequences and that of their restriction to the corresponding pure braid groups. In the terminology of [START_REF] Falk | The lower central series of a fiber-type arrangement[END_REF], we show that this restriction never give rises to an almost-direct product (an almostdirect product structure means that the extension is split, and that the induced action of the lower central series quotient K/Γ 2 (K) on the kernel K is trivial). We recall the definition due to Fox of these groups in terms of fundamental groups of configuration spaces [START_REF] Fox | The braid groups[END_REF]. Let Σ be a connected surface. Let F n (Σ) = Σ n \ ∆, where ∆ is the set of n-tuples x = (x 1 , . . . , x n ) ∈ Σ n for which x i = x j for some i = j. The fundamental group π 1 (F n (Σ)) is called the pure braid group on n strands of the surface Σ; it shall be denoted by P n (Σ). There is a natural action of the symmetric group S n on F n (Σ) by permutation of coordinates; the fundamental group π 1 (F n (Σ)/S n ) is called the braid group on n strands of the surface Σ and shall be denoted by B n (Σ). Then F n (Σ) is a regular n!-fold covering of F n (Σ)/S n that gives rise to the following short exact sequence:

1 -→ P n (Σ) -→ B n (Σ) -→ S n -→ 1. (1)
Regarded as a subgroup of S k+n , the group S k × S n acts on F k+n (Σ). The fundamental group π 1 (F k+n (Σ)/(S k × S n )) will be called the mixed braid group of Σ on (k, n) strands, and shall be denoted by B k,n (Σ). Notice that B k,n (Σ) embeds canonically in B k+n (Σ). These intermediate groups between pure braid and braid groups of a surface, known as 'mixed' braid groups, play an important rôle in [START_REF] An | A family of representations of braid groups on surfaces[END_REF]. They were defined previously in [START_REF] Gonçalves | The roots of the full twist for surface braid groups[END_REF][START_REF] Manfredini | Some subgroups of Artin's braid group[END_REF][START_REF] Paris | Geometric subgroups of surface braid groups[END_REF], and were studied in more detail in [START_REF] Gonçalves | The braid group Bn,m(S2) and a generalisation of the Fadell-Neuwirth short exact sequence[END_REF] in the case where Σ is the 2-sphere S 2 .

Fibrations and induced exact sequences

We recall that π 1 (F n (D 2 )) is isomorphic to the pure braid group on n strands, usually denoted by P n , while π 1 (F n (D 2 )/S n ) is isomorphic to the braid group B n on n strands. In what follows, the mixed braid group on (k, n) strands π 1 F k+n (D 2 )/(S k × S n ) will be denoted simply by B k,n .

The fibration F k+n (D 2 )/(S k × S n ) -→ F n (D 2 )/S n given by forgetting the first k coordinates is a locally-trivial fibration whose fibre over a point {x 1 , . . . , x n } may be identified with the orbit space F k (D 2 \ {x 1 , . . . , x n })/S k . From now on we denote D 2 \ {x 1 , . . . , x n } by D n . Let us also denote π 1 (F k (D n )/S k ) by B k (D n ); this group turns out to be isomorphic to the subgroup of B k+n consisting of braids where the last n strands are trivial (vertical). The long exact sequence in homotopy of the above fibration yields a short exact sequence.

Lemma 2.1. Let k, n ∈ N. The Fadell-Neuwirth fibration F k+n (D 2 ) -→ F n (D 2 )
induces the short exact sequence:

1 -→ B k (D n ) -→ B k,n -→ B n -→ 1 .
(MB)

In a similar way, we may obtain the more well-known short exact sequence of pure braid groups.

1 -→ P k (D n ) -→ P k+n -→ P n -→ 1.
(PB)

Here P k (D n ) denotes the fundamental group of F k (D n ), which is isomorphic to the subgroup of P k+n consisting of pure braids where the last n strands are vertical. Notice that the short exact sequences (M B) and (P B) split for all k ≥ 1, where the section is given geometrically by adding k trivial strands 'at infinity' (see for instance [START_REF] An | A family of representations of braid groups on surfaces[END_REF][START_REF] Bellingeri | On presentations of surface braid groups[END_REF]).

Linear representations for the braid group B n

When k = 1, the short exact sequence (P B) plays a central rôle in the study of Vassiliev invariants of braid groups and of Lie Algebras related to pure braid groups. We refer to [START_REF] Papadima | The universal finite-type invariant for braids, with integer coefficients[END_REF] for the classical case and to [START_REF] Bellingeri | Braids on surfaces and finite type invariants[END_REF][START_REF] Enriquez | On the Lie algebras of surface pure braid groups[END_REF][START_REF] González-Meneses | Vassiliev invariants for braids on surfaces[END_REF] for analogous results in the case of surface braid groups.

In what follows, we will focus on the relevance of such short exact sequences to linear representations of braid groups and their topological generalisations. Let us start with the case k = 1. The group B n may be interpreted as the mapping class group of D n [START_REF] Birman | Braids, Links, and Mapping Class Groups[END_REF]. We thus obtain an action of B n on D n that induces an action on π 1 (D n ), the latter being isomorphic to the free group F n on n generators. This action, which is faithful, coincides with the action by conjugation of B n on B 1 (D n ) defined by the natural section of (M B). In this way, we recover the famous Artin representation of the braid group B n as a subgroup of the group of automorphisms of F n . Analogously, we have an action of P n as the pure mapping class group of D n on P 1 (D n ) ≃ F n what is faithful and coincides with the action by conjugation of P n on P 1 (D n ) defined by the natural section of (P B). Composing the Artin representation with the Magnus representation associated to the length function p 1 : B 1 (D n ) -→ Z (see for instance [START_REF] Bardakov | Extending representations of braid groups to the automorphism groups of free groups[END_REF]) we obtain the (non reduced) Burau representation of B n . In the case of the pure braid group, we obtain the Gassner representation of P n ( [START_REF] Bardakov | Extending representations of braid groups to the automorphism groups of free groups[END_REF]) in a similar way.

The Burau representation also has a homological interpretation (see for instance Chapter 3 of [START_REF] Kassel | Braid groups[END_REF]). Furthermore, it admits certain generalisations. Indeed, for any k ≥ 1 we may observe that B n , regarded as the mapping class group of D n , acts on F k (D n )/S k and therefore on its fundamental group, B k (D n ). The induced action of B n on B k (D n ) coincides with the action by conjugation of B n on B k (D n ) defined by the natural section of (M B). In order to look for (linear) representations, we consider regular coverings associated with normal subgroups of B k (D n ), and we try to see if the induced action on homology is well defined. In other words, we wish to study surjections of B k (D n ) onto a group G k subject to certain constraints.

When k = 1, we consider as before the length function For k > 1, let G k be the group Z 2 = q, t . The corresponding morphism p k : B k (D n ) -→ G k for k > 1 sends the classical braid generators σ 1 , . . . , σ k to q and the generators ζ 1 , . . . , ζ n , corresponding to the generators of π 1 (D n ), to t. Since the action of

p 1 : B 1 (D n ) -→ G 1 = Z = t . Since the action of B n on B 1 (D n ) commutes with p 1 : B 1 (D n ) -→ Z,
B n on B k (D n ) commutes with p k : B k (D n ) -→ G k ,
it turns out that B n acts on the regular covering of F k (D n )/S k , and the induced action on the Borel-Moore middle homology group of such a covering space is in fact the kth Bigelow-Krammer-Lawrence representation of B n . In this way, for k > 1 we obtain faithful linear representations of B n (see [START_REF] Bigelow | Homological representations of the Iwahori-Hecke algebra[END_REF] for k = 2 and [START_REF] Zheng | Faithfulness of the Lawrence representation of braid group[END_REF] for k > 2). We refer the reader to [START_REF] Kassel | Braid groups[END_REF] for a complete description of these constructions. In what follows, we first motivate the choice of the above projections p k : B k (D n ) -→ G k using the lower central series of the corresponding groups. We then explain how the study of the lower central series of surface braid groups can be used to obtain the representations given in [START_REF] An | A family of representations of braid groups on surfaces[END_REF]. We will define also the notion of extension of a representation in a completely algebraic manner, and its obstructions.

If we wish to consider surjections of B k (D n ) onto some group G ′ k , in order to obtain a linear representation using the approach described above, the group G ′ k should be Abelian. Considering the short exact sequence (M B) on the level of Abelianisation, we obtain the following commutative diagram of short exact sequences:

1 / / B k (D n ) qk / / B k,n r k,n / / B n rn / / 1 1 / / ker ψk / / B k,n /Γ 2 (B k,n ) / / B n /Γ 2 (B n ) / / 1 (2)
where r k,n and r n are Abelianisation homomorphisms, and ψk is the homomorphism satisfying ψk • r k,n = r n • ψ k . It is straightforward to show that for all k ≥ 1, ker ψk and qk coincide respectively with the group G k and the morphism p k considered in the Bigelow-Krammer-Lawrence representations.

Exact sequences for surface braid groups

We now return to the general case. Let Σ be an orientable surface. The map

F k+n (Σ)/(S k × S n ) -→ F n (Σ)/S n
given by forgetting the first k coordinates is a locally-trivial fibration whose fibre may be identified with

F k (Σ\{x 1 , . . . , x n })/S k .
As in the case of pure braid groups [START_REF] Fadell | Configuration spaces[END_REF], the long exact sequence in homotopy of this fibration yields a short exact sequence.

Lemma 3.1. Let k, n ∈ N. The Fadell-Neuwirth fibration F k+n (Σ) -→ F n (Σ)
induces the short exact sequence:

1 -→ B k (Σ \ {x 1 , . . . , x n }) -→ B k,n (Σ) -→ B n (Σ) -→ 1 , (MSB)
where we suppose that n

≥ 3 if Σ = S 2 .
In what follows we shall refer to the above short exact sequence as (MSB) (mixed surface braid groups sequence), and we denote its restriction to the corresponding pure braid groups

1 -→ P k (Σ \ {x 1 , . . . , x n }) -→ P k+n (Σ) -→ P n (Σ) -→ 1 , (SPB)
by (SPB) (surface pure braid groups sequence). If Σ is the disc D 2 , we recover the sequence considered in the previous section that gives rise to the Bigelow-Krammer Lawrence representation. In a similar manner, we may study (MSB) in order to find representations of B n (Σ).

We have the following commutative diagram involving the short exact sequences ( 1), (SPB) and (MSB):

1 1 1 (3)
where the vertical arrows between (SPB) and (MSB) are inclusions, and the second vertical sequence is obtained by restricting the exact sequence (1) for k + n strings to B k,n (Σ). The third row of symmetric groups splits as a direct product.

The following lemma summarises some of the known results for the splitting problem for the sequences (SPB) and (MSB) (we refer to [START_REF] Fadell | The braid groups of E 2 and S 2[END_REF][START_REF] Gonçalves | The braid group Bn,m(S2) and a generalisation of the Fadell-Neuwirth short exact sequence[END_REF] for the case of S 2 . Lemma 3.2. Let Σ be a compact, connected orientable surface different from S 2 .

(a) Suppose that Σ has empty boundary. Proof. (a) (i) The statement is a consequence of [START_REF] Fadell | Configuration spaces[END_REF] and the fact that T 2 admits a non-vanishing vector field. (ii) Suppose that n = 1. Then (SPB) splits using [START_REF] Gonçalves | On the structure of surface pure braid groups[END_REF] in the orientable case.

The fact that the upper right-hand vertical arrow 3) is the identity yields a section for B k,1 (Σ) -→ B 1 (Σ). (iii) For (SPB), this follows from [START_REF] Gonçalves | On the structure of surface pure braid groups[END_REF]. Next, let k = 1, suppose that (MSB) splits, and let s be a section for B 1,n (Σ) -→ B n (Σ). For m ∈ N, let τ m : B m (Σ) -→ S m denote the usual permutation homomorphism that appears in the short exact sequence (1). If x ∈ P n (Σ) then τ n (x) = 1, and so τ 1+n (s(x)) = 1 by commutativity of the diagram [START_REF] Birman | Braids, Links, and Mapping Class Groups[END_REF] and the fact that k = 1 (by abuse of notation, τ 1+n also denotes the restriction of

P 1 (Σ) -→ B 1 (Σ) of the diagram (
τ 1+n to B 1,n (Σ)). Hence s(x) ∈ P 1+n (Σ). Since P 1+n (Σ) -→ P n (Σ) is the restriction of B 1,n (Σ) -→ B n (Σ) to P 1+n (Σ)
, the restriction of s to P n (Σ) gives rise to a section for (SPB), and so we obtain a contradiction.

(b) Suppose that Σ has non-empty boundary, and let C be a boundary component of Σ. Then Σ ′ = Σ \ C is homeomorphic to a compact surface with a single point deleted. The fact that Σ and Σ ′ are homotopy equivalent implies that their configuration spaces are also homotopy equivalent, and hence the pure braid groups (resp. braid groups, mixed braid groups) of Σ are isomorphic to the corresponding pure braid groups (resp. braid groups, mixed braid groups) of Σ ′ . Applying the methods of [START_REF] Gonçalves | On the structure of surface pure braid groups[END_REF], the short exact sequences (SPB) and (MSB) split for Σ ′ , and so split for Σ.

Taking into account the above discussion concerning the existence of braid group representations via the induced action on first homology, this lemma indicates that one might use (MSB) to look for representations of surface braid groups in the case where the boundary is non empty.

Lower central series for surface braid groups

Definitions and known results

In this section we will give some results on the lower central series of (mixed) surface braid groups that will turn out useful in the next section when we come to study their representations. Given a group G, we recall that the lower central series of G is the filtration

G = Γ 1 (G) ⊇ Γ 2 (G) ⊇ • • • , where Γ i (G) = [G, Γ i-1 (G)] for i ≥ 2.
The group G is said to be perfect if G = Γ 2 (G). Following P. Hall, for a group-theoretic property P, a group G is said to be residually P if for any (non-trivial) element x in G, there exists a group H with the property P and a surjective homomorphism ϕ :

G -→ H such that ϕ(x) = 1. It is well known that a group G is residually nilpotent if and only if i≥1 Γ i (G) = {1}.
In what follows, we denote a compact, connected orientable surface with one boundary component of positive genus g by Σ g . The surface Σ g \ {x 1 , . . . , x n } will be denoted by Σ g,n . We will focus on Σ g since, according to Lemma 3.2, for these particular surfaces the sequence (MSB) splits. The following result is well known (see [START_REF] Bellingeri | Lower central series of Artin-Tits and surface braid groups[END_REF][START_REF] Gorin | Algebraic equations with continuous coefficients and some problems of the algebraic theory of braids[END_REF] for instance). Proposition 4.1. Let B n be the Artin braid group on n ≥ 3 strands. Then

Γ 1 (B n )/Γ 2 (B n ) ∼ = Z and Γ 2 (B n ) = Γ 3 (B n ).
The case of braid groups of orientable surfaces of genus at least one, is much richer (the cases of the sphere S 2 and the punctured sphere were studied in [START_REF] Gonçalves | The roots of the full twist for surface braid groups[END_REF]): related statements for Σ g may be summarised as follows (see [START_REF] Bardakov | On residual properties of pure braid groups of closed surfaces[END_REF][START_REF] Bellingeri | Lower central series of Artin-Tits and surface braid groups[END_REF][START_REF] Gorin | Algebraic equations with continuous coefficients and some problems of the algebraic theory of braids[END_REF] for similar results for the other orientable surfaces).

Theorem 4.2. ([8]) Let g ≥ 1 and n ≥ 3. Then: (a) Γ 1 (B n ( Σ g ))/Γ 2 (B n ( Σ g )) = Z 2g ⊕ Z 2 . (b) Γ 2 (B n ( Σ g ))/Γ 3 (B n ( Σ g )) = Z. (c) Γ 3 (B n ( Σ g )) = Γ 4 (B n ( Σ g )). Moreover Γ 3 (B n ( Σ g )) is perfect for n ≥ 5. (d) B n ( Σ g ) is not residually nilpotent.

Group presentations for surface braid groups and their

3-commutator groups Relations:

σ i σ j = σ j σ i if |i -j| ≥ 2 (4)
σ i σ i+1 σ i = σ i+1 σ i σ i+1 for all 1 ≤ i ≤ n -2 (5) c i σ j = σ j c i for all j ≥ 2, c i = a i or b i and i = 1, . . . , g (6)
c i σ 1 c i σ 1 = σ 1 c i σ 1 c i for c i = a i or b i and i = 1, . . . , g (7)
a i σ 1 b i = σ 1 b i σ 1 a i σ 1 for i = 1, . . . , g (8)
c i σ -1 1 c j σ 1 = σ -1 1 c j σ 1 c i for c i = a i or b i , c j = a j or b j and 1 ≤ j < i ≤ g (9)
In Figure 1 we recall a geometric interpretation of the generators of B n ( Σ g ); we represent Σ g as a polygon with 4g sides, equipped with the standard identification of edges and one boundary component. We may consider braids as paths on the polygon, which we draw with the usual 'over and under' information at the crossing points. For the braid a i (respectively b j ), the only non-trivial string is the first one, which passes through the wall α i (respectively the wall β j ). The braids σ 1 , . . . , σ n-1 are the standard braid generators of the disc. One can easily write a braid represented by a loop of the first strand around the boundary component as the composition of the generators (see for instance Section 2.2 of [START_REF] Bellingeri | On presentations of surface braid groups[END_REF]).

[a 1 , b 1 ] = • • • = [a g , b g ] = σ 2 . ( (10)
) 11
We point out that the corresponding result proved in [8, Theorem 1 ] is in fact for closed surfaces but the proof given there can be repeated verbatim to prove Lemma 4.4.

The following Corollary is a straightforward consequence of Lemma 4.4.

Corollary 4.5. Let n ≥ 3. The group B n ( Σ g ) /Γ 3 (B n ( Σ g )) is isomorphic to the semi-direct product G g = (Z × Z g ) ⋊ Z g .
More precisely, the first factor Z is central and is generated by σ, the second factor Z g is generated by {a 1 , . . . , a g }, and the third factor Z g is generated by {b 1 , . . . , b g }. Any generator b j (for 1 ≤ j ≤ g) acts trivially on a 1 , . . . , a j-1 , a j+1 and b j a j b -1

j = σ -2 a j . Hence, B n ( Σ g ) /Γ 3 (B n ( Σ g )) is a central extension of Z 2g by Z.
Thus every element of B n (Σ g )/Γ 3 (B n (Σ g )) can be written in a unique way in the form σ p g i=1 a mi i g i=1 b ni i .

Group presentations for mixed braid groups of surfaces and their 3-commutator groups

Following the standard definition of a Coxeter system, we introduce the notion of a surface braid group system.

Definition 4.6. Let G be a group.

Let S = {σ 1 , • • • , σ k-1 }, AB = {a 1 , • • • , a g , b 1 , • • • , b g } and Z = {ζ 1 , . . . , ζ n } be subsets of G such that k ≥ 1 and g, n ≥ 0.
We say that (G, S, AB, Z) is a surface braid group system if G admits the following group presentation:

σ i σ j = σ j σ i ; |i -j| ≥ 2 σ i σ i+1 σ i = σ i+1 σ i σ i+1 ; 1 ≤ i ≤ k -2 a i σ j = σ j a i and b i σ j = σ j b i ; j ∈ {2, . . . , k -1}, i ∈ {1, . . . , g} a i σ 1 a i σ 1 = σ 1 a i σ 1 a i and b i σ 1 b i σ 1 = σ 1 b i σ 1 b i i ∈ {1, . . . , g} a i σ 1 b i = σ 1 b i σ 1 a i σ 1 ; i ∈ {1, . . . , g} c i (σ -1 1 c j σ 1 ) = (σ -1 1 c j σ 1 )c i ; c i ∈ {a i , b i }, c j ∈ {a j , b j }, j < i ζ j σ i = σ i ζ j i = 1; (σ -1 1 ζ j σ 1 )a ℓ = a ℓ (σ -1 1 ζ j σ 1 ) (σ -1 1 ζ j σ 1 )b ℓ = b ℓ (σ -1 1 ζ j σ 1 ); (σ -1 1 ζ j σ 1 )ζ ℓ = ζ ℓ (σ -1 1 ζ j σ 1 ) j < ℓ; (σ 1 ζ j σ 1 )ζ j = ζ j (σ 1 ζ j σ 1 ).
The following Lemma is a straightforward consequence of the group presentations given in [START_REF] Bellingeri | On presentations of surface braid groups[END_REF].

Lemma 4.7. (i) There exist S = {σ 1 , • • • , σ n } and AB = {a 1 , • • • , a g , b 1 , • • • , b g } such that (B n ( Σ g ), S, AB, ∅) is a surface braid group system. (ii) There exist S = {σ 1 , • • • , σ k }, AB = {a 1 , • • • , a g , b 1 , • • • , b g } and Z = {ζ 1 , . . . , ζ n } such that (B k ( Σ g,n ), S, AB, Z
) is a surface braid group system.

Proposition 4.8. The group B k,n ( Σ g ) admits the following group presentation:

Generating set: S ∪ S ∪ AB ∪ AB ∪ Z with S = {σ 1 , . . . , σn-1 }, S = {σ 1 , . . . , σ k-1 }, AB = {ã 1 , b1 , . . . , ãg , bg }, AB = {a 1 , b 1 , . . . , a g , b g }, Z = {ζ 1 , • • • , ζ n }.
Relations:

(a) the relations associated with the system (B k ( Σ g,n ), S, AB, Z);

(b) the relations associated with the system (B n ( Σ g ), S, AB, ∅);

(c) the relations describing the action of B n ( Σ g ) on B k ( Σ g,n );

(i) σi σ j σ-1 i = ãi σ j ã-1 i = bi σ j b-1 i = σ j ; (ii) σi a j σ-1 i = a j ; σi b j σ-1 i = b j (iii)    σi ζ i+1 σ-1 i = ζ i ; σi ζ i σ-1 i = ζ -1 i ζ i+1 ζ i ; σi ζ j σ-1 i = ζ j , j = i, i + 1;            ãi ζ 1 ã-1 i = ζ aiζ1 1 ; bi ζ 1 b-1 i = ζ biζ1 1 ; ãi ζ j ã-1 i = ζ [a -1 i ,ζ -1 1 ] j j = 1; bi ζ j b-1 i = ζ [b -1 i ,ζ -1 1 ] j j = 1; (iv)      ãi a i ã-1 i = ζ -1 1 a i ζ 1 ; ãi a j ã-1 i = a [a -1 i ,ζ -1 1 ] j i > j; ãi a ℓ ã-1 i = a ℓ , ℓ > i;      bi b i b-1 i = ζ -1 1 b i ζ 1 ; bi b j b-1 i = b [b -1 i ,ζ -1 1 ] j i > j; bi b ℓ b-1 i = b ℓ , ℓ > i; (v)      ãi b i ã-1 i = b i ζ 1 ; ãi b j ã-1 i = b [a -1 i ,ζ -1 1 ] j i > j; ãi b ℓ ã-1 i = b ℓ , ℓ > i      bi a i b-1 i = ζ -1 1 a i [b -1 i , ζ -1 1 ]; bi a j b-1 i = a [b -1 i ,ζ -1 1 ] j i > j; bi a ℓ b-1 i = a ℓ , ℓ > i;
where a b := b -1 ab.

Proof. As we recalled in Section 2, the short exact sequence (MSB):

1 -→ B k ( Σ g,n ) -→ B k,n ( Σ g ) -→ B n ( Σ g ) -→ 1 splits. Therefore, the group B k,n ( Σ g ) is isomor- phic to B n ( Σ g ) ⋉ B k ( Σ g,n ).
We may interpret the braids depicted in Figure 2 As in the case of B n ( Σ g )/Γ 3 (B n ( Σ g )) (Corollary 4.5), we may obtain a group presentation of B k,n ( Σ g ) /Γ 3 (B k,n ( Σ g )) from the previous proposition, and decompose the group as a semi-direct product. Lemma 4.9. Let k, n ≥ 3. Then the group B k,n ( Σ g ) /Γ 3 (B k,n ( Σ g )) has the following group presentation: Generators: σ, σ, ζ, a 1 , b 1 , . . . , a g , b g , ã1 , b1 , . . . , ãg , bg . Relations:

(a) [σ, a i ] = [σ, b i ] = [σ, ãi ] = [σ, bi ] = [σ, a i ] = [σ, b i ] = [σ, ãi ] = [σ, bi ] = [σ, σ] = 1; (b) [a i , a j ] = [a i , b j ] = 1 for i = j and [a j , b j ] = σ 2 ; (c) [ã i , ãj ] = [ã i , bj ] = 1 for i = j and [ã j , bj ] = σ2 (d) [a i , ãj ] = [b i , bj ] = 1 for any pair (i, j); α r β r α r β r a r r b α r β r σ i P P i i+1 P 1 z i P 1 P P P Q 1 1 Q n Q n Q 1 Q n Q 1 P k k Q 1 Q n Q i k Figure 2: The generators σ 1 , . . . , σ k-1 , a 1 , b 1 , . . . , a g , b g , ζ 1 , • • • , ζ n (e) [b i , ãj ] = [ bj , a i ] = 1 for i = j and [b i , ãi ] = [ bi , a i ] = ζ; (f ) [ζ, a i ] = [ζ, b i ] = [ζ, ãi ] = [ζ, bi ] = [ζ, σ] = [ζ, σ] = 1.
Proof. Consider the group presentation of B k,n ( Σ g ) given in Proposition 4.8 and the map p : B k,n ( Σ g ) -→ B k,n ( Σ g ) /Γ 3 (B k,n ( Σ g )). It follows from the braid relations σ i σ i+1 σ i = σ i+1 σ i σ i+1 and σi σi+1 σi = σi+1 σi σi+1 that σ i = σ i+1 [σ i , σ i+1 ] and σi = σi+1 [σ i , σi+1 ]. But [σ i , σi+1 ] and [σ i , σ i+1 ] belong to Γ 2 (B k,n ( Σ g )). Their images under p therefore belong to the centre of B k,n ( Σ g ) /Γ 3 (B k,n ( Σ g )). Since p(σ i ) and p(σ i+1 ) are center elements, the equality p(σ i σ i+1 σ i ) = p(σ i+1 σ i σ i+1 ) implies that p(σ i ) = p(σ i+1 ). We denote the image of σ i under p by σ. Similarly, the σj have the same image under p, which we denote by σ in what follows. By abuse of notation, we also denote p(a i ), p(b i ), p(ã i ) and p( bi ) by a i , b i , ãi and bi respectively. Using the fact that σ i a j = a j σ i for i = j, we obtain σa j = a j σ for all j. Similarly, we have σb j = b j σ, σã j = ãj σ, σb j = bj σ and σp(ζ j ) = p(ζ j )σ. We deduce from relations a i (σ -1 1 a j σ 1 ) = (σ -1 1 a j σ 1 )a i for i = j that a i a j = a j a i . Similarly we have a i b j = b j a i , ãi ãj = ãj ãi and bi ãj = ãj bi for i = j. For the same reason, we have ãi p(ζ j ) = p(ζ j )ã i and bi p(ζ j ) = p(ζ j ) bi . Now, from the equality a j σb j = σb j σa j σ, we deduce the relation [a j , b j ] = σ 2 . Similarly we have [ã j , bj ] = σ2 . From Relations (i) and (ii) of the presentation of

B k,n ( Σ g ), we have [σ, a i ] = [σ, b i ] = [σ, ãi ] = [σ, bi ] = [σ, σ] = 1. From Relations (iii) we see that σp(ζ i+1 )σ -1 = ζ i = σ j ζ i σ -1 j with j = i, i + 1.
Then, all the ζ i have the same image under p, which we denote by ζ.

Then [ζ, ãi ] = [ζ, bi ] = [ζ, σ] = [ζ, σ] = 1. Still using Relations (iii), we have [ζ, a i ] = [ζ, b i ] = 1. From Relations (iv) we α r β r α r β r a r r b α r β r σ Q 1 Q n Q 1 Q n Q 1 j Q j Q j+1 Q n P 1 P 1 P k P k
Figure 3: The generators σ1 , . . . , σn-1 , ã1 , b1 , . . . , ãg , bg

P 1 Q 1 α r β r β r α r Q 1 Q n P 1 P k Q 1 P 1
k,n ( Σ g ) /Γ 3 (B k,n ( Σ g )) if one takes σ = p(σ 1 ), σ = p(σ 1 ), ζ = p(ζ 1 ), a i = p(a i ), b i = p(b i ), ãi = p(ã i ) and bi = p( bi ).
Conversely, let G be the group defined by the presentation given in the lemma. We may check without difficulty that we have a group homomorphism from

B k,n ( Σ g ) to G that sends σ i , σj , a i ′ , b i ′′ , ãj ′ , ãj ′′ and ζ ℓ to σ, σ, a i ′ , b i ′′ , ãj ′ , ãj ′′ and ζ respectively. In order to prove that G is isomorphic to B k,n ( Σ g ) /Γ 3 (B k,n ( Σ g )),
B k,n ( Σ g ) Γ 3 (B k,n ( Σ g ))
is isomorphic to the semi-direct product:

H g := Z 3 × Z 2g ⋊ Z 2g .
More precisely, the first factor Z 3 is central and is generated by σ, σ, ζ, the second factor Z 2g is generated by {a 1 , . . . , a g , ã1 . . . , ãg }, and the third factor Z 2g is generated by {b 1 , . . . , b g , b1 . . . , bg }.

The actions defining the above semi-direct product are as described in Lemma 4.9.

Then B k,n ( Σ g ) /Γ 3 (B k,n ( Σ g )) can be seen as a central extension of Z 4g by Z 3 . We remark that the action of any generator on the previous ones is trivial except in at most two cases: for instance the only non-trivial actions of ãj are ãj bj ã-1 j = σ2b j and ãj b j ã-1

j = ζ -2 b j .
Finally, notice that every element w of B k,n ( Σ g ) /Γ 3 (B k,n ( Σ g )) may be written in a unique way in the form w =

σ p σq ζ r g i=1 a mi i ãMi i g i=1 b ni i bNi i .

Mixed surface braid sequences and representations of surface braid groups

As in previous sections, we will focus on connected orientable surfaces of positive genus with a single boundary component. One might ask whether it is possible to use the short exact sequence (M SB) to obtain representations of B n ( Σ g ) which are extensions of Bigelow-Krammer-Lawrence representations of B n . First, let us denote by ι n :

B n -→ B n ( Σ g ) and ι k,n : B k (D n ) -→ B k ( Σ g,n
) the homomorphisms induced by the inclusion of D 2 into Σ g and of D n into Σ g,n respectively. We recall that they are injective (see for instance [START_REF] Paris | Geometric subgroups of surface braid groups[END_REF]).

Remark 5.1. In particular B k (D n ) is generated as a subgroup of B k ( Σ g,n ) by σ 1 , . . . , σ k-1 and ζ 1 , . . . , ζ n (see for instance [START_REF] Bardakov | Representations of Artin-Tits and surface braid groups[END_REF][START_REF] Bellingeri | On presentations of surface braid groups[END_REF]).

Given β ∈ B n , we denote the induced action by conjugation of β on B k (D n ), and abusing notation, the action of β (regarded as an element of B n ( Σ g )) on B k ( Σ g,n ), by β * . As in Section 2, for the case k = 1 we consider the length function

p 1 : B 1 (D n ) -→ G 1 = Z = , while for k > 1 we set G k to be the group Z 2 = q, t . The corresponding homomorphism p k : B k (D n ) -→ G k for k > 1 sends σ 1 , .
. . , σ k to q and ζ 1 , . . . , ζ n to t. As we mentioned in Section 2, the fact that the action of

B n on B k (D n ) commutes with p k : B k (D n ) -→ G k implies that B n
acts on a regular covering. For k = 1 the induced action on homology gives rise to the Burau representation, while for k > 1 we obtain faithful linear representations of B n . Definition 5.2. Let P k : B k ( Σ g,n ) -→ G k ( Σ g ) be a surjective homomorphism. We will say that the homomorphism P k is a lifting extension of the map p k : B k (D n ) -→ G k defined above if there exists an injective homomorphism ῑk :

G k -→ G k ( Σ g ) such that P k • ι k,n = ῑk • p k , and if further for all β ∈ B n ( Σ g ) there exists a homomorphism β * : G k ( Σ g ) -→ G k ( Σ g ) such that β * • P k = P k • β * .
The second condition means that there is an induced action of B n ( Σ g ) on the homology of the covering space of F k ( Σ g,n )/S k . In other words, the surjection P k is a lifting extension of p k if the following diagram commutes for any β ∈ B n :

G k Id ῑk / / G k ( Σ g ) β * B k (D n ) p k b b b b E E E E E E E E E / / β * B k ( Σ g,n ) P k 9 9 9 9 t t t t t t t t t β * B k (D n ) p k | | | | y y y y y y y y y / / B k ( Σ g,n ) P k % % % % J J J J J J J J J G k ῑk / / G k ( Σ g ) (12)
We remark that the middle homology group

H BM k   F k ( Σ g,n ) S k   of the covering space F k ( Σ g,n ) S k of F k ( Σ g,n ) S k is a free Z[G k ( Σ g )]-module (see Lemma 3.3 of [1]) and that some β ∈ B n ( Σ g ) acts as a Z[G k ( Σ g )]-module morphism of H BM k ( F k ( Σ g,n )/S k ) if and only if the map β * : G k ( Σ g ) -→ G k ( Σ g )
defined above is the identity homomorphism (see Section 2 of [START_REF] An | A family of representations of braid groups on surfaces[END_REF]). If this property holds for all β ∈ B n ( Σ g ) we thus obtain a representation of

B n ( Σ g ) in Aut Z[G k ( Σg )] (H BM k   F k ( Σ g,n ) S k   ) which is a linear representation if G k ( Σ g ) is Abelian.
The above discussion gives rise naturally to the following definition, which provides a notion of extension of the Bigelow-Krammer-Lawrence representations from B n to B n ( Σ g ).

Definition 5.3. Let P k : B k ( Σ g,n ) -→ G k ( Σ g ) be a lifting extension of the ho- momorphism p k : B k (D n ) -→ G k .
The homomorphism P k is said to be a linear extension of p k if for any β ∈ B n ( Σ g ), we have that β * = Id and that G k ( Σ g ) is Abelian.

The following proposition states that it is not in fact possible to extend the Bigelow-Krammer-Lawrence representations from B n to B n ( Σ g ).

K g is isomorphic to B n ( Σ g )/Γ 3 (B n ( Σ g )), and therefore K g coincides with ker ψk . To prove the proposition, it is therefore sufficient to check that the given set of relations is a complete set of relations for K g . Let D g be the (abstract) group with the group presentation given in the statement. Let j : D g -→ K g be the (surjective) homomorphism sending every generator of D g to the corresponding generator of K g , and let ι : K g -→ B k,n ( Σ g )/Γ 3 (B k,n ( Σ g )) be the (injective) homomorphism given in diagram [START_REF] Blanchet | Non commutative representations of Torelli groups[END_REF]. We claim that the composition k = ι • j is injective, and therefore D g coincides with K g . In fact, it follows from the group presentation of D g that any element w ∈ D g can be written (in a unique way) as w = σ p ζ q g j=1 a mj j g j=1 b nj j . We call this decomposition of w its normal form in D g . On the other hand, any element w ′ ∈ B k,n ( Σ g )/Γ 3 (B k,n ( Σ g )) may be written uniquely as w ′ = σ p ζ q σr g j=1 (a mj j ãMj j ) g j=1 (b nj j bNj j ). We call this decomposition of w ′ its normal form in B k,n ( Σ g )/Γ 3 (B k,n ( Σ g )). Let w ∈ D g be written in its normal form. From the definition of k :

D g -→ B k,n ( Σ g )/Γ 3 (B k,n ( Σ g )), k(w) coincides with its normal form in B k,n ( Σ g )/Γ 3 (B k,n ( Σ g )). Therefore k(w) = 1 implies that w = 1.
Remark 5.6. Let k ≥ 3. Then the group ker ψk is the group

G Σ introduced in [1, Section 3]. The homomorphism P k : B k ( Σ g,n ) -→ ker ψk is the homomorphism Φ Σ : B k ( Σ g,n ) -→ G Σ also defined in [1, Section 3].
The homomorphism Φ Σ : B k ( Σ g,n ) -→ G Σ and the group G Σ defined in Section 3 of [START_REF] An | A family of representations of braid groups on surfaces[END_REF] were constructed in a technical manner in order to obtain (non-linear) representations of surface braid groups subject to certain homological constraints (Definition 2.2 of [START_REF] An | A family of representations of braid groups on surfaces[END_REF]). Proposition 5.5 and Remark 5.6 show that such technical constructions coincide with objects arising in the lower central series. On the other hand, reinterpreting Lemma 3.1 and Theorem 4.3 of [START_REF] An | A family of representations of braid groups on surfaces[END_REF], we conclude that the unique lifting extension of p k : B k (D n ) to B k ( Σ g,n ) arises from the lower central series and the homomorphism P k : B k ( Σ g,n ) -→ ker ψk , as we shall now explain in the following two propositions. Proposition 5.7. Let k ≥ 3, and let ψk : B k ( Σ g,n ) -→ ker ψk be the homomorphism defined above. The homomorphism ψk lifts to an action on the level of regular coverings.

Proof. We recall that there is an induced action of B n ( Σ g ) on the homology of the covering space of

F k ( Σ g,n )/S k β ∈ B n ( Σ g ) if there exists a homomorphism β * : G k ( Σ g ) -→ G k ( Σ g ) such that β * • ψk = ψk • β * .
As we remarked previously, we may replace the homomorphism P k : B k ( Σ g,n ) -→ ker ψk and the group ker ψk respectively by the homomorphism Φ Σ : B k ( Σ g,n ) -→ G Σ and the group G Σ given in Section 3 of [START_REF] An | A family of representations of braid groups on surfaces[END_REF]. The statement follows from Lemma 3.1 of [START_REF] An | A family of representations of braid groups on surfaces[END_REF].

Proposition 5.8. Let k ≥ 3. (i) The homomorphism ψk : B k ( Σ g,n ) -→ ker ψk is a lifting extension of p k : B k (D n ) -→ G k ; (ii) let P k : B k ( Σ g,n ) -→ G k ( Σ g ) be a lifting extension of p k : B k (D n ) -→ G k .
There is a canonical isomorphism ι : G k ( Σ g ) -→ ker ψk such that ι•P k sends any generator of B k ( Σ g,n ) to the corresponding coset of B k,n ( Σ g )/Γ 3 (B k,n ( Σ g )).

Proof. (i) In order to prove that ψk :

B k ( Σ g,n ) -→ ker ψk is a lifting extension of p k : B k (D n ) -→ G k , it suffices to show that ψk (B k (D n )) is isomorphic to Z 2 in
ker ψk . This is immediate because ψk (σ j ) = σ for any j = 1, . . . , k -1, and ψk (ζ l ) = ζ for any l = 1, . . . , n. The claim then follows from Remark 5.1

(ii) Let P k : B k ( Σ g,n ) -→ G k ( Σ g ) be a lifting extension of p k : B k (D n ) -→ G k .
Therefore P k (σ j ) = q for all j = 1, . . . , k -1, and P k (ζ l ) = t for all l = 1, . . . , n, where q, t ∈ G k ( Σ g ) generate a central subgroup isomorphic to Z 2 . One can check easily that these conditions imply that:

• the images of a 1 , b 1 , . . . , a g , b g commute with q and t;

• [P k (a i ), P k (b j )] = 1 for i = j;

• [P k (a i ), P k (b i )] = q 2 .
We can therefore define a surjection pk : ker ψk -→ G k ( Σ g ) such that pk (σ) = q, pk (ζ) = t and pk (a i ) = P k (a i ), pk (b i ) = P k (b i ).

We will prove that pk is actually an isomorphism. Let w ∈ ker ψk ,and consider 1 ≤ r ≤ g. By Proposition 5.5, we observe that for every generator x of the presentation, we have a We obtain pk (σ -2nr ) = q -2nr = 1 and pk (σ -2mr ) = q -2mr = 1, and thus m r = n r = 0. Since this is so for all r, we have w = σ c ζ d and pk (w) = q c t d = 1. Since q, t generate a subgroup that is isomorphic to Z 2 , we get c = d = 0 and w = 1. Hence pk is injective.

The cases k = 1, 2 are still open, mainly because we do not have a finite group presentation for ker ψk and B k,n ( Σ g )/Γ 3 (B k,n ( Σ g )) in these cases. As in Proposition 5.8, there is a natural surjection from ker ψk onto the group G Σ considered in Section 3 of [START_REF] An | A family of representations of braid groups on surfaces[END_REF], but it is not an isomorphism. Remark 5.9. Notice that in the proof of Proposition 5.8, we proved a slightly stronger result, i.e. that if H k is a group for which there exists a surjection h k : B k ( Σ g,n ) -→ H k satisfying h k (σ j ) = q for all j = 1, . . . , k -1 and h k (ζ l ) = t for all l = 1, . . . , n , where the subgroup q, t of H k is torsion free, then the group H k coincides with ker ψk . Using Lemma 4.9 and Theorem 4.3, one may easily adapt the proof of Proposition 5.8 in order to obtain the following result: Proposition 5.10. Let k, n ≥ 3.

(i) Let H be a group, and let λ Σg : B n ( Σ g ) -→ H be a surjective homomorphism such that λ Σg (B n ) is isomorphic to Z. Then there is an isomorphism ι :

H -→ B n ( Σ g )/Γ 3 (B n ( Σ g )) for which ι•λ Σg sends every generator of B n ( Σ g )
to the corresponding class of B n ( Σ g )/Γ 3 (B n ( Σ g )).

(ii) Let H be a group. Assume that h : B k,n ( Σ g ) -→ H is a surjective homomorphism such that the image of the subgroup generated by σ

1 , . . . , σ k-1 , σ1 , • • • , σn-1 is isomorphic to Z 2 .
Then there is an isomorphism ι :

H -→ B k,n ( Σ g ) Γ 3 (B k,n ( Σ g )) for which ι • h sends any generator of B k,n ( Σ g ) to the corresponding coset of B k,n ( Σ g ) Γ 3 (B k,n ( Σ g ) .
The above proposition is of additional interest in the study of the lower central series of surface braid groups, since it states that the only possible extension of the length function from

B n to B n (( Σ g ) is the canonical projection of B n ( Σ g ) onto B n ( Σ g )/Γ 3 (B n ( Σ g )).
It is interesting to remark that in the case of closed surfaces, we have the following result: Proposition 5.11. Let n ≥ 3 and let Σ be an orientable surface of positive genus. It is not possible to extend the length function λ : B n -→ Z to B n (Σ). In other words there is no surjection λ Σ of B n (Σ) onto a group F such that the restriction of λ Σ to B n coincides with λ.

Proof. Let λ Σ : B n (Σ) -→ F be such that λ Σ (σ 1 ) = . . . λ Σ (σ n-1 ). Set λ Σ (σ 1 ) = σ. Using the group presentation of B n (Σ) given in [START_REF] Bellingeri | On presentations of surface braid groups[END_REF], we see that σ 2(n+g-1) = 1. For further details, we refer the reader to the calculation of the group presentation of B n (Σ)/Γ 3 (B n (Σ) given in the proof of Theorem 1 in [START_REF] Bellingeri | Lower central series of Artin-Tits and surface braid groups[END_REF].

Appendix on exact sequences

Let us recall that the short exact sequences (M BS) and (P BS) also exist if Σ is a non-orientable surface. If n ≥ 2 and k ≥ 2 then the splitting of (MSB) for compact surfaces without boundary (also possibly non-orientable) is an open question. As the following example shows, the splitting of one of the two short exact sequences (SPB) and (MSB) does not imply in general that the other sequence splits.

= σ -1 3 σ -1 2 σ -1
1 ρ 1 (which is of order 16 by [START_REF] Gonçalves | The braid groups of the projective plane[END_REF]) and let ∆ 4 = σ 1 σ 2 σ 3 σ 1 σ 2 σ 1 denote the 'half-twist' braid (which is of order 4 by [START_REF] Van Buskirk | Braid groups of compact 2-manifolds with elements of finite order[END_REF]). Then [27, Proposition 15(a)] and standard properties of dicyclic groups imply that the subgroup H of B 4 (RP 2 ) generated by a 2 and a∆ 4 is isomorphic to the generalised quaternion group Q 16 of order 16. Let τ 4 : B 4 (RP 2 ) -→ S 4 denote the usual permutation homomorphism. A straightforward calculation shows that τ 4 (H) = (1, 3), [START_REF] Bardakov | Extending representations of braid groups to the automorphism groups of free groups[END_REF][START_REF] Bardakov | Representations of Artin-Tits and surface braid groups[END_REF] , which is isomorphic to S 2 × S 2 . Taking B 2,2 (RP 2 ) to be τ -1 4 ( (1, 3), [START_REF] Bardakov | Extending representations of braid groups to the automorphism groups of free groups[END_REF][START_REF] Bardakov | Representations of Artin-Tits and surface braid groups[END_REF] ), the restriction to H of the projection p : B 2,2 (RP 2 ) -→ B 2 (RP 2 ) given geometrically by forgetting the second and fourth strings is an isomorphism. This follows since ker(p) is torsion free and B 2 (RP 2 ) ∼ = Q 16 [START_REF] Van Buskirk | Braid groups of compact 2-manifolds with elements of finite order[END_REF]. In particular, p admits a section. So in this case, (MSB) splits, but (SPB) does not.

(b) Let Σ = S 2 . For all n ≥ 3 and all k ∈ N, (SPB) splits [START_REF] Fadell | Homotopy groups of configuration spaces and the string problem of Dirac[END_REF]. The question of the splitting of (MSB) is examined in [START_REF] Gonçalves | The braid group Bn,m(S2) and a generalisation of the Fadell-Neuwirth short exact sequence[END_REF]. For example, if n = 3 and k ≡ 1 mod 3, or if n ≥ 4 and k ≡ ε 1 (n-1)(n-2)-ε 2 n(n-2) mod n(n-1)(n-2), where ε 1 , ε 2 ∈ {0, 1}, then (MSB) does not split. So for these values of k and n, (SPB) splits, but (MSB) does not.

Let us finish this appendix by pointing out another interesting feature when we pass from short exact sequences of classical braid groups to short exact sequences of surface braid groups. The sequence (P B) (in the case k = 1) has the property that the induced action of the quotient on the Abelianisation of the kernel is trivial. Following [START_REF] Falk | The lower central series of a fiber-type arrangement[END_REF], we will call such a splitting extension an almost-direct product. The important remark for us in Theorem 3.1 of [START_REF] Falk | The lower central series of a fiber-type arrangement[END_REF] is that such an exact sequences induces exact sequences on the level of the lower central series quotients (see also [START_REF] González-Meneses | Vassiliev invariants for braids on surfaces[END_REF][START_REF] Papadima | The universal finite-type invariant for braids, with integer coefficients[END_REF]). Since P n is an iterated almost-direct product of free groups, P n 'inherits' various properties of F n , and it is possible to use this structure to derive a presentation for the Lie algebra associated to the lower central series of P n and to construct a universal finite type invariant for braid groups [START_REF] Papadima | The universal finite-type invariant for braids, with integer coefficients[END_REF]. On the other hand, the fact that P n acts trivially on the Abelianisation of F n allows us to compose the Artin representation with the Magnus representation, thus yielding the Gassner representation (we refer to [START_REF] Bardakov | Extending representations of braid groups to the automorphism groups of free groups[END_REF] for the details). Proposition 6.2. Let Σ be an orientable surface different from S 2 and T 2 . The sequence:

1

/ / P k (Σ \ {x 1 , . . . , x n }) / / P k+n (Σ) / / P n (Σ) / / 1 defines an almost-direct product structure for P k+n (Σ) if and only if n = 1.

Proof. The case n = 1 was proved in [START_REF] Bardakov | On residual properties of pure braid groups of closed surfaces[END_REF]. If n ≥ 2, as we recalled in Section 3, the sequence (P BS) splits only if Σ has boundary (Lemma 3.2). However, even when the sequence (P BS) splits, the extension is never an almost-direct product.

In fact, a straightforward calculation on the level of group presentations (given for instance in [START_REF] Bellingeri | On presentations of surface braid groups[END_REF][START_REF] Bellingeri | Lower central series of Artin-Tits and surface braid groups[END_REF]) shows that the natural section (corresponding to adding a strand 'at infinity') does not define a trivial action on the level of Abelianisation (see also relation (v ) of Proposition 4.8). The statement then follows from the following proposition, which shows that the existence of an almost-direct product structure is independent of the choice of section.

Proposition 6.3. Let 1 -→ K -→ G p -→ Q -→ 1 be a split extension of groups. Let s, s ′ be sections for p, and suppose that the induced action of Q on K via s on the Abelianisation K Ab = K/[K, K] is trivial. Then the same is true for the section s ′ .

Proof. Let k ∈ K and q ∈ Q. By hypothesis, s(q) k (s(q)) -1 ≡ k mod [K, K]. Let s ′ be another section for p. Then p • s ′ (q) = p • s(q), and so s ′ (q) (s(q)) -1 ∈ ker p. Thus there exists k ′ ∈ K such that s ′ (q) = k ′ s(q), and hence s ′ (q) k (s ′ (q)) -1 ≡ k ′ s(q) k (s(q)) -1 k ′-1 ≡ k ′ kk ′-1 ≡ k mod [K, K].

Thus the induced action of Q on K Ab via s ′ is also trivial.

  B n acts on the regular covering D n of D n . The induced action on the first homology group of D n is the (reduced) Burau representation of B n .

  (i) If Σ is the 2-torus T 2 then (SPB) splits for all k, n ∈ N. (ii) If n = 1 then both (SPB) and (MSB) split for all k ∈ N. (iii) Let n ≥ 2 and k ∈ N. If Σ = T 2 , then (SPB) does not split. If further k = 1 then (MSB) does not split. (b) If Σ has non-empty boundary then (SPB) and (MSB) split for all k, n ∈ N.

Theorem 4 . 3 .

 43 ([8]) Let n ≥ 1. The group B n ( Σ g ) admits the following group presentation: Generators: a 1 , b 1 , . . . , a g , b g , σ 1 , . . . , σ n-1 .

Figure 1 :

 1 Figure 1: The generators σ 1 , . . . , σ k-1 , a 1 , b 1 , . . . , a g , b g From Theorem 4.3 one may deduce the following result.

Lemma 4 . 4 .

 44 ([8]) Let n ≥ 3. The quotient group B n ( Σ g ) /Γ 3 (B n ( Σ g )) admits the following group presentation: Generators: a 1 , b 1 , . . . , a g , b g , σ. Relations: a 1 , b 1 , . . . , a g , b g and σ commute pairwise except (a i , b i ) i=1,...,g ;

  as geometric representatives of generators of B k ( Σ g,n ), and those depicted in Figure 3 as the coset representatives of generators of B n ( Σ g ) in B n ( Σ g ). The result follows by a straightforward verification of the corresponding geometric braids, see for instance Figure 4.

Figure 4 : 1 i and b i ζ 1

 411 Figure 4: The braids ãi b i ã-1 i and b i ζ 1 are isotopic.

Corollary 4 . 10 .

 410 we need to prove that in G, the equality [a, [b, c]] = 1 holds for all a, b, c in G. Using the equality [a, bc] = [a, b]b[a, c]b -1 , it is enough to consider the case where a, b and c are defining generators of G. But in these particular cases, the equality clearly holds since σ, σ and ζ belong to the centre of G, and therefore any commutator [x, y], where x, y are defining generators, is in the centre of G. Thus G and B k,n ( Σ g ) /Γ 3 (B k,n ( Σ g )) are isomorphic. Let k, n ≥ 3. The group

  r x = xa r except for x = b r , in which case we have a r b r = σ 2 b r a r . Therefore, if the normal form of w is σ c ζ d g j=1 b nj j a mj j , then a r w = σ 2nr wa r and [w, a r ] = σ -2nr . Similarly, [w, b r ] = σ 2mr . Now if pk (w) = 1 then pk ([w, a r ]) = pk ([w, b r ]) = 1.

Example 6 . 1 .

 61 (a) Let Σ = RP 2 and n = k = 2. First note that the pure braid sequence (SPB) does not split by [24, Theorem 3]. Secondly, using Van Buskirk's presentation of B n (RP 2 ) [35] in the case n = 4, let a

Acknowledgements

The authors were partially supported by the ANR project TheoGar 'Théorie de Garside' n o ANR-08-BLAN-0269-02.

Proposition 5.4. There is no homomorphism

Proof. This result is a reformulation of Lemma 2.6 of [START_REF] An | A family of representations of braid groups on surfaces[END_REF]. We sketch the proof. The action by conjugation of B n ( Σ g ) on B k ( Σ g,n ) is described in Proposition 4.8, where B k ( Σ g,n ) is the subgroup of B k,n ( Σ g ) generated by S, AB and Z. For any generator g, let us denote its image in G k ( Σ g ) by [g], and we consider bj as a generator of B n ( Σ g ). Since P k is a lifting extension of p k , the action of bj by conjugation induces the homomorphism ( bj

. Since P k is also a linear extension, ( bj ) * must coincide with the identity. One deduces that [ζ 1 ] = 1, but this cannot be true since the hypothesis that P k is a lifting extension of p k implies that

In what follows we show that for k ≥ 3, there is a unique group G k ( Σ g ) such that one may define a lifting extension

We first characterise the group G k ( Σ g ) which was defined in Section 3.1 of [START_REF] An | A family of representations of braid groups on surfaces[END_REF] (with the notation G Σ ) in terms of lower central series. We then show that this group is the unique group admitting a lifting extension for p k , and we construct the corresponding homomorphism

Consider the following diagram:

) where, by abuse of notation, r k,n and r n denote the canonical projections and ψk is the map such that ψk • r k,n = r n • ψ k . Following Lemma 4.9, we denote the generators of B k,n ( Σ g )/Γ 3 (B k,n ( Σ g )) by σ, σ, ζ, a 1 , b 1 , . . . , a g , b g , ã1 , b1 , . . . , ãg , bg .

Proposition 5.5. The group ker ψk admits the following presentation: [START_REF] Blanchet | Non commutative representations of Torelli groups[END_REF], one deduces that the group K g belongs to ker ψk . By Lemma 4.9, the group K g is normal in B k,n ( Σ g )/Γ 3 (B k,n ( Σ g )).

A straightforward calculation shows that the quotient B k,n ( Σ g )/Γ 3 (B k,n ( Σ g )) by