Zulip Chat Archive

Stream: new members

Topic: Raymond


view this post on Zulip Patrick Massot (Feb 07 2019 at 20:26):

I see a new mathematician online here! Hi Raymond!

view this post on Zulip Kevin Buzzard (Feb 07 2019 at 21:11):

A number theorist, no less!

view this post on Zulip Patrick Massot (Feb 07 2019 at 21:12):

Sébastien, we really need to find how to attract more geometers...

view this post on Zulip Sebastien Gouezel (Feb 07 2019 at 21:49):

First we have to define manifolds and tangent bundles and de Rham cohomology.

view this post on Zulip Patrick Massot (Feb 07 2019 at 21:51):

I know... But, before you came here, I was the only geometer, so I started perfectoid spaces with Kevin and Johan instead. And now I teach 13 hours per week until April :exhausted:

view this post on Zulip Jan-David Salchow (Feb 07 2019 at 23:23):

+1 for manifolds

view this post on Zulip Kevin Buzzard (Feb 08 2019 at 00:29):

I think manifolds is a wonderful goal.

view this post on Zulip Kenny Lau (Feb 08 2019 at 00:55):

I thought @Patrick Massot warned us against manifolds

view this post on Zulip Kevin Buzzard (Feb 08 2019 at 00:57):

He just said it was interesting how much work there was in the details which he usually left to the students

view this post on Zulip Johan Commelin (Feb 08 2019 at 07:12):

