Zulip Chat Archive

Stream: maths

Topic: Transfer homomorphism


view this post on Zulip Kenny Lau (Jun 15 2018 at 16:15):

Let G be a group and H a subgroup of finite index. Then, pick a set-theoretic section s:G/H->G where G/H is the right cosets. Then, the transfer homomorphism G^ab -> H^ab is defined by sending [[g]] to prod[x in G/H] s(x) g s(xg)^-1.

view this post on Zulip Kenny Lau (Jun 15 2018 at 16:15):

The wonderful thing about this homomorphism is that it is independent of the section s

view this post on Zulip Kenny Lau (Jun 15 2018 at 16:16):

but this also means that I will be lifting arbitrarily many quotients.

view this post on Zulip Kenny Lau (Jun 15 2018 at 16:16):

How should I do that?

view this post on Zulip Mario Carneiro (Jun 15 2018 at 16:16):

using choice

view this post on Zulip Kenny Lau (Jun 15 2018 at 16:16):

but it will be noncomputable

view this post on Zulip Mario Carneiro (Jun 15 2018 at 16:17):

obviously

view this post on Zulip Kenny Lau (Jun 15 2018 at 16:17):

can I make it computable?

view this post on Zulip Mario Carneiro (Jun 15 2018 at 16:17):

nothing about what you said sounds remotely computable

view this post on Zulip Kenny Lau (Jun 15 2018 at 16:17):

it seems computable to me

view this post on Zulip Kenny Lau (Jun 15 2018 at 16:17):

the map is independent of s

view this post on Zulip Kenny Lau (Jun 15 2018 at 16:17):

there is only finitely many choices to make

view this post on Zulip Mario Carneiro (Jun 15 2018 at 16:17):

How do you even know such a function s exists?

view this post on Zulip Kenny Lau (Jun 15 2018 at 16:18):

you don't need the function s. you just need to lift finitely many quotients

view this post on Zulip Kenny Lau (Jun 15 2018 at 16:18):

obviously s is noncomputable

view this post on Zulip Kenny Lau (Jun 15 2018 at 16:18):

but the transfer homomorphism should be computable

view this post on Zulip Mario Carneiro (Jun 15 2018 at 16:18):

How is G^ab defined

view this post on Zulip Kenny Lau (Jun 15 2018 at 16:18):

G quotient G commutator

view this post on Zulip Kenny Lau (Jun 15 2018 at 16:18):

G/[G,G]

view this post on Zulip Mario Carneiro (Jun 15 2018 at 16:19):

And in what sense is G/H finite

view this post on Zulip Kenny Lau (Jun 15 2018 at 16:19):

in the sense that H is a finite-index subgroup of G

view this post on Zulip Kenny Lau (Jun 15 2018 at 16:19):

so G/H is a fintype

view this post on Zulip Mario Carneiro (Jun 15 2018 at 16:20):

I mean, how are you expressing "finite index"

view this post on Zulip Kenny Lau (Jun 15 2018 at 16:20):

[fintype G/H]

view this post on Zulip Mario Carneiro (Jun 15 2018 at 16:21):

And how do you construct a section?

view this post on Zulip Kenny Lau (Jun 15 2018 at 16:21):

I don't

view this post on Zulip Mario Carneiro (Jun 15 2018 at 16:21):

Any section at all

view this post on Zulip Kenny Lau (Jun 15 2018 at 16:22):

section is noncomputable

view this post on Zulip Kenny Lau (Jun 15 2018 at 16:22):

but the transfer homomorphism is independent of section

view this post on Zulip Kenny Lau (Jun 15 2018 at 16:22):

so I need finitely many lifts

view this post on Zulip Mario Carneiro (Jun 15 2018 at 16:22):

Even ignoring the lifts

view this post on Zulip Kenny Lau (Jun 15 2018 at 16:22):

I can't construct any section computably

view this post on Zulip Kenny Lau (Jun 15 2018 at 16:23):

if that's what you mean

view this post on Zulip Mario Carneiro (Jun 15 2018 at 16:24):

I think I see what you mean with iterating lifts, that might be possible

