refactor(CategoryTheory): insert missing functor associators and unitors

[kim-em]

This PR inserts the functor associators and unitors that Mathlib currently omits, or applies in the wrong direction, when it identifies (F ⋙ G) ⋙ H with F ⋙ G ⋙ H or 𝟭 C ⋙ F with F by unfolding Functor.comp and Functor.id. None of these changes are necessary, but all reduce some defeq abuse that hopefully will make life easier in future.

It is extracted from Paul Reichert's experiment making Functor.comp and Functor.id instance_reducible with a semireducible map field (master...leanprover-community:mathlib4-nightly-testing:datokrat/functorcomp, discussed at https://leanprover.zulipchat.com/#narrow/channel/113488-general/topic/backward.2EisDefEq.2ErespectTransparency), keeping only the bracketing and unit fixes so that future experiments of this kind have less to repair. The Functor.comp_map proof changes from that branch are not included, and the corresponding changes for (pre)sheaves of modules are in a separate PR.

The notable API changes are: limit.pre_pre, post_post, pre_post and their duals now relate the two bracketings through HasLimit.isoOfNatIso (Functor.associator _ _ _); StructuredArrow.final_map₂_id takes β : T ⋙ S ⟶ 𝟭 C ⋙ T'; and Join.mkNatTrans and mkNatIso carry associators in their (autoparam) compatibility hypothesis.

🤖 Prepared with Claude Code

[github-actions]

PR summary e4dbc82828

Import changes for modified files

Dependency changes

File	Base Count	Head Count	Change
Mathlib.CategoryTheory.Monoidal.Cartesian.Basic	794	795	+1 (+0.13%)
Mathlib.CategoryTheory.Filtered.Final	837	838	+1 (+0.12%)
Mathlib.CategoryTheory.Comma.Final	839	840	+1 (+0.12%)
Mathlib.CategoryTheory.Limits.Constructions.Over.Connected	840	841	+1 (+0.12%)
Mathlib.CategoryTheory.Abelian.GrothendieckCategory.Subobject	1231	1232	+1 (+0.08%)
Mathlib.AlgebraicGeometry.ColimitsOver	2594	2595	+1 (+0.04%)

Import changes for all files

Files

Import difference

