## Stream: new members

### Topic: Raymond

#### Patrick Massot (Feb 07 2019 at 20:26):

I see a new mathematician online here! Hi Raymond!

#### Kevin Buzzard (Feb 07 2019 at 21:11):

A number theorist, no less!

#### Patrick Massot (Feb 07 2019 at 21:12):

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

#### Sebastien Gouezel (Feb 07 2019 at 21:49):

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

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

+1 for manifolds

#### Kevin Buzzard (Feb 08 2019 at 00:29):

I think manifolds is a wonderful goal.

#### Kenny Lau (Feb 08 2019 at 00:55):

I thought @Patrick Massot warned us against manifolds

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

#### Johan Commelin (Feb 08 2019 at 07:12):

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

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

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

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

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

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

lemma g_neg (g : G) (m : M) : g • (-m) = -(g• m) :=
begin
rw ←G_module.linear,
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

{ add := λ x y, ⟨x.1 + y.1, H0.add_closed x.1 y.1 x.2 y.2⟩,
/- begin
intros a b c,
apply subtype.eq,
--    show a.val + b.val + c.val = a.val + (b.val + c.val),
end ,-/
zero := ⟨0,g_zero⟩,
neg := λ x, ⟨-x.1, λ g, by rw [g_neg g x.1, x.2]⟩,

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


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

#### Kevin Buzzard (Feb 08 2019 at 13:55):

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

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

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

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

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

#### Kevin Buzzard (Feb 08 2019 at 17:20):

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

#### 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) :=

lemma smul_zero (g : G) : g • (0 : M) = 0 :=
variables {M}

lemma smul_neg (g : G) (m : M) : g • (-m) = -(g • m) :=

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}

{ 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

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


#### Kenny Lau (Feb 08 2019 at 19:48):

@Kevin Buzzard your file has been Kenny'd

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