Mathlib4 PRs

Stream: Copenhagen Masterclass 2023

[Adam Topaz]

!4#4505

[Adam Topaz]

@Dagur Ásgeirsson @Kevin Buzzard

[Scott Morrison]

:octopus: and :tada: are nice, I guess, but how about a review? :-)

[Filippo A. E. Nuccio]

I have started one.

[Adam Topaz]

Thanks @Filippo A. E. Nuccio I'll take a look soon.

Anyway, here's a bit of additional motivation ;) !4#4527 (this last PR still needs some work, but the main constructions are there)

[Filippo A. E. Nuccio]

I'll have a look at that one as well.

[Adam Topaz]

Thanks, but I'm still working on this one. I need to move some things to the right place.

[Filippo A. E. Nuccio]

Oh, I see. Then I will wait and then have a look :smile: :hourglass:

[Adam Topaz]

Maybe a quick summary of this last PR: It has two key results:

theorem effectiveEpiFamily_tfae
    {α : Type} [Fintype α] {B : CompHaus.{u}}
    (X : α → CompHaus.{u}) (π : (a : α) → (X a ⟶ B)) :
    [ EffectiveEpiFamily X π
    , Epi (Sigma.desc π)
    , ∀ b : B, ∃ (a : α) (x : X a), π a x = b
    ].TFAE :=

and

instance : Precoherent CompHaus.{u} :=

And, of course, as a result:

namespace Condensed

def Condensed.{u} (C : Type _) [Category C] :=
  Sheaf (CoherentTopology CompHaus.{u}) C

instance {C : Type _} [Category C] : Category (Condensed.{u} C) :=
  show Category (Sheaf _ _) from inferInstance

end Condensed

[Adam Topaz]

At some point someone should write down a definition of coherent categories, and show that CompHaus is actually coherent (and that coherent implies precoherent)

[Adam Topaz]

!4#4527 should be ready for review (@Johan Commelin @Dagur Ásgeirsson @Kevin Buzzard )

[Adam Topaz]

I would have pinged you too Filippo, but you had already said you would review it ;)

[Adam Topaz]

Oh, I should add some refs in the condensed file... let me do that now.

[Adam Topaz]

refs added!

[Dagur Asgeirsson]

I’ll take a look in the morning! Don’t know if I’m a qualified reviewer though 😅

[Adam Topaz]

Next one is up: !4#4909

[Dagur Asgeirsson]

I've opened #5761, #5762, #5763

[Dagur Asgeirsson]

Once David's PR is done we can add more to the ExtrDisc folder and start working on getting the explicit descriptions of condensed sets into mathlib

[Riccardo Brasca]

Thanks! If you are in the mood of opening PR we have the comparison between product/coproduct in the opposite category that can go to mathlib

[Riccardo Brasca]

But I can do it during the weekend

[Adam Topaz]

I left a few comments.

[Dagur Asgeirsson]

@Riccardo Brasca I’m away over the weekend so you can do it 😅 also feel free to address Adam’s comments. But if you don’t have time I’ll do it on Monday

[Dagur Asgeirsson]

Adam Topaz said:

I left a few comments.

Thanks for the suggestions. I've pushed revised versions of all three PR's.

[Dagur Asgeirsson]

I added more to the ExtrDisc/Basic file, depending on Gleason: #5808

[Dagur Asgeirsson]

@Jon Eugster @Boris Kjær I've opened #5858, planning to do the same for ExtrDisc

[Dagur Asgeirsson]

It's Profinite/Epi and Profinite/Coherent from the Copenhagen repo put together into one file Mathlib/Topology/Category/Profinite/EffectiveEpi

[Jon Eugster]

Thx! I can fix all the stylistic things on that PR tonight or tomorrow. and also add Sina & Nima as coauthors

[Dagur Asgeirsson]

Ok great! I just looked at the commit history when I wrote the list of coauthors

[Dagur Asgeirsson]

I've already fixed the style errors the linter gave, if that's what you're talking about

[Dagur Asgeirsson]

#5861

[Jon Eugster]

I pushed the the cleanups I was thinking about to both PRs. Mostly whitespaces, docstrings and such

[Dagur Asgeirsson]

All the sorry-free files in the Copenhagen repo have been PR-ed to mathlib. All the content is in two PR's: #6731 and #6810, which depend on some smaller PR's. Reviews are very welcome! In particular, those that are in need of review right now are: #6750, #6774, #6779 and #6810.

[Dagur Asgeirsson]

I should say that the code in #6731 still needs to be cleaned up a lot, but the rest of the file depends on #6750 which I would like others' opinion on before continuing

[Riccardo Brasca]

@Dagur Asgeirsson I am still on vacation without a computer, I will have a look on Friday, but thanks a lot for all the work!

[Dagur Asgeirsson]

#6876 now makes a lot of the original code triplication redundant. It defines regular and extensive categories, the regular and extensive topologies and proves that their union generates the coherent topology for precoherent, regular and extensive categories.

[Dagur Asgeirsson]

#6810, #6877, and #6919 are ready for review, and I think #7421 can be merged

[Johan Commelin]

I merged #7421 and left a comment on #6877. Maybe others can chime in on the other 2 PRs?

[Johan Commelin]

I need to run to my next meeting.

[Dagur Asgeirsson]

The explicit description (#6731) is now finally ready for review!

[Johan Commelin]

Left a comment about namespaces