Skip to content

feat: LCCC section #30373

New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Jump to bottom
Open
wants to merge 3 commits into
base: master
Choose a base branch
from
Open

feat: LCCC section #30373

wants to merge 3 commits into from

Conversation

sinhp
Copy link
Collaborator

@sinhp sinhp commented Oct 9, 2025 •
edited
Loading

This PR defines Over.sections, and proves it is a right adjoint to the Over.star, thereby solving an existing TODO in Over.pullback file.

In LCCCs development, the sections functor is used to define the right adjoint to the pullback functor Over.pullback.

Open in Gitpod

@github-actions github-actions bot added t-category-theory Category theory large-import Automatically added label for PRs with a significant increase in transitive imports labels Oct 9, 2025
@github-actions GitHub Actions
Copy link

github-actions bot commented Oct 9, 2025 •
edited
Loading

PR summary cc0d5cbbe4

Import changes exceeding 2%

% File
+52.82% Mathlib.CategoryTheory.Comma.Over.Pullback
+5.14% Mathlib.CategoryTheory.Galois.Examples

Import changes for modified files

Dependency changes

File Base Count Head Count Change
Mathlib.CategoryTheory.Comma.Over.Pullback 496 758 +262 (+52.82%)
Mathlib.CategoryTheory.Galois.Examples 1071 1126 +55 (+5.14%)
Import changes for all files
Files Import difference
10 files Mathlib.Algebra.Category.ModuleCat.Sheaf.PullbackContinuous Mathlib.CategoryTheory.Abelian.FreydMitchell Mathlib.CategoryTheory.Abelian.GrothendieckAxioms.Colim Mathlib.CategoryTheory.Abelian.GrothendieckCategory.ColimCoyoneda Mathlib.CategoryTheory.Abelian.GrothendieckCategory.Coseparator Mathlib.CategoryTheory.Abelian.GrothendieckCategory.EnoughInjectives Mathlib.CategoryTheory.Abelian.GrothendieckCategory.ModuleEmbedding.GabrielPopescu Mathlib.CategoryTheory.Abelian.GrothendieckCategory.ModuleEmbedding.Opposite Mathlib.CategoryTheory.Abelian.GrothendieckCategory.Monomorphisms Mathlib.CategoryTheory.Abelian.GrothendieckCategory.Subobject
 3
Mathlib.CategoryTheory.Abelian.GrothendieckAxioms.Indization Mathlib.CategoryTheory.Generator.Indization 4
3 files Mathlib.CategoryTheory.SmallObject.Basic Mathlib.CategoryTheory.SmallObject.IsCardinalForSmallObjectArgument Mathlib.Topology.CWComplex.Abstract.Basic
 9
5 files Mathlib.AlgebraicTopology.RelativeCellComplex.Basic Mathlib.CategoryTheory.MorphismProperty.FunctorCategory Mathlib.CategoryTheory.MorphismProperty.TransfiniteComposition Mathlib.CategoryTheory.SmallObject.TransfiniteCompositionLifting Mathlib.CategoryTheory.SmallObject.TransfiniteIteration
 11
Mathlib.Condensed.Light.CartesianClosed 15
Mathlib.Condensed.CartesianClosed 16
44 files Mathlib.AlgebraicGeometry.AffineSpace Mathlib.AlgebraicGeometry.Cover.Directed Mathlib.AlgebraicGeometry.Cover.Sigma Mathlib.AlgebraicGeometry.Fiber Mathlib.AlgebraicGeometry.GluingOneHypercover Mathlib.AlgebraicGeometry.IdealSheaf.Basic Mathlib.AlgebraicGeometry.IdealSheaf.Functorial Mathlib.AlgebraicGeometry.IdealSheaf.Subscheme 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.Descent 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.LocalClosure Mathlib.AlgebraicGeometry.Morphisms.LocalIso 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.Morphisms.UniversallyOpen Mathlib.AlgebraicGeometry.Noetherian Mathlib.AlgebraicGeometry.PullbackCarrier Mathlib.AlgebraicGeometry.Pullbacks Mathlib.AlgebraicGeometry.ResidueField Mathlib.AlgebraicGeometry.Sites.BigZariski Mathlib.AlgebraicGeometry.Sites.Pretopology Mathlib.AlgebraicGeometry.Sites.Representability Mathlib.AlgebraicGeometry.SpreadingOut Mathlib.AlgebraicGeometry.Stalk
 17
