feat(CategoryTheory): Locally Cartesian Closed Categories (Prelim) by sinhp · Pull Request #21525 · leanprover-community/mathlib4

sinhp · 2025-02-06T23:29:06Z

This PR defines the basic preliminaries for defining locally cartesian closed categories (LCCCs). In particular, using the calculus of mates we define certain natural isomorphisms involving Over.star and Over.pullback which will be crucial in defining the right adjoint to the pullback functor in the development of LCCCs.

…ian-closed-categories

…thub.com/leanprover-community/mathlib4 into sina-locally-cartesian-closed-categories

…ian-closed-categories

github-actions · 2025-02-07T00:11:10Z

PR summary 9c6c92b900

Import changes exceeding 2%

%	File
+52.40%	`Mathlib.CategoryTheory.Comma.Over.Pullback`
+2.31%	`Mathlib.CategoryTheory.Galois.Examples`

Import changes for modified files

Dependency changes

File	Base Count	Head Count	Change
Mathlib.CategoryTheory.Comma.Over.Pullback	437	666	+229 (+52.40%)
Mathlib.CategoryTheory.Galois.Examples	1084	1109	+25 (+2.31%)

Import changes for all files

Files	Import difference
`Mathlib.CategoryTheory.Abelian.FreydMitchell`	3
5 files `Mathlib.Algebra.Category.ModuleCat.Sheaf.PullbackContinuous` `Mathlib.CategoryTheory.Abelian.GrothendieckAxioms.Indization` `Mathlib.CategoryTheory.Generator.Indization` `Mathlib.Condensed.AB` `Mathlib.Condensed.Light.AB`	4
`Mathlib.Condensed.CartesianClosed` `Mathlib.Condensed.Light.CartesianClosed`	7
10 files `Mathlib.Algebra.Category.ModuleCat.Presheaf.Generator` `Mathlib.Algebra.Category.ModuleCat.Presheaf.Pullback` `Mathlib.RepresentationTheory.Character` `Mathlib.RepresentationTheory.FDRep` `Mathlib.RepresentationTheory.GroupCohomology.Basic` `Mathlib.RepresentationTheory.GroupCohomology.Functoriality` `Mathlib.RepresentationTheory.GroupCohomology.Hilbert90` `Mathlib.RepresentationTheory.GroupCohomology.LowDegree` `Mathlib.RepresentationTheory.GroupCohomology.Resolution` `Mathlib.RepresentationTheory.Invariants`	8
`Mathlib.CategoryTheory.Sites.SheafCohomology.Basic`	18
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`	19
`Mathlib.CategoryTheory.Limits.MorphismProperty`	20
`Mathlib.Algebra.Homology.LocalCohomology` `Mathlib.AlgebraicTopology.SingularHomology.Basic`	21
87 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.GrothendieckAxioms.Colim` `Mathlib.CategoryTheory.Abelian.GrothendieckAxioms.Connected` `Mathlib.CategoryTheory.Abelian.GrothendieckCategory.ColimCoyoneda` `Mathlib.CategoryTheory.Abelian.GrothendieckCategory.Coseparator` `Mathlib.CategoryTheory.Abelian.GrothendieckCategory.EnoughInjectives` `Mathlib.CategoryTheory.Abelian.GrothendieckCategory.ModuleEmbedding.Opposite` `Mathlib.CategoryTheory.Abelian.GrothendieckCategory.Monomorphisms` `Mathlib.CategoryTheory.Abelian.GrothendieckCategory.Subobject` `Mathlib.CategoryTheory.Abelian.Injective.Resolution` `Mathlib.CategoryTheory.Abelian.LeftDerived` `Mathlib.CategoryTheory.Abelian.Projective.Dimension` `Mathlib.CategoryTheory.Abelian.Projective.Resolution` `Mathlib.CategoryTheory.Abelian.RightDerived` `Mathlib.CategoryTheory.Idempotents.HomologicalComplex` `Mathlib.CategoryTheory.Monoidal.Tor` `Mathlib.CategoryTheory.Preadditive.Injective.Resolution` `Mathlib.CategoryTheory.Preadditive.Projective.Resolution`	22
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.Sites.CartesianClosed` `Mathlib.CategoryTheory.Sites.MayerVietorisSquare` `Mathlib.Topology.Sheaves.MayerVietoris`	23
3 files `Mathlib.Algebra.Category.Ring.Under.Limits` `Mathlib.CategoryTheory.Abelian.Monomorphisms` `Mathlib.RingTheory.Flat.CategoryTheory`	24
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`	25
18 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.Sheaf` `Mathlib.CategoryTheory.Abelian.GrothendieckAxioms.Types` `Mathlib.CategoryTheory.Abelian.GrothendieckCategory.Basic`	26
25 files `Mathlib.Algebra.Category.ModuleCat.Biproducts` `Mathlib.Algebra.Category.ModuleCat.Free` `Mathlib.Algebra.Category.ModuleCat.Simple` `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.Basic` `Mathlib.CategoryTheory.Abelian.Projective.Basic` `Mathlib.CategoryTheory.Abelian.Pseudoelements` `Mathlib.CategoryTheory.Abelian.Subobject` `Mathlib.CategoryTheory.Abelian.Yoneda` `Mathlib.CategoryTheory.Generator.Abelian` `Mathlib.CategoryTheory.Noetherian` `Mathlib.CategoryTheory.Preadditive.Schur` `Mathlib.CategoryTheory.Simple` `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`	27
3 files `Mathlib.CategoryTheory.SmallObject.Basic` `Mathlib.CategoryTheory.SmallObject.IsCardinalForSmallObjectArgument` `Mathlib.Topology.CWComplex.Abstract.Basic`	34
`Mathlib.Algebra.Category.Ring.Under.Basic` `Mathlib.Algebra.Homology.HomologicalComplexBiprod`	35
4 files `Mathlib.Algebra.Category.Grp.Subobject` `Mathlib.Algebra.Category.ModuleCat.Subobject` `Mathlib.AlgebraicTopology.RelativeCellComplex.Basic` `Mathlib.CategoryTheory.SmallObject.TransfiniteCompositionLifting`	36
4 files `Mathlib.Algebra.Homology.BifunctorAssociator` `Mathlib.Algebra.Homology.Monoidal` `Mathlib.CategoryTheory.Dialectica.Monoidal` `Mathlib.CategoryTheory.Generator.Sheaf`	39
3 files `Mathlib.Algebra.Homology.HomologicalComplexLimits` `Mathlib.Algebra.Homology.Square` `Mathlib.CategoryTheory.Generator.HomologicalComplex`	41
`Mathlib.CategoryTheory.Closed.Ideal`	42
3 files `Mathlib.Algebra.Homology.Additive` `Mathlib.Algebra.Homology.Embedding.Restriction` `Mathlib.Algebra.Homology.Linear`	43
4 files `Mathlib.CategoryTheory.Generator.Preadditive` `Mathlib.CategoryTheory.Localization.FiniteProducts` `Mathlib.CategoryTheory.Preadditive.Injective.LiftingProperties` `Mathlib.CategoryTheory.Preadditive.Projective.LiftingProperties`	44
`Mathlib.CategoryTheory.Adjunction.AdjointFunctorTheorems` `Mathlib.CategoryTheory.Sites.MorphismProperty`	45
9 files `Mathlib.AlgebraicTopology.RelativeCellComplex.AttachCells` `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`	46
5 files `Mathlib.Algebra.Homology.BifunctorFlip` `Mathlib.Algebra.Homology.Bifunctor` `Mathlib.Algebra.Homology.TotalComplexSymmetry` `Mathlib.Algebra.Homology.TotalComplex` `Mathlib.CategoryTheory.Limits.Shapes.Diagonal`	48
`Mathlib.CategoryTheory.Generator.Presheaf`	49
`Mathlib.CategoryTheory.Generator.Basic` `Mathlib.CategoryTheory.Subobject.Comma`	51
`Mathlib.CategoryTheory.Subpresheaf.Subobject`	52
`Mathlib.CategoryTheory.Subobject.HasCardinalLT`	61
`Mathlib.Algebra.Category.Ring.Adjunctions` `Mathlib.CategoryTheory.Dialectica.Basic`	68
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`	70
3 files `Mathlib.Algebra.Homology.ImageToKernel` `Mathlib.CategoryTheory.Subobject.Lattice` `Mathlib.CategoryTheory.Subobject.Limits`	75
`Mathlib.CategoryTheory.Subobject.FactorThru`	84
6 files `Mathlib.CategoryTheory.Subobject.Basic` `Mathlib.CategoryTheory.Subobject.MonoOver` `Mathlib.CategoryTheory.Subobject.Presheaf` `Mathlib.CategoryTheory.Subobject.Types` `Mathlib.CategoryTheory.Subobject.WellPowered` `Mathlib.CategoryTheory.Subterminal`	203
`Mathlib.CategoryTheory.Comma.Over.Pullback`	229

