Zulip Chat Archive

Stream: maths

Topic: Basic finite groups


view this post on Zulip Kenny Lau (Jul 27 2018 at 04:24):

Do we have the symmetry group of order n!?

view this post on Zulip Mario Carneiro (Jul 27 2018 at 05:04):

There is perm (fin n), and you should be able to prove it is finite with the right cardinality using list.length_permutations

view this post on Zulip Kenny Lau (Jul 27 2018 at 05:05):

equiv.perm (fin n)

view this post on Zulip Kenny Lau (Jul 27 2018 at 05:15):

Do we have C_2 and in general C_n?

view this post on Zulip Kenny Lau (Jul 27 2018 at 05:15):

i.e. the cyclic group of order 2 and n

view this post on Zulip Kenny Lau (Jul 27 2018 at 05:20):

hmm, Lean doesn't know that equiv.perm and list.perm are the same thing, so it might be hard to use list.length_permutations...

view this post on Zulip Mario Carneiro (Jul 27 2018 at 05:26):

hm, I'll put that on the todo list

view this post on Zulip Johan Commelin (Jul 27 2018 at 07:14):

We have Z/nZ\mathbb{Z}/n\mathbb{Z}, right?

view this post on Zulip Kenny Lau (Jul 27 2018 at 07:14):

oh right that's in the not-mathlib

view this post on Zulip Kenny Lau (Jul 27 2018 at 07:15):

I don't think they proved that it is a group

view this post on Zulip Johan Commelin (Jul 27 2018 at 07:15):

Aaah, I didn't keep track of what exactly ended up in mathlib.

view this post on Zulip Kenny Lau (Jul 27 2018 at 07:15):

by "not-mathlib" I mean the initial library

view this post on Zulip Johan Commelin (Jul 27 2018 at 07:15):

I assumed it was a ring by now.

view this post on Zulip Kenny Lau (Jul 27 2018 at 07:16):

no, there's no algebraic structure of fin n proven

view this post on Zulip Johan Commelin (Jul 27 2018 at 07:17):

But Chris did a lot of stuff mod n, right?

view this post on Zulip Kenny Lau (Jul 27 2018 at 07:17):

ah

view this post on Zulip Johan Commelin (Jul 27 2018 at 07:17):

Anyway, got to run... some talk on K-theory and motives is calling me.

view this post on Zulip Kevin Buzzard (Jul 27 2018 at 08:04):

@Johan Commelin The problem with fin n (the subtype of N) is that addition and subtraction are defined in core Lean in...umm...not really the way that a mathematician would expect. Chris Hughes did a bunch of stuff mod n yes, but not with fin n.

view this post on Zulip Kenny Lau (Jul 27 2018 at 08:06):

@Kevin Buzzard I don't really understand the problem with fin n though

view this post on Zulip Kevin Buzzard (Jul 27 2018 at 08:08):

definition two : fin 4 := 2
definition three : fin 4 := 3
#reduce (two-three).val -- 0
#reduce (two+three).val -- 1

Addition rolls over, subtraction stops at 0. It's in core so can never be fixed. But of course one couls just define Zmodn n to be fin n and start again.

view this post on Zulip Kenny Lau (Jul 27 2018 at 08:08):

oh, the definition in core is wrong

view this post on Zulip Kevin Buzzard (Jul 27 2018 at 08:08):

right

view this post on Zulip Kenny Lau (Jul 27 2018 at 10:04):

import data.fintype data.equiv.basic

namespace list

@[simp] lemma length_attach {α} (L : list α) :
  L.attach.length = L.length :=
length_pmap

@[simp] lemma nth_le_attach {α} (L : list α) (i) (H : i < L.attach.length) :
  (L.attach.nth_le i H).1 = L.nth_le i (length_attach L  H) :=
calc  (L.attach.nth_le i H).1
    = (L.attach.map subtype.val).nth_le i (by simpa using H) : by rw nth_le_map'
... = L.nth_le i _ : by congr; apply attach_map_val

@[simp] lemma nth_le_range {n} (i) (H : i < (range n).length) :
  nth_le (range n) i H = i :=
option.some.inj $ by rw [ nth_le_nth _, nth_range (by simpa using H)]

attribute [simp] length_of_fn
attribute [simp] nth_le_of_fn

-- Congratulations, I proved that two things which have
-- equally few lemmas are equal.
theorem of_fn_eq_pmap {α n} {f : fin n  α} :
  of_fn f = pmap (λ i hi, f i, hi) (range n) (λ _, mem_range.1) :=
by rw [pmap_eq_map_attach]; from ext_le (by simp)
  (λ i hi1 hi2, by simp at hi1; simp [nth_le_of_fn f i, hi1])

theorem nodup_of_fn {α n} {f : fin n  α} (hf : function.injective f) :
  nodup (of_fn f) :=
by rw of_fn_eq_pmap; from nodup_pmap
  (λ _ _ _ _ H, fin.veq_of_eq $ hf H) (nodup_range n)

end list



variable (n : )

def Sym : Type :=
equiv.perm (fin n)

instance : has_coe_to_fun (Sym n) :=
equiv.has_coe_to_fun

@[extensionality] theorem Sym.ext (σ τ : Sym n)
  (H :  i, σ i = τ i) : σ = τ :=
equiv.ext _ _ H

instance : group (Sym n) :=
equiv.perm_group

section perm

variable {n}

def Sym.to_list (σ : Sym n) : list (fin n) :=
list.of_fn σ

theorem Sym.to_list_perm (σ : Sym n) :
  σ.to_list ~ list.of_fn (1 : Sym n) :=
(list.perm_ext
  (list.nodup_of_fn $ σ.bijective.1)
  (list.nodup_of_fn $ (1 : Sym n).bijective.1)).2 $ λ f,
by rw [list.of_fn_eq_pmap, list.of_fn_eq_pmap, list.mem_pmap, list.mem_pmap]; from
⟨λ _, f.1, by simp [f.2], fin.eq_of_veq rfl,
λ _, (σ⁻¹ f).1, by simp [(σ⁻¹ f).2], by convert equiv.apply_inverse_apply σ f;
  from congr_arg _ (fin.eq_of_veq rfl)⟩⟩

def list.to_sym (L : list (fin n))
  (HL : L ~ list.of_fn (1 : Sym n)) : Sym n :=
{ to_fun := λ f, list.nth_le L f.1 $
    by rw [list.perm_length HL, list.length_of_fn]; from f.2,
  inv_fun := λ f, list.index_of f L,
    begin
      convert list.index_of_lt_length.2 _,
      { rw [list.perm_length HL, list.length_of_fn] },
      { rw [list.mem_of_perm HL, list.mem_iff_nth_le],
        refine f.1, _, _⟩,
        { rw list.length_of_fn,
          exact f.2 },
        { apply list.nth_le_of_fn } }
    end,
  left_inv := λ f, fin.eq_of_veq $ list.nth_le_index_of
    ((list.perm_nodup HL).2 $ list.nodup_of_fn $ λ _ _, id) _ _,
  right_inv := λ f, list.index_of_nth_le $ list.index_of_lt_length.2 $
    (list.mem_of_perm HL).2 $ list.mem_iff_nth_le.2 $
    f.1, by rw list.length_of_fn; from f.2,
      list.nth_le_of_fn _ _⟩ }

