group_equiv_left_cosets_times_subgroup

Stream: general

[Kenny Lau]

import data.equiv group_theory.coset

universe u

namespace quotient

variables {α : Type u} [s : setoid α]

def fibre : quotient s → set α :=
λ Q, {x | ⟦x⟧ = Q}

end quotient

namespace equiv

variables {α : Type u} [s : setoid α]

def equiv_fibre : α ≃ Σ Q : quotient s, quotient.fibre Q :=
⟨λ x, ⟨⟦x⟧, x, rfl⟩, λ x, x.2.1, λ x, rfl,
 λ ⟨Q, x, (hx : ⟦x⟧ = Q)⟩, sigma.eq hx $ by subst hx⟩

end equiv

variables {G : Type u} [group G] (S : set G) [is_subgroup S]

instance left_rel : setoid G :=
⟨λ x y, x⁻¹ * y ∈ S,
 λ x, by simp [is_submonoid.one_mem],
 λ x y hxy, have _ := is_subgroup.inv_mem hxy, by simpa using this,
 λ x y z hxy hyz, have _ := is_submonoid.mul_mem hxy hyz, by simpa [mul_assoc] using this⟩

def left_cosets' : Type u := quotient (left_rel S)

namespace is_subgroup

theorem fibre_equiv (L : left_cosets' S) : nonempty (quotient.fibre L ≃ S) :=
⟨⟨λ x, ⟨(quotient.out L)⁻¹ * x.1, quotient.exact ((quotient.out_eq L).trans x.2.symm)⟩,
  λ x, ⟨quotient.out L * x.1, eq.trans (eq.symm $ quotient.sound $ by simpa [(≈), setoid.r] using x.2) (quotient.out_eq L)⟩,
  λ ⟨x, hx⟩, subtype.eq $ by simp,
  λ ⟨x, hx⟩, subtype.eq $ by simp⟩⟩

theorem group_equiv_left_cosets_times_subgroup' : nonempty (G ≃ (left_cosets' S × S)) :=
⟨calc G
    ≃ Σ L : left_cosets' S, quotient.fibre L :
  equiv.equiv_fibre
... ≃ Σ L : left_cosets' S, S :
  equiv.sigma_congr_right (λ L, classical.choice $ fibre_equiv _ _)