383 files Mathlib.Algebra.Category.CommAlgCat.Monoidal Mathlib.Algebra.Category.CommBialgCat Mathlib.Algebra.Category.CommHopfAlgCat Mathlib.Algebra.Category.Grp.CartesianMonoidal Mathlib.Algebra.Category.Grp.LeftExactFunctor Mathlib.Algebra.Category.ModuleCat.Adjunctions Mathlib.Algebra.Category.ModuleCat.Differentials.Presheaf Mathlib.Algebra.Category.ModuleCat.LeftResolution Mathlib.Algebra.Category.ModuleCat.Presheaf.ColimitFunctor Mathlib.Algebra.Category.ModuleCat.Presheaf.Free Mathlib.Algebra.Category.ModuleCat.Presheaf.Generator Mathlib.Algebra.Category.ModuleCat.Presheaf.Monoidal Mathlib.Algebra.Category.ModuleCat.Presheaf.OfCommRing Mathlib.Algebra.Category.ModuleCat.Presheaf.Pullback Mathlib.Algebra.Category.ModuleCat.Presheaf.PushforwardZeroMonoidal Mathlib.Algebra.Category.ModuleCat.Sheaf.LocallyFree Mathlib.Algebra.Category.ModuleCat.Sheaf.PullbackContinuous Mathlib.Algebra.Category.ModuleCat.Sheaf.PullbackFree Mathlib.Algebra.Category.ModuleCat.Sheaf.Quasicoherent Mathlib.Algebra.Category.Ring.FinitePresentation Mathlib.Algebra.Category.Ring.Under.Property Mathlib.AlgebraicGeometry.AffineSpace Mathlib.AlgebraicGeometry.AffineTransitionLimit Mathlib.AlgebraicGeometry.AlgClosed.Basic Mathlib.AlgebraicGeometry.AlgebraicCycle.Basic Mathlib.AlgebraicGeometry.Artinian Mathlib.AlgebraicGeometry.Birational.Birational Mathlib.AlgebraicGeometry.Birational.Composition Mathlib.AlgebraicGeometry.Birational.Dominant Mathlib.AlgebraicGeometry.Birational.RationalMap Mathlib.AlgebraicGeometry.ColimitsOver Mathlib.AlgebraicGeometry.Cover.Directed Mathlib.AlgebraicGeometry.Cover.Over Mathlib.AlgebraicGeometry.Cover.QuasiCompact Mathlib.AlgebraicGeometry.Cover.Sigma Mathlib.AlgebraicGeometry.EffectiveEpi Mathlib.AlgebraicGeometry.Fiber Mathlib.AlgebraicGeometry.FunctionField Mathlib.AlgebraicGeometry.Geometrically.Basic Mathlib.AlgebraicGeometry.Geometrically.Connected Mathlib.AlgebraicGeometry.Geometrically.Integral Mathlib.AlgebraicGeometry.Geometrically.Irreducible Mathlib.AlgebraicGeometry.Geometrically.Reduced Mathlib.AlgebraicGeometry.GluingOneHypercover Mathlib.AlgebraicGeometry.Group.Abelian Mathlib.AlgebraicGeometry.Group.Affine Mathlib.AlgebraicGeometry.Group.Smooth Mathlib.AlgebraicGeometry.IdealSheaf.Basic Mathlib.AlgebraicGeometry.IdealSheaf.Functorial Mathlib.AlgebraicGeometry.IdealSheaf.IrreducibleComponent Mathlib.AlgebraicGeometry.IdealSheaf.Subscheme Mathlib.AlgebraicGeometry.LimitsOver Mathlib.AlgebraicGeometry.Limits Mathlib.AlgebraicGeometry.Modules.Sheaf Mathlib.AlgebraicGeometry.Modules.Tilde 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.Etale Mathlib.AlgebraicGeometry.Morphisms.FinitePresentation Mathlib.AlgebraicGeometry.Morphisms.FiniteType Mathlib.AlgebraicGeometry.Morphisms.Finite Mathlib.AlgebraicGeometry.Morphisms.FlatDescent Mathlib.AlgebraicGeometry.Morphisms.FlatMono Mathlib.AlgebraicGeometry.Morphisms.FlatRank Mathlib.AlgebraicGeometry.Morphisms.Flat Mathlib.AlgebraicGeometry.Morphisms.FormallyUnramified Mathlib.AlgebraicGeometry.Morphisms.Immersion Mathlib.AlgebraicGeometry.Morphisms.Integral Mathlib.AlgebraicGeometry.Morphisms.IsIso Mathlib.AlgebraicGeometry.Morphisms.LocalClosure Mathlib.AlgebraicGeometry.Morphisms.LocalFlatDescent Mathlib.AlgebraicGeometry.Morphisms.LocalIso Mathlib.AlgebraicGeometry.Morphisms.OpenImmersion Mathlib.AlgebraicGeometry.Morphisms.Preimmersion Mathlib.AlgebraicGeometry.Morphisms.Proper Mathlib.AlgebraicGeometry.Morphisms.QuasiCompact Mathlib.AlgebraicGeometry.Morphisms.QuasiFinite Mathlib.AlgebraicGeometry.Morphisms.QuasiSeparated Mathlib.AlgebraicGeometry.Morphisms.RingHomProperties Mathlib.AlgebraicGeometry.Morphisms.SchemeTheoreticallyDominant Mathlib.AlgebraicGeometry.Morphisms.Separated Mathlib.AlgebraicGeometry.Morphisms.SmoothFiber 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.Morphisms.WeaklyEtale Mathlib.AlgebraicGeometry.Noetherian Mathlib.AlgebraicGeometry.Normalization Mathlib.AlgebraicGeometry.OrderOfVanishing Mathlib.AlgebraicGeometry.PointsPi Mathlib.AlgebraicGeometry.ProjectiveSpectrum.Proper Mathlib.AlgebraicGeometry.Properties Mathlib.AlgebraicGeometry.PullbackCarrier Mathlib.AlgebraicGeometry.Pullbacks Mathlib.AlgebraicGeometry.QuasiAffine Mathlib.AlgebraicGeometry.RelativeGluing Mathlib.AlgebraicGeometry.ResidueField Mathlib.AlgebraicGeometry.Sites.AffineEtale Mathlib.AlgebraicGeometry.Sites.Affine Mathlib.AlgebraicGeometry.Sites.BigZariski Mathlib.AlgebraicGeometry.Sites.ConstantSheaf Mathlib.AlgebraicGeometry.Sites.ElladicCohomology Mathlib.AlgebraicGeometry.Sites.EtalePoint Mathlib.AlgebraicGeometry.Sites.Etale Mathlib.AlgebraicGeometry.Sites.Fpqc Mathlib.AlgebraicGeometry.Sites.Pretopology Mathlib.AlgebraicGeometry.Sites.Proetale Mathlib.AlgebraicGeometry.Sites.QuasiCompact Mathlib.AlgebraicGeometry.Sites.Representability Mathlib.AlgebraicGeometry.Sites.SheafQuasiCompact Mathlib.AlgebraicGeometry.Sites.SmallAffineZariski Mathlib.AlgebraicGeometry.Sites.Small Mathlib.AlgebraicGeometry.SpreadingOut Mathlib.AlgebraicGeometry.Stalk Mathlib.AlgebraicGeometry.ValuativeCriterion Mathlib.AlgebraicGeometry.ZariskisMainTheorem Mathlib.AlgebraicTopology.EilenbergSteenrod Mathlib.AlgebraicTopology.ModelCategory.Over Mathlib.AlgebraicTopology.Quasicategory.Basic Mathlib.AlgebraicTopology.Quasicategory.InnerFibration Mathlib.AlgebraicTopology.Quasicategory.Nerve Mathlib.AlgebraicTopology.Quasicategory.StrictBicategory Mathlib.AlgebraicTopology.Quasicategory.StrictSegal Mathlib.AlgebraicTopology.Quasicategory.TwoTruncatedQuasicategory Mathlib.AlgebraicTopology.RelativeCellComplex.Basic Mathlib.AlgebraicTopology.SimplicialCategory.Basic Mathlib.AlgebraicTopology.SimplicialCategory.SimplicialObject Mathlib.AlgebraicTopology.SimplicialNerve Mathlib.AlgebraicTopology.SimplicialSet.AnodyneExtensions.Basic Mathlib.AlgebraicTopology.SimplicialSet.AnodyneExtensions.Inner.Basic Mathlib.AlgebraicTopology.SimplicialSet.AnodyneExtensions.Inner.PushoutProduct Mathlib.AlgebraicTopology.SimplicialSet.AnodyneExtensions.PairingCore Mathlib.AlgebraicTopology.SimplicialSet.AnodyneExtensions.PushoutProduct Mathlib.AlgebraicTopology.SimplicialSet.AnodyneExtensions.RankNat Mathlib.AlgebraicTopology.SimplicialSet.AnodyneExtensions.Rank Mathlib.AlgebraicTopology.SimplicialSet.AnodyneExtensions.RelativeCellComplex Mathlib.AlgebraicTopology.SimplicialSet.AnodyneExtensions.UnionProd Mathlib.AlgebraicTopology.SimplicialSet.CategoryWithFibrations Mathlib.AlgebraicTopology.SimplicialSet.FiniteProd Mathlib.AlgebraicTopology.SimplicialSet.HoFunctorMonoidal Mathlib.AlgebraicTopology.SimplicialSet.Homology.HomotopyInvariance Mathlib.AlgebraicTopology.SimplicialSet.HomotopyCat Mathlib.AlgebraicTopology.SimplicialSet.Homotopy Mathlib.AlgebraicTopology.SimplicialSet.KanComplex.MulStruct Mathlib.AlgebraicTopology.SimplicialSet.KanComplex Mathlib.AlgebraicTopology.SimplicialSet.Monoidal Mathlib.AlgebraicTopology.SimplicialSet.Monomorphisms Mathlib.AlgebraicTopology.SimplicialSet.NerveAdjunction Mathlib.AlgebraicTopology.SimplicialSet.NonsingularColimit Mathlib.AlgebraicTopology.SimplicialSet.Nonsingular Mathlib.AlgebraicTopology.SimplicialSet.Presentable Mathlib.AlgebraicTopology.SimplicialSet.ProdStdSimplexOne Mathlib.AlgebraicTopology.SimplicialSet.ProdStdSimplex Mathlib.AlgebraicTopology.SimplicialSet.PushoutProduct Mathlib.AlgebraicTopology.SimplicialSet.RelativeMorphism Mathlib.AlgebraicTopology.SimplicialSet.Skeleton Mathlib.AlgebraicTopology.SimplicialSet.TopAdj Mathlib.AlgebraicTopology.SingularHomology.HomologyZero Mathlib.AlgebraicTopology.SingularHomology.HomotopyInvarianceTopCat Mathlib.AlgebraicTopology.SingularHomology.HomotopyInvariance Mathlib.CategoryTheory.Abelian.FreydMitchell Mathlib.CategoryTheory.Abelian.GrothendieckAxioms.Colim Mathlib.CategoryTheory.Abelian.GrothendieckAxioms.Indization Mathlib.CategoryTheory.Abelian.GrothendieckAxioms.PresheafOfModules Mathlib.CategoryTheory.Abelian.GrothendieckAxioms.SheafOfModules Mathlib.CategoryTheory.Abelian.GrothendieckCategory.ColimCoyoneda Mathlib.CategoryTheory.Abelian.GrothendieckCategory.Coseparator Mathlib.CategoryTheory.Abelian.GrothendieckCategory.EnoughInjectives Mathlib.CategoryTheory.Abelian.GrothendieckCategory.HasExt Mathlib.CategoryTheory.Abelian.GrothendieckCategory.ModuleEmbedding.GabrielPopescu Mathlib.CategoryTheory.Abelian.GrothendieckCategory.ModuleEmbedding.Opposite Mathlib.CategoryTheory.Abelian.GrothendieckCategory.Monomorphisms Mathlib.CategoryTheory.Abelian.GrothendieckCategory.Subobject Mathlib.CategoryTheory.Abelian.Indization Mathlib.CategoryTheory.Action.Monoidal Mathlib.CategoryTheory.Adhesive.Over Mathlib.CategoryTheory.Adhesive.PushoutProduct Mathlib.CategoryTheory.Bicategory.CatEnriched Mathlib.CategoryTheory.Category.Cat.CartesianClosed Mathlib.CategoryTheory.Category.Cat.Colimit Mathlib.CategoryTheory.Comma.Final Mathlib.CategoryTheory.CopyDiscardCategory.Cartesian Mathlib.CategoryTheory.Distributive.Cartesian Mathlib.CategoryTheory.Enriched.Basic Mathlib.CategoryTheory.Enriched.EnrichedCat Mathlib.CategoryTheory.Enriched.FunctorCategory Mathlib.CategoryTheory.Enriched.HomCongr Mathlib.CategoryTheory.Enriched.Limits.HasConicalLimits Mathlib.CategoryTheory.Enriched.Limits.HasConicalProducts Mathlib.CategoryTheory.Enriched.Limits.HasConicalPullbacks Mathlib.CategoryTheory.Enriched.Limits.HasConicalTerminal Mathlib.CategoryTheory.Enriched.Opposite Mathlib.CategoryTheory.Enriched.Ordinary.Basic Mathlib.CategoryTheory.Filtered.Final Mathlib.CategoryTheory.Filtered.FinallySmall Mathlib.CategoryTheory.Functor.FunctorHom Mathlib.CategoryTheory.Functor.TypeValuedFlat Mathlib.CategoryTheory.Generator.Indization Mathlib.CategoryTheory.LiftingProperties.PushoutProduct Mathlib.CategoryTheory.Limits.ConstructLimitMap Mathlib.CategoryTheory.Limits.Constructions.Over.Basic Mathlib.CategoryTheory.Limits.Constructions.Over.Connected Mathlib.CategoryTheory.Limits.FinallySmall Mathlib.CategoryTheory.Limits.Indization.Category Mathlib.CategoryTheory.Limits.Indization.Equalizers Mathlib.CategoryTheory.Limits.Indization.FilteredColimits Mathlib.CategoryTheory.Limits.Indization.IndObject Mathlib.CategoryTheory.Limits.Indization.LocallySmall Mathlib.CategoryTheory.Limits.Indization.ParallelPair Mathlib.CategoryTheory.Limits.Indization.Products Mathlib.CategoryTheory.Limits.MorphismProperty Mathlib.CategoryTheory.Limits.Preserves.Shapes.Preorder Mathlib.CategoryTheory.Limits.Shapes.Preorder.TransfiniteCompositionOfShape Mathlib.CategoryTheory.Limits.Shapes.Preorder.WellOrderContinuous Mathlib.CategoryTheory.Limits.Shapes.Pullback.EquifiberedLimits Mathlib.CategoryTheory.Limits.Sifted Mathlib.CategoryTheory.Localization.BousfieldTransfiniteComposition Mathlib.CategoryTheory.LocallyCartesianClosed.ChosenPullbacksAlong Mathlib.CategoryTheory.LocallyCartesianClosed.ExponentiableMorphism Mathlib.CategoryTheory.LocallyCartesianClosed.Over Mathlib.CategoryTheory.LocallyCartesianClosed.Sections Mathlib.CategoryTheory.Monoidal.Arrow Mathlib.CategoryTheory.Monoidal.Cartesian.Basic Mathlib.CategoryTheory.Monoidal.Cartesian.Cat Mathlib.CategoryTheory.Monoidal.Cartesian.CommGrp_ Mathlib.CategoryTheory.Monoidal.Cartesian.CommMon_ Mathlib.CategoryTheory.Monoidal.Cartesian.Comon_ Mathlib.CategoryTheory.Monoidal.Cartesian.FunctorCategory Mathlib.CategoryTheory.Monoidal.Cartesian.GrpLimits Mathlib.CategoryTheory.Monoidal.Cartesian.Grp_ Mathlib.CategoryTheory.Monoidal.Cartesian.Grp Mathlib.CategoryTheory.Monoidal.Cartesian.InfSemilattice Mathlib.CategoryTheory.Monoidal.Cartesian.Mod_ Mathlib.CategoryTheory.Monoidal.Cartesian.Mod Mathlib.CategoryTheory.Monoidal.Cartesian.Mon_ Mathlib.CategoryTheory.Monoidal.Cartesian.Mon Mathlib.CategoryTheory.Monoidal.Cartesian.Normal Mathlib.CategoryTheory.Monoidal.Cartesian.Over Mathlib.CategoryTheory.Monoidal.Cartesian.Ring Mathlib.CategoryTheory.Monoidal.Cartesian.ShrinkYoneda Mathlib.CategoryTheory.Monoidal.Closed.Cartesian Mathlib.CategoryTheory.Monoidal.Closed.Enrichment Mathlib.CategoryTheory.Monoidal.Closed.FunctorCategory.Basic Mathlib.CategoryTheory.Monoidal.Closed.FunctorToTypes Mathlib.CategoryTheory.Monoidal.Closed.Functor Mathlib.CategoryTheory.Monoidal.Closed.Ideal Mathlib.CategoryTheory.Monoidal.Closed.Types Mathlib.CategoryTheory.Monoidal.Closed.Zero Mathlib.CategoryTheory.Monoidal.CommGrp_ Mathlib.CategoryTheory.Monoidal.Functor.Types Mathlib.CategoryTheory.Monoidal.Grp_ Mathlib.CategoryTheory.Monoidal.Grp Mathlib.CategoryTheory.Monoidal.Internal.Types.Basic Mathlib.CategoryTheory.Monoidal.Internal.Types.CommGrp_ Mathlib.CategoryTheory.Monoidal.Internal.Types.Grp_ Mathlib.CategoryTheory.Monoidal.Internal.Types.Grp Mathlib.CategoryTheory.Monoidal.Limits.Colimits Mathlib.CategoryTheory.Monoidal.PushoutProduct Mathlib.CategoryTheory.Monoidal.Ring Mathlib.CategoryTheory.Monoidal.Types.Basic Mathlib.CategoryTheory.Monoidal.Types.Coyoneda Mathlib.CategoryTheory.MorphismProperty.CommaSites Mathlib.CategoryTheory.MorphismProperty.FunctorCategory Mathlib.CategoryTheory.MorphismProperty.Ind Mathlib.CategoryTheory.MorphismProperty.TransfiniteComposition Mathlib.CategoryTheory.ObjectProperty.Ind Mathlib.CategoryTheory.Preadditive.CommGrp_ Mathlib.CategoryTheory.Preadditive.Indization Mathlib.CategoryTheory.Presentable.Adjunction Mathlib.CategoryTheory.Presentable.Basic Mathlib.CategoryTheory.Presentable.CardinalDirectedPoset Mathlib.CategoryTheory.Presentable.CardinalFilteredPresentation Mathlib.CategoryTheory.Presentable.CardinalPure Mathlib.CategoryTheory.Presentable.ColimitPresentation Mathlib.CategoryTheory.Presentable.Comma Mathlib.CategoryTheory.Presentable.Dense Mathlib.CategoryTheory.Presentable.Directed Mathlib.CategoryTheory.Presentable.EssentiallyLarge Mathlib.CategoryTheory.Presentable.Finite Mathlib.CategoryTheory.Presentable.IsCardinalFiltered Mathlib.CategoryTheory.Presentable.IsDiscrete Mathlib.CategoryTheory.Presentable.Limits Mathlib.CategoryTheory.Presentable.LocallyPresentable Mathlib.CategoryTheory.Presentable.OrthogonalReflection Mathlib.CategoryTheory.Presentable.PreservesCardinalPresentable Mathlib.CategoryTheory.Presentable.Presheaf Mathlib.CategoryTheory.Presentable.Retracts Mathlib.CategoryTheory.Presentable.SharplyLT.Basic Mathlib.CategoryTheory.Presentable.SharplyLT.Lemmas Mathlib.CategoryTheory.Presentable.SolutionSetCondition Mathlib.CategoryTheory.Presentable.StrongGenerator Mathlib.CategoryTheory.Presentable.Type Mathlib.CategoryTheory.Presentable.Uniformization Mathlib.CategoryTheory.Sites.CartesianClosed Mathlib.CategoryTheory.Sites.CartesianMonoidal Mathlib.CategoryTheory.Sites.Descent.Precoverage Mathlib.CategoryTheory.Sites.LocalSite Mathlib.CategoryTheory.Sites.Monoidal Mathlib.CategoryTheory.Sites.Point.Basic Mathlib.CategoryTheory.Sites.Point.Category Mathlib.CategoryTheory.Sites.Point.Comap Mathlib.CategoryTheory.Sites.Point.Conservative Mathlib.CategoryTheory.Sites.Point.Map Mathlib.CategoryTheory.Sites.Point.OfIsCofiltered Mathlib.CategoryTheory.Sites.Point.Over Mathlib.CategoryTheory.Sites.Point.Presheaf Mathlib.CategoryTheory.Sites.Point.Skyscraper Mathlib.CategoryTheory.SmallObject.Basic Mathlib.CategoryTheory.SmallObject.IsCardinalForSmallObjectArgument Mathlib.CategoryTheory.SmallObject.TransfiniteCompositionLifting Mathlib.CategoryTheory.SmallObject.TransfiniteIteration Mathlib.Condensed.AB Mathlib.Condensed.Discrete.Characterization Mathlib.Condensed.Discrete.Colimit Mathlib.Condensed.Discrete.Module Mathlib.Condensed.EffectiveEpi Mathlib.Condensed.Epi Mathlib.Condensed.Explicit Mathlib.Condensed.Functors Mathlib.Condensed.Light.AB Mathlib.Condensed.Light.EffectiveEpi Mathlib.Condensed.Light.Epi Mathlib.Condensed.Light.Explicit Mathlib.Condensed.Light.Functors Mathlib.Condensed.Light.InternallyProjective Mathlib.Condensed.Light.Limits Mathlib.Condensed.Light.Module Mathlib.Condensed.Light.Monoidal Mathlib.Condensed.Light.Sequence Mathlib.Condensed.Light.Small Mathlib.Condensed.Limits Mathlib.Condensed.Module Mathlib.Condensed.Solid Mathlib.Order.Interval.Set.Final Mathlib.RepresentationTheory.Action Mathlib.RepresentationTheory.Character Mathlib.RepresentationTheory.Coinduced Mathlib.RepresentationTheory.Coinvariants Mathlib.RepresentationTheory.FDRep Mathlib.RepresentationTheory.FinGroupCharZero Mathlib.RepresentationTheory.FiniteIndex Mathlib.RepresentationTheory.Homological.FiniteCyclic Mathlib.RepresentationTheory.Homological.GroupCohomology.Basic Mathlib.RepresentationTheory.Homological.GroupCohomology.FiniteCyclic 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.FiniteCyclic Mathlib.RepresentationTheory.Homological.GroupHomology.Functoriality Mathlib.RepresentationTheory.Homological.GroupHomology.LongExactSequence Mathlib.RepresentationTheory.Homological.GroupHomology.LowDegree Mathlib.RepresentationTheory.Homological.GroupHomology.Shapiro Mathlib.RepresentationTheory.Homological.Resolution Mathlib.RepresentationTheory.Homological.TateCohomology.Basic Mathlib.RepresentationTheory.Induced Mathlib.RepresentationTheory.Invariants Mathlib.RepresentationTheory.Rep.Basic Mathlib.RepresentationTheory.Rep.Iso Mathlib.RepresentationTheory.Rep.Res Mathlib.RepresentationTheory.Tannaka Mathlib.Topology.CWComplex.Abstract.Basic Mathlib.Topology.Category.CompHausLike.Cartesian Mathlib.Topology.Category.LightProfinite.Cartesian Mathlib.Topology.Category.LightProfinite.Extend Mathlib.Topology.Category.Profinite.Extend Mathlib.Topology.Category.TopCat.Monoidal Mathlib.Topology.Category.TopPair Mathlib.Topology.Homotopy.TopCat.Basic Mathlib.Topology.Homotopy.TopCat.Path Mathlib.Topology.Homotopy.TopCat.ToSSet Mathlib.Topology.Homotopy.TopCat.ZerothHomotopy Mathlib.Topology.Sets.BaseChangeNhds Mathlib.Topology.Sheaves.Points