Declarations diff

+ Functor.toOverTerminal
+ Limits.baseChange
+ Over.sigmaReindexNatIsoTensorLeft
+ Over.sigmaReindexNatIsoTensorLeft_hom_app
+ Reindex
+ Sigma
+ baseChange
+ counit_app
+ counit_app_pullback_fst
+ counit_app_pullback_snd
+ counit_app_pullback_snd_eq_homMk
+ equivOverTerminal
+ equivalenceRightAdjointIsoInverse
+ forgetAdjStar
+ fst
+ fstProj
+ fstProj_sigma_fst
+ homEquiv
+ homEquiv_symm
+ isBinaryProductSigmaReindex
+ iteratedSliceBackward_forget
+ map
+ mapAdjunction
+ map_comp_fst
+ map_homMk_left
+ map_left
+ overHomMk
+ sigmaReindexIsoProd
+ sigmaReindexIsoProdMk
+ sigmaReindexIsoProd_hom_comp_fst
+ sigmaReindexIsoProd_hom_comp_snd
+ sigmaSymmetryIso
+ sndProj
+ starIsoToOverTerminal
+ starIteratedSliceForwardIsoPullback
+ starPullbackIsoStar
+ star_map
+ symmetryObjIso
+ symmetry_hom
+ unit_app
++ hom
++- star

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).

