LemmaStatement: AI-adaptedProof: AI-generated

How statement and proof provenance work

The first chip identifies the source of the statement or construction; the second identifies the source of its local proof or verification.

Literature-sourced: the exact statement appears in a cited source; only wording and notation differ.
AI-adapted: a semantically identical restatement of literature-sourced material, modulo indexing, notation, and boundary cases adopted by the library.
AI-generated: a genuinely novel statement formulated by AI, with no source for the claim itself.

These labels describe origin, not correctness: citations and verification chips remain separate evidence.

Intermediate exact sequences and deck morphism in Theorem 6.7

PDF p. 26: (6.9)–(6.11), source proof

Statement

Assume the Axiom of Choice. Let $(W, S)$ be a finite-rank spherical Coxeter system, so $W$ is finite, and let $J \subseteq S$ . Let $A$ be its Artin–Tits group, $π : A \to W$ the standard projection, and $W_{J}, A_{J}$ the standard parabolic subgroups generated by $J$ . Put $N = N (W, J) = {Norm}_{W} (W_{J}) / W_{J}$ and $N (A, J) = {Norm}_{A} (A_{J}) / A_{J}$ . Let $D$ be the relative arrangement groupoid, $R$ the reduced ribbon groupoid, $G : D \to R$ the crossing-to-ribbon functor and $Q : D \to D / N$ the orbit functor. A vertex group is the group of arrows from a specified object to itself. Write $d = (e, J)$ , $D_{J} = D_{d}$ and $R_{J}$ for the vertex group of $R$ at $J$ .

Let $X$ be the relative complexified arrangement complement, $p : D \to Π_{1} (X)$ the equivariant equivalence, $x = p (d)$ and $\overset{ˉ}{x}$ the image of $x$ in $X / N$ . With first-path-first products and ordinary composition of deck transformations, the exact sequence $1 \to D_{J} \overset{Q}{\to} (D / N)_{Q d} \to N \to 1$ is isomorphic, with identity on $N$ , to the topological covering sequence $1 \to π_{1} (X, x) \to π_{1} (X / N, \overset{ˉ}{x}) \to N \to 1$ . It is also isomorphic, with identity on $D_{J}$ and $N$ , to $1 \to D_{J} \overset{G}{\to} R_{J} \overset{ψ}{\to} N \to 1$ .

For $μ \in R_{J}$ , its unique $G$ -lift from $d$ ends at $(π (μ), J)$ ; in particular $π (μ)$ is the minimum-length representative of its right $W_{J}$ -coset and $ψ (μ) = π (μ) W_{J}$ . Under the isomorphism $R_{J} ≅ N (A, J)$ induced by quotienting by $A_{J}$ , $ψ$ agrees with the map $\overline{π} : N (A, J) \to N$ induced by $π$ .

