feat: The Preliminaries for Locally Cartesian Closed Categories

[sinhp]

See #21525

This PR defines the basic preliminaries for defining locally cartesian closed categories (LCCCs): Over.Sigma, Over.Reindex are short-hands for object part of the action of Over.map and Over.pullback. These are useful for developing consistent notations for locally cartesian closed categories (lcccs). The basic API of Over.Sigma (push) and Over.Reindex (pull) is developed and we prove that pull-push is isomorphic to the cartesian binary product in the slices. In fact, we prove the stronger statement, namely that the pull-push composition (Over.pullback Y.hom) ⋙ (Over.map Y.hom) is naturally isomorphic to the left tensor product functor Y × _ in Over X. This is going to be crucial in our mate-based approach to lcccs.

Also, using the calculus of mates we define certain natural isomorphisms involving Over.star and Over.pullback which will be used in defining the right adjoint to the pullback functor in the development of LCCCs.

---

[github-actions]

PR summary 5da820350a

Import changes for modified files

No significant changes to the import graph

Import changes for all files

Files	Import difference
Mathlib.CategoryTheory.LocallyCartesianClosed.Prelim (new file)	760

---

Declarations diff

+ ChosenPullback
+ Functor.toOverTerminal
+ Over.sigmaReindexNatIsoTensorLeft
+ Over.sigmaReindexNatIsoTensorLeft_hom_app
+ counit_app
+ equivOverTerminal
+ homEquiv
+ homEquiv_symm
+ instance (X : C) : CartesianMonoidalCategory (Over X) := by
+ instance [HasBinaryProducts C] : (forget X).IsLeftAdjoint := ⟨_, ⟨forgetAdjStar X⟩⟩
+ instance [HasBinaryProducts C] : (star X).IsRightAdjoint := ⟨_, ⟨forgetAdjStar X⟩⟩
+ instance {Y X : C} (f : Y ⟶ X) [h : HasPullbacksAlong f] : ChosenPullback f
+ isBinaryProductSigmaReindex
+ iteratedSliceBackward_forget
+ mapPullackIsoProd
+ mapPullackIsoProd'
+ mapPullackIsoProd_hom_comp_fst
+ mapPullackIsoProd_hom_comp_snd
+ pullback_def
+ pullback_hom
+ pullback_map
+ reindexFst
+ reindexFst_left
+ reindexSnd
+ reindexSnd_homMk_pullback_fst
+ reindexSnd_left
+ sigma_def
+ sigma_hom
+ sigma_map
+ starIsoToOverTerminal
+ starIteratedSliceForwardIsoPullback
+ starPullbackIsoStar
+ star_map
+ unit_app

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.

---

No changes to technical debt.

You can run this locally as

./scripts/technical-debt-metrics.sh pr_summary

• The relative value is the weighted sum of the differences with weight given by the inverse of the current value of the statistic.
• The absolute value is the relative value divided by the total sum of the inverses of the current values (i.e. the weighted average of the differences).

[joelriou]

Just a few quick remarks for now:

