Minimal axioms for Module

Stream: new members

[Martin C. Martin]

Group has .ofLeftAxioms and .ofRightAxioms to define a group structure
on a type with the minimum proof obligations. Is there something similar for Module, so I don't have to define all of:

example  {F : Type _} [Field F] {G : Type _} [AddCommGroup G] : Module F G where
  smul a v := sorry
  one_smul := sorry
  mul_smul := sorry
  smul_zero := sorry
  zero_smul := sorry
  smul_add := sorry
  add_smul := sorry

?

[Martin C. Martin]

Ideally just define:

  smul
  mul_smul : ∀ a b : F, ∀ v : V, (a * b) • v = a • b • v
  one_smul : ∀ v : V, (1 : F) • v = v
  smul_add : ∀ a : F, ∀ u v : V, a • (u + v) = a • u + a • v
  add_smul : ∀ a b : F, ∀ v : V, (a + b) • v = a • v + b • v

[Kevin Buzzard]

It might be a nice exercise to make such a constructor if one isn't already there.

[Martin C. Martin]

I guess all the helper function needs to generate is smul_zero and zero_smul.

[Julian Külshammer]

I had a similar exercise in a summer camp we had for lean with a handrolled vector space type in lean3: https://github.com/Julian-Kuelshammer/summer_maths_it_camp/blob/main/src/solutions/sheet03.lean

[Martin C. Martin]

And I guess those aren't true when we have an AddCommMonoid, but only when we have AddCommGroup? I think the standard proof uses a • 0 = a • 0 + a • 0, and you need neg to cancel?

[Martin C. Martin]

Ah there's Module.ofCore.

[Eric Wieser]

Perhaps we should move that into a MinimalAxioms file to match the others?

[Martin C. Martin]

Also, the others are called ofMinimalAxioms, except for Group where they're called ofLeftAxioms and ofRightAxioms. Would people be open to a PR that moved Module.ofCore to a MinimalAxioms file and renamed it ofMinimalAxioms?

[Martin C. Martin]

This would be a breaking change, in the sense that users who were depending on ofCore would need a new include, as well as to rename their call. How do we handle breaking changes? Are they ok on master?

[Johan Commelin]

mathlib master has breaking changes all the time. So that's not an issue

[Martin C. Martin]

Is there a starter guide for developing mathlib4? I forked, cloned, then did:

 rm -rf .lake; lake update && lake exe cache get

but the cache get fails with:

Downloaded: 0 file(s) [attempted 3979/3979 = 100%] (0% success)
Warning: some files were not found in the cache.
This usually means that your local checkout of mathlib4 has diverged from upstream.
If you push your commits to a branch of the mathlib4 repository, CI will build the oleans and they will be available later.
No cache files to decompress

What am I doing wrong?

[Martin C. Martin]

Then, when I start VS Code, it takes forever to rebuild imports, then errors out.

[Patrick Massot]

Where did you see you need to run lake update?

[Martin C. Martin]

I didn't, I guessed. :) Should I skip that?

[Patrick Massot]

Yes.

[Patrick Massot]

You can also skip removing the .lake folder if you just cloned.

[Patrick Massot]

Martin C. Martin said:

Is there a starter guide for developing mathlib4?

I forgot to answer that part: the answer is meant to be https://leanprover-community.github.io/contribute/index.html. If this isn't good enough then please tell us.

[Martin C. Martin]

Ah cool thanks.

[Martin C. Martin]

The video tutorial for creating a PR is for mathlib3. I'm watching it now, I'll let you know if I notice any significant differences.

[Martin C. Martin]

Although the title of the video does have OBSOLETE. :)

[Martin C. Martin]

It uses lakeproject, and is also about configuring git and VS code, not just about the PR part. Since there's no replacement video, maybe just remove that link? Or link to github's docs on creating a PR?

[Patrick Massot]

I will remove that sentence, and hope someone can record an updated video.

[Martin C. Martin]

Woohoo, my first pull request for Mathlib4!

https://github.com/leanprover-community/mathlib4/pull/8853