1

---

Declarations diff (regex)

+ curriedTensorPostCompIso
+ curriedTensorPreCompIso
+ curriedTensorPreCompPostIso
+ opOpCompLeftOpOpIso
+ whiskeringLeftObjCompWhiskeringRightObjIso

You can run this locally as follows

## from your `mathlib4` directory:
git clone https://github.com/leanprover-community/mathlib-ci.git ../mathlib-ci

## summary with just the declaration names:
../mathlib-ci/scripts/pr_summary/declarations_diff.sh <optional_commit>

## more verbose report:
../mathlib-ci/scripts/pr_summary/declarations_diff.sh long <optional_commit>

The doc-module for scripts/pr_summary/declarations_diff.sh in the mathlib-ci repository contains some details about this script.

Declarations diff (Lean)

✅ Lean-aware diff — post-build, computed from the Lean environment (commit e4dbc82).

• +15 new declarations
• −0 removed declarations

+CategoryTheory.Functor.opOpCompLeftOpOpIso
+CategoryTheory.Functor.opOpCompLeftOpOpIso_hom_app
+CategoryTheory.Functor.opOpCompLeftOpOpIso_inv_app
+CategoryTheory.Functor.whiskeringLeftObjCompWhiskeringRightObjIso
+CategoryTheory.Functor.whiskeringLeftObjCompWhiskeringRightObjIso_hom_app_app
+CategoryTheory.Functor.whiskeringLeftObjCompWhiskeringRightObjIso_inv_app_app
+CategoryTheory.MonoidalCategory.curriedTensorPostCompIso
+CategoryTheory.MonoidalCategory.curriedTensorPostCompIso_hom_app_app
+CategoryTheory.MonoidalCategory.curriedTensorPostCompIso_inv_app_app
+CategoryTheory.MonoidalCategory.curriedTensorPreCompIso
+CategoryTheory.MonoidalCategory.curriedTensorPreCompIso_hom_app_app
+CategoryTheory.MonoidalCategory.curriedTensorPreCompIso_inv_app_app
+CategoryTheory.MonoidalCategory.curriedTensorPreCompPostIso
+CategoryTheory.MonoidalCategory.curriedTensorPreCompPostIso_hom_app_app
+CategoryTheory.MonoidalCategory.curriedTensorPreCompPostIso_inv_app_app

---

Decrease in strong tech debt: (relative, absolute) = (5.00, 0.01)

Current number	Change	Type (strong)
erw	491	-5

No changes to weak technical debt.

Current commit e4dbc82828
Reference commit 572e4d091b

This script lives in the mathlib-ci repository. To run it locally, from your mathlib4 directory:

git clone https://github.com/leanprover-community/mathlib-ci.git ../mathlib-ci
../mathlib-ci/scripts/reporting/technical-debt-metrics.py 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).

[robin-carlier]

!bench

[leanprover-radar]

Benchmark results for e4dbc82 against 572e4d0 are in. No significant results found. @robin-carlier

• 🟥 build//instructions: +5.2G (+0.00%)

Medium changes (1✅)

• ✅ build/module/Mathlib.CategoryTheory.Functor.KanExtension.Basic//instructions: -2.0G (-3.64%)

Small changes (2🟥)

• 🟥 build/module/Mathlib.CategoryTheory.Monoidal.Multifunctor//instructions: +2.7G (+5.18%) (reduced significance based on *//lines)
• 🟥 build/module/Mathlib.CategoryTheory.Whiskering//instructions: +773.0M (+1.87%)