Mathlib.Condensed.AB Mathlib.Condensed.Light.AB 18
18 files Mathlib.RepresentationTheory.GroupCohomology.Basic Mathlib.RepresentationTheory.GroupCohomology.Functoriality Mathlib.RepresentationTheory.GroupCohomology.Hilbert90 Mathlib.RepresentationTheory.GroupCohomology.LowDegree Mathlib.RepresentationTheory.GroupCohomology.Resolution Mathlib.RepresentationTheory.Homological.FiniteCyclic Mathlib.RepresentationTheory.Homological.GroupCohomology.Basic Mathlib.RepresentationTheory.Homological.GroupCohomology.Functoriality Mathlib.RepresentationTheory.Homological.GroupCohomology.Hilbert90 Mathlib.RepresentationTheory.Homological.GroupCohomology.LongExactSequence Mathlib.RepresentationTheory.Homological.GroupCohomology.LowDegree Mathlib.RepresentationTheory.Homological.GroupCohomology.Shapiro Mathlib.RepresentationTheory.Homological.GroupHomology.Basic Mathlib.RepresentationTheory.Homological.GroupHomology.Functoriality Mathlib.RepresentationTheory.Homological.GroupHomology.LongExactSequence Mathlib.RepresentationTheory.Homological.GroupHomology.LowDegree Mathlib.RepresentationTheory.Homological.GroupHomology.Shapiro Mathlib.RepresentationTheory.Homological.Resolution
 24
Mathlib.CategoryTheory.Sites.SheafCohomology.Basic 31
7 files Mathlib.RepresentationTheory.Character Mathlib.RepresentationTheory.Coinvariants Mathlib.RepresentationTheory.FDRep Mathlib.RepresentationTheory.FiniteIndex Mathlib.RepresentationTheory.Induced Mathlib.RepresentationTheory.Invariants Mathlib.RepresentationTheory.Tannaka
 32
Mathlib.Algebra.Homology.GrothendieckAbelian 34
3 files Mathlib.Algebra.Category.ModuleCat.Presheaf.Generator Mathlib.Algebra.Category.ModuleCat.Presheaf.Pullback Mathlib.AlgebraicTopology.SingularHomology.Basic
 35
3 files Mathlib.AlgebraicGeometry.Gluing Mathlib.AlgebraicGeometry.ProjectiveSpectrum.Basic Mathlib.CategoryTheory.Abelian.GrothendieckAxioms.Sheaf
 36
Mathlib.CategoryTheory.Abelian.GrothendieckAxioms.Types 37
4 files Mathlib.Algebra.Category.Grp.AB Mathlib.Algebra.Category.ModuleCat.AB Mathlib.CategoryTheory.Abelian.GrothendieckAxioms.Connected Mathlib.RingTheory.PicardGroup
 38
14 files Mathlib.AlgebraicGeometry.AffineScheme Mathlib.AlgebraicGeometry.Cover.MorphismProperty Mathlib.AlgebraicGeometry.Cover.Open Mathlib.AlgebraicGeometry.FunctionField Mathlib.AlgebraicGeometry.GammaSpecAdjunction Mathlib.AlgebraicGeometry.OpenImmersion Mathlib.AlgebraicGeometry.ProjectiveSpectrum.Scheme Mathlib.AlgebraicGeometry.Properties Mathlib.AlgebraicGeometry.Restrict Mathlib.AlgebraicGeometry.Sites.MorphismProperty Mathlib.AlgebraicGeometry.Sites.SmallAffineZariski Mathlib.CategoryTheory.Abelian.GrothendieckAxioms.Basic Mathlib.CategoryTheory.Abelian.GrothendieckAxioms.FunctorCategory Mathlib.CategoryTheory.Abelian.GrothendieckCategory.Basic
 39
3 files Mathlib.Algebra.Category.CommBialgCat Mathlib.Algebra.Homology.AlternatingConst Mathlib.AlgebraicTopology.ExtraDegeneracy
 42
