feat(CategoryTheory): Locally Cartesian Closed Categories

[sinhp]

This PR defines locally cartesian closed categories in terms of existence of the pushforward functors (right adjoint to the pullback functor) for all morphisms. We develop basic API and special notations (Σ_ , Δ_, Π_) usually found in the literature of polynomial functors as well as in the categorical semantics in locally cartesian closed categories. This PR proves that a locally cartesian closed category with a terminal object is cartesian closed, and that the slices of a locally cartesian closed category are locally cartesian closed.

Some of the content is based on the project of formalization of polynomial functors at the Trimester "Prospect of Formal Mathematics" at the Hausdorff Institute (HIM) in Bonn. https://github.com/sinhp/Poly

I found this implementation of locally cartesian closed categories amenable to polynomial functors formalization.

Co-authored-by: Emily Riehl eriehl@jhu.edu

---

[github-actions]

PR summary 6efafde0b8

Import changes exceeding 2%

%	File
+51.98%	Mathlib.CategoryTheory.Comma.Over.Pullback
+2.65%	Mathlib.CategoryTheory.Galois.Examples

Import changes for modified files

Dependency changes

File	Base Count	Head Count	Change
Mathlib.CategoryTheory.Comma.Over.Pullback	429	652	+223 (+51.98%)
Mathlib.CategoryTheory.Galois.Examples	1058	1086	+28 (+2.65%)

Import changes for all files

