Porting goals for Copenhagen master class

Stream: mathlib4

[Adam Topaz]

Hi All --
During the porting meeting yesterday @Scott Morrison asked what files we need to be ported before the Copenhagen masterclass in June (@Kevin Buzzard and I are planning to use Lean4).

I came up with the following:

1. https://leanprover-community.github.io/mathlib-port-status/file/category_theory/sites/dense_subsite
2. https://leanprover-community.github.io/mathlib-port-status/file/topology/category/CompHaus/projective
3. https://leanprover-community.github.io/mathlib-port-status/file/topology/category/Profinite/as_limit

Item 1 is already tracked by the port progress bot, while the main thing blocking the other two is Topology/Category/Top/Limits which has some issues under discussion here.

The only other thing that's absolutely required is the definition of projective objects, which is already underway in !4#3615
There are various other things from homological algebra that would be "nice to have", but the above what I think are essential.

[Scott Morrison]

Great! I have added CompHaus.projective and Profinite.as_limit to the port progress bot, and will do a one-off run on them them.

[Kevin Buzzard]

I'm actively working on dense_subsite by the way. !4#3605 is ready for review!

[Scott Morrison]

I pushed some minor changes.

[Scott Morrison]

There are two remaining TODOs which propose asking on github.

[Scott Morrison]

Could you do that / link to the topics from the PR?