Mathlib.Algebra.Category.CommAlgCat.Monoidal Mathlib.Algebra.Homology.LocalCohomology 43
Mathlib.Algebra.Category.Ring.Under.Limits 44
Mathlib.NumberTheory.LSeries.PrimesInAP Mathlib.Tactic 46
23 files 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.MooreComplex Mathlib.CategoryTheory.Sites.CartesianClosed Mathlib.CategoryTheory.Sites.MayerVietorisSquare Mathlib.Topology.Sheaves.MayerVietoris
 47
Mathlib.Algebra.Homology.ConcreteCategory Mathlib.CategoryTheory.Abelian.Monomorphisms 49
Mathlib.Algebra.Category.CommAlgCat.FiniteType Mathlib.RingTheory.Flat.CategoryTheory 51
27 files Mathlib.Algebra.Category.ModuleCat.Biproducts Mathlib.Algebra.Category.ModuleCat.Free Mathlib.Algebra.Homology.ShortComplex.ConcreteCategory Mathlib.Algebra.Homology.ShortComplex.ModuleCat Mathlib.Algebra.Module.PID Mathlib.Analysis.Fourier.FiniteAbelian.PontryaginDuality Mathlib.FieldTheory.Galois.NormalBasis Mathlib.GroupTheory.FiniteAbelian.Basic Mathlib.GroupTheory.FiniteAbelian.Duality Mathlib.NumberTheory.DirichletCharacter.Orthogonality Mathlib.NumberTheory.MulChar.Duality Mathlib.NumberTheory.NumberField.Discriminant.Different Mathlib.NumberTheory.RamificationInertia.Unramified Mathlib.RingTheory.DedekindDomain.Different Mathlib.RingTheory.Flat.TorsionFree Mathlib.RingTheory.Grassmannian Mathlib.RingTheory.LocalRing.Module Mathlib.RingTheory.Regular.Category Mathlib.RingTheory.RingHom.Etale Mathlib.RingTheory.RingHom.Smooth Mathlib.RingTheory.Smooth.Local Mathlib.RingTheory.Smooth.Locus Mathlib.RingTheory.Spectrum.Prime.FreeLocus Mathlib.RingTheory.Unramified.LocalRing Mathlib.Topology.Category.Profinite.Nobeling.Induction Mathlib.Topology.Category.Profinite.Nobeling.Successor Mathlib.Topology.Category.Profinite.Nobeling
 54
18 files Mathlib.Algebra.Category.ContinuousCohomology.Basic Mathlib.Algebra.Homology.DerivedCategory.Ext.EnoughInjectives Mathlib.Algebra.Homology.DerivedCategory.Ext.EnoughProjectives Mathlib.Algebra.Homology.DerivedCategory.Ext.ExactSequences Mathlib.CategoryTheory.Abelian.Ext Mathlib.CategoryTheory.Abelian.Injective.Dimension Mathlib.CategoryTheory.Abelian.Projective.Dimension Mathlib.CategoryTheory.Galois.Action Mathlib.CategoryTheory.Galois.Basic Mathlib.CategoryTheory.Galois.Decomposition Mathlib.CategoryTheory.Galois.Equivalence 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
 55
58 files Mathlib.Algebra.Homology.BifunctorHomotopy Mathlib.Algebra.Homology.BifunctorShift Mathlib.Algebra.Homology.DerivedCategory.Basic Mathlib.Algebra.Homology.DerivedCategory.ExactFunctor Mathlib.Algebra.Homology.DerivedCategory.Ext.Basic Mathlib.Algebra.Homology.DerivedCategory.Ext.ExtClass Mathlib.Algebra.Homology.DerivedCategory.Fractions Mathlib.Algebra.Homology.DerivedCategory.FullyFaithful Mathlib.Algebra.Homology.DerivedCategory.HomologySequence Mathlib.Algebra.Homology.DerivedCategory.Linear Mathlib.Algebra.Homology.DerivedCategory.ShortExact Mathlib.Algebra.Homology.DerivedCategory.SingleTriangle Mathlib.Algebra.Homology.DerivedCategory.TStructure Mathlib.Algebra.Homology.Embedding.AreComplementary Mathlib.Algebra.Homology.Embedding.CochainComplex Mathlib.Algebra.Homology.Embedding.Connect 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.CategoryTheory.Abelian.Injective.Resolution Mathlib.CategoryTheory.Abelian.LeftDerived Mathlib.CategoryTheory.Abelian.Projective.Resolution Mathlib.CategoryTheory.Abelian.RightDerived Mathlib.CategoryTheory.Monoidal.Tor Mathlib.CategoryTheory.Preadditive.Injective.Resolution Mathlib.CategoryTheory.Preadditive.Projective.Resolution
 56
