## Stream: maths

### Topic: Structure Theorem

#### Ken Lee (Dec 01 2019 at 13:37):

I want to prove the structure theorem of finitely generated modules over a PID in Lean.
I'm trying to define free modules by isomorphic to direct sum R^n.
But I don't understand why in linear_algebra.direct_sum_module, the indexing type iota of a direct sum direct_sum iota beta needs to have decidable equality. In fact, I don't think I know what having "decidable equality" means, can someone explain please?

#### Patrick Massot (Dec 01 2019 at 14:41):

https://leanprover.github.io/theorem_proving_in_lean/type_classes.html#decidable-propositions is probably a good starting point

#### Ken Lee (Dec 01 2019 at 15:24):

For p : Prop, p is decidable is supposed to mean we can prove either p or \not p.
This is captured in Lean by the class decidable p since if
one has either hp : p or hnp : \not p, then one has an instance of decidable p.
So decidable_eq \iota means equality of terms in \iota is decidable?

#### Ken Lee (Dec 01 2019 at 15:43):

And the reason we care about decidable propositions is because
sometimes we want to define data depending on the validity of a proposition?
So for the case of index of direct sums... I'm not sure what this means :thinking:

#### Patrick Massot (Dec 01 2019 at 15:55):

In principle decidable instances could make things computable. But I don't anything about this. I simply fake decidability using classical.prop_decidable each time Lean complains.

#### Chris Hughes (Dec 01 2019 at 15:57):

I think that this should probably be changed in line with finsupp, and we should just use classical decidable equality for direct sum

#### Kevin Buzzard (Dec 01 2019 at 16:17):

@Ken Lee I think @Amelia Livingston has already made a start on this, maybe you want to talk to her on Thurs or before?

"Decidable equality" is a computer science thing. If you switch on classical mode (i.e. mathematician mode) like Patrick says then it becomes automatic, that's why you've not heard of it. I think that if you've got an up to date mathlib you can just type open_locale classical and then never have to worry about this again.

#### Ken Lee (Dec 01 2019 at 16:41):

@Kevin Buzzard Thanks for the fix. Yes, I have already talked with Amelia about this.
She said she's looking to restart and do the Smith Normal Form proof since they did it in Algebra 3.
I was thinking of doing the proof via splitting the module into free and torsion, splitting torsion into p-torsion submodules,
then doing structure theorem for p-torsion.

#### Kevin Buzzard (Dec 01 2019 at 16:43):

Ok great! The theorem will give you both the structure theorem for finite abelian groups and the Jordan canonical form which I think are the last two theorems from M2PM2 which need formalising

#### Ken Lee (Dec 01 2019 at 16:59):

Question about the definition of dimension of a vector space:
Why is it not defined as the cardinality of some basis? (It is defined as the minimal cardinality.)
The dimension theorem proves these definition match anyway.
In other words, is it bad if I defined rank of a free module as cardinality of just some basis?

#### Kevin Buzzard (Dec 01 2019 at 17:54):

Over the zero ring, the zero module has the basis {} and the basis {0}. But this is a bit of a pathological case.

#### Kevin Buzzard (Dec 01 2019 at 17:55):

For a non-zero ring, these definitions will all be equivalent so it doesn't matter (to me at least) which one you choose, although at some point I guess you'll have to prove that they're equivalent.

#### Reid Barton (Dec 01 2019 at 20:15):

(commutative ring)

#### Kevin Buzzard (Dec 01 2019 at 20:53):

Good point, I was proving this by reducing modulo a maximal ideal

#### Chris Hughes (Dec 01 2019 at 20:59):

Since bases are indexed now, there are infinite bases for the zero module over the zero ring.

Last updated: May 12 2021 at 07:17 UTC