Transfer homomorphism

Stream: maths

[Kenny Lau]

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.

[Kenny Lau]

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

[Kenny Lau]

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

[Kenny Lau]

How should I do that?

[Mario Carneiro]

using choice

[Kenny Lau]

but it will be noncomputable

[Mario Carneiro]

obviously

[Kenny Lau]

can I make it computable?

[Mario Carneiro]

nothing about what you said sounds remotely computable

[Kenny Lau]

it seems computable to me

[Kenny Lau]

the map is independent of s

[Kenny Lau]

there is only finitely many choices to make

[Mario Carneiro]

How do you even know such a function s exists?

[Kenny Lau]

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

[Kenny Lau]

obviously s is noncomputable

[Kenny Lau]

but the transfer homomorphism should be computable

[Mario Carneiro]

How is G^ab defined

[Kenny Lau]

G quotient G commutator

[Kenny Lau]

G/[G,G]

[Mario Carneiro]

And in what sense is G/H finite

[Kenny Lau]

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

[Kenny Lau]

so G/H is a fintype

[Mario Carneiro]

I mean, how are you expressing "finite index"

[Kenny Lau]

[fintype G/H]

[Mario Carneiro]

And how do you construct a section?

[Kenny Lau]

I don't

[Mario Carneiro]

Any section at all

[Kenny Lau]

section is noncomputable

[Kenny Lau]

but the transfer homomorphism is independent of section

[Kenny Lau]

so I need finitely many lifts

[Mario Carneiro]

Even ignoring the lifts

[Kenny Lau]

I can't construct any section computably

[Kenny Lau]

if that's what you mean

[Mario Carneiro]

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

[Kenny Lau]

hmm

[Kenny Lau]

but it will be very hard

[Mario Carneiro]

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

[Kenny Lau]

each element of the product is not well-defined

[Kenny Lau]

it is the product itself which is well-defined

[Mario Carneiro]

You have a single quotient in the output

[Mario Carneiro]

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

[Mario Carneiro]

Do you have decidable equality on G/H?

[Kenny Lau]

is that necessary?

[Kenny Lau]

I feel that it is already computable

[Mario Carneiro]

it comes up in the construction of the functions

[Kenny Lau]

how would you do it?

[Mario Carneiro]

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

[Kenny Lau]

but everything is finite here

[Kenny Lau]

the axioms should be enough

[Mario Carneiro]

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

[Kenny Lau]

hmm

[Kenny Lau]

this is very hard

[Kenny Lau]

can I even do this in 3 days

[Mario Carneiro]

It's less than 100 lines for sure

[Mario Carneiro]

Also, decidable equality is definitely necessary for constructing sections

[Kenny Lau]

I don't want to construct any section

[Mario Carneiro]

You do, that's the whole point

[Mario Carneiro]

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

[Kenny Lau]

hmm

[Mario Carneiro]

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

[Kenny Lau]

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

[Mario Carneiro]

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

[Kenny Lau]

but everything is finite

[Mario Carneiro]

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

[Kenny Lau]

then why do I need it now

[Kenny Lau]

even if the choice is coordinated

[Kenny Lau]

it's still finite

[Mario Carneiro]

to define the section that coordinates the choices

[Kenny Lau]

but everything is well-defined

[Mario Carneiro]

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

[Kenny Lau]

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

[Mario Carneiro]

That's not the problem

[Mario Carneiro]

You want a function G/H -> G

[Kenny Lau]

list.rec is computable

[Kenny Lau]

multiset.rec is computable

[Mario Carneiro]

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

[Kenny Lau]

finset.rec is computable

[Kenny Lau]

hmm

[Mario Carneiro]

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

[Kenny Lau]

I only have one quotient though

[Kenny Lau]

it's just G/H

[Mario Carneiro]

That doesn't make too much of a difference

[Mario Carneiro]

The point here is the interchanging of pi and quot

[Kenny Lau]

I see

[Mario Carneiro]

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

[Kenny Lau]

I see

[Mario Carneiro]

because it has an obvious VM interpretation

[Kenny Lau]

but is it provable?

[Mario Carneiro]

but you can only prove it for I finite

[Mario Carneiro]

and even then I believe it implies decidable equality of I

[Kevin Buzzard]

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?

[Mario Carneiro]

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

[Reid Barton]

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

[Reid Barton]

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

[Mario Carneiro]

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

[Mario Carneiro]

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

[Reid Barton]

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

[Reid Barton]

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

[Mario Carneiro]

I see, yes that's bad

[Mario Carneiro]

So maybe just replacequot with quotient everywhere

[Mario Carneiro]

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

[Mario Carneiro]

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 _

[Mario Carneiro]

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?

[Kenny Lau]

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

[Mario Carneiro]

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

[Kenny Lau]

yes

[Mario Carneiro]

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

[Kenny Lau]

@Kevin Buzzard

[Mario Carneiro]

[[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)

[Mario Carneiro]

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

[Kenny Lau]

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

[Kenny Lau]

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

[Mario Carneiro]

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

[Kenny Lau]

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

[Mario Carneiro]

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.

[Kenny Lau]

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

[Mario Carneiro]

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

[Kenny Lau]

:o

[Kevin Buzzard]

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