Mathlib.CategoryTheory.Idempotents.HomologicalComplex Mathlib.RingTheory.Invariant.Profinite 57
129 files Mathlib.AlgebraicGeometry.EllipticCurve.Reduction Mathlib.AlgebraicTopology.Quasicategory.Basic Mathlib.AlgebraicTopology.Quasicategory.Nerve Mathlib.AlgebraicTopology.Quasicategory.StrictSegal Mathlib.AlgebraicTopology.SimplicialSet.CategoryWithFibrations Mathlib.AlgebraicTopology.SimplicialSet.KanComplex Mathlib.Analysis.Fourier.ZMod Mathlib.Analysis.SpecialFunctions.Complex.CircleAddChar Mathlib.CategoryTheory.MorphismProperty.Ind Mathlib.FieldTheory.Laurent Mathlib.FieldTheory.RatFunc.AsPolynomial Mathlib.FieldTheory.RatFunc.Degree Mathlib.NumberTheory.ClassNumber.Finite Mathlib.NumberTheory.ClassNumber.FunctionField Mathlib.NumberTheory.Cyclotomic.Basic Mathlib.NumberTheory.Cyclotomic.Discriminant Mathlib.NumberTheory.Cyclotomic.Embeddings Mathlib.NumberTheory.Cyclotomic.Gal Mathlib.NumberTheory.Cyclotomic.PID Mathlib.NumberTheory.Cyclotomic.PrimitiveRoots Mathlib.NumberTheory.Cyclotomic.Rat Mathlib.NumberTheory.Cyclotomic.Three Mathlib.NumberTheory.DirichletCharacter.GaussSum Mathlib.NumberTheory.FLT.Three Mathlib.NumberTheory.Fermat Mathlib.NumberTheory.FunctionField Mathlib.NumberTheory.GaussSum Mathlib.NumberTheory.JacobiSum.Basic Mathlib.NumberTheory.LSeries.DirichletContinuation Mathlib.NumberTheory.LSeries.Nonvanishing Mathlib.NumberTheory.LSeries.ZMod Mathlib.NumberTheory.LegendreSymbol.AddCharacter Mathlib.NumberTheory.LegendreSymbol.JacobiSymbol Mathlib.NumberTheory.LegendreSymbol.QuadraticChar.GaussSum Mathlib.NumberTheory.LegendreSymbol.QuadraticReciprocity Mathlib.NumberTheory.LucasLehmer Mathlib.NumberTheory.NumberField.AdeleRing Mathlib.NumberTheory.NumberField.Basic Mathlib.NumberTheory.NumberField.CMField Mathlib.NumberTheory.NumberField.CanonicalEmbedding.Basic Mathlib.NumberTheory.NumberField.CanonicalEmbedding.ConvexBody Mathlib.NumberTheory.NumberField.CanonicalEmbedding.FundamentalCone Mathlib.NumberTheory.NumberField.CanonicalEmbedding.NormLeOne Mathlib.NumberTheory.NumberField.CanonicalEmbedding.PolarCoord Mathlib.NumberTheory.NumberField.ClassNumber Mathlib.NumberTheory.NumberField.Completion Mathlib.NumberTheory.NumberField.DedekindZeta Mathlib.NumberTheory.NumberField.Discriminant.Basic Mathlib.NumberTheory.NumberField.Discriminant.Defs Mathlib.NumberTheory.NumberField.Embeddings Mathlib.NumberTheory.NumberField.EquivReindex Mathlib.NumberTheory.NumberField.FinitePlaces Mathlib.NumberTheory.NumberField.FractionalIdeal Mathlib.NumberTheory.NumberField.House Mathlib.NumberTheory.NumberField.Ideal.Asymptotics Mathlib.NumberTheory.NumberField.Ideal.Basic Mathlib.NumberTheory.NumberField.Ideal.KummerDedekind Mathlib.NumberTheory.NumberField.Ideal Mathlib.NumberTheory.NumberField.InfinitePlace.Basic Mathlib.NumberTheory.NumberField.InfinitePlace.Completion Mathlib.NumberTheory.NumberField.InfinitePlace.Embeddings Mathlib.NumberTheory.NumberField.InfinitePlace.Ramification Mathlib.NumberTheory.NumberField.InfinitePlace.TotallyRealComplex Mathlib.NumberTheory.NumberField.Norm Mathlib.NumberTheory.NumberField.ProductFormula Mathlib.NumberTheory.NumberField.Units.Basic Mathlib.NumberTheory.NumberField.Units.DirichletTheorem Mathlib.NumberTheory.NumberField.Units.Regulator Mathlib.NumberTheory.Padics.WithVal Mathlib.NumberTheory.PrimesCongruentOne Mathlib.NumberTheory.RamificationInertia.Basic Mathlib.NumberTheory.RamificationInertia.Galois Mathlib.RingTheory.DedekindDomain.AdicValuation Mathlib.RingTheory.DedekindDomain.Dvr Mathlib.RingTheory.DedekindDomain.Factorization Mathlib.RingTheory.DedekindDomain.FiniteAdeleRing Mathlib.RingTheory.DedekindDomain.Instances Mathlib.RingTheory.DedekindDomain.IntegralClosure Mathlib.RingTheory.DedekindDomain.PID Mathlib.RingTheory.DedekindDomain.SInteger Mathlib.RingTheory.DedekindDomain.SelmerGroup Mathlib.RingTheory.Etale.Field Mathlib.RingTheory.FractionalIdeal.Norm Mathlib.RingTheory.Frobenius Mathlib.RingTheory.Ideal.Int Mathlib.RingTheory.Ideal.Norm.AbsNorm Mathlib.RingTheory.Ideal.Norm.RelNorm Mathlib.RingTheory.IntegralClosure.IntegralRestrict Mathlib.RingTheory.Invariant.Basic Mathlib.RingTheory.Invariant Mathlib.RingTheory.KrullDimension.Module Mathlib.RingTheory.LaurentSeries Mathlib.RingTheory.LittleWedderburn Mathlib.RingTheory.LocalProperties.Basic Mathlib.RingTheory.LocalProperties.IntegrallyClosed Mathlib.RingTheory.LocalProperties.Reduced Mathlib.RingTheory.LocalProperties.Semilocal Mathlib.RingTheory.Localization.Finiteness Mathlib.RingTheory.Localization.Free Mathlib.RingTheory.Polynomial.Cyclotomic.Basic Mathlib.RingTheory.Polynomial.Cyclotomic.Eval Mathlib.RingTheory.Polynomial.Cyclotomic.Expand Mathlib.RingTheory.Polynomial.Cyclotomic.Factorization Mathlib.RingTheory.Polynomial.Cyclotomic.Roots Mathlib.RingTheory.Polynomial.Eisenstein.IsIntegral Mathlib.RingTheory.Regular.Depth Mathlib.RingTheory.RingHom.FaithfullyFlat Mathlib.RingTheory.RingHom.FinitePresentation Mathlib.RingTheory.RingHom.FiniteType Mathlib.RingTheory.RingHom.Finite Mathlib.RingTheory.RingHom.Flat Mathlib.RingTheory.RingHom.Injective Mathlib.RingTheory.RingHom.Integral Mathlib.RingTheory.RingHom.Locally Mathlib.RingTheory.RingHom.OpenImmersion Mathlib.RingTheory.RingHom.StandardSmooth Mathlib.RingTheory.RingHom.Surjective Mathlib.RingTheory.RingHom.Unramified Mathlib.RingTheory.RingHomProperties Mathlib.RingTheory.RootsOfUnity.AlgebraicallyClosed Mathlib.RingTheory.Spectrum.Prime.Module Mathlib.RingTheory.Support Mathlib.RingTheory.Trace.Quotient Mathlib.RingTheory.Unramified.Field Mathlib.RingTheory.Unramified.Locus Mathlib.RingTheory.Valuation.Discrete.Basic Mathlib.Tactic.NormNum.LegendreSymbol Mathlib.Topology.Algebra.Ring.Compact Mathlib.Topology.Algebra.Valued.WithVal
 58