@[simp] lemma list.to_sym_apply (L : list (fin n))
  (HL : L ~ list.of_fn (1 : Sym n)) (i) :
  (L.to_sym HL) i = L.nth_le i.1 (by simp [list.perm_length HL, i.2]) :=
rfl

@[simp] lemma Sym.to_list_to_sym (σ : Sym n) :
  σ.to_list.to_sym σ.to_list_perm = σ :=
Sym.ext _ _ _ $ λ i, fin.eq_of_veq $ by simp [Sym.to_list]

end perm

instance : decidable_eq (Sym n) :=
@function.injective.decidable_eq _ _ Sym.to_list _ $ λ σ τ h,
Sym.ext n _ _ $ λ i,
have H1 : σ.to_list.nth_le i.1 _ = _,
  from list.nth_le_of_fn _ _,
have H2 : τ.to_list.nth_le i.1 _ = _,
  from list.nth_le_of_fn _ _,
by rw [ H1,  H2]; congr; exact h

instance : fintype (Sym n) :=
fintype.of_list (list.pmap
  (λ L HL, list.to_sym L HL)
  (list.permutations (list.of_fn (1 : Sym n)))
  (λ _, (list.mem_permutations _ _).1)) $ λ σ,
list.mem_pmap.2 σ.to_list,
  (list.mem_permutations _ _).2 σ.to_list_perm,
  by simp

/-
theorem Sym.card : fintype.card (Sym n) = nat.fact n :=
calc  fintype.card (Sym n)
    = _ : _
... = (list.of_fn ((1 : Sym n) : fin n → fin n)).permutations.length : list.to_finset_card_of_nodup sorry
... = nat.fact (list.of_fn ((1 : Sym n) : fin n → fin n)).length : list.length_permutations _
... = nat.fact n : by simp
-/

view this post on Zulip Kenny Lau (Jul 27 2018 at 10:04):

@Mario Carneiro I think this all can go to mathlib

view this post on Zulip Kenny Lau (Jul 27 2018 at 10:17):

theorem Cayley (α : Type*) [group α] [fintype α] :
   f : α  Sym (fintype.card α), function.injective f  is_group_hom f :=
nonempty.rec_on (fintype.card_eq.1 $ fintype.card_fin $ fintype.card α) $ λ φ,
⟨λ x, ⟨λ i, φ.symm (x * φ i), λ i, φ.symm (x⁻¹ * φ i),
  λ i, by simp, λ i, by simp,
λ x y H, have H1 : _ := congr_fun (equiv.mk.inj H).1 (φ.symm 1), by simpa using H1,
⟨λ x y, Sym.ext _ _ _ $ λ i, by simp [mul_assoc]⟩⟩

view this post on Zulip Kenny Lau (Jul 27 2018 at 10:17):

Cayley's theorem :P

view this post on Zulip Kenny Lau (Jul 27 2018 at 10:19):

TODO: prove that your list of permutations has no duplicates

view this post on Zulip Kevin Buzzard (Jul 27 2018 at 10:26):

I think @Chris Hughes and @Morenikeji Neri were thinking about this sort of thing last week (they were interested in proving that the size of S_n was n!). Chris also defined the signature of a permutation -- it was interesting to think of a workable definition. Eventually we settled on sgn(σ)=(1)N(σ)sgn(\sigma)=(-1)^{N(\sigma)} where N(σ)N(\sigma) is the number of pairs (i,j)(i,j) with i<ji<j and σ(i)>σ(j)\sigma(i)>\sigma(j).

view this post on Zulip Kenny Lau (Jul 27 2018 at 10:26):

did they prove that it is a homomorphism?

view this post on Zulip Johan Commelin (Jul 27 2018 at 10:27):

@Johan Commelin The problem with fin n (the subtype of N) is that addition and subtraction are defined in core Lean in...umm...not really the way that a mathematician would expect. Chris Hughes did a bunch of stuff mod n yes, but not with fin n.

Right, but no-one said that C_n needed to have fin n as carrier type. I don't know what Chris used as carrier type, but I suppose one could use that. Or, like you suggest, just define C_n to be fin n, use that the definition is not reducible, and put new algebraic structures on it that behave properly.

view this post on Zulip Kevin Buzzard (Jul 27 2018 at 10:30):

did they prove that it is a homomorphism?

You need both that, and the fact that the signature of a transposition is -1. Neither are too hard ("in maths") and I would imagine that Chris could manage them in Lean, but I don't know if he did it.

view this post on Zulip Chris Hughes (Jul 27 2018 at 10:52):

I

did they prove that it is a homomorphism?

You need both that, and the fact that the signature of a transposition is -1. Neither are too hard ("in maths") and I would imagine that Chris could manage them in Lean, but I don't know if he did it.

I'm working on it now. After that I plan to find the product of disjoint cycles representation computably.

view this post on Zulip Kevin Buzzard (Jul 27 2018 at 10:56):

I know that this disjoint cycles result is presented to the first years as one of the highlights of the group theory course, but is it actually useful? I think the only reason they do this is that they have to do something group-ish and for some unknown reason they do not define homomorphisms of groups until the 2nd year at Imperial! All this will change with the new syllabus. This disjoint cycle stuff feels to me to be very much a product of a bygone era, when the classification was an active area of research (I suspect the course was written by one of the old school finite group theorists that used to work here).

view this post on Zulip Kevin Buzzard (Jul 27 2018 at 10:56):

OTOH maybe the philosophy is "do everything"

view this post on Zulip Chris Hughes (Jul 27 2018 at 15:06):

Maybe I won't do that then. I thought it would be cool to do a has_repr, for perm with disjoint cycle notation. I've proved sign is a hom, but not surjectivity yet.

view this post on Zulip Kevin Buzzard (Jul 27 2018 at 15:54):

I thought it would be cool to do a has_repr, for perm with disjoint cycle notation.

That is a good point! The other possibility for has_repr is just listing (sigma(1),sigma(2),...,sigma(n))but that is (a) unnecessarily big and (b) hard to interpret, so I'm not sure it's of much use. Go with disjoint cycles if you can face it -- making stuff look nice is important!

view this post on Zulip Kenny Lau (Jul 28 2018 at 11:13):

https://github.com/kckennylau/Lean/blob/master/Sym.lean

view this post on Zulip Kenny Lau (Jul 28 2018 at 11:13):

def Sym.equiv : Sym n  fin n.fact :=
nat.rec_on n Sym.equiv_0 $ λ n ih,
calc  Sym (n+1)
     (fin (n+1) × fin n.fact) : Sym.equiv_succ ih
