## Stream: maths

### Topic: Transfer homomorphism

#### 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.

#### Kenny Lau (Jun 15 2018 at 16:16):

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

#### Kenny Lau (Jun 15 2018 at 16:16):

How should I do that?

using choice

#### Kenny Lau (Jun 15 2018 at 16:16):

but it will be noncomputable

obviously

#### Kenny Lau (Jun 15 2018 at 16:17):

can I make it computable?

#### Mario Carneiro (Jun 15 2018 at 16:17):

nothing about what you said sounds remotely computable

#### Kenny Lau (Jun 15 2018 at 16:17):

it seems computable to me

#### Kenny Lau (Jun 15 2018 at 16:17):

the map is independent of s

#### Kenny Lau (Jun 15 2018 at 16:17):

there is only finitely many choices to make

#### Mario Carneiro (Jun 15 2018 at 16:17):

How do you even know such a function s exists?

#### Kenny Lau (Jun 15 2018 at 16:18):

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

#### Kenny Lau (Jun 15 2018 at 16:18):

obviously s is noncomputable

#### Kenny Lau (Jun 15 2018 at 16:18):

but the transfer homomorphism should be computable

#### Mario Carneiro (Jun 15 2018 at 16:18):

How is G^ab defined

#### Kenny Lau (Jun 15 2018 at 16:18):

G quotient G commutator

G/[G,G]

#### Mario Carneiro (Jun 15 2018 at 16:19):

And in what sense is G/H finite

#### Kenny Lau (Jun 15 2018 at 16:19):

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

#### Kenny Lau (Jun 15 2018 at 16:19):

so G/H is a fintype

#### Mario Carneiro (Jun 15 2018 at 16:20):

I mean, how are you expressing "finite index"

[fintype G/H]

#### Mario Carneiro (Jun 15 2018 at 16:21):

And how do you construct a section?

I don't

#### Mario Carneiro (Jun 15 2018 at 16:21):

Any section at all

#### Kenny Lau (Jun 15 2018 at 16:22):

section is noncomputable

#### Kenny Lau (Jun 15 2018 at 16:22):

but the transfer homomorphism is independent of section

#### Kenny Lau (Jun 15 2018 at 16:22):

so I need finitely many lifts

#### Mario Carneiro (Jun 15 2018 at 16:22):

Even ignoring the lifts

#### Kenny Lau (Jun 15 2018 at 16:22):

I can't construct any section computably

#### Kenny Lau (Jun 15 2018 at 16:23):

if that's what you mean

#### Mario Carneiro (Jun 15 2018 at 16:24):

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

hmm

#### Kenny Lau (Jun 15 2018 at 16:24):

but it will be very hard

#### Mario Carneiro (Jun 15 2018 at 16:24):

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

#### Kenny Lau (Jun 15 2018 at 16:24):

each element of the product is not well-defined

#### Kenny Lau (Jun 15 2018 at 16:24):

it is the product itself which is well-defined

#### Mario Carneiro (Jun 15 2018 at 16:24):

You have a single quotient in the output

#### Mario Carneiro (Jun 15 2018 at 16:25):

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

#### Mario Carneiro (Jun 15 2018 at 16:26):

Do you have decidable equality on G/H?

#### Kenny Lau (Jun 15 2018 at 16:26):

is that necessary?

#### Kenny Lau (Jun 15 2018 at 16:26):

I feel that it is already computable

#### Mario Carneiro (Jun 15 2018 at 16:26):

it comes up in the construction of the functions

#### Kenny Lau (Jun 15 2018 at 16:27):

how would you do it?

#### 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

#### Kenny Lau (Jun 15 2018 at 16:29):

but everything is finite here

#### Kenny Lau (Jun 15 2018 at 16:29):

the axioms should be enough

#### Mario Carneiro (Jun 15 2018 at 16:29):

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

hmm

#### Kenny Lau (Jun 15 2018 at 16:29):

this is very hard

#### Kenny Lau (Jun 15 2018 at 16:29):

can I even do this in 3 days

#### Mario Carneiro (Jun 15 2018 at 16:29):

