[Merged by Bors] - deduplicate pullback and baseChange

[sinhp]

Deduplication of Over.pullback and Over.baseChange. Over.baseChange has been renamed to Over.pullback and simp lemmas added to Over.pullback and Over.mapPullbackAdj.

---

[github-actions]

PR summary 4c04c8899a

Import changes for modified files

Dependency changes

File	Base Count	Head Count	Change
Mathlib.CategoryTheory.Adjunction.Over	404	428	+24 (+5.94%)
Mathlib.CategoryTheory.Subobject.MonoOver	445	438	-7 (-1.57%)
Mathlib.CategoryTheory.Limits.Shapes.Diagonal	537	543	+6 (+1.12%)
Mathlib.CategoryTheory.MorphismProperty.Limits	539	545	+6 (+1.11%)
Mathlib.Algebra.Homology.HomologicalComplexLimits	667	663	-4 (-0.60%)
Mathlib.CategoryTheory.Subobject.Comma	540	538	-2 (-0.37%)
Mathlib.CategoryTheory.Limits.Over	415	414	-1 (-0.24%)

Import changes for all files

Files	Import difference
4 files Mathlib.CategoryTheory.Subobject.Types Mathlib.CategoryTheory.Subobject.Basic Mathlib.CategoryTheory.Dialectica.Basic Mathlib.CategoryTheory.Subobject.WellPowered	-8
3 files Mathlib.CategoryTheory.Closed.Ideal Mathlib.CategoryTheory.Subterminal Mathlib.CategoryTheory.Subobject.MonoOver	-7
20 files Mathlib.Algebra.Homology.Functor Mathlib.Algebra.Homology.Additive Mathlib.CategoryTheory.Subobject.Limits Mathlib.Algebra.Homology.TotalComplexSymmetry Mathlib.Algebra.Homology.Single Mathlib.CategoryTheory.Preadditive.Generator Mathlib.Algebra.Homology.HomologicalComplex Mathlib.CategoryTheory.Subobject.FactorThru Mathlib.Algebra.Homology.ImageToKernel Mathlib.Algebra.Homology.Embedding.Extend Mathlib.Algebra.Homology.HomologicalBicomplex Mathlib.CategoryTheory.Dialectica.Monoidal Mathlib.Algebra.Homology.TotalComplex Mathlib.Algebra.Homology.DifferentialObject Mathlib.CategoryTheory.Subobject.Lattice Mathlib.Algebra.Homology.Linear Mathlib.CategoryTheory.Generator Mathlib.Algebra.Homology.Embedding.Restriction Mathlib.Algebra.Homology.Bifunctor Mathlib.Algebra.Homology.Augment	-6
5 files Mathlib.CategoryTheory.Preadditive.Schur Mathlib.CategoryTheory.Noetherian Mathlib.CategoryTheory.Abelian.Subobject Mathlib.CategoryTheory.Simple Mathlib.CategoryTheory.Idempotents.HomologicalComplex	-5
8 files Mathlib.Algebra.Category.Grp.Subobject Mathlib.Algebra.Category.ModuleCat.Simple Mathlib.Algebra.Category.ModuleCat.Subobject Mathlib.Algebra.Homology.HomologicalComplexLimits Mathlib.Algebra.Homology.HomologicalComplexBiprod Mathlib.AlgebraicTopology.DoldKan.Notations Mathlib.AlgebraicTopology.AlternatingFaceMapComplex Mathlib.AlgebraicTopology.MooreComplex	-4
67 files Mathlib.CategoryTheory.Abelian.Generator Mathlib.AlgebraicTopology.DoldKan.EquivalencePseudoabelian Mathlib.AlgebraicTopology.DoldKan.SplitSimplicialObject Mathlib.CategoryTheory.Abelian.RightDerived Mathlib.CategoryTheory.Abelian.Pseudoelements Mathlib.Algebra.Homology.Opposite Mathlib.Algebra.Homology.DerivedCategory.HomologySequence Mathlib.CategoryTheory.Abelian.Ext Mathlib.Algebra.Category.Grp.AB5 Mathlib.Algebra.Homology.Embedding.IsSupported Mathlib.Algebra.Homology.HomotopyCategory.Pretriangulated Mathlib.AlgebraicTopology.DoldKan.Homotopies Mathlib.Algebra.Homology.ShortComplex.HomologicalComplex Mathlib.Algebra.Homology.HomotopyCategory.HomComplexShift Mathlib.Algebra.Homology.HomotopyCategory.MappingCone Mathlib.Algebra.Homology.TotalComplexShift Mathlib.CategoryTheory.Abelian.ProjectiveResolution Mathlib.AlgebraicTopology.DoldKan.GammaCompN Mathlib.Algebra.Homology.DerivedCategory.Ext Mathlib.Algebra.Homology.HomotopyCategory.HomologicalFunctor Mathlib.Algebra.Homology.HomotopyCategory.Triangulated Mathlib.Algebra.Homology.HomotopyCategory.SingleFunctors Mathlib.CategoryTheory.Abelian.Injective Mathlib.CategoryTheory.Monoidal.Tor Mathlib.CategoryTheory.Abelian.Projective Mathlib.Algebra.Homology.HomotopyCategory.HomComplex Mathlib.Algebra.Homology.DerivedCategory.SingleTriangle Mathlib.AlgebraicTopology.DoldKan.EquivalenceAdditive Mathlib.Algebra.Homology.DerivedCategory.ShortExact Mathlib.Algebra.Homology.HomotopyCategory.Shift Mathlib.AlgebraicTopology.DoldKan.HomotopyEquivalence Mathlib.Algebra.Homology.Refinements Mathlib.AlgebraicTopology.DoldKan.Normalized Mathlib.AlgebraicTopology.DoldKan.Faces Mathlib.Algebra.Homology.Localization Mathlib.Algebra.Homology.BifunctorHomotopy Mathlib.AlgebraicTopology.DoldKan.Equivalence Mathlib.AlgebraicTopology.DoldKan.Decomposition Mathlib.Algebra.Homology.SingleHomology Mathlib.CategoryTheory.Subobject.Comma Mathlib.AlgebraicTopology.DoldKan.PInfty Mathlib.AlgebraicTopology.DoldKan.FunctorGamma Mathlib.Algebra.Homology.HomologySequenceLemmas Mathlib.CategoryTheory.Preadditive.ProjectiveResolution Mathlib.Algebra.Homology.HomologicalComplexAbelian Mathlib.CategoryTheory.Abelian.Exact Mathlib.Algebra.Homology.QuasiIso Mathlib.AlgebraicTopology.DoldKan.NCompGamma Mathlib.Algebra.Homology.HomotopyCategory.ShiftSequence Mathlib.Algebra.Homology.HomotopyCategory.ShortExact Mathlib.CategoryTheory.Abelian.InjectiveResolution Mathlib.CategoryTheory.Preadditive.InjectiveResolution Mathlib.CategoryTheory.Abelian.LeftDerived Mathlib.Algebra.Homology.Homotopy Mathlib.Algebra.Homology.HomotopyCofiber Mathlib.Algebra.Homology.HomologySequence Mathlib.Algebra.Homology.HomotopyCategory Mathlib.Algebra.Homology.HomotopyCategory.DegreewiseSplit Mathlib.AlgebraicTopology.DoldKan.FunctorN Mathlib.Algebra.Homology.BifunctorShift Mathlib.Algebra.Homology.ShortComplex.ExactFunctor Mathlib.Algebra.Homology.DerivedCategory.Basic Mathlib.Algebra.Homology.Factorizations.Basic Mathlib.Algebra.Homology.DerivedCategory.ExactFunctor Mathlib.AlgebraicTopology.DoldKan.NReflectsIso Mathlib.AlgebraicTopology.DoldKan.Degeneracies Mathlib.AlgebraicTopology.DoldKan.Projections	-2
10 files Mathlib.Topology.Category.Profinite.Nobeling Mathlib.CategoryTheory.Limits.Presheaf Mathlib.CategoryTheory.Limits.Preserves.FunctorCategory Mathlib.AlgebraicTopology.SingularSet Mathlib.CategoryTheory.Limits.Indization.IndObject Mathlib.CategoryTheory.Closed.Types Mathlib.CategoryTheory.Sites.CoverPreserving Mathlib.CategoryTheory.Limits.Over Mathlib.CategoryTheory.Functor.Flat Mathlib.CategoryTheory.Limits.FilteredColimitCommutesFiniteLimit	-1
26 files Mathlib.AlgebraicGeometry.Morphisms.OpenImmersion Mathlib.AlgebraicGeometry.Sites.BigZariski Mathlib.AlgebraicGeometry.Morphisms.Basic Mathlib.AlgebraicGeometry.Morphisms.QuasiCompact Mathlib.AlgebraicGeometry.Morphisms.ClosedImmersion Mathlib.AlgebraicGeometry.Noetherian Mathlib.AlgebraicGeometry.Morphisms.RingHomProperties Mathlib.Algebra.Homology.ShortComplex.ModuleCat Mathlib.AlgebraicGeometry.Pullbacks Mathlib.Algebra.Category.ModuleCat.Biproducts Mathlib.RingTheory.Flat.CategoryTheory Mathlib.AlgebraicGeometry.Morphisms.Separated Mathlib.GroupTheory.FiniteAbelian Mathlib.AlgebraicGeometry.Morphisms.Constructors Mathlib.Algebra.Module.PID Mathlib.AlgebraicGeometry.Limits Mathlib.AlgebraicGeometry.Morphisms.QuasiSeparated Mathlib.Algebra.Homology.LocalCohomology Mathlib.AlgebraicGeometry.Morphisms.FiniteType Mathlib.AlgebraicTopology.ExtraDegeneracy Mathlib.CategoryTheory.Galois.Examples Mathlib.Algebra.Homology.ShortComplex.ConcreteCategory Mathlib.Algebra.Category.ModuleCat.Free Mathlib.AlgebraicGeometry.GluingOneHypercover Mathlib.AlgebraicGeometry.Morphisms.UniversallyClosed Mathlib.Algebra.Homology.ConcreteCategory	1
4 files Mathlib.CategoryTheory.Galois.GaloisObjects Mathlib.CategoryTheory.Galois.Decomposition Mathlib.CategoryTheory.Galois.Basic Mathlib.CategoryTheory.Galois.Prorepresentability	2
Mathlib.CategoryTheory.Adjunction.AdjointFunctorTheorems	3
3 files Mathlib.CategoryTheory.Localization.FiniteProducts Mathlib.CategoryTheory.Limits.Shapes.Diagonal Mathlib.CategoryTheory.MorphismProperty.Limits	6
Mathlib.CategoryTheory.Adjunction.Over	24