More explicitly, let $q_{J} : R_{J} \to N (A, J)$ be the quotient isomorphism, let $G^{'} : D / N \to R$ be the isomorphism with $G = G^{'} Q$ , and let $\overset{ˉ}{p} : D / N \to Π_{1} (X / N)$ be induced by $p$ . Write $p_{d}$ , ${\overset{ˉ}{p}}_{Q d}$ and $G_{Q d}^{'}$ for the induced vertex-group maps. The comparison from the $Q$ -sequence to the topological sequence has components $(p_{d}, {\overset{ˉ}{p}}_{Q d}, {i d}_{N})$ ; the comparison from the $Q$ -sequence to the ribbon sequence has components $({i d}_{D_{J}}, G_{Q d}^{'}, {i d}_{N})$ . Consequently the resulting algebraic-to-topological comparison has middle map $Φ = {\overset{ˉ}{p}}_{Q d} \circ (G_{Q d}^{'})^{- 1} \circ q_{J}^{- 1} : N (A, J) \to π_{1} (X / N, \overset{ˉ}{x})$ .

Statement references

The Axiom of Choice

Coxeter-system, roots, length and weak-order conventions

Artin–Tits group, pure subgroup and positive lifts

Assignment from wall crossings to ribbon generators

Equivariant equivalence with fundamental groupoids

Relative free action, normal cover and exact sequence

Normal Deligne–ribbon cover and its deck group

Spherical Artin normaliser splitting

Normaliser quotient exact sequence

Morphisms of group extensions

Equivalence of group extensions with fixed kernel and fixed quotient

Facts & Assumptions

[F1]

$π : A \to W$ is a group homomorphism. The groupoid $D$ has chamber labels $(y, I)$ as objects. A simple crossing of index $a$ sends $(y, I)$ to $(y v_{a, I}, K)$ , and $G$ sends it to the elementary ribbon $μ_{a, I}$ from $I$ to $K$ . The groupoid is generated by these crossings and their inverses; $π (μ_{a, I}) = v_{a, I}$ . Assignment from wall crossings to ribbon generators Simple wall-crossing elements and maps Ribbon generators lift wall-crossing morphisms Artin–Tits group, pure subgroup and positive lifts

[F2]

The functor $G$ factors as $G^{'} Q$ , where $G^{'} : D / N \to R$ is an isomorphism; $Q$ and $G$ are normal coverings with deck group identified with $N$ through its action on $D$ . Normal Deligne–ribbon cover and its deck group

[F3]

A normal covering of connected groupoids gives an exact vertex-group sequence whose last map sends a loop to the deck transformation carrying the chosen source to the endpoint of its unique lift. Vertex-group exact sequence of a normal groupoid cover

[F4]

Under the Axiom of Choice, the equivariant equivalence $p$ induces an equivalence $\overset{ˉ}{p} : D / N \to Π_{1} (X / N)$ with $\overset{ˉ}{p} Q = q_{*} p$ , where $q : X \to X / N$ is the orbit map. The $N$ -action on $X$ is free and has the disjoint-neighbourhood property; $q$ is a normal covering and gives the topological exact sequence in the Statement. With first-path-first products, its last map sends a loop to the unique element of $N$ carrying its lift's initial point to its endpoint. Equivariant equivalence with fundamental groupoids Relative free action, normal cover and exact sequence Choice is used in that supplier to choose connecting paths for all objects when constructing quasi-inverses; no further choice is used in the vertex-group comparison below. The Axiom of Choice

[F5]

For $g \in {Norm}_{W} (W_{J})$ , its class acts on $(e, J)$ as $(y, J)$ , where $y$ is the minimum-length element of $g W_{J}$ . This action on chamber labels is free. Normaliser action on labels, orbits and adjacency

[F6]

The quotient map restricts to an isomorphism $R_{J} \to N (A, J)$ , and $π$ induces $\overline{π} : N (A, J) \to N$ . Spherical Artin normaliser splitting Normaliser quotient exact sequence

[F7]

A morphism of extensions is a commutative diagram of the three group homomorphisms; an equivalence with fixed end groups has isomorphisms on the middle groups and identity maps on those end groups. Morphisms of group extensions Equivalence of group extensions with fixed kernel and fixed quotient

[F8]

Any two relative chambers are joined by a finite sequence of simple wall crossings. Finite wall-crossing connectivity

Proof

Given: The spherical Coxeter system, subset $J$ , constructions and basepoints in the Statement, with the Axiom of Choice.

Proof technique: direct.

Goal: Compare the three exact sequences and calculate the ribbon deck map.

1.1F1F2F3F7F8given

The chamber label $d = (e, J)$ exists, so $D$ is nonempty. By [F1] and [F8], any two objects are joined by an arrow, so $D$ is connected. It is small because its chamber labels form a set and its arrows are equivalence classes of finite words in the generating crossings and their inverses. The orbit functor $Q$ is surjective on objects, hence its target is also nonempty and connected; the isomorphism $G^{'}$ in [F2] gives the same properties for $R$ . By [F2] and [F3], $Q$ yields the first exact sequence, and $G$ yields the ribbon sequence. Since $G = G^{'} Q$ , the vertex-group isomorphism induced by $G^{'}$ commutes with the injections from $D_{J}$ . A lift through $G$ is the same arrow as the lift through $Q$ of its $G^{'}$ -preimage. Consequently the two endpoint maps agree under the common deck-group identification with $N$ . This gives the asserted isomorphism of extensions.

1.2F1F2given

Write the unique lift of $μ$ from $d$ as a finite composite of crossings and inverse crossings. At a positive crossing, [F1] multiplies the first chamber coordinate on the right by the projection of its ribbon. For an inverse crossing, reversing the same formula multiplies it by the inverse projection. Induction over the composite therefore shows that its endpoint is $(π (μ), J)$ , since $μ$ is a loop at $J$ . This is a chamber label, so its first coordinate is the minimum-length representative of its right $W_{J}$ -coset.

2.1F3F4F7step 1.1

The Choice assumption permits the quasi-inverses in [F4]. An equivalence of groupoids is fully faithful, so $p$ and $\overset{ˉ}{p}$ induce isomorphisms on the indicated vertex groups. The square in [F4] makes these isomorphisms commute with the injections. If a quotient-groupoid loop lifts from $d$ to $n d$ , its image under $p$ is a path class from $x$ to $n x$ by equivariance. Thus the topological endpoint map sends its image to the same $n$ . The topological sequence is exact by [F4], and the resulting diagram is the claimed isomorphism of exact sequences.

3.1F2F3F4F5F6F7step 1.1step 1.2step 2.1∎

By [F6], $π (μ)$ normalises $W_{J}$ . By [F5] and the minimality in step 1.2, the class $π (μ) W_{J}$ carries $d$ to $(π (μ), J)$ . The action is free, so [F3] identifies this class with $ψ (μ)$ . Finally, the isomorphism in [F6] sends $μ$ to $μ A_{J}$ , and the induced map $\overline{π}$ sends that coset to $π (μ) W_{J}$ . Hence $ψ = \overline{π}$ under this isomorphism. In step 1.1 the comparison from the $Q$ -sequence to the ribbon sequence has middle map $G_{Q d}^{'}$ , and in step 2.1 the comparison to the topological sequence has middle map ${\overset{ˉ}{p}}_{Q d}$ . Transport the ribbon middle group to $N (A, J)$ by $q_{J}$ from [F6]. Composing the inverse ribbon comparison with the topological comparison therefore gives $Φ = {\overset{ˉ}{p}}_{Q d} \circ (G_{Q d}^{'})^{- 1} \circ q_{J}^{- 1}$ . Each comparison commutes with the endpoint maps, so $Φ$ commutes with the maps to $N$ and identifies their kernels; restricting $Φ$ identifies the algebraic kernel with the topological kernel. This proves the stated components and completes all comparisons.

Source notes

The article reference attributes the intermediate claims. The explicit Choice qualification records the hypothesis of the current equivalence supplier and does not attribute a defect to the original article. The proof uses the completed suppliers and does not take the article's comparison as a premise.

Depends on

Used by · 2

Dependency tree · 2 levels

Each result is drawn at its shortest distance from this item. Arrows run from prerequisites to the items that use them; this item has a heavier outline. External source nodes link directly to the cited text. The view shows up to two dependency steps; open a prerequisite to continue.

Sources

Normalisers of parabolic subgroups of Artin–Tits groups and Tits cone intersections · PDF p. 26, proof of Theorem 6.7, equations (6.9)–(6.11)