UniMath / SymmetryBook

This book will be an undergraduate textbook written in the univalent style, taking advantage of the presence of symmetry in the logic at an early stage.
Creative Commons Attribution Share Alike 4.0 International
371 stars 22 forks source link

Sign homomorphism #138

Open UlrikBuchholtz opened 2 years ago

UlrikBuchholtz commented 2 years ago

I've now written up the new approach to the sign homomorphism in Sec. 4.5 (after commit c20b570).

Please have a look! There's a little puzzle left: I give a pointed map, Bsgn, from n-element sets to 2-element sets that defines the sign homomorphism sgn : Σₙ → Σ₂. I also define sign homomorphisms sgn : Aut(A) → Σ₂, for all n-element sets A, but these can't all share the same classifying map. (Making it pointed for all A would trivialize it.) I tried to explain this situation, but since I'm myself still a little mystified by it, there's probably room for improvements, which would be very welcome.

bidundas commented 2 years ago

Thanks - I look forward to looking at it!

Among other things, I also enjoyed the tiny comment typical of Niel (“Why not just …”), the overflow is a small treasure. I had a problem seeing that Speyer’s (2) did anything more than proving that there are AT MOST two representations

Bjorn

On 18 Mar 2022, at 08:32, Ulrik Buchholtz @.***> wrote:

I've now written up the new approach to the sign homomorphism in Sec. 4.5 (after commit c20b570).

Please have a look! There's a little puzzle left: I give a pointed map, Bsgn, from n-element sets to 2-element sets that defines the sign homomorphism sgn : Σₙ → Σ₂. I also define sign homomorphisms sgn : Aut(A) → Σ₂, for all n-element sets A, but these can't all share the same classifying map. (Making it pointed for all A would trivialize it.) I tried to explain this situation, but since I'm myself still a little mystified by it, there's probably room for improvements, which would be very welcome.

— Reply to this email directly, view it on GitHub, or unsubscribe. Triage notifications on the go with GitHub Mobile for iOS or Android. You are receiving this because you are subscribed to this thread.

DanGrayson commented 2 years ago

Here is another proof of transitivity, possibly simpler:

Consider f ~ f' ~ f''.

Now for each e:E we have just the following possibilities:

  f(e) = f'(e) = f''(e)  f(e) = f''(e)
  f(e) ≠ f'(e) = f''(e)  f(e) ≠ f''(e)
  f(e) = f'(e) ≠ f''(e)  f(e) ≠ f''(e)
  f(e) ≠ f'(e) ≠ f''(e)  f(e) = f''(e)

(The fourth case follows because there are only two possible values for the functions.)

Now count: the number of inequalities f(e) ≠ f''(e) is the number of inequalities f(e) ≠ f'(e) plus the number of inequalities f'(e) ≠ f''(e) minus 2 times the number of times the fourth case occurs. Hence, it's even.

DanGrayson commented 2 years ago

Was this notation previously defined?

Screen Shot 2022-03-18 at 9 43 32 AM
DanGrayson commented 2 years ago

The inability to make Bsgn a pointed map seems to be a fundamental stumbling block, but you got around it neatly. The way you got around it can be stated a little more generally: given a non-pointed map f : BG -> BH, with H abelian, one can construct a homomorphism of abstract groups G -> H. The point is that the two homomorphisms that result from two paths making f pointed differ by conjugation by some element of H, but conjugation is trivial in an abelian group.

DanGrayson commented 2 years ago

Here is another proof of transitivity, possibly simpler:

Consider f ~ f' ~ f''.

Now for each e:E we have just the following possibilities:

  f(e) = f'(e) = f''(e)  f(e) = f''(e)
  f(e) ≠ f'(e) = f''(e)  f(e) ≠ f''(e)
  f(e) = f'(e) ≠ f''(e)  f(e) ≠ f''(e)
  f(e) ≠ f'(e) ≠ f''(e)  f(e) = f''(e)

(The fourth case follows because there are only two possible values for the functions.)

Now count: the number of inequalities f(e) ≠ f''(e) is the number of inequalities f(e) ≠ f'(e) plus the number of inequalities f'(e) ≠ f''(e) minus 2 times the number of times the fourth case occurs. Hence, it's even.

PS: The same reasoning shows that ¬ ( f ~ f' ) ∧ ¬ ( f' ~ f'' ) ⇒ f ~ f''

DanGrayson commented 2 years ago

There are three equivalent concepts mentioned, but it's unspecified how to pass between them:

I wonder if there's a way to stick to just one of them.

DanGrayson commented 2 years ago