• the additions to Comma.Over.Pullback should probably go in a separate file, because it is already quite long, and it seems it has strange side effects on an unrelated file Galois/Examples;
• the assumption HasPullbacks is weakened in PRs by @Jlh18 (see [Merged by Bors] - refactor: weaken HasPullbacks to HasPullback in Over.Pullback #29795), so that some coordination about the changes to be made should happen;
• I am not sure exactly where/when this remark should be made again, but I think @jcommelin had suggested that at some point we should allow "chosen pullbacks" (which I understand by saying that for a morphism f we could have a ChosenPullback f typeclass with the data of a choice of functor between Over categories that is right adjoint to the obvious functor), I think it is important for future computations.

[sinhp]

Just a few quick remarks for now:

• the additions to Comma.Over.Pullback should probably go in a separate file, because it is already quite long, and it seems it has strange side effects on an unrelated file Galois/Examples;

What about making a new file in the new folder LocallyCartesianClosed named "Prelim.lean"? Otherwise, please suggest a location for this. The effect on Galois/Examples is indeed strange, but I don't think it's gonna be resolved just by changing the file name.
We had a discussion about this on Zulip here:
https://leanprover.zulipchat.com/#narrow/channel/144837-PR-reviews/topic/.2321525.20Locally.20Cartesian.20Closed.20Categories/near/498346104

• the assumption HasPullbacks is weakened in PRs by @Jlh18 (see refactor: weaken HasPullbacks to HasPullback in Over.Pullback #29795), so that some coordination about the
  changes to be made should happen;

@Jlh18 , Is this close to being merged? Seems this is weaker assumption for a couple of theorems in lccc prelim.

• I am not sure exactly where/when this remark should be made again, but I think @jcommelin had suggested that at some point we should allow "chosen pullbacks" (which I understand by saying that for a morphism f we could have a ChosenPullback f typeclass with the data of a choice of functor between Over categories that is right adjoint to the obvious functor), I think it is important for future computations.

We already have cartesian monoidal category structure on slice categories thanks to Andrew's work – incidentally one reason the LCCC work got merge conflict back in February, and had to wait for that work to be done. But, it is nicer to do it that way. I am using this monoidal structure. If I don't misread what you say, then ChosenPullback f for every f also gives a cartesian monoidal structure on slices.

Also, on the semantics side, I think with ChosenPullback f the codomain fibration will be a a cloven fibration, whereas with HasPullbacks you have a general Grothendieck fibration. I think the codomain functor for LCCCs is a general Grothendieck fibration not necessarily a cloven one. So, in a way Π f, ChosenPullback f results in a stricter semantics.

[joelriou]

• the additions to Comma.Over.Pullback should probably go in a separate file, because it is already quite long, and it seems it has strange side effects on an unrelated file Galois/Examples;

... The effect on Galois/Examples is indeed strange, but I don't think it's gonna be resolved just by changing the file name.

Well, your additions may have changed the import graph of other files, which may be the reason for the breakage in Galois categories. Putting the new code in a separate file should solve this issue...

• the assumption HasPullbacks is weakened in PRs by @Jlh18 (see refactor: weaken HasPullbacks to HasPullback in Over.Pullback #29795), so that some coordination about the
  changes to be made should happen;

@Jlh18 , Is this close to being merged? Seems this is weaker assumption for a couple of theorems in lccc prelim.

• I am not sure exactly where/when this remark should be made again, but I think @jcommelin had suggested that at some point we should allow "chosen pullbacks" (which I understand by saying that for a morphism f we could have a ChosenPullback f typeclass with the data of a choice of functor between Over categories that is right adjoint to the obvious functor), I think it is important for future computations.

Also, on the semantics side, I think with ChosenPullback f the codomain fibration will be a a cloven fibration, whereas with HasPullbacks you have a general Grothendieck fibration.

I have no idea how what you say answer my suggestion. In your code, it seems that there is data for the right adjoints of the pullback functors on the Over categories, the suggestion is to include also data for the pullback functors themselves, as "chosen" right adjoints of Over.map. How could this make something less general than the definition where the pullback functors would be defined using the limits given by HasPullbacks!?

(Ah, actually, it seems you do not include data for the pushforwards. As a structure on a category, it would make sense to have data for these functors.)

[sinhp]

Just a few quick remarks for now:

• the additions to Comma.Over.Pullback should probably go in a separate file, because it is already quite long, and it seems it has strange side effects on an unrelated file Galois/Examples;

What about making a new file in the new folder LocallyCartesianClosed named "Prelim.lean"? Otherwise, please suggest a location for this. The effect on Galois/Examples is indeed strange, but I don't think it's gonna be resolved just by changing the file name. We had a discussion about this on Zulip here: https://leanprover.zulipchat.com/#narrow/channel/144837-PR-reviews/topic/.2321525.20Locally.20Cartesian.20Closed.20Categories/near/498346104

• the assumption HasPullbacks is weakened in PRs by @Jlh18 (see refactor: weaken HasPullbacks to HasPullback in Over.Pullback #29795), so that some coordination about the
  changes to be made should happen;

@Jlh18 , Is this close to being merged? Seems this is weaker assumption for a couple of theorems in lccc prelim.

• I am not sure exactly where/when this remark should be made again, but I think @jcommelin had suggested that at some point we should allow "chosen pullbacks" (which I understand by saying that for a morphism f we could have a ChosenPullback f typeclass with the data of a choice of functor between Over categories that is right adjoint to the obvious functor), I think it is important for future computations.

We already have cartesian monoidal category structure on slice categories thanks to Andrew's work – incidentally one reason the LCCC work got merge conflict back in February, and had to wait for that work to be done. But, it is nicer to do it that way. I am using this monoidal structure. If I don't misread what you say, then ChosenPullback f for every f also gives a cartesian monoidal structure on slices.

Also, on the semantics side, I think with ChosenPullback f the codomain fibration will be a a cloven fibration, whereas with HasPullbacks you have a general Grothendieck fibration. I think the codomain functor for LCCCs is a general Grothendieck fibration not necessarily a cloven one. So, in a way Π f, ChosenPullback f results in a stricter semantics.

• the additions to Comma.Over.Pullback should probably go in a separate file, because it is already quite long, and it seems it has strange side effects on an unrelated file Galois/Examples;

... The effect on Galois/Examples is indeed strange, but I don't think it's gonna be resolved just by changing the file name.

Well, your additions may have changed the import graph of other files, which may be the reason for the breakage in Galois categories. Putting the new code in a separate file should solve this issue...

• the assumption HasPullbacks is weakened in PRs by @Jlh18 (see refactor: weaken HasPullbacks to HasPullback in Over.Pullback #29795), so that some coordination about the
  changes to be made should happen;

@Jlh18 , Is this close to being merged? Seems this is weaker assumption for a couple of theorems in lccc prelim.

• I am not sure exactly where/when this remark should be made again, but I think @jcommelin had suggested that at some point we should allow "chosen pullbacks" (which I understand by saying that for a morphism f we could have a ChosenPullback f typeclass with the data of a choice of functor between Over categories that is right adjoint to the obvious functor), I think it is important for future computations.

Also, on the semantics side, I think with ChosenPullback f the codomain fibration will be a a cloven fibration, whereas with HasPullbacks you have a general Grothendieck fibration.

I have no idea how what you say answer my suggestion. In your code, it seems that there is data for the right adjoints of the pullback functors on the Over categories, the suggestion is to include also data for the pullback functors themselves, as "chosen" right adjoints of Over.map. How could this make something less general than the definition where the pullback functors would be defined using the limits given by HasPullbacks!?

(Ah, actually, it seems you do not include data for the pushforwards. As a structure on a category, it would make sense to have data for these functors.)

It seems I was confused about your comment. I thought it is concerning the file Comma.Over.Pullback, but it seems you are actually commenting on #30375 PR and not this PR, correct?

[mathlib4-merge-conflict-bot]

This pull request has conflicts, please merge master and resolve them.

[sinhp]

@joelriou

I addressed your first two points in this last commit.

If I understand correctly, your third point applies to a different PR, namely #30375, which I shall address by changes to that PR separately.

[joelriou]

Could you remove unnecessary parentheses in the whole file? (And add simp/reassoc attributes to lemmas when applicable.)

[joelriou]

We should not create data using tactics.

[sinhp]

seems the culprit was fapply at the beginning of the construction of iso. it is now addressed in the last commit.

[joelriou]

Could you not use Equivalence.mk which does not have good definitional properties?

[joelriou]

This equivalence should be defined more generally for any object satisfying IsTerminal.

[joelriou]

This should be removed. (It seems it is a particular case of Adjunction.rightAdjointUniq.)

[joelriou]

There should not be a capital initial.

[joelriou]

Could you move this to the IsTerminal namespace? Also, the inverse functor could probably be "inlined" in the definition of the equivalence. Could you also add the simps attribute?

[joelriou]

After looking at this PR more closely, I am feeling a little bit skeptical as most of the definitions only duplicates what we already have (sigma is basically Over.map, and reindex is Over.pullback, sndProj is just (mapPullbackAdj Y.hom).counit.app Z). We may have some missing definitions for Over.map/pullback, but for the coherence of the library, I believe the better formulations should be in terms of Over.map and Over.pullback.
I would have a different opinion if the definitions in this PR were made in terms of the pullback functor for a typeclass containing data like:

class Over.ChosenPullback {Y X : C} (f : Y ⟶ X) where
  pullback : Over X ⥤ Over Y
  mapPullbackAdj : Over.map f ⊣ pullback 

[sinhp]

After looking at this PR more closely, I am feeling a little bit skeptical as most of the definitions only duplicates what we already have (sigma is basically Over.map, and reindex is Over.pullback, sndProj is just (mapPullbackAdj Y.hom).counit.app Z). We may have some missing definitions for Over.map/pullback, but for the coherence of the library, I believe the better formulations should be in terms of Over.map and Over.pullback. I would have a different opinion if the definitions in this PR were made in terms of the pullback functor for a typeclass containing data like:

class Over.ChosenPullback {Y X : C} (f : Y ⟶ X) where
  pullback : Over X ⥤ Over Y
  mapPullbackAdj : Over.map f ⊣ pullback 

@joelriou

In the PR (#30375) about the basics of lcccs I have defined that a morphism f : I ⟶ J is exponentiable if the pullback functor Over J ⥤ Over I has a right adjoint.

abbrev ExponentiableMorphism [HasPullbacks C] : MorphismProperty C :=
  fun _ _ f ↦ IsLeftAdjoint (Over.pullback f)

In an earlier version I had the following

class ExponentiableMorphism [HasPullbacks C] {I J : C} (f : I ⟶ J) where
  /-- The pushforward functor -/
  pushforward : Over I ⥤ Over J
  /-- The pushforward functor is right adjoint to the pullback functor -/
  adj : pullback f ⊣ pushforward := by infer_instance

which has a field providing the data of the adjunction rather than merely its existence. I think this is more compatible with the Over.ChosenPullback you are proposing. In the absence of data (i.e. the former definition), we get

abbrev pushforward (f : I ⟶ J) [ExponentiableMorphism f] :=
  rightAdjoint (Over.pullback f)

which uses Choice. I think having data instead of property can be useful in this regard, that is it makes the theory computable. However, sometimes it is useful to prove a morphism is exponentiable simply by showing that the right adjoint exists rather than constructing the right adjoint, e.g. using AFT or SAFT or something like that. But, I guess in those particular cases we can use Choice to get the right adjoint from existence.

I am fine with redeveloping lccc-prelim with Over.ChosenPullback.

The current file proves the following results which did not exist in mathlib. These are important for supporting the rest of theory LCCCs that we have built:

• The iso pullback Y.hom ⋙ map Y.hom ≅ tensorLeft Y, this is used in LCCC.Basic to prove a morphism with a pushforward is an exponentiable object in the slice category.

• isos star (⊤_ C) ≅ Functor.toOverTerminal C

• star (Over.mk f) ⋙ (Over.mk f).iteratedSliceForward ≅ pullback f to go back and forth between cartesian closedness of slices and locally cartesian closedness.

• star Y ⋙ pullback f ≅ star X used in Beck-Chevalley file.

As for the notations, yes, of course we can write sigma Y U as (Over.map Y.hom).obj U and similarly for reindex but then some of the stuff about lcccs and their internal logic becomes hard to read without these abbreviations. See page 5 of https://arxiv.org/pdf/0906.4931 for my motivations for introducing these abbreviations. However, this is a design choice, I'm happy to remove these if you think it is more compatible with mathlib style.

Here's a proposal:

• remove sigma and reindex and write (Over.map _).obj and (Over.ChosenPullback _).obj instead.
• prove that HasFiniteWidePullbacks C assumption gives an instance of Over.ChosenPullback C where the latter means Over.ChosenPullback f for every f in C.

Do we want to transfer instances of HasPullbackAlong f to Over.ChosenPullback f?

[sinhp]

@joelriou
Another thing to note that is that a : Over.ChosenPullback f and b : Over.ChosenPullback g gives c : Over.ChosenPullback (f.comp g) when the latter makes sense. However the pullback map c.pullback _ "chooses" is not the equal to a.pullback (b.pullback _) but only isomorphic. so we the term is "Chosen" needs to be understood in "up to iso" sense.

In particular if you have f an inverse for g, then f.comp g = id will have two induced instances Over.ChosenPullback id, one from the identity and the other from composition, and there is no way to show they are the same. Won't this be problematic?

[joelriou]

In particular if you have f an inverse for g, then f.comp g = id will have two induced instances Over.ChosenPullback id, one from the identity and the other from composition, and there is no way to show they are the same. Won't this be problematic?
Over.ChosenPullback.id/comp should only be definitions, not instances...

[joelriou]

The current file proves the following results which did not exist in mathlib. These are important for supporting the rest of theory LCCCs that we have built:

The process would be easier if each PR was short and with a specific scope.

As for the notations, yes, of course we can write sigma Y U as (Over.map Y.hom).obj U and similarly for reindex but then some of the stuff about lcccs and their internal logic becomes hard to read without these abbreviations.

Yes, but we may also be interested in the functoriality of Over categories and not care at all about the internal logic interpretation/semantics! Scoped notations (not abbrev) may resolve such discrepancies between the expectations of different users...

Here's a proposal:

* remove `sigma` and `reindex` and write `(Over.map _).obj ` and `(Over.ChosenPullback _).obj ` instead.

* prove that `HasFiniteWidePullbacks C` assumption gives an instance of `Over.ChosenPullback C` where the latter means `Over.ChosenPullback f` for every `f` in `C`.

HasPullbacks C would be more appropriate, and HasPullbacksAlong f would be even better. (This proof would be about a line long anyway.

Do we want to transfer instances of HasPullbackAlong f to Over.ChosenPullback f?

They should basically be no automatic instances of Over.ChosenPullback (apart maybe on Type _), only a definition.

[sinhp]

Sounds good, I'll try to implement these in the next commit. Hopefully the file will become much shorter.