...  fin (n+1).fact : fin_prod

instance : decidable_eq (Sym n) :=
equiv.decidable_eq_of_equiv Sym.equiv

instance : fintype (Sym n) :=
fintype.of_equiv _ Sym.equiv.symm

theorem Sym.card : fintype.card (Sym n) = nat.fact n :=
(fintype.of_equiv_card Sym.equiv.symm).trans $
fintype.card_fin _

view this post on Zulip Kenny Lau (Jul 28 2018 at 11:28):

@Mario Carneiro into which files should the content of my file go?

view this post on Zulip Kevin Buzzard (Jul 28 2018 at 11:41):

Mathematicians do a huge amount of work under various finiteness hypotheses. It's very easy to write down the definition of a vector space in Lean, but nobody ever proves theorems about vector spaces other than the most trivial things. The vector spaces that people care about have extra structure on, for example they're finite-dimensional, or they're separable Hilbert spares or whatever -- some extra finiteness assumptions. As a simple example, my students seem to need "order of the element divides the order of the group" a lot at the minute, and this is a theorem about finite groups. As a more complex example, a commutative ring is Noetherian if all its ideals are finitely-generated. I have a several-hundred-page-long book about etale cohomology which on page 1, when explaining assumptions and notation, says "all rings are assumed Noetherian". [and they're also all commutative].

This makes me wonder whether "finite group" should be promoted in the heierarchy, to be a class of its own, extending group, and that theorems about finite groups like "order of the element divides order of the group" and "Sym n is a finite group" could go in there.

view this post on Zulip Chris Hughes (Jul 28 2018 at 11:58):

What's the advantage of [finite_group G] over [fintype G] and [group G]? Bundling classes only really makes sense when there are fields that depend on both structures, like left_distrib depending on both monoid and add_monoid

view this post on Zulip Kevin Buzzard (Jul 28 2018 at 12:02):

Well I guess that's what I wanted to discuss. Could one not also ask what the advantage of [group G] was over [monoid G] and [has_inv G] and [has_mul_left_inv G] or some such question?

view this post on Zulip Kevin Buzzard (Jul 28 2018 at 12:04):

We decide that group is important somehow, important enough to have its own typeclass. I am suggesting that finite-dimensional vector spaces, finite groups and Noetherian rings are also important enough to have their own typeclasses because these are the things that people study in practice. A group is a basic foundational concept in mathematics but there are only a few theorems that you can prove about all groups without any hypotheses because a general group is extremely general.

view this post on Zulip Kevin Buzzard (Jul 28 2018 at 12:07):

I see. You are arguing that finite_group G should be interpreted as "group for which the underlying type is finite" because in some sense these are completely unrelated concepts. But a theorem like "order of the element divides the order of the group" depends on both structures. This is not a field though, it's a theorem. So is that the design principle? If you have 100 theorems about finite groups then that's not enough -- the user is expected to say "a group, for which the underlying set is finite" 100 times?

And of course there are 100 theorems about finite groups -- Sylow's theorems are just the tip of the iceberg Chris :-) The 3rd year group theory course (at least the one I took as an UG) was just 24 lectures of definitions and theorems about finite groups. Maybe that's changed now the landscape has changed, I'm not sure, but all our definitions of solvable, nilpotent etc were almost immediately implied to the finite group case, and only applied to that case.

view this post on Zulip Mario Carneiro (Jul 28 2018 at 12:25):

maybe group_theory? It's pretty basic, but I'm not sure about the restriction to fin n entailed here. Anything that doesn't mention Sym can go in its respective files

view this post on Zulip Kenny Lau (Jul 28 2018 at 14:48):

Let's say we want to define the signature/parity of the permutation. In which type should the signature/parity live?

view this post on Zulip Kevin Buzzard (Jul 28 2018 at 14:57):

That's an interesting question. I am not sure anyone ever adds signatures together. I would argue that mathematically it lives in an abstract group with two elements called +1 and -1. However the CS people might want to choose a concrete implementation of this group rather than building it from scratch I guess.

view this post on Zulip Kevin Buzzard (Jul 28 2018 at 14:58):

I will remark that the people defining quadratic residues / non-residues in my summer project just defined the values of the Legendre symbol to be integers.

view this post on Zulip Chris Hughes (Jul 28 2018 at 15:05):

I defined it to be an integer mod 2.

view this post on Zulip Chris Hughes (Jul 28 2018 at 15:07):

I imagine you probably want a group structure on the image, so you can prove it's a group_hom, and it's kernel is a subgroup etc.

view this post on Zulip Kenny Lau (Jul 28 2018 at 15:07):

right

view this post on Zulip Chris Hughes (Jul 28 2018 at 15:09):

Unfortunately, the add groups not being groups issue comes into play here.

view this post on Zulip Chris Hughes (Jul 28 2018 at 15:10):

And it would be nice if all tactics like finish also worked on anything isomorphic to Prop

view this post on Zulip Kenny Lau (Jul 28 2018 at 15:12):

then which group should i define it on?

view this post on Zulip Kevin Buzzard (Jul 28 2018 at 15:16):

the subtype of Z consisting of things which square to 1?

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

is that the best group?

view this post on Zulip Kevin Buzzard (Jul 28 2018 at 15:16):

What about an abstract group of order 2 equipped with a coercion to Z?

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

or maybe I should just create an inductive type

view this post on Zulip Kevin Buzzard (Jul 28 2018 at 15:17):

right

view this post on Zulip Kevin Buzzard (Jul 28 2018 at 15:17):

Maybe forget about the coercion to Z and see how long it takes people to complain.

view this post on Zulip Kenny Lau (Jul 28 2018 at 15:17):

why do we need coercion to Z?

view this post on Zulip Chris Hughes (Jul 28 2018 at 15:18):

It seems like the best thing is to choose a canonical group of order 2, and always use that for anything that requires a group of order 2. That group should be called either C2, or integers mod 2,

view this post on Zulip Kenny Lau (Jul 28 2018 at 15:18):

but we would also need Cn

view this post on Zulip Chris Hughes (Jul 28 2018 at 15:18):

Exactly.

view this post on Zulip Kenny Lau (Jul 28 2018 at 15:19):

and how would we build that?

view this post on Zulip Chris Hughes (Jul 28 2018 at 15:19):

But there's no point having C2 and some other group of order 2 with a different name

view this post on Zulip Kevin Buzzard (Jul 28 2018 at 15:20):

inductive mu2
| plus_one : mu2
| minus_one : mu2

open mu2

definition neg : mu2  mu2
| plus_one := minus_one
| minus_one := plus_one

instance : has_one mu2 := plus_one
instance : has_neg mu2 := neg

#check (-1 : mu2)
#check (1 : mu2)

view this post on Zulip Kenny Lau (Jul 28 2018 at 15:21):

ok

view this post on Zulip Kevin Buzzard (Jul 28 2018 at 15:21):

