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

sinhp · 2025-02-26T12:38:56Z

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 prove the following:

Existence of the pushforward functors is equivalent to cartesian closed slices.
Any locally cartesian closed category with a terminal object is cartesian closed.
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

[ ] depends on: feat(CategoryTheory): Locally Cartesian Closed Categories (Prelim) #21525
[ ] depends on: feat(CategoryTheory): Locally Cartesian Closed Categories (Sections Right Adjoint) #22319

…ian-closed-categories

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

…ian-closed-categories

For monoidal structure

…ian-closed-categories

`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>

…ian-closed-categories

…artesian-closed-categories

…ian-closed-categories

asked by the reviewer

…ian-closed-categories

github-actions · 2025-02-26T12:39:57Z

PR summary e323e05d58

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
`Mathlib.CategoryTheory.Comma.Over.Sections` (new file)	671
`Mathlib.CategoryTheory.LocallyCartesianClosed.Basic` (new file)	672

Declarations diff

+ CartesianClosedOver.hasPushforwards
+ ExponentiableMorphism
+ Functor.toOverTerminal
+ HasPushforwards
+ Limits.baseChange
+ LocallyCartesianClosed
+ Over.sigmaReindexNatIsoTensorLeft
+ Over.sigmaReindexNatIsoTensorLeft_hom_app
+ OverMkHom
+ Pi
+ Reindex
+ Sigma
+ baseChange
+ cartesianClosed
+ cartesianClosedOver
+ comp
+ coreHomEquiv
+ counit_app
+ counit_app_pullback_fst
+ counit_app_pullback_snd
+ counit_app_pullback_snd_eq_homMk
+ curryId
+ equivOverTerminal
+ equivalenceRightAdjointIsoInverse
+ ev
+ ev'
+ expIso
+ exponentiableOverMk
+ forgetAdjStar
+ fst
+ fstProj
+ fstProj_sigma_fst
+ homEquiv
+ homEquiv_symm
+ id
+ isBinaryProductSigmaReindex
+ iteratedSliceBackward_forget
+ map
+ mapAdjunction
+ map_comp_fst
+ map_homMk_left
+ map_left
+ mkOfCartesianClosedOver
+ mkOfHasPushforwards
+ ofOverExponentiable
+ overHomMk
+ overLocallyCartesianClosed
+ prodIsoTensorObj
+ prodIsoTensorObj_hom_fst
+ prodIsoTensorObj_hom_snd
+ prodIsoTensorObj_inv_fst
+ prodIsoTensorObj_inv_snd
+ prodMap_comp_prodIsoTensorObj_hom
+ pushforwardAdj
+ pushforwardCompIso
+ pushforwardCurry
+ pushforwardUncurry
+ pushforward_curry_uncurry
+ pushforward_uncurry_curry
+ pushfowardIdIso
+ sections
+ sectionsCurry
+ sectionsCurryAux
+ sectionsMap
+ sectionsMap_comp
+ sectionsMap_id
+ sectionsObj
+ sectionsUncurry
+ sections_curry_uncurry
+ sections_uncurry_curry
+ sigmaReindexIsoProd
+ sigmaReindexIsoProdMk
+ sigmaReindexIsoProd_hom_comp_fst
+ sigmaReindexIsoProd_hom_comp_snd
+ sigmaSymmetryIso
+ sndProj
+ starIsoToOverTerminal
+ starIteratedSliceForwardIsoPullback
+ starPullbackIsoStar
+ starSectionsAdj
+ star_map
+ symmetryObjIso
+ symmetry_hom
+ unit_app
++ hom
++ pushforward
++- 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).

mathlib4-dependent-issues-bot · 2025-02-26T12:44:32Z

This PR/issue depends on:

feat(CategoryTheory): Locally Cartesian Closed Categories (Prelim) #21525
feat(CategoryTheory): Locally Cartesian Closed Categories (Sections Right Adjoint) #22319
By Dependent Issues (🤖). Happy coding!

…ian-closed-categories

…mmunity/mathlib4 into sina-lccc-sections

…community/mathlib4 into sina-lccc-definition

leanprover-community-bot-assistant · 2025-04-09T13:30:48Z

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

sinhp and others added 30 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

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

f84c317

…ian-closed-categories

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

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>

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

8df2a83

…ian-closed-categories

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

3fb85cb

…ian-closed-categories

Over.sections

6efafde

whiskerLeft_prod_map

95b8435

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

58c5b52

…ian-closed-categories

adding Over.Sections to mathlib

f594238

How I would do it

b9152e8

Merge remote-tracking branch 'origin/markus/sina' into sina-locally-c…

c9ed46d

…artesian-closed-categories

doc strings

4615aee

sinhp added 10 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

move Over.Sections to the next PR for focus review

931288f

sections as the right adjoint of star

4c221d0

definition of lccc

798f924

github-actions bot added large-import Automatically added label for PRs with a significant increase in transitive imports t-category-theory Category theory labels Feb 26, 2025

doc strings

e143365

mathlib4-dependent-issues-bot added the blocked-by-other-PR This PR depends on another PR (this label is automatically managed by a bot) label Feb 26, 2025

fix

2eb8d16

sinhp mentioned this pull request Feb 26, 2025

feat(CategoryTheory): Locally Cartesian Closed Categories (Beck-Chevalley Conditions) #22340

Open

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

sinhp added 7 commits March 6, 2025 17:51

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

9c6c92b

…ian-closed-categories

sections as the right adjoint of star

c73be83

Merge branch 'sina-lccc-sections' of https://github.com/leanprover-co…

823fc7d

…mmunity/mathlib4 into sina-lccc-sections

definition of lccc

7070f70

doc strings

1f108f2

fix

5804281

Merge branch 'sina-lccc-definition' of https://github.com/leanprover-…

e323e05

…community/mathlib4 into sina-lccc-definition

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

sinhp mentioned this pull request Oct 9, 2025

feat(CategoryTheory): Basics of Locally Cartesian Closed Categories #30375

Open

3 tasks

Provide feedback

Saved searches

Use saved searches to filter your results more quickly

feat(CategoryTheory): Locally Cartesian Closed Categories (Definition)#22321

feat(CategoryTheory): Locally Cartesian Closed Categories (Definition)#22321
sinhp wants to merge 56 commits intomasterfrom
sina-lccc-definition

sinhp commented Feb 26, 2025 •

edited

Loading

Uh oh!

github-actions bot commented Feb 26, 2025 •

edited

Loading

Import changes for modified files

Declarations diff

Uh oh!

mathlib4-dependent-issues-bot commented Feb 26, 2025

Uh oh!

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

Uh oh!

Reviewers

Assignees

Labels

Projects

Milestone

Development

Uh oh!

4 participants

Conversation

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

Uh oh!

Uh oh!

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

Uh oh!

PR summary e323e05d58

Import changes for modified files

Declarations diff

Uh oh!

mathlib4-dependent-issues-bot commented Feb 26, 2025

Uh oh!

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

Uh oh!

Reviewers

Assignees

Labels

Projects

Milestone

Development

Uh oh!

4 participants

sinhp commented Feb 26, 2025 •

edited

Loading

github-actions bot commented Feb 26, 2025 •

edited

Loading