Raymond

Stream: new members

[Patrick Massot]

I see a new mathematician online here! Hi Raymond!

[Kevin Buzzard]

A number theorist, no less!

[Patrick Massot]

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

[Sebastien Gouezel]

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

[Patrick Massot]

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:

[Jan-David Salchow]

+1 for manifolds

[Kevin Buzzard]

I think manifolds is a wonderful goal.

[Kenny Lau]

I thought @Patrick Massot warned us against manifolds

[Kevin Buzzard]

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

[Johan Commelin]

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

[Patrick Massot]

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]

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]

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]

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]

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

[Kevin Buzzard]

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]

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

[Kevin Buzzard]

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]

@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]

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]

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]

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

[Kenny Lau]

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

[Kenny Lau]

@Kevin Buzzard your file has been Kenny'd

[Kevin Buzzard]

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