I think the group law for the target of the signature map is traditionally multiplication

view this post on Zulip Chris Hughes (Jul 28 2018 at 15:24):

But I think it's worth breaking with that tradition for the sake of only having one group of order 2 in lean to deal with.

view this post on Zulip Kenny Lau (Jul 28 2018 at 15:28):

section mu2

@[derive decidable_eq]
inductive mu2 : Type
| plus_one : mu2
| minus_one : mu2

open mu2

definition neg : mu2  mu2
| plus_one := minus_one
| minus_one := plus_one

instance : has_one mu2 := plus_one
instance : has_neg mu2 := neg

instance : comm_group mu2 :=
{ mul := λ x y, mu2.rec_on x (mu2.rec_on y 1 (-1)) (mu2.rec_on y (-1) 1),
  mul_assoc := λ x y z, by cases x; cases y; cases z; refl,
  mul_one := λ x, by cases x; refl,
  one_mul := λ x, by cases x; refl,
  inv := id,
  mul_left_inv := λ x, by cases x; refl,
  mul_comm := λ x y, by cases x; cases y; refl,
  .. mu2.has_one }

instance : fintype mu2 :=
{ elems := {1, -1},
  complete := λ x, mu2.cases_on x (or.inr $ or.inl rfl) (or.inl rfl) }

theorem mu2.card : fintype.card mu2 = 2 :=
rfl

end mu2

view this post on Zulip Kenny Lau (Jul 28 2018 at 15:28):

theorem mu2.card : fintype.card mu2 = 2 :=
rfl

view this post on Zulip Kenny Lau (Jul 28 2018 at 15:44):

instance : decidable_linear_order (fin n) :=
{ le_refl := λ i, hi, nat.le_refl i,
  le_trans := λ i, hi j, hj k, hk hij hjk, nat.le_trans hij hjk,
  le_antisymm := λ i, hi j, hj hij hji, fin.eq_of_veq $ nat.le_antisymm hij hji,
  le_total := λ i, hi j, hj, or.cases_on (@nat.le_total i j) or.inl or.inr,
  decidable_le := fin.decidable_le,
  .. fin.has_le, .. }

view this post on Zulip Johan Commelin (Jul 28 2018 at 17:36):

We want 2 cyclic groups of order n, one multiplicative, the other additive.

view this post on Zulip Johan Commelin (Jul 28 2018 at 17:38):

The mu_n example by Kevin will pop up a lot in number theory.

view this post on Zulip Johan Commelin (Jul 28 2018 at 17:38):

I suppose that Lean Forward is going to do quite a bit of number theory pretty soon.

view this post on Zulip Johan Commelin (Jul 28 2018 at 17:39):

And then additive cyclic groups also show up everywhere (e.g. integers mod n).

view this post on Zulip Johan Commelin (Jul 28 2018 at 17:41):

If R is a ring, do we already know that units R is a group? If R is in fact a field, then every finite subgroup of units R is a cyclic group. This is a cute theorem about (finite!) groups. And those cyclic groups are pretty multiplicative.

view this post on Zulip Kenny Lau (Jul 28 2018 at 18:52):

def Sym.is_valid (L : list (Sym n)) : Prop :=
 τ  L,  i j, i  j  τ = Sym.swap i j

Sym.list_swap_valid :  (σ : Sym ?M_1), Sym.is_valid (Sym.list_swap σ)

Sym.list_swap_prod :  (σ : Sym ?M_1), list.prod (Sym.list_swap σ) = σ

view this post on Zulip Kenny Lau (Jul 28 2018 at 18:52):

I proved constructively that every permutation can be written as the product of transpositions

view this post on Zulip Kenny Lau (Jul 28 2018 at 18:52):

I actually didn't know that it is possible with at most n transpositions

view this post on Zulip Kenny Lau (Jul 28 2018 at 18:52):

so I actually learnt (discovered) something new

view this post on Zulip Kenny Lau (Jul 28 2018 at 18:53):

I also learnt how to use well_founded.fix and well_founded.induction

view this post on Zulip Johan Commelin (Jul 28 2018 at 18:56):

You can do it with \le (n-1) transpositions, right?

view this post on Zulip Kenny Lau (Jul 28 2018 at 18:57):

yes

view this post on Zulip Kenny Lau (Jul 28 2018 at 18:57):

https://github.com/kckennylau/Lean/blob/master/Sym.lean

view this post on Zulip Johan Commelin (Jul 28 2018 at 18:57):

So now we only need disjoint cycle representation.

view this post on Zulip Kenny Lau (Jul 28 2018 at 18:57):

although I didn't prove the bound

view this post on Zulip Kenny Lau (Jul 28 2018 at 18:57):

no, we don't need DCR

view this post on Zulip Kenny Lau (Jul 28 2018 at 18:57):

it is way overrated

view this post on Zulip Johan Commelin (Jul 28 2018 at 18:57):

It is nice for printing stuff.

view this post on Zulip Kenny Lau (Jul 28 2018 at 19:03):

we should prove the homomorphism first

view this post on Zulip Johan Commelin (Jul 28 2018 at 19:06):

That shouldn't be too hard anymore, right?

view this post on Zulip Kenny Lau (Jul 28 2018 at 19:06):

no, that's a whole nother business

view this post on Zulip Kenny Lau (Jul 28 2018 at 19:06):

they involve completely different skills

view this post on Zulip Johan Commelin (Jul 28 2018 at 19:07):

What, the homomorphism?

view this post on Zulip Kenny Lau (Jul 28 2018 at 19:07):

yes

view this post on Zulip Johan Commelin (Jul 28 2018 at 19:07):

Hmmm, does it help if you change the definition of sgn?

view this post on Zulip Johan Commelin (Jul 28 2018 at 19:08):

Maybe not

view this post on Zulip Kenny Lau (Jul 28 2018 at 19:08):

you need to prove that if a bunch of transpositions multiply to 1, then you have an even number of transpositions

view this post on Zulip Kenny Lau (Jul 28 2018 at 19:08):

that involves somehow traversing the whole list

view this post on Zulip Johan Commelin (Jul 28 2018 at 19:09):

Fair enough

view this post on Zulip Kenny Lau (Jul 28 2018 at 19:10):

which I'm not exactly comfortable with doing in Lean

view this post on Zulip Kevin Buzzard (Jul 28 2018 at 19:15):

you need to prove that if a bunch of transpositions multiply to 1, then you have an even number of transpositions

AFAIK the best way to do this is to compute with signatures via the definition Chris used -- signature of sigma is (-1) ^ (the number of pairs (i,j) with i < j and sigma(i) > sigma(j) )

view this post on Zulip Kenny Lau (Jul 28 2018 at 19:15):

hmm, maybe

view this post on Zulip Kevin Buzzard (Jul 28 2018 at 19:34):

It's not so hard to prove that this is multiplicative. You can say that an unordered pair is "switched" if their order is switched -- this is well-defined. if sigma switches a pair and tau switches them back then the composite scores 0 and each of sigma and tau scores 1.