…ian-closed-categories

For monoidal structure

…ian-closed-categories

Mathlib/CategoryTheory/Adjunction/Over.lean

`IsConnected` in Mathlib.CategoryTheory.Galois.Examples refers to docs#CategoryTheory.PreGaloisCategory.IsConnected. But, this PR changes the import tree such that now docs#CategoryTheory.IsConnected is available in Mathlib.CategoryTheory.Galois.Examples and now Lean interprets the IsConnected as CategoryTheory.IsConnected and no longer as CategoryTheory.PreGaloisCategory.IsConnected.

Co-authored-by: github-actions[bot] <41898282+github-actions[bot]@users.noreply.github.com>

joelriou · 2025-02-09T22:53:28Z

Mathlib/CategoryTheory/Adjunction/Over.lean

+lemma inv_obj (F : C ⥤ D) [F.IsEquivalence] (X : D) : (F.inv.obj X) = F.objPreimage X := by rfl
+
+lemma inv_map (F : C ⥤ D) [F.IsEquivalence] {X Y : D} (f : X ⟶ Y) :
+    F.inv.map f = F.preimage ((F.objObjPreimageIso X).hom ≫ f ≫ (F.objObjPreimageIso Y).inv) := by
+  rfl
+
+lemma asEquivalence_inverse (F : C ⥤ D) [F.IsEquivalence] : (F.asEquivalence).inverse = F.inv := by
+  rfl


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.

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. :)

@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.

…ian-closed-categories

asked by the reviewer

…ian-closed-categories

sinhp · 2025-02-26T10:52:39Z

@joelriou @b-mehta

