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

[callesonne]

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 define IsFibered, we also define cartesian arrows with respect to p as the structure IsCartesian. We also prove some basic results about cartesian arrows. See the repository Stacks-project for more WIP on fibered categories using these definitions.

Co-authored-by: Paul Lezeau [email protected]

---

• [ ] depends on: #12978

[grunweg]

Let me label this with awaiting-review --- since I presume that, once the dependent PR is merged, you'd like a review :-) awaiting-review

[callesonne]

I also have a question about design approach @joelriou . In https://github.com/Paul-Lez/Stacks-project, we have a notion of BasedCategory defined as follows:

/-- A based category over `𝒮` is a category `𝒳` together with a functor `p : 𝒳 ⥤ 𝒮` -/
structure BasedCategory (𝒮 : Type u₁) [Category.{v₁} 𝒮] where
  (cat : Type u₂)
  [isCat : Category.{v₂} cat]
  (p : cat ⥤ 𝒮)

We developed this as a preliminary step to dealing with functors between different fibered categories, and we showed that BasedCategory 𝒮 forms a strict bicategory. Now, do you think it could be good to rewrite the code defining IsFibered and IsCartesian to use 𝒳 : BasedCategory 𝒮 as a parameter instead of p : 𝒳 ⥤ 𝒮? Or is it unecessary to lock p inside 𝒳 : BasedCategory 𝒮, since we don't talk about functors between (pre-)fibered categories in this PR anyways?

[callesonne]

Here is an update on this PR. I have split it into 4 smaller PRs. This one now only concerns the definition of a fibered category, defined as in SGA, and also an alternate constructor for using the definition as in e.g. Stacks project.

[github-actions[bot]]

PR summary c01f68f57f

Import changes for modified files

No significant changes to the import graph

Import changes for all files

Files	Import difference

---

Declarations diff

+ Functor.IsFibered + instance (p : 𝒳 ⥤ 𝒮) [p.IsFibered] {R S T : 𝒮} (f : R ⟶ S) (g : S ⟶ T) {a b c : 𝒳} (φ : a ⟶ b) + isStronglyCartesian_of_exists_isCartesian + isStronglyCartesian_of_isCartesian + of_exists_isStronglyCartesian + pullbackPullbackIso ++ domainUniqueUpToIso_hom_isHomLift ++ domainUniqueUpToIso_inv_isHomLift

You can run this locally as follows

## summary with just the declaration names:
./scripts/declarations_diff.sh <optional_commit>

## more verbose report:
./scripts/declarations_diff.sh long <optional_commit>

The doc-module for script/declarations_diff.sh contains some details about this script.

[mathlib4-dependent-issues-bot]

This PR/issue depends on:

• ~~leanprover-community/mathlib4#13416~~
• ~~leanprover-community/mathlib4#13410~~
• ~~leanprover-community/mathlib4#13393~~
• ~~leanprover-community/mathlib4#12978~~ By Dependent Issues (🤖). Happy coding!

[kbuzzard]

Thanks! Note the whitespace comment.

bors d+ joelriou

[mathlib-bors[bot]]

:v: callesonne can now approve this pull request. To approve and merge a pull request, simply reply with bors r+. More detailed instructions are available here.

[mattrobball]

Oops. Meant to delegate to @joelriou

bors d-

[mattrobball]

See if this syntax works

bors d+=joelriou

[mathlib-bors[bot]]

:v: callesonne can now approve this pull request. To approve and merge a pull request, simply reply with bors r+. More detailed instructions are available here.

[jcommelin]

bors d=joelriou

[mathlib-bors[bot]]

:v: joelriou can now approve this pull request. To approve and merge a pull request, simply reply with bors r+. More detailed instructions are available here.

[kbuzzard]

@joelriou are you happy with this now?

[joelriou]

Thanks!

bors merge

[mathlib-bors[bot]]

Pull request successfully merged into master.

Build succeeded:

• Build
• Lint style