Proof of Cauchy's theorem 7.3.2

[pcapriotti]

The proof of theorem 7.3.2 looks wrong. In the definition of A, the type (S,j) = (S,j) is equivalent to p for all (S,j), and that means that its C_p action is trivial. In fact, for a non-trivial cyclic action it wouldn't be possible to define the map μ, since the product of a tuple is not equivariant for non-abelian G.

I think A should be defined as A(S,j) = S → UG instead. That gives the intended cyclic action which is used later in the proof.

The problem is then that μ cannot be defined. However, the equation in the definition of X, as a whole, is equivariant. Therefore, X should be replaced by something like X(S,j) = Σ (g : A(S,j)), T(g), where T: (S -> UG) -> Prop expresses the property that the product of the tuple is trivial.

Since T is a proposition, one can define it on a trivial torsor (S,j) with α: (S,j) = Z/p, and show that it doesn't depend on α. There might be a more direct definition, but I can't see it.

[pierrecagne]

@pcapriotti Thanks for the remarks about the proof. Keep in mind that this part of the book is still very rough and WIP.

I might be mistaken but it seems you read the definition of A and μ as being somewhat equivariant type families/maps. This is not the case: A is the type family as written, and μ is then perfectly defined as it is (the fact that G is non-abelian does not prevent to take the product of an ordered tuple in G). I do agree however that the action X does not seem to embody what we want (and maybe this is your point after all).

The informal idea of the proof, as I understand it, is as follows: consider the subset of (UG)ᵖ comprising the tuples whose ordered product is the neutral element; prove that there is a Cₚ-action on it that "shift" the tuple (if g₀g₁⋯gₚ₋₁ = e, then g₁⋯gₚ₋₁g₀ = e also by just multiplying the first equation by g₀ on the right and g₀⁻¹ on the left); showing that this action has non trivial fixpoints, that is there is some non neutral g such that gᵖ = e.

This action is supposed to be embodied by X in the proof. Indeed, X(sh_{Cₚ}) is the set of tuples whose ordered product is the neutral element of UG. To be sure that the action of Cₚ is the one we want, we have to compute the action of X on paths in BCₚ. Given p : (S,j) = (S',j'), the bijection X(p) : X(S,j) = X(S',j') can only really be one thing, that is the map g ↦ g(p⁻¹_p). And this is easily proven by path induction. This is problematic because when instantiated with (S,j) ≡ (S',j') ≡ (𝕡, suc), this give us that X(p) is the identity bijection for all p since Cₚ is abelian.

Your type family A seems to be on the right track, but as you say, it is then difficult to define μ because we don't have an explicit enumeration of S. We should come up with an alternative definition of this type family A. (I'll assign myself for now, I'll see if I find the time to fix this in the coming days.)

[pcapriotti]

@pcapriotti Thanks for the remarks about the proof. Keep in mind that this part of the book is still very rough and WIP.

I might be mistaken but it seems you read the definition of A and μ as being somewhat equivariant type families/maps. This is not the case: A is the type family as written, and μ is then perfectly defined as it is (the fact that G is non-abelian does not prevent to take the product of an ordered tuple in G). I do agree however that the action X does not seem to embody what we want (and maybe this is your point after all).

I agree with this. As written, the proof is correct up to the point where X is specialised to Z/p. Technically, the mistake is that the action is trivial and not the tuple shift as written in the proof. But of course for the purposes of this proof you don't want the action to be trivial, so the actual mistake is in the definition of A, μ and X.

The informal idea of the proof, as I understand it, is as follows: consider the subset of (UG)ᵖ comprising the tuples whose ordered product is the neutral element; prove that there is a Cₚ-action on it that "shift" the tuple (if g₀g₁⋯gₚ₋₁ = e, then g₁⋯gₚ₋₁g₀ = e also by just multiplying the first equation by g₀ on the right and g₀⁻¹ on the left); showing that this action has non trivial fixpoints, that is there is some non neutral g such that gᵖ = e.

This action is supposed to be embodied by X in the proof. Indeed, X(sh_{Cₚ}) is the set of tuples whose ordered product is the neutral element of UG. To be sure that the action of Cₚ is the one we want, we have to compute the action of X on paths in BCₚ. Given p : (S,j) = (S',j'), the bijection X(p) : X(S,j) = X(S',j') can only really be one thing, that is the map g ↦ g(p⁻¹_p). And this is easily proven by path induction. This is problematic because when instantiated with (S,j) ≡ (S',j') ≡ (𝕡, suc), this give us that X(p) is the identity bijection for all p since Cₚ is abelian.

That's right. An even easier way to see this is to follow through with the observation (contained in the proof) that (S,j) = (S,j) is equivalent to 𝕡 for all (S,j). So the family of types (S,j) = (S,j) over BC_p is in fact a constant family, i.e. the corresponding C_p action is trivial.

Your type family A seems to be on the right track, but as you say, it is then difficult to define μ because we don't have an explicit enumeration of S. We should come up with an alternative definition of this type family A. (I'll assign myself for now, I'll see if I find the time to fix this in the coming days.)

I might be wrong, but I don't think it's possible to define μ. As I suggested above, I think one way is basically to define the proposition μ(g) = e directly (for g : A(S,j)), without actually defining μ first. And that can be done by hand by providing it for the base point and proving one coherence.

[pierrecagne]

Not sure how to reference a commit, but check commit 85b0e92c5ed54500c81de92a2f919e6c45d46b14 for an attempt to fix the proof.

[pcapriotti]

Looks good now. If I understand correctly, the trick is to change the condition in the definition of X by quantifying over all cyclic permutations. This produces an equivalent condition, but one that is equivariant. Nice!