3 files Mathlib.CategoryTheory.Abelian.Injective.Basic Mathlib.CategoryTheory.Abelian.Projective.Basic Mathlib.CategoryTheory.Abelian.Yoneda
 60
8 files Mathlib.Algebra.Category.ModuleCat.Simple Mathlib.Algebra.Homology.ShortComplex.ExactFunctor Mathlib.CategoryTheory.Abelian.Exact Mathlib.CategoryTheory.Abelian.Pseudoelements Mathlib.CategoryTheory.Generator.Abelian Mathlib.CategoryTheory.Noetherian Mathlib.CategoryTheory.Subobject.ArtinianObject Mathlib.CategoryTheory.Subobject.NoetherianObject
 61
4 files Mathlib.Algebra.Category.CommAlgCat.Basic Mathlib.CategoryTheory.Abelian.Subobject Mathlib.CategoryTheory.Preadditive.Schur Mathlib.CategoryTheory.Simple
 62
3 files Mathlib.Algebra.Homology.BifunctorAssociator Mathlib.Algebra.Homology.Monoidal Mathlib.CategoryTheory.Dialectica.Monoidal
 64
3 files Mathlib.CategoryTheory.Closed.Ideal Mathlib.CategoryTheory.Generator.Sheaf Mathlib.CategoryTheory.Sites.MorphismProperty
 66