view this post on Zulip Chris Hughes (Jul 28 2018 at 19:36):

I have proved it's multiplicative, and that transpositions are odd. My proof that transpositions are conjugate was brilliant, I did split_ifs and then solved 84 goals at once with cc

view this post on Zulip Patrick Massot (Jul 28 2018 at 19:39):

I have a challenge for all the permutation experts. From a permutation of fin n (or any version) define a map from a product of n topological space to the permuted product and prove it's continuous. When n=2, this is continuous_id and continuous_swap. Part of the challenge is that A × B × C is not the type of triple (x.1, x.2, x.3), it's secretely A × (B × C) with elements (x.1, (x.2.1, x.2.2))

view this post on Zulip Patrick Massot (Jul 28 2018 at 19:40):

Note that I don't need this, I only want to make sure you don't get bored

view this post on Zulip Kenny Lau (Jul 28 2018 at 19:40):

can you give us the inputs? i.e. how is the n topological space represented?

view this post on Zulip Johan Commelin (Jul 28 2018 at 19:44):

I have proved it's multiplicative, and that transpositions are odd. My proof that transpositions are conjugate was brilliant, I did split_ifs and then solved 84 goals at once with cc

Hmm, that crazy number 84 really has some special place in mathematics... (https://en.wikipedia.org/wiki/Hurwitz%27s_automorphisms_theorem)

view this post on Zulip Kevin Buzzard (Jul 28 2018 at 20:23):

That's great! Somehow I'm surprised it's quite so many. You have the transposition (a b) and then you're trying to figure out whether the pair (i j) got re-aranged. So you have cases depending on whether i<a,i=a,a<i<b,i=b,i>b and the same with j. The clever thing is to get it so that the goals are solvable afterwards I guess, rather than just counting.

view this post on Zulip Chris Hughes (Jul 28 2018 at 20:28):

The proof had nothing to do with sign. This was the proof

lemma transpose_conj {α : Type*} [decidable_eq α] {a b x y : α}
  (hab : a  b) (hxy : x  y) :
   f : perm α, f * transpose x y * f⁻¹ = transpose a b :=
if x = b then transpose y a
else if y = a then transpose x b
else transpose x a * transpose y b, equiv.ext _ _ $ λ n,
begin
  unfold_coes,
  dsimp [transpose, inv_def, mul_def, equiv.symm, equiv.trans, function.comp],
  simp only [ite_apply, ite_inv_apply],
  split_ifs; cc
end

view this post on Zulip Kenny Lau (Jul 28 2018 at 20:29):

TIL unfold_coes

view this post on Zulip Patrick Massot (Jul 28 2018 at 20:51):

can you give us the inputs? i.e. how is the n topological space represented?

The example that I actually needed is at https://github.com/PatrickMassot/lean-perfectoid-spaces/blob/652422a5e5dd00f07ef3dc768bc774784904cb00/src/for_mathlib/topological_structures.lean#L7-L19

view this post on Zulip Kenny Lau (Jul 29 2018 at 06:30):

@Kevin Buzzard unfortunately this theorem is not true: sgn.inversion (σ * τ) i j = sgn.inversion τ i j * sgn.inversion σ (τ i) (τ j)

view this post on Zulip Kenny Lau (Jul 29 2018 at 06:30):

and it makes my life defining sign using inversion hard

view this post on Zulip Kenny Lau (Jul 29 2018 at 06:30):

def sgn.inversion (σ : Sym n) (i j : fin n) : mu2 :=
if i < j  σ i > σ j then -1 else 1

view this post on Zulip Kevin Buzzard (Jul 29 2018 at 09:55):

How about you define it on unordered pairs? Then it's ok

view this post on Zulip Kenny Lau (Jul 29 2018 at 09:55):

how do you define unordered pairs?

view this post on Zulip Chris Hughes (Jul 29 2018 at 09:58):

quotient

view this post on Zulip Kenny Lau (Jul 29 2018 at 09:58):

did you use quotient?

view this post on Zulip Chris Hughes (Jul 29 2018 at 09:58):

No. I used pairs such that x.2 > x.1

view this post on Zulip Kenny Lau (Jul 29 2018 at 09:58):

and you still managed to prove that it is multiplicative? :o

view this post on Zulip Chris Hughes (Jul 29 2018 at 09:59):

A lot of ite faffing

view this post on Zulip Kenny Lau (Jul 29 2018 at 09:59):

it's mainly the finset prod that I'm uncomfortable with

view this post on Zulip Kevin Buzzard (Jul 29 2018 at 10:01):

Also allow the possibility that i>j and sigma i < sigma j

view this post on Zulip Chris Hughes (Jul 29 2018 at 10:01):

I used sum_bij where the bij was one of the perms I was multiplying, subject to some ite faffing to get the order right.

view this post on Zulip Kenny Lau (Jul 29 2018 at 10:01):

ok

view this post on Zulip Chris Hughes (Jul 29 2018 at 10:01):

Also allow the possibility that i>j and sigma i < sigma j

Won't you always get even if you do that?

view this post on Zulip Kenny Lau (Jul 29 2018 at 10:02):

just prove that it is divisible by 2 and then divide by 2 :P

view this post on Zulip Kevin Buzzard (Jul 29 2018 at 10:03):

Or just count over unordered pairs :-)

view this post on Zulip Chris Hughes (Jul 29 2018 at 18:35):

Done product of transpositions as well. Not sure there was any point making the very last definition computable or not, but it might have some usage. https://github.com/dorhinj/leanstuff/blob/master/signatures.lean

view this post on Zulip Kenny Lau (Jul 29 2018 at 18:45):

https://github.com/kckennylau/Lean/blob/master/Sym.lean

def sgn (σ : Sym n) : mu2 :=
(-1) ^ σ.list_step.length

instance sgn.is_group_hom : is_group_hom (@sgn n) :=
begin
  constructor,
  intros σ τ,
  unfold sgn,
  rw [ pow_add,  list.length_append],
  rw [mu2.neg_one_pow, eq_comm, mu2.neg_one_pow],
  refine congr_arg _ _,
  apply length_mod_two_eq,
  simp
end

theorem sgn_step (s : step n) :
  sgn s.eval = -1 :=
suffices s.eval.list_step.length % 2 = [s].length % 2,
  by unfold sgn; rw [mu2.neg_one_pow, this]; refl,
length_mod_two_eq _ _ $ by simp

view this post on Zulip Kenny Lau (Jul 29 2018 at 18:46):

10 minutes behind you :-)

view this post on Zulip Kevin Buzzard (Jul 29 2018 at 18:46):

So now you can both define determinant of an n x n matrix!

view this post on Zulip Kenny Lau (Jul 29 2018 at 18:47):

oh no, we could already define determinant just fine, it's the multiplicative part that needs this result

view this post on Zulip Chris Hughes (Jul 29 2018 at 18:47):