view this post on Zulip Kenny Lau (Jun 15 2018 at 16:24):

hmm

view this post on Zulip Kenny Lau (Jun 15 2018 at 16:24):

but it will be very hard

view this post on Zulip Mario Carneiro (Jun 15 2018 at 16:24):

But you will have to redo the work of finset.pi

view this post on Zulip Kenny Lau (Jun 15 2018 at 16:24):

each element of the product is not well-defined

view this post on Zulip Kenny Lau (Jun 15 2018 at 16:24):

it is the product itself which is well-defined

view this post on Zulip Mario Carneiro (Jun 15 2018 at 16:24):

You have a single quotient in the output

view this post on Zulip Mario Carneiro (Jun 15 2018 at 16:25):

or even a trunc, if you express the section property in a subtype

view this post on Zulip Mario Carneiro (Jun 15 2018 at 16:26):

Do you have decidable equality on G/H?

view this post on Zulip Kenny Lau (Jun 15 2018 at 16:26):

is that necessary?

view this post on Zulip Kenny Lau (Jun 15 2018 at 16:26):

I feel that it is already computable

view this post on Zulip Mario Carneiro (Jun 15 2018 at 16:26):

it comes up in the construction of the functions

view this post on Zulip Kenny Lau (Jun 15 2018 at 16:27):

how would you do it?

view this post on Zulip Mario Carneiro (Jun 15 2018 at 16:28):

I am reminded of a discussion with @Gabriel Ebner about generalizing the quotient axioms to allow for indexed families of quotients

view this post on Zulip Kenny Lau (Jun 15 2018 at 16:29):

but everything is finite here

view this post on Zulip Kenny Lau (Jun 15 2018 at 16:29):

the axioms should be enough

view this post on Zulip Mario Carneiro (Jun 15 2018 at 16:29):

But it's provable in the finite case, and that's what I would prove

view this post on Zulip Kenny Lau (Jun 15 2018 at 16:29):

hmm

view this post on Zulip Kenny Lau (Jun 15 2018 at 16:29):

this is very hard

view this post on Zulip Kenny Lau (Jun 15 2018 at 16:29):

can I even do this in 3 days

view this post on Zulip Mario Carneiro (Jun 15 2018 at 16:29):

It's less than 100 lines for sure

view this post on Zulip Mario Carneiro (Jun 15 2018 at 16:31):

Also, decidable equality is definitely necessary for constructing sections

view this post on Zulip Kenny Lau (Jun 15 2018 at 16:31):

I don't want to construct any section

view this post on Zulip Mario Carneiro (Jun 15 2018 at 16:31):

You do, that's the whole point

view this post on Zulip Mario Carneiro (Jun 15 2018 at 16:31):

You are lifting stuff from a quotient but that's not so important

view this post on Zulip Kenny Lau (Jun 15 2018 at 16:32):

hmm

view this post on Zulip Mario Carneiro (Jun 15 2018 at 16:33):

Are you suggesting that there is a way to define the transfer that avoids reference to any section?

view this post on Zulip Kenny Lau (Jun 15 2018 at 16:33):

If I do a product indexed by a fintype do I need decidable equality?

view this post on Zulip Mario Carneiro (Jun 15 2018 at 16:33):

I assume you have to make coordinated choices in order to define the sums

view this post on Zulip Kenny Lau (Jun 15 2018 at 16:33):

but everything is finite

view this post on Zulip Mario Carneiro (Jun 15 2018 at 16:35):

No, products of elements in a commutative group over a finset does not require decidable_eq

view this post on Zulip Kenny Lau (Jun 15 2018 at 16:35):

then why do I need it now

view this post on Zulip Kenny Lau (Jun 15 2018 at 16:35):

even if the choice is coordinated

view this post on Zulip Kenny Lau (Jun 15 2018 at 16:35):

it's still finite

view this post on Zulip Mario Carneiro (Jun 15 2018 at 16:35):

to define the section that coordinates the choices

view this post on Zulip Kenny Lau (Jun 15 2018 at 16:35):

but everything is well-defined

view this post on Zulip Mario Carneiro (Jun 15 2018 at 16:36):

