C[0,1] is an \R module

Stream: new members

[Vasily Ilin]

I want to show that C[0,1] is an \R-module. GitHub copilot was able to handle the proof that it's a commutative monoid but not that it's a module. Can I get a hint please? I think I'm also not using the statement C01_comm_monoid correctly in C01_module. What is the correct syntax there? Thank you

import tactic -- imports all the Lean tactics
import linear_algebra.basis
import data.real.basic
import data.complex.basic
import data.complex.module

def C01 := { f : set.Icc (0:ℝ) 1 → ℝ | continuous f }

def C01_comm_monoid : add_comm_monoid C01 :=
{ add := λ f g, ⟨λ x, f.val x + g.val x, continuous.add f.property g.property⟩,
  add_assoc := λ f g h, subtype.eq (add_assoc _ _ _),
  zero := ⟨λ x, 0, continuous_const⟩,
  zero_add := λ f, subtype.eq (zero_add _),
  add_zero := λ f, subtype.eq (add_zero _),
  add_comm := λ f g, subtype.eq (add_comm _ _) }

def C01_module (C01_comm_monoid : add_comm_monoid C01) : module ℝ C01 :=
{ smul := λ a f, ⟨λ x, a * f.val x, continuous.mul continuous_const f.property⟩,
  one_smul := λ f, subtype.eq (one_mul _),
  mul_smul := λ a b f, subtype.eq (mul_assoc _ _ _),
  smul_add :=
    begin
      intros a f g,
      apply subtype.eq,
      ext x,
      sorry,
    end,
  smul_zero := λ a, subtype.eq (mul_zero _),
  add_smul := λ a b f, subtype.eq (add_mul _ _ _),
  zero_smul := λ f, subtype.eq (zero_mul _) }

[Moritz Doll]

you are aware of docs#continuous_map.module ?

[Vasily Ilin]

nope! I tried to find it in mathlib but could not. Lean is so daunting...

[Vasily Ilin]

Since I don't understand the mathlib statement though, I would rather prove it myself

[Vasily Ilin]

Actually, I have a different question. What is a good sequence of resources to learn Lean? I have tried the following:

1. I have solved (most of) the exercises in formalising-mathematics-2022 by Kevin Buzzard. Once everything is set up for me, the proofs are usually easy. It's the setting up part that I am struggling with.
2. I have tried formalizing Hopf algebras and showed that k[x] is a Hopf algebra. That was very hard and Leo Meyer did most of the heavy lifting.
3. I have tried formalizing "Linear algebra done right" but each exercise takes forever, and I got help from this server on most of them.

The only way to get better is to work through the book "Theorem Proving in Lean" but that is extremely not fun and a lot of the concepts seem not applicable to "normal" theorem proving. Maybe there is another resource that explains things like:

1. Difference between class, structure, instance, def, etc
2. How to find things in mathlib
3. Other things that are not just applying existing theorems inside a begin end block -- that seems to be the easy part.

[Jireh Loreaux]

I haven't fired up Lean, but I think at your sorry you'll want docs#mul_add

[Johan Commelin]

@Vasily Ilin Are you aware of the stuff at https://leanprover-community.github.io/learn.html ?

[Vasily Ilin]

I was not aware of that, Johan. Thank you!

[Kevin Buzzard]

That formalising-mathematics course isn't about filling in those sorries -- the guts of the course is people doing their own projects. Do a project, get stuck, ask for help!

[Kevin Buzzard]

@Vasily Ilin you were stuck because (C01_comm_monoid : add_comm_monoid C01) is wrong. Once you fix it by using the typeclass inference system, mul_add works fine.

import tactic -- imports all the Lean tactics
import linear_algebra.basis
import data.real.basic
import data.complex.basic
import data.complex.module

def C01 := { f : set.Icc (0:ℝ) 1 → ℝ | continuous f }

-- instance, not def
instance C01_comm_monoid : add_comm_monoid C01 :=
{ add := λ f g, ⟨λ x, f.val x + g.val x, continuous.add f.property g.property⟩,
  add_assoc := λ f g h, subtype.eq (add_assoc _ _ _),
  zero := ⟨λ x, 0, continuous_const⟩,
  zero_add := λ f, subtype.eq (zero_add _),
  add_zero := λ f, subtype.eq (add_zero _),
  add_comm := λ f g, subtype.eq (add_comm _ _) }

-- don't give the instance explicitly!
instance C01_module : module ℝ C01 :=
{ smul := λ a f, ⟨λ x, a * f.val x, continuous.mul continuous_const f.property⟩,
  one_smul := λ f, subtype.eq (one_mul _),
  mul_smul := λ a b f, subtype.eq (mul_assoc _ _ _),
  smul_add :=
    begin
      rintros a ⟨f, hf⟩ ⟨g, hg⟩,
      ext x,
      exact mul_add a (f x) (g x),
    end,
  smul_zero := λ a, subtype.eq (mul_zero _),
  add_smul := λ a b f, subtype.eq (add_mul _ _ _),
  zero_smul := λ f, subtype.eq (zero_mul _) }

[Kevin Buzzard]

The problem with your attempt is that (C01_comm_monoid : add_comm_monoid C01) creates a local variable called C01_comm_monoid and with no definition (it's just a constant). In particular it has nothing to do with the definition just above it, so the addition is just defined as "some addition exists" as opposed to the formula for addition you were giving above it.

[Vasily Ilin]

Thank you for such a detailed explanation!

[Eric Wieser]

Vasily Ilin said:

Since I don't understand the mathlib statement though, I would rather prove it myself

Is it the mathlib statement you don't understand, or is the "proof" (really, definition)?