Is your sign defined using the list of transpositions?

view this post on Zulip Kenny Lau (Jul 29 2018 at 18:47):

yes

view this post on Zulip Kenny Lau (Jul 29 2018 at 18:47):

oh, and trust me, do not look at Lines 720 - 831

view this post on Zulip Kenny Lau (Jul 29 2018 at 18:48):

https://github.com/kckennylau/Lean/blob/master/Sym.lean#L720

view this post on Zulip Kenny Lau (Jul 29 2018 at 18:48):

Is your sign defined using the list of transpositions?

def sgn (σ : Sym n) : mu2 :=
(-1) ^ σ.list_step.length

view this post on Zulip Kenny Lau (Jul 29 2018 at 18:48):

and list_step is a computable (!) function

view this post on Zulip Kenny Lau (Jul 29 2018 at 18:49):

def list_step (σ : Sym n) : list (step n) :=
by refine well_founded.fix list_step.aux.wf _ σ; from
λ σ ih, if H : σ.support =  then []
  else let i, hi := σ.support_choice H in
    step.mk' (σ i) i (support_def.1 hi)
    :: ih (swap (σ i) i * σ) (support_swap_mul hi)

view this post on Zulip Kenny Lau (Jul 29 2018 at 18:49):

by induction (recursion) on the support

view this post on Zulip Chris Hughes (Jul 29 2018 at 18:49):

What's it do?

view this post on Zulip Kenny Lau (Jul 29 2018 at 18:49):

it expresses a permutation as a product of transpositions

view this post on Zulip Kenny Lau (Jul 29 2018 at 18:51):

I just realized kernel of group hom is not in mathlib

view this post on Zulip Kenny Lau (Jul 29 2018 at 18:53):

(btw if anyone is reading my code, all my "choice" functions are computable :P)

view this post on Zulip Kevin Buzzard (Jul 29 2018 at 19:09):

I think kernel of a group hom is somewhere in mathlib...is_group_hom.ker?

view this post on Zulip Kenny Lau (Jul 29 2018 at 19:10):

ah right

view this post on Zulip Kenny Lau (Jul 29 2018 at 19:12):

def Alt : Type :=
is_group_hom.ker (@Sym.sgn n)

instance : group (Alt n) :=
by unfold Alt; apply_instance

view this post on Zulip Kevin Buzzard (Jul 29 2018 at 19:14):

You can now prove A_5 is simple by counting conjugacy classes.

view this post on Zulip Kenny Lau (Jul 29 2018 at 19:14):

hmm, not the proof of simple that i know

view this post on Zulip Kenny Lau (Jul 29 2018 at 19:14):

is there an easier proof?

view this post on Zulip Kevin Buzzard (Jul 29 2018 at 19:14):

oh no, we could already define determinant just fine, it's the multiplicative part that needs this result

Yes, in fact Keji did it already, by expanding along the top row. He could prove nothing about it from this definition :-)

view this post on Zulip Kenny Lau (Jul 29 2018 at 19:15):

how about Chris proving that any simple group must have order at least 60 lol

view this post on Zulip Kevin Buzzard (Jul 29 2018 at 19:16):

is there an easier proof?

You could use Sylow to prove that group of order strictly dividing 60 was solvable, and then there's some crappy trick with 3-cycles (which I used to set on the 2nd year group theory course) which shows that A_5 has no non-trivial cyclic quotients. The counting proof is pretty trivial! Any normal subgroup is a union of conjugacy classes but any non-trivial sum of conj class sizes doesn't even equal a divisor of 60.

view this post on Zulip Kenny Lau (Jul 29 2018 at 19:48):

2018-07-30.png

view this post on Zulip Kenny Lau (Jul 29 2018 at 19:48):

glorious

view this post on Zulip Kenny Lau (Jul 29 2018 at 19:48):

theorem eq_sgn (f : Sym n  mu2) [is_group_hom f]
  (s : step n) (H1 : f s.eval = -1) (σ : Sym n) :
  f σ = sgn σ :=
begin
  have H2 :  t : step n, f t.eval = -1,
  { intro t,
    by_cases H2 : s.1 = t.1,
    { by_cases H3 : s.2 = t.2,
      { rw [ step.ext _ _ H2 H3, H1] },
      have H4 : t.eval = swap s.2 t.2 * s.eval * swap s.2 t.2,
      { dsimp [step.eval, swap], ext k, dsimp,
        have := ne_of_lt s.3, have := ne_of_lt t.3,
        split_ifs; cc },
      simp [H4, is_group_hom.mul f, H1] },
    by_cases H3 : s.1 = t.2,
    { have H4 : t.eval = swap s.2 t.1 * s.eval * swap s.2 t.1,
      { dsimp [step.eval, swap], ext k, dsimp,
        have := ne_of_lt s.3, have := ne_of_lt t.3,
        split_ifs; cc },
      simp [H4, is_group_hom.mul f, H1] },
    by_cases H4 : s.2 = t.1,
    { have H5 : t.eval = swap s.1 t.2 * s.eval * swap s.1 t.2,
      { dsimp [step.eval, swap], ext k, dsimp,
        have := ne_of_lt s.3, have := ne_of_lt t.3,
        split_ifs; cc },
      simp [H5, is_group_hom.mul f, H1] },
    by_cases H5 : s.2 = t.2,
    { have H6 : t.eval = swap s.1 t.1 * s.eval * swap s.1 t.1,
      { dsimp [step.eval, swap], ext k, dsimp,
        have := ne_of_lt s.3, have := ne_of_lt t.3,
        split_ifs; cc },
      simp [H6, is_group_hom.mul f, H1] },
    have H6 : t.eval = swap s.1 t.1 * swap s.2 t.2 * s.eval * swap s.2 t.2 * swap s.1 t.1,
    { dsimp [step.eval, swap], ext k, dsimp,
      have := ne_of_lt s.3, have := ne_of_lt t.3,
      split_ifs; cc },
    rw H6,
    repeat { rw is_group_hom.mul f },
    rw [H1, mul_assoc (f (swap s.1 t.1)), mul_assoc (f (swap s.1 t.1))],
    rw [mu2.mul_neg_one, mu2.neg_mul_self], simp },
  have H3 := list_step_prod σ,
  revert H3, generalize : list_step σ = L, intro H3, subst H3,
  induction L with hd tl ih, { simp [is_group_hom.one f] },
  simp [is_group_hom.mul f, ih, H2]
end

view this post on Zulip Kenny Lau (Jul 29 2018 at 19:48):

@Kevin Buzzard @Chris Hughes

view this post on Zulip Kevin Buzzard (Jul 29 2018 at 19:49):

Ouch

view this post on Zulip Kenny Lau (Jul 29 2018 at 20:52):

I think I just discovered a uniform definition of a permutation that can conjugate (ab) to become (cd)

view this post on Zulip Kenny Lau (Jul 29 2018 at 20:52):

uniform as in doesn't rely on casing