Joël asked if for the purpose of a more focussed reviews, I could extract a PR mostly containing the first chunk of modifications. This is now done, and the PR message at the top is accordingly updated. In particular, there will be not changes to file Equivalence as I found a workaround to prove things without looking into the blackbox of asEquivalence and in particular its inverse.

The next PR will define the section functor depending on the current PR! This will be used in the PR after that which adds the new folder LocallyCartesianClosed and the file Basic in that folder.

And then after that separate PRs for the following stuff:

Beck-Chevalley condition as a file in the folder LocallyCartesianClosed
LCCC structure on Types as a file in the folder LocallyCartesianClosed
LCCC structure on Presheaf Categories as a file in the folder LocallyCartesianClosed
Polyonomial functors

…ian-closed-categories

leanprover-community-bot-assistant · 2025-04-09T13:22:00Z

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

sinhp added 10 commits January 28, 2025 14:46

Create Basic.lean

c4c0c12

ExponentiableMorphism

11ac00d

forgetAdjStar lemmas

5f5909c

notation

d0a6efd

BinaryDan

d3c28b2

Merge remote-tracking branch 'origin/master' into sina-locally-cartes…

f088a51

…ian-closed-categories

CartesianClosedOver

7886c5c

Merge branch 'sina-locally-cartesian-closed-categories' of https://gi…

608f448

…thub.com/leanprover-community/mathlib4 into sina-locally-cartesian-closed-categories

locally cartesian closed done

e091fa9

renaming

cd426e4

leanprover-community-bot-assistant added the merge-conflict The PR has a merge conflict with master, and needs manual merging. (this label is managed by a bot) label Feb 6, 2025

Merge remote-tracking branch 'origin/master' into sina-locally-cartes…

f84c317

…ian-closed-categories

github-actions bot added large-import Automatically added label for PRs with a significant increase in transitive imports and removed merge-conflict The PR has a merge conflict with master, and needs manual merging. (this label is managed by a bot) labels Feb 7, 2025

sinhp added 5 commits February 7, 2025 08:28

Merge remote-tracking branch 'origin/master' into sina-locally-cartes…

35d6579

…ian-closed-categories

pruning

3172763

universe outside namespace

266a870

HasFiniteWidePullbacks C instead of HasPullbacks C

49c9e86

For monoidal structure

Merge remote-tracking branch 'origin/master' into sina-locally-cartes…

f0f9cea

…ian-closed-categories

joelriou reviewed Feb 7, 2025

View reviewed changes

Mathlib/CategoryTheory/Adjunction/Over.lean Outdated Show resolved Hide resolved

sinhp and others added 5 commits February 7, 2025 15:59

lake exe mk_all

d8e412a

docstrings and lemma simp-NF

68573b0

references for notations Σ_ and Δ_

63a95ae

Update docs/references.bib

0905067

Co-authored-by: github-actions[bot] <41898282+github-actions[bot]@users.noreply.github.com>

sinhp added the t-category-theory Category theory label Feb 8, 2025

joelriou reviewed Feb 9, 2025

View reviewed changes

joelriou added the awaiting-author A reviewer has asked the author a question or requested changes. label Feb 9, 2025

sinhp mentioned this pull request Feb 11, 2025

[Merged by Bors] - feat(CategoryTheory): reorganizing Over categories #21717

Closed

sinhp added 5 commits February 15, 2025 12:46

Merge remote-tracking branch 'origin/master' into sina-locally-cartes…

0c979c1

…ian-closed-categories

linter

1dbe638

unneccesary import

4414d47

pruning

4b5695f

iteratedSliceBackward_forget

4a8f4b6

leanprover-community-bot-assistant added the merge-conflict The PR has a merge conflict with master, and needs manual merging. (this label is managed by a bot) label Feb 25, 2025

sinhp added 2 commits February 26, 2025 00:13

large refactoring

89f117d

Merge remote-tracking branch 'origin/master' into sina-locally-cartes…

8678be3

…ian-closed-categories

github-actions bot removed the merge-conflict The PR has a merge conflict with master, and needs manual merging. (this label is managed by a bot) label Feb 25, 2025