Files	Import difference
4 files Mathlib.Condensed.AB Mathlib.Condensed.CartesianClosed Mathlib.Condensed.Light.AB Mathlib.Condensed.Light.CartesianClosed	7
7 files Mathlib.RepresentationTheory.Character Mathlib.RepresentationTheory.FDRep Mathlib.RepresentationTheory.GroupCohomology.Basic Mathlib.RepresentationTheory.GroupCohomology.Hilbert90 Mathlib.RepresentationTheory.GroupCohomology.LowDegree Mathlib.RepresentationTheory.GroupCohomology.Resolution Mathlib.RepresentationTheory.Invariants	9
Mathlib.Algebra.Category.ModuleCat.Presheaf.Generator Mathlib.Algebra.Category.ModuleCat.Presheaf.Pullback	11
Mathlib.CategoryTheory.Sites.CartesianClosed	15
Mathlib.CategoryTheory.Sites.SheafCohomology.Basic	21
10 files Mathlib.AlgebraicGeometry.Cover.Over Mathlib.AlgebraicGeometry.Morphisms.FormallyUnramified Mathlib.AlgebraicGeometry.Morphisms.Immersion Mathlib.AlgebraicGeometry.Morphisms.Proper Mathlib.AlgebraicGeometry.Morphisms.Separated Mathlib.AlgebraicGeometry.PointsPi Mathlib.AlgebraicGeometry.ProjectiveSpectrum.Proper Mathlib.AlgebraicGeometry.RationalMap Mathlib.AlgebraicGeometry.Sites.Small Mathlib.AlgebraicGeometry.ValuativeCriterion	22
Mathlib.CategoryTheory.Limits.MorphismProperty	23
Mathlib.Algebra.Homology.LocalCohomology Mathlib.AlgebraicTopology.SingularHomology.Basic	24
78 files Mathlib.Algebra.Homology.AlternatingConst Mathlib.Algebra.Homology.BifunctorHomotopy Mathlib.Algebra.Homology.BifunctorShift Mathlib.Algebra.Homology.ConcreteCategory Mathlib.Algebra.Homology.DerivedCategory.Basic Mathlib.Algebra.Homology.DerivedCategory.ExactFunctor Mathlib.Algebra.Homology.DerivedCategory.Ext.Basic Mathlib.Algebra.Homology.DerivedCategory.Ext.ExactSequences Mathlib.Algebra.Homology.DerivedCategory.Ext.ExtClass Mathlib.Algebra.Homology.DerivedCategory.HomologySequence Mathlib.Algebra.Homology.DerivedCategory.ShortExact Mathlib.Algebra.Homology.DerivedCategory.SingleTriangle Mathlib.Algebra.Homology.Embedding.CochainComplex Mathlib.Algebra.Homology.Embedding.ExtendHomology Mathlib.Algebra.Homology.Embedding.Extend Mathlib.Algebra.Homology.Embedding.HomEquiv Mathlib.Algebra.Homology.Embedding.IsSupported Mathlib.Algebra.Homology.Embedding.RestrictionHomology Mathlib.Algebra.Homology.Embedding.StupidTrunc Mathlib.Algebra.Homology.Embedding.TruncGEHomology Mathlib.Algebra.Homology.Embedding.TruncGE Mathlib.Algebra.Homology.Embedding.TruncLEHomology Mathlib.Algebra.Homology.Embedding.TruncLE Mathlib.Algebra.Homology.Factorizations.Basic Mathlib.Algebra.Homology.HomologicalComplexAbelian Mathlib.Algebra.Homology.HomologySequenceLemmas Mathlib.Algebra.Homology.HomologySequence Mathlib.Algebra.Homology.HomotopyCategory.DegreewiseSplit Mathlib.Algebra.Homology.HomotopyCategory.HomComplexShift Mathlib.Algebra.Homology.HomotopyCategory.HomComplex Mathlib.Algebra.Homology.HomotopyCategory.HomologicalFunctor Mathlib.Algebra.Homology.HomotopyCategory.MappingCone Mathlib.Algebra.Homology.HomotopyCategory.Pretriangulated Mathlib.Algebra.Homology.HomotopyCategory.ShiftSequence Mathlib.Algebra.Homology.HomotopyCategory.Shift Mathlib.Algebra.Homology.HomotopyCategory.ShortExact Mathlib.Algebra.Homology.HomotopyCategory.SingleFunctors Mathlib.Algebra.Homology.HomotopyCategory.Triangulated Mathlib.Algebra.Homology.HomotopyCategory Mathlib.Algebra.Homology.HomotopyCofiber Mathlib.Algebra.Homology.Homotopy Mathlib.Algebra.Homology.Localization Mathlib.Algebra.Homology.Opposite Mathlib.Algebra.Homology.QuasiIso Mathlib.Algebra.Homology.Refinements Mathlib.Algebra.Homology.ShortComplex.HomologicalComplex Mathlib.Algebra.Homology.SingleHomology Mathlib.Algebra.Homology.TotalComplexShift Mathlib.AlgebraicTopology.AlternatingFaceMapComplex Mathlib.AlgebraicTopology.DoldKan.Decomposition Mathlib.AlgebraicTopology.DoldKan.Degeneracies Mathlib.AlgebraicTopology.DoldKan.EquivalenceAdditive Mathlib.AlgebraicTopology.DoldKan.EquivalencePseudoabelian Mathlib.AlgebraicTopology.DoldKan.Equivalence Mathlib.AlgebraicTopology.DoldKan.Faces Mathlib.AlgebraicTopology.DoldKan.FunctorGamma Mathlib.AlgebraicTopology.DoldKan.FunctorN Mathlib.AlgebraicTopology.DoldKan.GammaCompN Mathlib.AlgebraicTopology.DoldKan.Homotopies Mathlib.AlgebraicTopology.DoldKan.HomotopyEquivalence Mathlib.AlgebraicTopology.DoldKan.NCompGamma Mathlib.AlgebraicTopology.DoldKan.NReflectsIso Mathlib.AlgebraicTopology.DoldKan.Normalized Mathlib.AlgebraicTopology.DoldKan.Notations Mathlib.AlgebraicTopology.DoldKan.PInfty Mathlib.AlgebraicTopology.DoldKan.Projections Mathlib.AlgebraicTopology.DoldKan.SplitSimplicialObject Mathlib.AlgebraicTopology.ExtraDegeneracy Mathlib.AlgebraicTopology.MooreComplex Mathlib.CategoryTheory.Abelian.Ext Mathlib.CategoryTheory.Abelian.InjectiveResolution Mathlib.CategoryTheory.Abelian.LeftDerived Mathlib.CategoryTheory.Abelian.ProjectiveDimension Mathlib.CategoryTheory.Abelian.ProjectiveResolution Mathlib.CategoryTheory.Abelian.RightDerived Mathlib.CategoryTheory.Monoidal.Tor Mathlib.CategoryTheory.Preadditive.InjectiveResolution Mathlib.CategoryTheory.Preadditive.ProjectiveResolution	25
40 files Mathlib.AlgebraicGeometry.AffineSpace Mathlib.AlgebraicGeometry.Fiber Mathlib.AlgebraicGeometry.GluingOneHypercover Mathlib.AlgebraicGeometry.Gluing Mathlib.AlgebraicGeometry.IdealSheaf Mathlib.AlgebraicGeometry.Limits Mathlib.AlgebraicGeometry.Morphisms.AffineAnd Mathlib.AlgebraicGeometry.Morphisms.Affine Mathlib.AlgebraicGeometry.Morphisms.Basic Mathlib.AlgebraicGeometry.Morphisms.ClosedImmersion Mathlib.AlgebraicGeometry.Morphisms.Constructors Mathlib.AlgebraicGeometry.Morphisms.Etale Mathlib.AlgebraicGeometry.Morphisms.FinitePresentation Mathlib.AlgebraicGeometry.Morphisms.FiniteType Mathlib.AlgebraicGeometry.Morphisms.Finite Mathlib.AlgebraicGeometry.Morphisms.Flat Mathlib.AlgebraicGeometry.Morphisms.Integral Mathlib.AlgebraicGeometry.Morphisms.IsIso Mathlib.AlgebraicGeometry.Morphisms.OpenImmersion Mathlib.AlgebraicGeometry.Morphisms.Preimmersion Mathlib.AlgebraicGeometry.Morphisms.QuasiCompact Mathlib.AlgebraicGeometry.Morphisms.QuasiSeparated Mathlib.AlgebraicGeometry.Morphisms.RingHomProperties Mathlib.AlgebraicGeometry.Morphisms.Smooth Mathlib.AlgebraicGeometry.Morphisms.SurjectiveOnStalks Mathlib.AlgebraicGeometry.Morphisms.UnderlyingMap Mathlib.AlgebraicGeometry.Morphisms.UniversallyClosed Mathlib.AlgebraicGeometry.Morphisms.UniversallyInjective Mathlib.AlgebraicGeometry.Noetherian Mathlib.AlgebraicGeometry.PullbackCarrier Mathlib.AlgebraicGeometry.Pullbacks Mathlib.AlgebraicGeometry.ResidueField Mathlib.AlgebraicGeometry.Sites.BigZariski Mathlib.AlgebraicGeometry.Sites.Etale Mathlib.AlgebraicGeometry.Sites.MorphismProperty Mathlib.AlgebraicGeometry.SpreadingOut Mathlib.AlgebraicGeometry.Stalk Mathlib.CategoryTheory.Idempotents.HomologicalComplex Mathlib.CategoryTheory.Sites.MayerVietorisSquare Mathlib.Topology.Sheaves.MayerVietoris	26
Mathlib.Algebra.Category.Ring.Under.Limits Mathlib.RingTheory.Flat.CategoryTheory	27
10 files Mathlib.CategoryTheory.Galois.Action Mathlib.CategoryTheory.Galois.Basic Mathlib.CategoryTheory.Galois.Decomposition Mathlib.CategoryTheory.Galois.EssSurj Mathlib.CategoryTheory.Galois.Examples Mathlib.CategoryTheory.Galois.Full Mathlib.CategoryTheory.Galois.GaloisObjects Mathlib.CategoryTheory.Galois.IsFundamentalgroup Mathlib.CategoryTheory.Galois.Prorepresentability Mathlib.CategoryTheory.Galois.Topology	28
19 files Mathlib.Algebra.Category.Grp.AB Mathlib.Algebra.Category.ModuleCat.AB Mathlib.AlgebraicGeometry.AffineScheme Mathlib.AlgebraicGeometry.Cover.MorphismProperty Mathlib.AlgebraicGeometry.Cover.Open Mathlib.AlgebraicGeometry.FunctionField Mathlib.AlgebraicGeometry.GammaSpecAdjunction Mathlib.AlgebraicGeometry.OpenImmersion Mathlib.AlgebraicGeometry.ProjectiveSpectrum.Basic Mathlib.AlgebraicGeometry.ProjectiveSpectrum.Scheme Mathlib.AlgebraicGeometry.Properties Mathlib.AlgebraicGeometry.Restrict Mathlib.AlgebraicGeometry.Sites.SmallAffineZariski Mathlib.CategoryTheory.Abelian.GrothendieckAxioms.Basic Mathlib.CategoryTheory.Abelian.GrothendieckAxioms.FunctorCategory Mathlib.CategoryTheory.Abelian.GrothendieckAxioms.Indization Mathlib.CategoryTheory.Abelian.GrothendieckAxioms.Sheaf Mathlib.CategoryTheory.Abelian.GrothendieckAxioms.Types Mathlib.CategoryTheory.Abelian.GrothendieckCategory	29
20 files Mathlib.Algebra.Category.ModuleCat.Biproducts Mathlib.Algebra.Category.ModuleCat.Free Mathlib.Algebra.Homology.ShortComplex.ConcreteCategory Mathlib.Algebra.Homology.ShortComplex.ExactFunctor Mathlib.Algebra.Homology.ShortComplex.ModuleCat Mathlib.Algebra.Module.PID Mathlib.Analysis.Fourier.FiniteAbelian.PontryaginDuality Mathlib.CategoryTheory.Abelian.Exact Mathlib.CategoryTheory.Abelian.Injective Mathlib.CategoryTheory.Abelian.Projective Mathlib.CategoryTheory.Abelian.Pseudoelements Mathlib.CategoryTheory.Generator.Abelian Mathlib.CategoryTheory.Generator.Indization Mathlib.GroupTheory.FiniteAbelian.Basic Mathlib.GroupTheory.FiniteAbelian.Duality Mathlib.NumberTheory.DirichletCharacter.Orthogonality Mathlib.NumberTheory.LSeries.PrimesInAP Mathlib.NumberTheory.MulChar.Duality Mathlib.RingTheory.AdicCompletion.AsTensorProduct Mathlib.Topology.Category.Profinite.Nobeling	30
5 files Mathlib.Algebra.Category.ModuleCat.Simple Mathlib.CategoryTheory.Abelian.Subobject Mathlib.CategoryTheory.Noetherian Mathlib.CategoryTheory.Preadditive.Schur Mathlib.CategoryTheory.Simple	31
3 files Mathlib.Algebra.Homology.HomologicalComplexBiprod Mathlib.Algebra.Homology.Square Mathlib.Topology.CWComplex.Abstract.Basic	37
4 files Mathlib.Algebra.Category.Ring.Under.Basic Mathlib.AlgebraicTopology.RelativeCellComplex.Basic Mathlib.CategoryTheory.Generator.Sheaf Mathlib.CategoryTheory.SmallObject.TransfiniteCompositionLifting	39
Mathlib.Algebra.Category.Grp.Subobject Mathlib.Algebra.Category.ModuleCat.Subobject	40
Mathlib.CategoryTheory.Dialectica.Monoidal	42
Mathlib.Algebra.Homology.HomologicalComplexLimits	43
Mathlib.Algebra.Homology.BifunctorAssociator Mathlib.Algebra.Homology.Monoidal	44
6 files Mathlib.Algebra.Homology.Additive Mathlib.Algebra.Homology.Embedding.Restriction Mathlib.Algebra.Homology.Linear Mathlib.CategoryTheory.Adjunction.AdjointFunctorTheorems Mathlib.CategoryTheory.Closed.Ideal Mathlib.CategoryTheory.Generator.Preadditive	46
Mathlib.CategoryTheory.Generator.Presheaf Mathlib.CategoryTheory.Localization.FiniteProducts	51
5 files Mathlib.Algebra.Homology.BifunctorFlip Mathlib.Algebra.Homology.Bifunctor Mathlib.Algebra.Homology.TotalComplexSymmetry Mathlib.Algebra.Homology.TotalComplex Mathlib.CategoryTheory.Sites.MorphismProperty	52
10 files Mathlib.AlgebraicTopology.RelativeCellComplex.AttachCells Mathlib.CategoryTheory.Generator.Basic Mathlib.CategoryTheory.Limits.Preserves.Shapes.Square Mathlib.CategoryTheory.Limits.Shapes.Pullback.Square Mathlib.CategoryTheory.MorphismProperty.LiftingProperty Mathlib.CategoryTheory.MorphismProperty.Limits Mathlib.CategoryTheory.MorphismProperty.OverAdjunction Mathlib.CategoryTheory.MorphismProperty.Representable Mathlib.CategoryTheory.MorphismProperty.RetractArgument Mathlib.CategoryTheory.SmallObject.Construction	53
Mathlib.CategoryTheory.Limits.Shapes.Diagonal	56
Mathlib.CategoryTheory.Subobject.Comma	58
8 files Mathlib.Algebra.Homology.Augment Mathlib.Algebra.Homology.DifferentialObject Mathlib.Algebra.Homology.Double Mathlib.Algebra.Homology.Embedding.Boundary Mathlib.Algebra.Homology.Functor Mathlib.Algebra.Homology.HomologicalBicomplex Mathlib.Algebra.Homology.HomologicalComplex Mathlib.Algebra.Homology.Single	65
3 files Mathlib.Algebra.Homology.ImageToKernel Mathlib.CategoryTheory.Subobject.Lattice Mathlib.CategoryTheory.Subobject.Limits	70
Mathlib.Algebra.Category.Ring.Adjunctions	72
Mathlib.CategoryTheory.Dialectica.Basic	76
Mathlib.CategoryTheory.Subobject.FactorThru	83
5 files Mathlib.CategoryTheory.Subobject.Basic Mathlib.CategoryTheory.Subobject.MonoOver Mathlib.CategoryTheory.Subobject.Types Mathlib.CategoryTheory.Subobject.WellPowered Mathlib.CategoryTheory.Subterminal	197
Mathlib.CategoryTheory.Comma.Over.Pullback	223
Mathlib.CategoryTheory.Comma.Over.Sections (new file) Mathlib.CategoryTheory.LocallyCartesianClosed.Basic (new file)	653