How are you going to remember your finitely many choices if not with a function? And how is that function indexed?

view this post on Zulip Kenny Lau (Jun 15 2018 at 16:36):

isn't it the philosophy of quotient that if your choices are well-defined then you are computable?

view this post on Zulip Mario Carneiro (Jun 15 2018 at 16:36):

That's not the problem

view this post on Zulip Mario Carneiro (Jun 15 2018 at 16:36):

You want a function G/H -> G

view this post on Zulip Kenny Lau (Jun 15 2018 at 16:37):

list.rec is computable

view this post on Zulip Kenny Lau (Jun 15 2018 at 16:37):

multiset.rec is computable

view this post on Zulip Mario Carneiro (Jun 15 2018 at 16:37):

that means distinguishing elements of G/H when they are sent to different members of G

view this post on Zulip Kenny Lau (Jun 15 2018 at 16:37):

finset.rec is computable

view this post on Zulip Kenny Lau (Jun 15 2018 at 16:39):

hmm

view this post on Zulip Mario Carneiro (Jun 15 2018 at 16:55):

Here's a way to state the section property without groups:

def choices {ι : Type*} [fintype ι] {α : ι → Type*} (R : ∀ i, α i → α i → Prop)
    (f : ∀ i, quot (R i)) : quot (λ (a b : Π i, α i), ∀ i, R i (a i) (b i)) := sorry

view this post on Zulip Kenny Lau (Jun 15 2018 at 16:56):

I only have one quotient though

view this post on Zulip Kenny Lau (Jun 15 2018 at 16:56):

it's just G/H

view this post on Zulip Mario Carneiro (Jun 15 2018 at 16:57):

That doesn't make too much of a difference

view this post on Zulip Mario Carneiro (Jun 15 2018 at 16:58):

The point here is the interchanging of pi and quot

view this post on Zulip Kenny Lau (Jun 15 2018 at 16:58):

I see

view this post on Zulip Mario Carneiro (Jun 15 2018 at 17:00):

It seems reasonable to have that function as a computable axiom, this is what Gabriel and I discussed

view this post on Zulip Kenny Lau (Jun 15 2018 at 17:00):

I see

view this post on Zulip Mario Carneiro (Jun 15 2018 at 17:00):

because it has an obvious VM interpretation

view this post on Zulip Kenny Lau (Jun 15 2018 at 17:01):

but is it provable?

view this post on Zulip Mario Carneiro (Jun 15 2018 at 17:01):

but you can only prove it for I finite

view this post on Zulip Mario Carneiro (Jun 15 2018 at 17:01):

and even then I believe it implies decidable equality of I

view this post on Zulip Kevin Buzzard (Jun 15 2018 at 17:14):

Kenny, if you are under time constraints, why not just make it noncomputable, make sure everything else is done, and come back to it later if you have time?

view this post on Zulip Mario Carneiro (Jun 15 2018 at 17:16):

I will look into this theorem, and report back if I can prove it. Feel free to assume it

view this post on Zulip Reid Barton (Jun 15 2018 at 17:17):

This version is not quite right though, because for example one of the R i could be the empty relation, and then the "product relation" is also empty

view this post on Zulip Reid Barton (Jun 15 2018 at 17:19):

You need to assume the R i are at least reflexive, or build the "product relation" differently, like the Cartesian product of graphs

view this post on Zulip Mario Carneiro (Jun 15 2018 at 17:21):

That's fine, quot implicitly takes the equivalence closure of the given relation

view this post on Zulip Mario Carneiro (Jun 15 2018 at 17:21):

quotient is the variant that explicitly assumes the relation is an equivalence already

view this post on Zulip Reid Barton (Jun 15 2018 at 17:22):

But, say, R 1 might be nontrivial, while R 2 is empty, and then λ (a b : Π i, α i), ∀ i, R i (a i) (b i) is empty, so we haven't made any identifications in \a 1 \x \a 2

view this post on Zulip Reid Barton (Jun 15 2018 at 17:23):

then we'd have a map quot (R 1) \to \a 1. Or is that okay?

view this post on Zulip Mario Carneiro (Jun 15 2018 at 17:24):