It's less than 100 lines for sure

#### Mario Carneiro (Jun 15 2018 at 16:31):

Also, decidable equality is definitely necessary for constructing sections

#### Kenny Lau (Jun 15 2018 at 16:31):

I don't want to construct any section

#### Mario Carneiro (Jun 15 2018 at 16:31):

You do, that's the whole point

#### Mario Carneiro (Jun 15 2018 at 16:31):

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

hmm

#### 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?

#### Kenny Lau (Jun 15 2018 at 16:33):

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

#### Mario Carneiro (Jun 15 2018 at 16:33):

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

#### Kenny Lau (Jun 15 2018 at 16:33):

but everything is finite

#### Mario Carneiro (Jun 15 2018 at 16:35):

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

#### Kenny Lau (Jun 15 2018 at 16:35):

then why do I need it now

#### Kenny Lau (Jun 15 2018 at 16:35):

even if the choice is coordinated

#### Kenny Lau (Jun 15 2018 at 16:35):

it's still finite

#### Mario Carneiro (Jun 15 2018 at 16:35):

to define the section that coordinates the choices

#### Kenny Lau (Jun 15 2018 at 16:35):

but everything is well-defined

#### 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?

#### 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?

#### Mario Carneiro (Jun 15 2018 at 16:36):

That's not the problem

#### Mario Carneiro (Jun 15 2018 at 16:36):

You want a function G/H -> G

#### Kenny Lau (Jun 15 2018 at 16:37):

list.rec is computable

#### Kenny Lau (Jun 15 2018 at 16:37):

multiset.rec is computable

#### Mario Carneiro (Jun 15 2018 at 16:37):

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

#### Kenny Lau (Jun 15 2018 at 16:37):

finset.rec is computable

hmm

#### 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


#### Kenny Lau (Jun 15 2018 at 16:56):

I only have one quotient though

it's just G/H

#### Mario Carneiro (Jun 15 2018 at 16:57):

That doesn't make too much of a difference

#### Mario Carneiro (Jun 15 2018 at 16:58):

The point here is the interchanging of pi and quot

I see

#### 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

I see

#### Mario Carneiro (Jun 15 2018 at 17:00):

because it has an obvious VM interpretation

#### Kenny Lau (Jun 15 2018 at 17:01):

but is it provable?

#### Mario Carneiro (Jun 15 2018 at 17:01):

but you can only prove it for I finite

#### Mario Carneiro (Jun 15 2018 at 17:01):

and even then I believe it implies decidable equality of I

#### 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?

#### 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

#### 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

#### 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

#### Mario Carneiro (Jun 15 2018 at 17:21):

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

#### Mario Carneiro (Jun 15 2018 at 17:21):

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

#### 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

#### Reid Barton (Jun 15 2018 at 17:23):

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

#### Mario Carneiro (Jun 15 2018 at 17:25):

So maybe just replacequot with quotient everywhere

#### Mario Carneiro (Jun 15 2018 at 17:25):

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

#### 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 _  #### 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? #### Kenny Lau (Jun 15 2018 at 19:24): by sending [[g]] to [[prod[x in G/H] s(x) g s(xg)^-1]]. #### Mario Carneiro (Jun 15 2018 at 19:24): Does [[g h]] = [[g]][[h]]? #### Kenny Lau (Jun 15 2018 at 19:25): yes #### Mario Carneiro (Jun 15 2018 at 19:25): Then don't the s(x) parts cancel? #### Kenny Lau (Jun 15 2018 at 19:25): @Kevin Buzzard #### 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) #### 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 #### Kenny Lau (Jun 15 2018 at 19:26): oh you can't do that, g is not in H #### Kenny Lau (Jun 15 2018 at 19:27): s(x) g s(xg)^-1 is in H #### Mario Carneiro (Jun 15 2018 at 19:27): I know, but they should still be equal as members of G #### Kenny Lau (Jun 15 2018 at 19:27): no, because H^ab is H/[H,H] #### 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. #### Kenny Lau (Jun 15 2018 at 21:17): I see. Then I'll just come up with a section noncomputably then. #### 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


:o

#### 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