---

Declarations diff

+ CartesianClosedOver.hasPushforwards
+ ExponentiableMorphism
+ Functor.toOverTerminal
+ HasPushforwards
+ Limits.baseChange
+ LocallyCartesianClosed
+ Over.sigmaReindexNatIsoTensorLeft
+ Over.sigmaReindexNatIsoTensorLeft_hom_app
+ OverMkHom
+ Reindex
+ Sigma
+ asEquivalenceInverseNatIso
+ asEquivalence_inverse
+ baseChange
+ cartesianClosed
+ cartesianClosedOver
+ comp
+ counit_app
+ counit_app_pullback_fst
+ counit_app_pullback_snd
+ counit_app_pullback_snd_eq_homMk
+ equivOverTerminal
+ ev
+ expIso
+ exponentiableOverMk
+ forgetAdjStar
+ fst
+ fstProj
+ fstProj_sigma_fst
+ functorRightAdjointIsoInverse
+ homEquiv
+ homEquiv_symm
+ id
+ inv_map
+ inv_obj
+ isBinaryProductSigmaReindex
+ map
+ mapAdjunction
+ mapStarIso
+ map_comp_fst
+ map_homMk_left
+ map_left
+ mkOfCartesianClosedOver
+ mkOfHasPushforwards
+ overHomMk
+ overLocallyCartesianClosed
+ pushforward
+ pushforwardCompIso
+ pushforwardCurry
+ pushforwardCurryAux
+ pushforwardFunctor
+ pushforwardMap
+ pushforwardUncurry
+ pushforward_curry_uncurry
+ pushforward_uncurry_curry
+ pushfowardIdIso
+ sections
+ sectionsCurry
+ sectionsCurryAux
+ sectionsFunctor
+ sectionsMap
+ sectionsMap_comp
+ sectionsMap_id
+ sectionsUncurry
+ sections_curry_uncurry
+ sections_uncurry_curry
+ sigmaReindexIsoProd
+ sigmaReindexIsoProdMk
+ sigmaReindexIsoProd_hom_comp_fst
+ sigmaReindexIsoProd_hom_comp_snd
+ sigmaSymmetryIso
+ sndProj
+ star
+ starSectionAdjunction
+ symmetryObjIso
+ symmetry_hom
+ toOverTerminalStarIso
+ unit_app
++ curryId
++ expMapFstProj
++ hom
++ pushforwardObj

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]

