Structure Theorem

Stream: maths

[Ken Lee]

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]

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

[Ken Lee]

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]

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]

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]

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]

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

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

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]

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]

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]

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]

(commutative ring)

[Kevin Buzzard]

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

[Chris Hughes]

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