Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Sign homomorphism #138

Open
UlrikBuchholtz opened this issue Mar 18, 2022 · 13 comments
Open

Sign homomorphism #138

UlrikBuchholtz opened this issue Mar 18, 2022 · 13 comments

Comments

@UlrikBuchholtz
Copy link
Contributor

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
Copy link
Contributor

bidundas commented Mar 18, 2022 via email

@DanGrayson
Copy link
Member

DanGrayson commented Mar 18, 2022

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
Copy link
Member

Was this notation previously defined?

Screen Shot 2022-03-18 at 9 43 32 AM

@DanGrayson
Copy link
Member

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
Copy link
Member

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
Copy link
Member

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

  • putting a structure of directed graph on an undirected graph
  • ordering each set in a family of 2-element sets
  • picking an element from each set in a family of 2-element sets

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

@DanGrayson
Copy link
Member

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
Copy link
Member

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
Copy link
Contributor

marcbezem commented Mar 31, 2022

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
Copy link
Member

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
Copy link
Member

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

@marcbezem
Copy link
Contributor

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
Copy link
Contributor

marcbezem commented Apr 14, 2022

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.

Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Labels
None yet
Projects
None yet
Development

No branches or pull requests

5 participants