... ≃ (left_cosets' S × S) :
  equiv.sigma_equiv_prod _ _ ⟩

end is_subgroup

[Kenny Lau]

@Mario Carneiro @Johannes Hölzl do you think this is better than the one in mathlib?

[Kenny Lau]

https://github.com/leanprover/mathlib/blob/master/group_theory/coset.lean

[Mario Carneiro]

I suggest skipping the nonempty here, there's not much point to it

[Kenny Lau]

it is uncomputable

[Mario Carneiro]

ok

[Kenny Lau]

but I'm making verseion 2 where that is computable

[Mario Carneiro]

just use noncomputable def instead

[Kenny Lau]

oh?

[Kenny Lau]

@Johannes Hölzl what do you think

[Mario Carneiro]

it's definitely a classical theorem, but wrapping in nonempty just means using choice later

[Johannes Hölzl]

I agree with Mario, using nonempty was a bad idea on my side.

[Kenny Lau]

ok

[Kenny Lau]

import data.equiv group_theory.coset

universe u

namespace quotient

variables {α : Type u} [s : setoid α]

def fibre : quotient s → set α :=
λ Q, {x | ⟦x⟧ = Q}

end quotient

namespace equiv

variables {α : Type u} [s : setoid α]

def equiv_fibre : α ≃ Σ Q : quotient s, quotient.fibre Q :=
⟨λ x, ⟨⟦x⟧, x, rfl⟩, λ x, x.2.1, λ x, rfl,
 λ ⟨Q, x, (hx : ⟦x⟧ = Q)⟩, sigma.eq hx $ by subst hx⟩

end equiv

variables {G : Type u} [group G] (S : set G) [is_subgroup S]

instance left_rel : setoid G :=
⟨λ x y, x⁻¹ * y ∈ S,
 λ x, by simp [is_submonoid.one_mem],
 λ x y hxy, have _ := is_subgroup.inv_mem hxy, by simpa using this,
 λ x y z hxy hyz, have _ := is_submonoid.mul_mem hxy hyz, by simpa [mul_assoc] using this⟩

def left_cosets' : Type u := quotient (left_rel S)

namespace is_subgroup

def fibre_equiv (g : G) : quotient.fibre ⟦g⟧ ≃ S :=
⟨λ x, ⟨x.1⁻¹ * g, quotient.exact x.2⟩,
 λ x, ⟨g * x⁻¹, quotient.sound $ by simpa [(≈), setoid.r] using x.2⟩,
 λ ⟨x, hx⟩, subtype.eq $ by simp,
 λ ⟨g, hg⟩, subtype.eq $ by simp⟩

noncomputable def group_equiv_left_cosets_times_subgroup' :
  G ≃ (left_cosets' S × S) :=
calc G ≃ Σ L : left_cosets' S, quotient.fibre L :
  equiv.equiv_fibre
    ... ≃ Σ L : left_cosets' S, quotient.fibre ⟦quotient.out L⟧ :
  equiv.sigma_congr_right (λ L, by simp)
    ... ≃ Σ L : left_cosets' S, S :
  equiv.sigma_congr_right (λ L, fibre_equiv _ _)
    ... ≃ (left_cosets' S × S) :
  equiv.sigma_equiv_prod _ _

end is_subgroup

[Kenny Lau]

version 2

[Kenny Lau]

who is Mitchell Rowett?

[Kevin Buzzard]

Student of Scott?

[Kevin Buzzard]

UG I think

[Kenny Lau]

would he/she mind if, you know, I basically refactor the whole thing

[Kevin Buzzard]

Isn't the logic of doing the non-empty version that you can go from that to the noncomputable version but you can't go back?

[Kenny Lau]

I don't get you

[Mario Carneiro]

full file refactorings are permitted in mathlib, you don't need permission from the original author (and conversely, be prepared for your work to be refactored to unrecognizability in the future)

[Kenny Lau]

@Mario Carneiro should I refactor coset?

[Johannes Hölzl]

Mitchel did the coset theory, the things your changing were mine. I think we can add a more general version of equiv_fibre:

namespace equiv

def equiv_fibre {α : Type*} {β : Type*} {f : α → β} : α ≃ Σb:β, f ⁻¹' {b} :=
⟨λa, ⟨f a, a, by simp⟩, λ x, x.2.1, λ x, rfl,
 λ ⟨b, a, hx⟩, have f a = b, by simpa using hx, sigma.eq this (by subst this; refl)⟩

end equiv

[Kenny Lau]

how do you make those red rectangles?

[Mario Carneiro]

```lean ... ```

[Johannes Hölzl]

I don't know were they come from. I just copied stuff from vs code.

[Kenny Lau]

I mean red rectangles

[Kenny Lau]

oh, lean

[Mario Carneiro]

the red rectangles are what happens when the syntax highlighter gets confused

[Kenny Lau]

@Johannes Hölzl did I tell you how much I hate {b}?

[Mario Carneiro]

On further review, I'm not sure it can be changed, the definition singleton a = insert a empty is in core.lean

[Johannes Hölzl]

@Kenny Lau you shouldn't depend too much on definitional equality. It breaks modularity of the library.

[Kenny Lau]

don't you like it when every theorem is just rfl?

[Johannes Hölzl]

Of course I like it, but I also hate it to not be able to change a definition because it would break 1000 places in mathlib.

[Kenny Lau]

import data.equiv group_theory.coset

universes u v

variables {α : Type u} {β : Type v} (f : α → β)

def fibre (y : β) : set α :=
{x | f x = y}

namespace equiv

def equiv_fibre : α ≃ Σ y : β, fibre f y :=
⟨λ x, ⟨f x, x, rfl⟩, λ x, x.2.1, λ x, rfl,
 λ ⟨y, x, (hx : f x = y)⟩, sigma.eq hx $ by subst hx⟩

end equiv

variables {G : Type u} [group G] (S : set G) [is_subgroup S]

instance left_rel : setoid G :=
⟨λ x y, x⁻¹ * y ∈ S,
 λ x, by simp [is_submonoid.one_mem],
 λ x y hxy, have _ := is_subgroup.inv_mem hxy, by simpa using this,
 λ x y z hxy hyz, have _ := is_submonoid.mul_mem hxy hyz, by simpa [mul_assoc] using this⟩

def left_cosets' : Type u := quotient (left_rel S)

namespace is_subgroup

def fibre_equiv (g : G) : fibre quotient.mk ⟦g⟧ ≃ S :=
⟨λ x, ⟨x.1⁻¹ * g, quotient.exact x.2⟩,
 λ x, ⟨g * x⁻¹, quotient.sound $ by simpa [(≈), setoid.r] using x.2⟩,
 λ ⟨x, hx⟩, subtype.eq $ by simp,
 λ ⟨g, hg⟩, subtype.eq $ by simp⟩

noncomputable def group_equiv_left_cosets_times_subgroup' :
  G ≃ (left_cosets' S × S) :=
calc G ≃ Σ L : left_cosets' S, fibre quotient.mk L :
  equiv.equiv_fibre quotient.mk
    ... ≃ Σ L : left_cosets' S, fibre quotient.mk ⟦quotient.out L⟧ :
  equiv.sigma_congr_right (λ L, by simp)
    ... ≃ Σ L : left_cosets' S, S :
  equiv.sigma_congr_right (λ L, fibre_equiv _ _)
    ... ≃ (left_cosets' S × S) :
  equiv.sigma_equiv_prod _ _

end is_subgroup

[Johannes Hölzl]

In Isabelle one can always change a definition, make it more general. And then just prove that it is the same.

[Kenny Lau]

Isabelle is crap

[Mario Carneiro]

be sure to have good reasons to make invective statements

[Kenny Lau]

it's nonconstructive

[Johannes Hölzl]

Well, your claim is also nonconstructive

[Kenny Lau]

so how is version 3?

[Johannes Hölzl]

I think we should stay with f ⁻¹' {b}.

[Mario Carneiro]

the other advantage of not giving the definition a name is we don't need to debate if it should be fibre or fiber :upside_down_face:

[Kenny Lau]

who cares about cosets of sub-not-groups?

[Mario Carneiro]

I guess Patrick might, that is the same as the translate of a set

[Kenny Lau]

why would he care?

[Mario Carneiro]

it relates to affine spaces and the group conjugation action. It also comes up with "neighborhoods of zero" in a topological group

[Kenny Lau]

singleton is really unusable

[Kenny Lau]

import data.equiv group_theory.coset

universes u v

namespace equiv

def equiv_fib {α : Type u} {β : Type v} (f : α → β) :
  α ≃ Σ y : β, {x // f x = y} :=
⟨λ x, ⟨f x, x, rfl⟩, λ x, x.2.1, λ x, rfl,
 λ ⟨y, x, (hx : f x = y)⟩, sigma.eq hx $ by subst hx⟩

end equiv

variables {G : Type u} [group G] (S : set G) [is_subgroup S]

instance left_rel : setoid G :=
⟨λ x y, x⁻¹ * y ∈ S,
 λ x, by simp [is_submonoid.one_mem],
 λ x y hxy, have _ := is_subgroup.inv_mem hxy, by simpa using this,
 λ x y z hxy hyz, have _ := is_submonoid.mul_mem hxy hyz, by simpa [mul_assoc] using this⟩

def left_cosets' : Type u := quotient (left_rel S)

namespace is_subgroup

def fib_equiv (g : G) : {x // ⟦x⟧ = ⟦g⟧} ≃ S :=
⟨λ x, ⟨x.1⁻¹ * g, quotient.exact x.2⟩,
 λ x, ⟨g * x⁻¹, quotient.sound $ by simpa [(≈), setoid.r] using x.2⟩,
 λ ⟨x, hx⟩, subtype.eq $ by simp,
 λ ⟨g, hg⟩, subtype.eq $ by simp⟩

noncomputable def group_equiv_left_cosets_times_subgroup' :
  G ≃ (left_cosets' S × S) :=
calc G ≃ Σ L : left_cosets' S, {x // ⟦x⟧ = L} :
  equiv.equiv_fib quotient.mk
    ... ≃ Σ L : left_cosets' S, {x // ⟦x⟧ = ⟦quotient.out L⟧} :
  equiv.sigma_congr_right (λ L, by simp)
    ... ≃ Σ L : left_cosets' S, S :
  equiv.sigma_congr_right (λ L, fib_equiv _ _)
    ... ≃ (left_cosets' S × S) :
  equiv.sigma_equiv_prod _ _

end is_subgroup

[Kenny Lau]

conflict between fibre and fiber resolved :P

[Chris Hughes]

Slightly shortened.

def equiv_fib {α : Type u} {β : Type v} (f : α → β) :
  α ≃ Σ y : β, {x // f x = y} :=
⟨λ x, ⟨f x, x, rfl⟩, λ x, x.2.1, λ x, rfl,
 λ ⟨y, x, ⟨hx⟩⟩, rfl⟩

[Kenny Lau]

you win

[Mario Carneiro]

it's a bit weird to write ⟨hx⟩ in the last bit there, since it's refl. Use λ ⟨_, x, rfl⟩, rfl instead

[Kenny Lau]

wait, how does that also work :o

[Kenny Lau]

oh, automatic casing