I see, yes that's bad

view this post on Zulip Mario Carneiro (Jun 15 2018 at 17:25):

So maybe just replacequot with quotient everywhere

view this post on Zulip Mario Carneiro (Jun 15 2018 at 17:25):

although then I have to show that the pi of equivalences is an equivalence

view this post on Zulip Mario Carneiro (Jun 15 2018 at 17:39):

Here's the noncomputable version:

instance pi_setoid {ι : Type*} {α : ι → Type*} [∀ i, setoid (α i)] : setoid (Π i, α i) :=
{ r := λ a b, ∀ i, a i ≈ b i,
  iseqv := ⟨
    λ a i, setoid.refl _,
    λ a b h i, setoid.symm (h _),
    λ a b c h₁ h₂ i, setoid.trans (h₁ _) (h₂ _)⟩ }

noncomputable def quotient.choice {ι : Type*} {α : ι → Type*} [S : ∀ i, setoid (α i)]
  (f : ∀ i, quotient (S i)) : @quotient (Π i, α i) (by apply_instance) :=
⟦λ i, (f i).out⟧

theorem quotient.choice_eq {ι : Type*} {α : ι → Type*} [∀ i, setoid (α i)]
  (f : ∀ i, α i) : quotient.choice (λ i, ⟦f i⟧) = ⟦f⟧ :=
quotient.sound $ λ i, quotient.mk_out _

view this post on Zulip Mario Carneiro (Jun 15 2018 at 19:24):

Let G be a group and H a subgroup of finite index. Then, pick a set-theoretic section s:G/H->G where G/H is the right cosets. Then, the transfer homomorphism G^ab -> H^ab is defined by sending [[g]] to prod[x in G/H] s(x) g s(xg)^-1.

Shouldn't there be a [[]] in the definition there somewhere?

view this post on Zulip Kenny Lau (Jun 15 2018 at 19:24):

by sending [[g]] to [[prod[x in G/H] s(x) g s(xg)^-1]].

view this post on Zulip Mario Carneiro (Jun 15 2018 at 19:24):

Does [[g h]] = [[g]][[h]]?

view this post on Zulip Kenny Lau (Jun 15 2018 at 19:25):

yes

view this post on Zulip Mario Carneiro (Jun 15 2018 at 19:25):

Then don't the s(x) parts cancel?

view this post on Zulip Kenny Lau (Jun 15 2018 at 19:25):

@Kevin Buzzard

view this post on Zulip Mario Carneiro (Jun 15 2018 at 19:26):

[[prod[x in G/H] s(x) g s(xg)^-1]] = (prod[x in G/H] [[s(x)]]) (prod[x in G/H] [[g]]) (prod[x in G/H] [[s(xg)]]^-1)

view this post on Zulip Mario Carneiro (Jun 15 2018 at 19:26):

and prod[x in G/H] [[s(xg)]]^-1 = prod[x in G/H] [[s(x)]]^-1 by reindexing

view this post on Zulip Kenny Lau (Jun 15 2018 at 19:26):

oh you can't do that, g is not in H

view this post on Zulip Kenny Lau (Jun 15 2018 at 19:27):

s(x) g s(xg)^-1 is in H

view this post on Zulip Mario Carneiro (Jun 15 2018 at 19:27):

I know, but they should still be equal as members of G

view this post on Zulip Kenny Lau (Jun 15 2018 at 19:27):

no, because H^ab is H/[H,H]

view this post on Zulip Mario Carneiro (Jun 15 2018 at 19:46):

Okay, I think I have something close to a proof that decidable_eq of the coset relation is necessary. Suppose you know fintype G/H. Ignoring quotients for a moment, thinking "computationally", this is essentially a list of elements of G which chooses exactly one element of every coset (or, if you prefer, a bijection (not an equiv) from fin n to G/H). Now that looks like the section we want, but the problem is the computation of s(xg) that we need later. The function x |-> xg is a permutation of G/H which corresponds to a permutation of the list s, but computationally it's not that easy since if we take our representative s(x) and multiply by g we get s(x)g, which is in the same coset as s(xg) but is not usually the same. So we need a way of searching our list s to find the value that is in the same coset as s(x)g, and there is no way to do this from the given data.

