Calle Sönne

feat(topology/category/profinite): Initial work to show that profinite sets are limits of finite discrete sets

3

Initial work to show that profinite sets are limits of finite discrete sets. Formalizes the diagram of discrete sets over which a given profinite set will be the limit, and...

feat(FiberCategory/Fibered): definition of a fibered category

1

We define the class `IsFibered p` which captures what it means for a functor `p : 𝒳 ⥤ 𝒮` to be a fibered category and add some basic API. To...

feat(FiberedCategory/HomLift): definition of IsHomLift

3

We define the notion `IsHomLift` which aims to provide API for working with equalities `p(\phi) = f` for a functor `p` and morphisms `\phi`, `f`. This API is extensively used...

feat(Limits/Shapes/Pullback): add pasting lemmas and API

1

This PR proves some additional pasting lemmas and adds some general API to pullbacks. This contribution was inspired by the AIM workshop "Formalizing algebraic geometry" in June 2024. --- These...

feat(Bicategory/Functorbicategory): define bicategory of pseudofunctors

3

This PR contains a definition of the bicategory of pseudofunctors, in the file `Bicategory/FunctorBicategory/Pseudo.lean`. It also moves the file `Bicategory/Functorbicategory.lean` to `Bicategory/FunctorBicategory/Oplax.lean`. --- - [x] depends on: #14028 - [...

feat(Bicactegory/NaturalTransformation): refactor strong natural transformations

2

This PR is a minor refactor of strong natural transformations. Previously, I had defined strong natural transformations between oplax functors. Now I specialize this directly to pseudofunctors and improve the...

feat(Bicategory/Oplax): Fix simp lemmas and renaming

2

This PR renames `OplaxNatTrans` to `OplaxTrans` and puts it in the `Oplax` namespace (as the should be oplax natural transformations also between lax functors). It also removes `@[simp]` from `OplaxTrans.id`...

chore(Bicategory): restructure oplax modifications

1

This PR moves Oplax modifications to its own file `Modification/Oplax.lean` and also moves `FunctorBicategory.lean` to `FunctorBicategory/Oplax.lean`. This will improve the file structure for later PRs generalizing these constructions to pseudofunctors....