4 files Mathlib.Algebra.Homology.BifunctorFlip Mathlib.Algebra.Homology.Bifunctor Mathlib.Algebra.Homology.TotalComplexSymmetry Mathlib.Algebra.Homology.TotalComplex
 67
3 files Mathlib.Algebra.Category.Grp.Subobject Mathlib.Algebra.Category.ModuleCat.Subobject Mathlib.Algebra.Homology.HomologicalComplexBiprod
 70
4 files Mathlib.Algebra.Homology.Additive Mathlib.Algebra.Homology.Embedding.Restriction Mathlib.Algebra.Homology.Linear Mathlib.Algebra.Homology.Square
 71
Mathlib.CategoryTheory.Adjunction.AdjointFunctorTheorems Mathlib.CategoryTheory.Subobject.HasCardinalLT 72
3 files Mathlib.Algebra.Category.Ring.Under.Basic Mathlib.Algebra.Homology.HomologicalComplexLimits Mathlib.CategoryTheory.Generator.HomologicalComplex
 73
3 files Mathlib.CategoryTheory.MorphismProperty.Local Mathlib.CategoryTheory.Preadditive.Injective.LiftingProperties Mathlib.CategoryTheory.Preadditive.Projective.LiftingProperties
 74
9 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 Mathlib.CategoryTheory.Localization.FiniteProducts
 75
22 files Mathlib.AlgebraicTopology.ModelCategory.Basic Mathlib.AlgebraicTopology.ModelCategory.BrownLemma Mathlib.AlgebraicTopology.ModelCategory.Cylinder Mathlib.AlgebraicTopology.ModelCategory.Homotopy Mathlib.AlgebraicTopology.ModelCategory.Instances Mathlib.AlgebraicTopology.ModelCategory.IsCofibrant Mathlib.AlgebraicTopology.ModelCategory.JoyalTrick Mathlib.AlgebraicTopology.ModelCategory.LeftHomotopy Mathlib.AlgebraicTopology.ModelCategory.PathObject Mathlib.AlgebraicTopology.ModelCategory.RightHomotopy Mathlib.AlgebraicTopology.RelativeCellComplex.AttachCells Mathlib.CategoryTheory.Generator.Preadditive Mathlib.CategoryTheory.Limits.Preserves.Shapes.Square Mathlib.CategoryTheory.Limits.Shapes.Pullback.Square Mathlib.CategoryTheory.MorphismProperty.Descent Mathlib.CategoryTheory.MorphismProperty.LiftingProperty Mathlib.CategoryTheory.MorphismProperty.Limits Mathlib.CategoryTheory.MorphismProperty.OverAdjunction Mathlib.CategoryTheory.MorphismProperty.Representable Mathlib.CategoryTheory.MorphismProperty.RetractArgument Mathlib.CategoryTheory.MorphismProperty.WeakFactorizationSystem Mathlib.CategoryTheory.SmallObject.Construction
 76