sinhp added 7 commits February 26, 2025 10:04

Merge remote-tracking branch 'origin/master' into sina-locally-cartes…

2d325aa

…ian-closed-categories

setting Galois back to master

bf72039

prune

86938c6

this file will go into a new PR for focus review

7c21d5b

asked by the reviewer

doc string

d58aa70

ref moved to the next PR

449059f

Merge remote-tracking branch 'origin/master' into sina-locally-cartes…

b39a3a5

…ian-closed-categories

sinhp changed the title ~~feat(CategoryTheory): Locally Cartesian Closed Categories~~ feat(CategoryTheory): Locally Cartesian Closed Categories (Prelim) Feb 26, 2025

sinhp removed the awaiting-author A reviewer has asked the author a question or requested changes. label Feb 26, 2025

move Over.Sections to the next PR for focus review

931288f

leanprover-community-bot-assistant added the merge-conflict The PR has a merge conflict with master, and needs manual merging. (this label is managed by a bot) label Mar 5, 2025

Merge remote-tracking branch 'origin/master' into sina-locally-cartes…

9c6c92b

…ian-closed-categories

github-actions bot removed the merge-conflict The PR has a merge conflict with master, and needs manual merging. (this label is managed by a bot) label Mar 6, 2025

leanprover-community-bot-assistant added the merge-conflict The PR has a merge conflict with master, and needs manual merging. (this label is managed by a bot) label Apr 9, 2025

This was referenced Oct 8, 2025

locally cartesian closed categories-1 #30343

Closed

feat(CategoryTheory): The Preliminaries for Locally Cartesian Closed Categories #30366

Open

Provide feedback

Saved searches

Use saved searches to filter your results more quickly

feat(CategoryTheory): Locally Cartesian Closed Categories (Prelim)#21525

feat(CategoryTheory): Locally Cartesian Closed Categories (Prelim)#21525
sinhp wants to merge 46 commits intomasterfrom
sina-locally-cartesian-closed-categories

sinhp commented Feb 6, 2025 •

edited

Loading

Uh oh!

github-actions bot commented Feb 7, 2025 •

edited

Loading

Import changes for modified files

Declarations diff

Uh oh!

Uh oh!

joelriou Feb 9, 2025 •

edited

Loading

Uh oh!

sinhp Feb 9, 2025

Uh oh!

sinhp Feb 11, 2025

Uh oh!

sinhp commented Feb 26, 2025 •

edited

Loading

Uh oh!

leanprover-community-bot-assistant commented Apr 9, 2025

Uh oh!

Reviewers

Assignees

Labels

Projects

Milestone

Development

Uh oh!

5 participants

Conversation

sinhp commented Feb 6, 2025 • edited Loading Uh oh! There was an error while loading. Please reload this page.

Uh oh!

Uh oh!

github-actions bot commented Feb 7, 2025 • edited Loading Uh oh! There was an error while loading. Please reload this page.

Uh oh!

PR summary 9c6c92b900

Import changes for modified files

Declarations diff

Uh oh!

Uh oh!

joelriou Feb 9, 2025 • edited Loading Uh oh! There was an error while loading. Please reload this page.

Uh oh!

Choose a reason for hiding this comment

Uh oh!

sinhp Feb 9, 2025

Choose a reason for hiding this comment

Uh oh!

sinhp Feb 11, 2025

Choose a reason for hiding this comment

Uh oh!

sinhp commented Feb 26, 2025 • edited Loading Uh oh! There was an error while loading. Please reload this page.

Uh oh!

Uh oh!

leanprover-community-bot-assistant commented Apr 9, 2025

Uh oh!

Reviewers

Assignees

Labels

Projects

Milestone

Development

Uh oh!

5 participants

sinhp commented Feb 6, 2025 •

edited

Loading

github-actions bot commented Feb 7, 2025 •

edited

Loading

joelriou Feb 9, 2025 •

edited

Loading

sinhp commented Feb 26, 2025 •

edited

Loading