Hoi @Raymond. Je bent ineens heel populair (-; :thumbs_up:

view this post on Zulip Patrick Massot (Feb 08 2019 at 08:02):

I thought Patrick Massot warned us against manifolds

I said we should do manifolds, but it's slightly more complicated than you may think. But really we should be finishing stuff, especially when we announced them everywhere. So I won't work on manifolds until perfectoid spaces are done. In the mean time, everybody is welcome to do calculus which is ridiculously missing and will block manifolds anyway.

view this post on Zulip Raymond (Feb 08 2019 at 08:57):

Hi all! I started learning lean after @David Holmes told me it was fun, and I am going through these problems on Kevin's website now. It still feels like a lot of trial-and-error, but I am slowly getting used to this.

view this post on Zulip Kevin Buzzard (Feb 08 2019 at 09:02):

I wrote those problems in about 5 seconds flat and I'm sure they're completely unbalanced. There is a certain art to it all. I have some time for Lean now but there are about 10 things I want to do, and making good teaching materials is one of them, but currently everything is a bit haphazard.

view this post on Zulip David Holmes (Feb 08 2019 at 13:50):

Hi @Raymond, nice to see you! I forgot I used the word `fun'... Actually, it was really fun after I got through the logic puzzles (a => b stuff). It was constructing the natural and the complex numbers that I really liked. I should play with this again...

view this post on Zulip Kevin Buzzard (Feb 08 2019 at 13:52):

I just spent an hour with a joint maths/computing student building group cohomology from scratch. We got as far as H^0 but she was just a learner so we went slowly.

import algebra.module

class G_module (G : Type*) [group G] (M : Type*)
  extends add_comm_group M, has_scalar G M :=
(id :  m : M, (1 : G)  m = m)
(mul :  g h : G,  m : M, g  (h  m) = (g * h)  m)
(linear :  g : G,  m n : M, g  (m + n) = g  m + g  n)

definition H0 (G : Type*) [group G] (M : Type*) [G_module G M]
:= {m : M //  g : G, g  m = m}

variables (G : Type*) [group G] (M : Type*) [G_module G M]

variables {G} {M}

lemma g_zero (g : G) : g  (0 : M) = 0 :=
begin
  have h : 0 + g  (0 : M) = g  0 + g  0,
    calc
    0 + g  (0 : M) = g  0 : zero_add _
    ...             = g  (0 + 0) : by rw [add_zero (0 : M)]
    ...         = g  0 + g  0 : G_module.linear g 0 0,
   symmetry,
   exact add_right_cancel h
end

lemma g_neg (g : G) (m : M) : g  (-m) = -(g m) :=
begin
  apply eq_neg_of_add_eq_zero,
  rw G_module.linear,
  rw neg_add_self,
  exact g_zero g
end

theorem H0.add_closed (m n : M)
  (hm :  g : G, g  m = m) (hn :  g : G, g  n = n) :
 g : G, g  (m + n) = m + n :=
begin
  intro g,
  rw G_module.linear,
  rw hm,
  rw hn,
end

definition H0.add_comm_group : add_comm_group (H0 G M) :=
{ add := λ x y, x.1 + y.1, H0.add_closed x.1 y.1 x.2 y.2,
  add_assoc := λ a b c, subtype.eq (add_assoc _ _ _),
  /- begin
    intros a b c,
    apply subtype.eq,
--    show a.val + b.val + c.val = a.val + (b.val + c.val),
    exact add_assoc _ _ _
  end ,-/
  zero := 0,g_zero,
  zero_add := λ a, subtype.eq (zero_add _),
  add_zero := λ a, subtype.eq (add_zero _),
  neg := λ x, ⟨-x.1, λ g, by rw [g_neg g x.1, x.2],
  add_left_neg := λ a, subtype.eq (add_left_neg _),
  add_comm := λ a b, subtype.eq (add_comm _ _)}

variables {N : Type*} [G_module G N]

variable (G)

definition G_module_hom (f : M  N) : Prop :=
 g : G,  m : M, f (g  m) = g  (f m)

lemma H0.G_module_hom (f : M  N) (h : G_module_hom G f) (g : G) (m : M)
(hm :  g : G, g  m = m):
g  f m = f m :=
begin
  rw h,
  rw hm g,
end

def H0_f (f : M  N) (hf : G_module_hom G f) : H0 G M  H0 G N :=
λ x, f x.1, λ g, H0.G_module_hom G f hf g x.1 x.2

lemma id.G_module_hom : G_module_hom G (id : M  M) :=
λ g m, rfl
/-begin
  intro g,
  intro m,
  refl,
end
-/

view this post on Zulip Kevin Buzzard (Feb 08 2019 at 13:54):

It just feels like the machine is holding your hand and nothing can go wrong. And what's really stupid is that for all I know, this is the first time, or perhaps one of the first times, people have done group cohomology in this formal proof setting. A lot of existing code in these systems is not this sort of masters level algebra.

view this post on Zulip Kevin Buzzard (Feb 08 2019 at 13:55):

@Kenny Lau I think all my lemmas and definitions are named very poorly.

view this post on Zulip Kevin Buzzard (Feb 08 2019 at 13:56):

I know the proofs are golfable but I realised that I couldn't really think of good lemma names on my feet and I didn't want to stop and start browsing through similar constructions because of time pressure

view this post on Zulip Kevin Buzzard (Feb 08 2019 at 13:57):

@David Holmes Kenny did H^1 for his 1st year project: https://github.com/kckennylau/local-langlands-abelian/blob/master/src/group_cohomology.lean -- as part of his work on formalising the local Langlands conjectures

view this post on Zulip Raymond (Feb 08 2019 at 16:50):

Hi @Raymond, nice to see you! I forgot I used the word `fun'... Actually, it was really fun after I got through the logic puzzles (a => b stuff). It was constructing the natural and the complex numbers that I really liked. I should play with this again...

O well, that was just my interpretation of what you were telling me.

The thing which confuses me a bit now are what things simp does and does not simplify. For my complex numbers some equalities are just the usual properties for the reals, but it sometimes does not recognise this as such.

view this post on Zulip Kevin Buzzard (Feb 08 2019 at 17:20):

Using simp is an art, and making it work with new structures that you make is even more than an art. It's a large database of results of the form A = B and P <-> Q, with the left hand side "more complicated" than the right hand side. The strategy, of course, is that if simp spots anything in the goal which is deemed "more complicated", it replaces it with the "less complicated" thing, and keeps going until it either gets stuck or ends up with something of the form X = X, in which case it proves it using reflexivity of equality :-) If you make a new thing, then you should make some "simp lemmas" (by proving them and tagging them with @[simp]) and you want to prove just the right things to take the argument in the direction you want it to go.

view this post on Zulip Kevin Buzzard (Feb 08 2019 at 17:20):

I don't think I understood simp well until I understood definitional equality.

view this post on Zulip Kenny Lau (Feb 08 2019 at 19:48):

import algebra.module group_theory.subgroup

class group_module (G : Type*) [group G] (M : Type*) [add_comm_group M] extends has_scalar G M :=
(one_smul :  m : M, (1 : G)  m = m)
(smul_smul :  g h : G,  m : M, g  (h  m) = (g * h)  m)
(smul_add :  g : G,  m n : M, g  (m + n) = g  m + g  n)

namespace group_module

variables {G : Type*} [group G] {M : Type*} [add_comm_group M] [group_module G M]

variables (M)
instance is_add_group_hom_smul (g : G) : is_add_group_hom (() g : M  M) :=
group_module.smul_add g

lemma smul_zero (g : G) : g  (0 : M) = 0 :=
is_add_group_hom.zero _
variables {M}

lemma smul_neg (g : G) (m : M) : g  (-m) = -(g  m) :=
is_add_group_hom.neg _ _

definition fixed_points (G : Type*) [group G] (M : Type*) [add_comm_group M] [group_module G M] : set M :=
{m : M |  g : G, g  m = m}

instance fixed_points.is_add_subgroup : is_add_subgroup (fixed_points G M) :=
{ add_mem := λ m n hm hn g, by rw [smul_add, hm g, hn g],
  zero_mem := smul_zero M,
  neg_mem := λ m hm g, by rw [smul_neg, hm g] }

definition H0 (G : Type*) [group G] (M : Type*) [add_comm_group M] [group_module G M] :=
fixed_points G M

instance H0.add_comm_group : add_comm_group (H0 G M) :=
{ add_comm := λ m n, subtype.eq $ add_comm _ _,
  .. @subtype.add_group _ _ _ fixed_points.is_add_subgroup }

end group_module

variables {G : Type*} [group G] {M : Type*} [add_comm_group M] [group_module G M]
variables {N : Type*} [add_comm_group N] [group_module G N]

variable (G)

def is_group_module_hom (f : M  N) : Prop :=
 g : G,  m : M, f (g  m) = g  (f m)

namespace is_group_module_hom
open group_module

def map_H0 (f : M  N) (hf : is_group_module_hom G f) (x : H0 G M) : H0 G N :=
f x.1, λ g, by rw [ hf, x.2]

lemma id.group_module_hom : is_group_module_hom G (id : M  M) :=
λ g m, rfl

end is_group_module_hom

view this post on Zulip Kenny Lau (Feb 08 2019 at 19:48):

@Kevin Buzzard your file has been Kenny'd

view this post on Zulip Kevin Buzzard (Feb 08 2019 at 20:26):

@Anca Ciobanu Above is a version which is much harder to understand :-)


Last updated: May 06 2021 at 22:13 UTC