---

Declarations diff

+ mapPushoutAdj
+ pushoutId
+ pushoutIsLeftAdjoint
-++ pullbackComp

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>

[emilyriehl]

This addresses issue #13998.

[emilyriehl]

@sinhp maybe this no longer needs to be a draft?

[sinhp]

@sinhp maybe this no longer needs to be a draft?

indeed, just made it "ready for review".

[kim-em]

@sinhp, @emilyriehl, just noting that this needs to have a git merge origin/master and the conflicts resolved before it can be reviewed.

[emilyriehl]

Thanks for explaining how to fix this @semorrison. Should be ready to review now.

[kim-em]

My only concern here is that you've somehow pulled in more imports in Mathlib.CategoryTheory.Adjunction.Over (+24 transitive imports) and a few more imports into downstream files Mathlib.CategoryTheory.Localization.FiniteProducts, Mathlib.CategoryTheory.Limits.Shapes.Diagonal, Mathlib.CategoryTheory.MorphismProperty.Limits, according to #14519 (comment).

It's not critical, but we do like to avoid import creep.

I had a look at what has changed using

lake exe graph --from Mathlib.CategoryTheory.Category.Basic --to Mathlib.CategoryTheory.Adjunction.Over --reduce p.pdf

before and after this PR. Mathlib.CategoryTheory.Mates pulls in Mathlib.CategoryTheory.Conj, which then for its second half (but I think not for mates?) needs Mathlib.CategoryTheory.Endomorphism which then pulls in a bunch of algebra files.

If we want to fix this (either before or after merging this PR), I think we should try to split Conj, moving its second half to a new file, and hopefully Mates doesn't need to import that.

[kim-em]

Looking more, yes, Conj can be split into a first half called HomCongr, and then leave the second half as Conj.

If @sinhp or @emilyriehl would be game to do this (not necessarily immediately) I'm otherwise happy to merge here. If this doesn't sound fun I'm happy to merge in any case, and hopefully we can get to this split later.

[emilyriehl]

@semorrison I've never tried to split a file, but I'd be happy to figure it out, because I'm sure I'll learn something in the process. (I'll ask on the zulip for help.) I'd prefer to merge this now to preempt future merge conflicts. I'll send you a new PR next week (or possibly the week after) to address the imports issue.

[kim-em]

bors merge

[mathlib-bors]

This PR was included in a batch that was canceled, it will be automatically retried

[mathlib-bors]

Pull request successfully merged into master.

Build succeeded:

• Build
• Lint style