This should not be in this file, and I am quite sure we can avoid providing too much API for Functor.asEquivalence, which should be considered as a black box equivalence of categories with a prescribed .functor field.

In order to get more focussed reviews, could you extract a PR mostly containing the first chunk of modifications to this file Adjunction.Over. Actually, I am not completely convinced that some definitions (including existing ones) are in the right location.
Then, I would suggest you start with a PR which just moves the file CategoryTheory.Comma.Over to Category.Comma.Over.Basic, Comma.OverClass to Comma.Over.OverClass, and the existing content of Adjunction.Over to Comma.Over.Pullback.

[sinhp]

Re reorganizing and moving Over files: I very much agree with what you proposed. Then I do another PR about that.

Re Functor.asEquivalence: I originally put them in CategoryTheory.Equivalence file, would that be a better choice?

But mainly, in LCCCs, we construct natural isomorphisms between pushforwards as mate of corresponding nat isos of left adjoints. The API

Equivalence.asEquivalenceInverse (e : C ≌ D) :
     (e.functor).asEquivalence.inverse ≅ e.inverse := by

was necessary to prove star (⊤_ C) ≅ Functor.toOverTerminal C using this mate philosophy which happens consistently in the LCCC development.

It might be possible to not use this philosophy in constructing star (⊤_ C) ≅ Functor.toOverTerminal C.

But, I think it might be useful to know in general that if promote an equivalence to an adjoint equivalence and the inverse inv remains the same as inverse of original equivalence. I couldn't prove this fact without Equivalence.asEquivalenceInverse, but maybe there is a way I missed.

Anyhow, I think the important point is the reorganization which I'll do after I wake up. :)

[sinhp]

@joelriou Just to make sure I'm on the same page, after #21717, is the idea to make a new separate PR for the changes made to Adjunction.Over (or, Comma.Over.Pullback after #21717)? This would include namespaces Sigma, Reindex, the section BinaryProduct, TensorLeft and new lemmas about star.

[b-mehta]

Just to mention that I have an old development of locally cartesian closed categories here: https://github.com/b-mehta/topos/blob/master/src/locally_cartesian_closed.lean, which you may like to look at too. (This development from 5 years ago is what gave rise to the current implementation of cartesian closed categories and of sheaves and sites in mathlib!) Note that this is Lean 3, and was written when has_finite_limits meant what would currently mean HasChosenFiniteLimits.