Importing Specific Defintions

Stream: general

[Ross Truscott]

Hi there!

Super basic question here, Im learning Lean as part of a class and im trying to (re)prove Artin-Wedderburn, so I of course need to be able to talk about simple modules, but im not actually sure how to define a module to be simple. I guess part of this issue is that I am somewhat unsure of how to read the docs.

What I currently have written is,

import Mathlib.Algebra.Field.Defs
import Mathlib.Algebra.Module.Basic
import Mathlib.Algebra.Ring.Basic
import Mathlib.Data.Matrix.Basic
import Mathlib.Algebra.Ring.Equiv
import Mathlib.Algebra.DirectSum.Module

--Define a ring R and a simple R-module S.

variable (R : Type u_2) [Ring R] (S : Type u_4) [AddCommGroup S] [Module R S] extends
  IsSimpleOrder (Submodule R S) :
Prop

But im pretty sure this is just nonsense. Could any point me in the right direction? I do apologise, I realise this is very basic, but im feeling quite lost!

[metakuntyyy]

Would that help? https://leanprover-community.github.io/mathlib4_docs/Mathlib/RingTheory/SimpleModule/Basic.html#IsSimpleModule

[metakuntyyy]

In your case I guess it would be [IsSimpleModule R S]

[Ross Truscott]

Thats where I copied the code from, as I said I think this is an issue of me not really knowing how to read the docs. How can I, or have I, use the IsSimpleOrder thing to make S simple?

[metakuntyyy]

You just add it as a typeclass after [Module R S]

[Ross Truscott]

I tried that, but I get

Unknown identifier `IsSimpleModule`

Have I made a mistake with my imports?

[metakuntyyy]

That should work.

import Mathlib

universe u v

variable (R : Type u) [Ring R] (S : Type v) [AddCommGroup S] [Module R S] [IsSimpleModule R S]

[Ross Truscott]

Oh actually yes I think that's it, I dont think I actually have the definition imported (because I dont want to import Schurs lemma, which is in Mathlib.RingTheory.SimpleModule.Basic!) Anyway, thanks for your help, I appreciate that is super basic

[Ross Truscott]

Is it possible to import just the definition from Mathlib.RingTheory.SimpleModule.Basic? I tried Mathlib.RingTheory.SimpleModule.Basic.IsSimpleModule but it doesn't seem happy with that

[Ross Truscott]

I basically want the definitions from Mathlib.RingTheory.SimpleModule.Basic but none of the theorems, is there any way for me to do that?

[Ruben Van de Velde]

No

[Ross Truscott]

Is there a convenient way to copy the existing definitions from the library into my own project?

[Riccardo Brasca]

If you are OK with importing what Mathlib.RingTheory.SimpleModule.Basic depends on you can just copy/paste the definitions you want. But if you don't want to import mathlib at all I don't think there is a reasonable way to do it.

[Ross Truscott]

That may be what I'll need to do then hmm....

I'll import it for now and strip it back later I guess. Thanks!

[Kevin Buzzard]

Just import the theorems and don't use them. This is what my students do all the time

[metakuntyyy]

I guess it also depends on what theorems you expect as prerequisites.

[Ross Truscott]

I think my concern is that if I use simp for example, can I be sure that it isnt going to use any theorems that Id rather prove for myself? For example that package contains Schurs lemma, and Artin-Wedderburn, the latter being the ultimate goal for the project and the form something I had planned to prove along the way

[Kevin Buzzard]

Your optimism is great but I would not worry about this, you'll find that theorem proving is actually much harder than you think. You will be spelling out everything and simp only proves things which are mathematically trivial. You will be spelling out the proof in gory detail. I have been teaching undergraduates to do exactly this kind of thing for 4 years now. Trust me, just import everything and type in the proof you want to formalize, it works fine. You will not be accidentally proving anything difficult, quite the opposite; at the beginning of your Lean journey you will be banging your head against the wall failing to prove obvious things and no tactic will work.

[Kevin Buzzard]

In short, you will never see a tactic doing something which isn't totally trivial to do in a line of calculation on paper, if you're trying to prove Artin-Wedderburn.