view this post on Zulip Kenny Lau (Jun 15 2018 at 21:17):

I see. Then I'll just come up with a section noncomputably then.

view this post on Zulip Mario Carneiro (Jun 15 2018 at 21:19):

Here's the computable version of that theorem:

def quotient.fin_choice_aux {ι : Type*} [decidable_eq ι]
  {α : ι → Type*} [S : ∀ i, setoid (α i)] :
  ∀ (l : list ι), (∀ i ∈ l, quotient (S i)) → @quotient (Π i ∈ l, α i) (by apply_instance)
| []     f := ⟦λ i, false.elim⟧
| (i::l) f := begin
  refine quotient.lift_on₂ (f i (list.mem_cons_self _ _))
    (quotient.fin_choice_aux l (λ j h, f j (list.mem_cons_of_mem _ h)))
    _ _,
  exact λ a l, ⟦λ j h,
    if e : j = i then by rw e; exact a else
    l _ (h.resolve_left e)⟧,
  refine λ a₁ l₁ a₂ l₂ h₁ h₂, quotient.sound (λ j h, _),
  by_cases e : j = i; simp [e],
  { subst j, exact h₁ },
  { exact h₂ _ _ }
end

theorem quotient.fin_choice_aux_eq {ι : Type*} [decidable_eq ι]
  {α : ι → Type*} [S : ∀ i, setoid (α i)] :
  ∀ (l : list ι) (f : ∀ i ∈ l, α i), quotient.fin_choice_aux l (λ i h, ⟦f i h⟧) = ⟦f⟧
| []     f := quotient.sound (λ i h, h.elim)
| (i::l) f := begin
  simp [quotient.fin_choice_aux, quotient.fin_choice_aux_eq l],
  refine quotient.sound (λ j h, _),
  by_cases e : j = i; simp [e],
  subst j, refl
end

def quotient.fin_choice {ι : Type*} [fintype ι] [decidable_eq ι]
  {α : ι → Type*} [S : ∀ i, setoid (α i)]
  (f : ∀ i, quotient (S i)) : @quotient (Π i, α i) (by apply_instance) :=
quotient.lift_on (@quotient.rec_on _ _ (λ l : multiset ι,
    @quotient (Π i ∈ l, α i) (by apply_instance))
    finset.univ.1
    (λ l, quotient.fin_choice_aux l (λ i _, f i))
    (λ a b h, begin
      have := λ a, quotient.fin_choice_aux_eq a (λ i h, quotient.out (f i)),
      simp [quotient.out_eq] at this,
      simp [this],
      let g := λ a:multiset ι, ⟦λ (i : ι) (h : i ∈ a), quotient.out (f i)⟧,
      refine eq_of_heq ((eq_rec_heq _ _).trans (_ : g a == g b)),
      congr' 1, exact quotient.sound h,
    end))
  (λ f, ⟦λ i, f i (finset.mem_univ _)⟧)
  (λ a b h, quotient.sound $ λ i, h _ _)


theorem quotient.fin_choice_eq {ι : Type*} [fintype ι] [decidable_eq ι]
  {α : ι → Type*} [∀ i, setoid (α i)]
  (f : ∀ i, α i) : quotient.fin_choice (λ i, ⟦f i⟧) = ⟦f⟧ :=
begin
  let q, swap, change quotient.lift_on q _ _ = _,
  have : q = ⟦λ i h, f i⟧,
  { dsimp [q],
    exact quotient.induction_on
      (@finset.univ ι _).1 (λ l, quotient.fin_choice_aux_eq _ _) },
  simp [this], exact setoid.refl _
end

view this post on Zulip Kenny Lau (Jun 15 2018 at 21:19):

:o

view this post on Zulip Kevin Buzzard (Jun 16 2018 at 10:24):

Canceling s -- [[]] is being used for both the map G->Gab and H->Hab so they don't cancel. Spending the weekend in a field without much internet so don't expect too much from me until sun pm


Last updated: May 06 2021 at 17:38 UTC