view this post on Zulip Chris Hughes (Jul 29 2018 at 20:53):

How would you manage that?

view this post on Zulip Kenny Lau (Jul 29 2018 at 20:53):

exercise to the reader :P

view this post on Zulip Kenny Lau (Jul 29 2018 at 20:53):

to be fair, I did use swap, which relies on casing

view this post on Zulip Kenny Lau (Jul 29 2018 at 20:53):

swap a b swaps a and b regardless of whether they are distinct

view this post on Zulip Chris Hughes (Jul 29 2018 at 20:54):

That's easy then.

view this post on Zulip Chris Hughes (Jul 29 2018 at 20:54):

Probably

view this post on Zulip Kenny Lau (Jul 29 2018 at 20:54):

what's your answer?

view this post on Zulip Kenny Lau (Jul 29 2018 at 20:54):

oh btw a and b are distinct; and c and d are distinct

view this post on Zulip Chris Hughes (Jul 29 2018 at 20:57):

I give up

view this post on Zulip Chris Hughes (Jul 29 2018 at 20:57):

I can shorten a proof by a few lines if I work it out.

view this post on Zulip Kenny Lau (Jul 29 2018 at 20:58):

def eq_sgn_aux4 (s t : step n) : Sym n :=
swap (swap s.1 t.1 s.2) t.2 * swap s.1 t.1

theorem eq_sgn_aux3 (s t : step n) :
  eq_sgn_aux4 s t s.1 = t.1 :=
begin
  dsimp [eq_sgn_aux4, swap],
  have := ne_of_lt s.3,
  have := ne_of_lt t.3,
  simp, split_ifs; cc
end

theorem eq_sgn_aux2 (s t : step n) :
  eq_sgn_aux4 s t s.2 = t.2 :=
begin
  dsimp [eq_sgn_aux4, swap],
  simp
end

view this post on Zulip Chris Hughes (Jul 29 2018 at 20:58):

But also probably massively slow down cimpilation time

view this post on Zulip Kenny Lau (Jul 29 2018 at 20:58):

looks like I'm finally useful :P

view this post on Zulip Kevin Buzzard (Jul 29 2018 at 20:59):

(ac)(bd) conjugates (ab) into (cd). In general conjugating by g sends (abc) to (ga gb gc) and the same for products of cycles

view this post on Zulip Kenny Lau (Jul 29 2018 at 20:59):

your thing only works when we have more separation axioms

view this post on Zulip Kenny Lau (Jul 29 2018 at 20:59):

here we only know that a != b and c != d

view this post on Zulip Kevin Buzzard (Jul 29 2018 at 20:59):

No

view this post on Zulip Kenny Lau (Jul 29 2018 at 21:00):

wait what

view this post on Zulip Kenny Lau (Jul 29 2018 at 21:01):

ok now I'm shocked

view this post on Zulip Kenny Lau (Jul 29 2018 at 21:01):

I don't believe it

view this post on Zulip Kenny Lau (Jul 29 2018 at 21:02):

ah

view this post on Zulip Kenny Lau (Jul 29 2018 at 21:07):

/me finds a hole to hide from his embarrassment

view this post on Zulip Kenny Lau (Jul 29 2018 at 21:14):

in my defense, my definition is easier to work with

view this post on Zulip Kenny Lau (Jul 29 2018 at 21:15):

def eq_sgn_aux4 (s t : step n) : Sym n :=
swap (swap s.1 t.1 s.2) t.2 * swap s.1 t.1

theorem eq_sgn_aux3 (s t : step n) :
  eq_sgn_aux4 s t s.1 = t.1 :=
begin
  dsimp [eq_sgn_aux4, swap],
  have := ne_of_lt s.3,
  have := ne_of_lt t.3,
  simp, split_ifs; cc
end

theorem eq_sgn_aux2 (s t : step n) :
  eq_sgn_aux4 s t s.2 = t.2 :=
begin
  dsimp [eq_sgn_aux4, swap],
  simp
end

theorem eq_sgn_aux (s t : step n) :
  eq_sgn_aux4 s t * s.eval * (eq_sgn_aux4 s t)⁻¹ = t.eval :=
begin
  ext k,
  by_cases H1 : k = t.1,
  { subst H1,
    dsimp [step.eval],
    simp [equiv.symm_apply_eq.2 (eq_sgn_aux3 s t).symm, eq_sgn_aux2] },
  by_cases H2 : k = t.2,
  { subst H2,
    dsimp [step.eval],
    simp [equiv.symm_apply_eq.2 (eq_sgn_aux2 s t).symm, eq_sgn_aux3] },
  dsimp [step.eval, swap],
  simp [H1, H2, eq_sgn_aux2, eq_sgn_aux3]
end

theorem eq_sgn (f : Sym n  mu2) [is_group_hom f]
  (s : step n) (H1 : f s.eval = -1) (σ : Sym n) :
  f σ = sgn σ :=
begin
  have H2 :  t : step n, f t.eval = -1,
  { intro t,
    rw [ eq_sgn_aux s t],
    simp [is_group_hom.mul f, is_group_hom.inv f, H1] },
  have H3 := list_step_prod σ,
  revert H3, generalize : list_step σ = L, intro H3, subst H3,
  induction L with hd tl ih, { simp [is_group_hom.one f] },
  simp [is_group_hom.mul f, ih, H2]
end

view this post on Zulip Kenny Lau (Jul 29 2018 at 21:15):

@Chris Hughes did it help you?

view this post on Zulip Chris Hughes (Jul 29 2018 at 21:16):

If a = d then (ac)(bd)(ab)(bd)(ac) a = (ac)(ba)(ab)(ba)(ac) a = a != c = (cd) a. What's my mistake? I'm probably being an idiot.

view this post on Zulip Kenny Lau (Jul 29 2018 at 21:17):

hmm...

view this post on Zulip Kenny Lau (Jul 29 2018 at 21:21):

@Chris Hughes how did you find that counter-example?

view this post on Zulip Kevin Buzzard (Jul 29 2018 at 21:21):

(cd)a=a.

view this post on Zulip Kenny Lau (Jul 29 2018 at 21:21):

(cd)a = (ca)a = c

view this post on Zulip Kevin Buzzard (Jul 29 2018 at 21:22):

It's certainly true that if sigma sends x to y, then g sigma g^{-1} sends gx to gy.

view this post on Zulip Kenny Lau (Jul 29 2018 at 21:22):

yes, that is true

view this post on Zulip Chris Hughes (Jul 29 2018 at 21:22):

example :  x y a b : fin 3, x  y  a  b 
  transpose x b * transpose y a * transpose x y * (transpose x b * transpose y a)⁻¹ 
  transpose a b := dec_trivial

view this post on Zulip Kenny Lau (Jul 29 2018 at 21:22):

ah

view this post on Zulip Kenny Lau (Jul 29 2018 at 21:23):

relying on the automation

view this post on Zulip Kevin Buzzard (Jul 29 2018 at 21:23):

