computability using set supports

Stream: Berkeley Lean Seminar

[Yakov Pechersky]

@Aaron Anderson Even though I mentioned in a Github comment that I closed the set typed perm.support because of your dec_trivial, I still went and did the work to make sure it still works. You can check branch#pechersky/perm-support-refactor, group_theory.specific_groups.alternating compiles without having to change the dec_trivial step

[Yakov Pechersky]

Some of the proofs got simpler, and I bet some of the juggling you had to do with (f : {x // x ∈ (σ.support : set α)} ≃ {x // x ∈ (τ.support : set α)}) can get much neater

[Yakov Pechersky]

I didn't do much refactoring to remove fintype

[Yakov Pechersky]

Just wanted to check that dec_trivial still works

[Yakov Pechersky]

So if you and co agree, we can do it piece by piece. I also hope that for the solvability, after I actually get the form_perm working, you'll be able to express all of this cleaner.

[Aaron Anderson]

That’s great. I bet that the explicit calculations will get easier with form_perm, but I’m still pleased that this way works.

[Yakov Pechersky]

So I think, if possible, we get the file separation refactor merged when we can, then try to go the finset -> set refactor on top of that. The branch shows that it is possible with the current state of master (and your PR), but that branch has all sorts of cruft on it -- it'll be easier to start anew

[Yakov Pechersky]

Additionally, we can choose to keep all of them statements about card on fintype underlying types, and transfer those over to the more general case later as well.

[Yakov Pechersky]

One way to do this would be to have an initial helper lemma stating that on a fintype, perm.support (the set version), when coerced via set.to_finset, is equal to the current definition that uses finset.univ.filter.