Here is another proof of transitivity, possibly simpler: Consider f ~ f' ~ f''. Now for each e:E we have just the following possibilities:

  f(e) = f'(e) = f''(e)  f(e) = f''(e)
  f(e) ≠ f'(e) = f''(e)  f(e) ≠ f''(e)
  f(e) = f'(e) ≠ f''(e)  f(e) ≠ f''(e)
  f(e) ≠ f'(e) ≠ f''(e)  f(e) = f''(e)

PS: The same reasoning shows that ¬ ( f ~ f' ) ∧ ¬ ( f' ~ f'' ) ⇒ f ~ f''

PPS: and that shows the number of equivalence classes is at most 2

DanGrayson commented 2 years ago

The inability to make Bsgn a pointed map seems to be a fundamental stumbling block, but you got around it neatly. The way you got around it can be stated a little more generally: given a non-pointed map f : BG -> BH, with H abelian, one can construct a homomorphism of abstract groups G -> H. The point is that the two homomorphisms that result from two paths making f pointed differ by conjugation by some element of H, but conjugation is trivial in an abelian group.

That prompted me to consider the following digression.

Consider a map f : BG --> BH pointed with a path p : f() = . Then the induced homomorphism of abstract groups sends g : ΩBG to p ∘ f(g) ∘ p^-1 : ΩBH. Now replace (f,p) by (f,h∘p) for some nontrivial h : ΩBH. Then it induces the abstract homomorphism that sends g to h ∘ (p ∘ f(g) ∘ p^-1) ∘ h^-1. The element h might commute with all of the elements (p ∘ f(g) ∘ p^-1), rendering the two abstract group homomorphisms the same, but with no obvious path of type (f,p) = (f,h∘p). But lemma 4.10.1 in the section "4.10 Homomorphisms; abstract vs. concrete" says there must be one. Is it easy to see it in this case? Or must the full strength of the lemma be applied?

(Why not promote the lemma to a theorem?)

marcbezem commented 2 years ago

In the special case where BH is the circle I know an easy argument. I take q = h∘p, freeing h to be used for a path (homotopy) f = f not being the reflexivity path, but one with h(*) = (inv q)∘p. Then we get (f,p) = (f,q) using h. We use a family e_z of equivalences of type (base=base) -> (z=z) that we know for the circle. Define r := (inv e_f(*))((inv q)∘p) : base=base. Define h(x) := (e_f(x))(r) : f(x) = f(x) for all x: BG, then indeed h(*) = (inv q)∘p.

pierrecagne commented 2 years ago

The argument given by Marc works for any H such that BH admits an element in Π(z:BH)((sh ⥱ sh) ⥲ (z ⥱ z)) . It makes me think: for any group H, we do have an element of Π(z:BH) ‖(sh ⥱ sh) ⥲ (z ⥱ z)‖ by connectedness of BH. Do we have a good handle of those groups for which we actually have the former (which is strictly stronger than the latter)? In the case of the circle, the element called e by Marc is defined by circle-induction IIRC, so it kind of comes from outside of the group-world.

DanGrayson commented 2 years ago

Is there an analogue of circle induction that works for any group BH?

marcbezem commented 2 years ago

Here is an argument for BΣ₂, rather ad hoc and seemingly completely different from the circle. (Sorry to have missed our Zoom.) Denote the standard two-element set by 2. We will construct a family of equivalences e_A : 2=2 ⥲ A=A parametrized by an arbitrary two-element set A. For such A we can prove that for all a:A there exists a unique b:A that is different from a. (The is statement is a proposition and it holds for A=2.) Using that (2=2)=2 we can define e_A by distinguishing two cases: one in which we take refl_A and one in which apply univalence to the equivalence sending each a:A to the other element b (the well-known swap). Every e_A is indeed an equivalence since this statement is a proposition and it holds for A=2. (Could be an exercise in the book.)

marcbezem commented 2 years ago

The argument given by Marc works for any H such that BH admits an element in Π(z:BH)((sh ⥱ sh) ⥲ (z ⥱ z)) . It makes me think: for any group H, we do have an element of Π(z:BH) ‖(sh ⥱ sh) ⥲ (z ⥱ z)‖ by connectedness of BH. Do we have a good handle of those groups for which we actually have the former (which is strictly stronger than the latter)? In the case of the circle, the element called e by Marc is defined by circle-induction IIRC, so it kind of comes from outside of the group-world.

@pierrecagne: a starting point could be to try to prove it for all abelian groups.

Edit: I had first "if one has an element in Π(z:BH)((sh ⥱ sh) ⥲ (z ⥱ z)) the group H is abelian", but I actually don't know that.