6 files Mathlib.Algebra.Homology.ImageToKernel Mathlib.CategoryTheory.ExtremalEpi Mathlib.CategoryTheory.Generator.Basic Mathlib.CategoryTheory.Generator.Presheaf Mathlib.CategoryTheory.Subobject.Lattice Mathlib.CategoryTheory.Subobject.Limits
 80
Mathlib.CategoryTheory.Subobject.Comma Mathlib.CategoryTheory.Subpresheaf.Subobject 85
7 files Mathlib.CategoryTheory.Dialectica.Basic Mathlib.CategoryTheory.Subobject.Basic Mathlib.CategoryTheory.Subobject.FactorThru Mathlib.CategoryTheory.Subobject.Presheaf Mathlib.CategoryTheory.Subobject.Types Mathlib.CategoryTheory.Subobject.WellPowered Mathlib.CategoryTheory.Topos.Classifier
 89
Mathlib.CategoryTheory.Subobject.MonoOver Mathlib.CategoryTheory.Subterminal 92
Mathlib.CategoryTheory.Limits.Shapes.Diagonal 93
Mathlib.CategoryTheory.Comma.Over.Pullback 262
Mathlib.CategoryTheory.LocallyCartesianClosed.Sections (new file) 759

Declarations diff

+ Functor.toOverTerminal
+ Limits.baseChange
+ Over.sigmaReindexNatIsoTensorLeft
+ Over.sigmaReindexNatIsoTensorLeft_hom_app
+ Reindex
+ Sigma
+ baseChange
+ coreHomEquiv
+ counit_app
+ counit_app_pullback_fst
+ counit_app_pullback_snd
+ counit_app_pullback_snd_eq_homMk
+ curryId
+ equivOverTerminal
+ equivalenceRightAdjointIsoInverse
+ fst
+ fstProj
+ fstProj_sigma_fst
+ 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⟩⟩
+ isBinaryProductSigmaReindex
+ iteratedSliceBackward_forget
+ map
+ mapAdjunction
+ map_comp_fst
+ map_homMk_left
+ map_left
+ overHomMk
+ prodIsoTensorObj
+ prodIsoTensorObj_hom_fst
+ prodIsoTensorObj_hom_snd
+ prodIsoTensorObj_inv_fst
+ prodIsoTensorObj_inv_snd
+ prodMap_comp_prodIsoTensorObj_hom
+ 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
+-+ forgetAdjStar
+-+ star
- forgetMapTerminal
- instance : (forget X).IsLeftAdjoint := ⟨_, ⟨forgetAdjStar X⟩⟩
- instance : (star X).IsRightAdjoint := ⟨_, ⟨forgetAdjStar X⟩⟩
- isLeftAdjoint_post
- postAdjunctionLeft

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

@sinhp sinhp changed the title feat: Lccc section feat: LCCC section Oct 9, 2025
@sinhp sinhp mentioned this pull request Oct 9, 2025
Open
1 task
@mathlib4-dependent-issues-bot 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 Oct 9, 2025
@mathlib4-dependent-issues-bot
Copy link
Collaborator

This PR/issue depends on:

@mathlib4-merge-conflict-bot mathlib4-merge-conflict-bot added the merge-conflict The PR has a merge conflict with master, and needs manual merging. (this label is managed by a bot) label Oct 10, 2025
@mathlib4-merge-conflict-bot
Copy link
Collaborator

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

Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Reviewers
No reviews
Assignees
No one assigned
Labels
blocked-by-other-PR This PR depends on another PR (this label is automatically managed by a bot) large-import Automatically added label for PRs with a significant increase in transitive imports merge-conflict The PR has a merge conflict with master, and needs manual merging. (this label is managed by a bot) t-category-theory Category theory
Projects
None yet
Milestone
No milestone
Development

Successfully merging this pull request may close these issues.
3 participants
@sinhp @mathlib4-dependent-issues-bot @mathlib4-merge-conflict-bot