Oh ha ha (ac)(bd) is not the map sending a to c and b to d

view this post on Zulip Kevin Buzzard (Jul 29 2018 at 21:24):

The map that conjugates (ab) into (cd) is "anything sending a to c and b to d"

view this post on Zulip Kevin Buzzard (Jul 29 2018 at 21:24):

In fact the general solution is "either send a to c and b to d, or send a to d and b to c -- and do anything you like with everything else"

view this post on Zulip Chris Hughes (Jul 29 2018 at 21:31):

How briefly can you write down such a function?

view this post on Zulip Kenny Lau (Jul 29 2018 at 21:31):

I just did

view this post on Zulip Kenny Lau (Jul 29 2018 at 21:31):

def eq_sgn_aux4 (s t : step n) : Sym n :=
swap (swap s.1 t.1 s.2) t.2 * swap s.1 t.1

theorem eq_sgn_aux3 (s t : step n) :
  eq_sgn_aux4 s t s.1 = t.1 :=
begin
  dsimp [eq_sgn_aux4, swap],
  have := ne_of_lt s.3,
  have := ne_of_lt t.3,
  simp, split_ifs; cc
end

theorem eq_sgn_aux2 (s t : step n) :
  eq_sgn_aux4 s t s.2 = t.2 :=
begin
  dsimp [eq_sgn_aux4, swap],
  simp
end

theorem eq_sgn_aux (s t : step n) :
  eq_sgn_aux4 s t * s.eval * (eq_sgn_aux4 s t)⁻¹ = t.eval :=
begin
  ext k,
  by_cases H1 : k = t.1,
  { subst H1,
    dsimp [step.eval],
    simp [equiv.symm_apply_eq.2 (eq_sgn_aux3 s t).symm, eq_sgn_aux2] },
  by_cases H2 : k = t.2,
  { subst H2,
    dsimp [step.eval],
    simp [equiv.symm_apply_eq.2 (eq_sgn_aux2 s t).symm, eq_sgn_aux3] },
  dsimp [step.eval, swap],
  simp [H1, H2, eq_sgn_aux2, eq_sgn_aux3]
end

view this post on Zulip Chris Hughes (Jul 29 2018 at 21:32):

Why does swap have 3 arguments?

view this post on Zulip Chris Hughes (Jul 29 2018 at 21:32):

I see

view this post on Zulip Kenny Lau (Jul 29 2018 at 21:32):

it only has 2, then it is coerced to become a function

view this post on Zulip Kenny Lau (Jul 29 2018 at 21:38):

I finally proved that my step is a fintype

view this post on Zulip Kenny Lau (Jul 29 2018 at 21:39):

example :  s t : step 3,
  swap s.1 t.1 * swap s.2 t.2 * s.eval * swap s.2 t.2 * swap s.1 t.1
   t.eval :=
dec_trivial

view this post on Zulip Chris Hughes (Jul 29 2018 at 21:41):

What is step?

view this post on Zulip Kenny Lau (Jul 29 2018 at 21:41):

@[derive decidable_eq]
structure step : Type :=
(fst : fin n)
(snd : fin n)
(lt  : fst < snd)

view this post on Zulip Kenny Lau (Jul 29 2018 at 21:42):

it represents a transposition

view this post on Zulip Kenny Lau (Jul 29 2018 at 21:42):

https://github.com/kckennylau/Lean/blob/master/Sym.lean

view this post on Zulip Chris Hughes (Jul 29 2018 at 21:43):

I used something similar

def fin_pairs_lt (n : ) : finset (Σ a : fin n, fin n) :=
(univ : finset (fin n)).sigma (λ a, (range a.1).attach_fin
  (λ m hm, lt_trans (mem_range.1 hm) a.2))

view this post on Zulip Kevin Buzzard (Jul 29 2018 at 21:45):

The fact that if sigma sends x to y then g sigma g^{-1} sends gx to gy is a special case of "transport de structure". It's more easily seen if you generalise. If sigma is a permutation of a set X, and if g is a bijection between X and another set Y, then g identifies X and Y, so sigma transports over to a permutation of Y. The explicit formula for the permutation of Y is g sigma g^{-1}. If you think of g as a dictionary identifying X and Y, then a in X gets identified with ga in Y, and b in X gets identified with gb in Y. If sigma sends a to b, then the transported sigma sends ga to gb. The counterintuitive idea now is to imagine that X = Y and that g is not the identity map but perhaps some other bijection. If you think about things this way then the fact that e.g. conjugate permutations have the same cycle type becomes trivial.

view this post on Zulip Chris Hughes (Jul 29 2018 at 22:08):

I had to think about it like that when I defined sign on an arbitrary fintype, and not just fin. I used equiv_fin to define the sign, but I had to prove that sign did not depend on which equiv_fin I chose, which i used the conjugation property for by combining my two different equiv_fins together to make a perm and conjugating by that perm

view this post on Zulip Kenny Lau (Jul 30 2018 at 07:24):

theorem inversions_eq_sgn :  σ : Sym n, inversions σ = sgn σ :=
nat.cases_on n dec_trivial $ λ n,
nat.cases_on n dec_trivial $ λ n σ,
eq_sgn inversions (step01 n) inversions_step01 σ

view this post on Zulip Kevin Buzzard (Jul 30 2018 at 07:28):

example :  x y a b : fin 3, x  y  a  b 
  transpose x b * transpose y a * transpose x y * (transpose x b * transpose y a)⁻¹ 
  transpose a b := dec_trivial

Did this work out of the box? I was going to use it in my talk today! But

theorem A :  a b : fin 3, a = b := dec_trivial

doesn't work for me. Do I need an import?

view this post on Zulip Kenny Lau (Jul 30 2018 at 07:28):

maybe import fintype

view this post on Zulip Kenny Lau (Jul 30 2018 at 07:33):

this is interesting. fintype.decidable_exists_fintype isn't in the online Lean

view this post on Zulip Kenny Lau (Jul 30 2018 at 07:34):

it was added 18 days ago

view this post on Zulip Kevin Buzzard (Jul 30 2018 at 07:40):

Oh I think that might have been because of some other problem I had, which Chris fixed. Oh I remember -- it was for Ellen's dots and boxes project. She wanted to write basic definitions like "if the number of times this multiset contains 3 is at most 1, and if ..., then blah" and Lean was demanding decidability proofs. I asked why and Chris and Simon just fixed everything up so it worked.

view this post on Zulip Kenny Lau (Jul 30 2018 at 07:41):

'tis a small world

view this post on Zulip Kevin Buzzard (Jul 30 2018 at 07:42):

rofl I had a scratch file open with the "not working" theorem A, and I just imported analysis.topology.continuity to think about Patrick's comment about continuous being a class and it fixed my proof :-)

view this post on Zulip Kenny Lau (Jul 30 2018 at 07:42):

lol


Last updated: May 10 2021 at 07:15 UTC