feat(CategoryTheory/Subobject): extend image subobject API

[mckoen]

Extends some API for image subobjects. This PR exists to split up #41769.

---

• depends on: feat(CategoryTheory/Subobject): extend exists and pullback API #42757

[github-actions]

PR summary 3438f481ef

Import changes for modified files

Dependency changes

File	Base Count	Head Count	Change
Mathlib.CategoryTheory.Subobject.Basic	679	680	+1 (+0.15%)
Mathlib.CategoryTheory.Subobject.Lattice	754	755	+1 (+0.13%)
Mathlib.CategoryTheory.Subobject.Limits	755	756	+1 (+0.13%)

Import changes for all files

Files

Import difference

341 files Mathlib.Algebra.Category.Grp.AB Mathlib.Algebra.Category.Grp.Subobject Mathlib.Algebra.Category.ModuleCat.AB Mathlib.Algebra.Category.ModuleCat.Biproducts Mathlib.Algebra.Category.ModuleCat.ChangeOfRingsExact Mathlib.Algebra.Category.ModuleCat.Descent Mathlib.Algebra.Category.ModuleCat.Ext.Basic Mathlib.Algebra.Category.ModuleCat.Ext.DimensionShifting Mathlib.Algebra.Category.ModuleCat.Ext.Finite Mathlib.Algebra.Category.ModuleCat.Ext.HasExt Mathlib.Algebra.Category.ModuleCat.Free Mathlib.Algebra.Category.ModuleCat.InjectiveDimension Mathlib.Algebra.Category.ModuleCat.LeftResolution Mathlib.Algebra.Category.ModuleCat.Localization Mathlib.Algebra.Category.ModuleCat.Presheaf.Generator Mathlib.Algebra.Category.ModuleCat.Presheaf.Pullback Mathlib.Algebra.Category.ModuleCat.ProjectiveDimension Mathlib.Algebra.Category.ModuleCat.Sheaf.PullbackContinuous Mathlib.Algebra.Category.ModuleCat.Sheaf.PullbackFree Mathlib.Algebra.Category.ModuleCat.Simple Mathlib.Algebra.Category.ModuleCat.Subobject Mathlib.Algebra.Category.ModuleCat.Ulift Mathlib.Algebra.Homology.Additive Mathlib.Algebra.Homology.AlternatingConst Mathlib.Algebra.Homology.Augment Mathlib.Algebra.Homology.BifunctorAssociator Mathlib.Algebra.Homology.BifunctorFlip Mathlib.Algebra.Homology.BifunctorHomotopy Mathlib.Algebra.Homology.BifunctorShift Mathlib.Algebra.Homology.Bifunctor Mathlib.Algebra.Homology.CochainComplexOpposite Mathlib.Algebra.Homology.CochainComplexPlus Mathlib.Algebra.Homology.ConcreteCategory Mathlib.Algebra.Homology.DerivedCategory.Basic Mathlib.Algebra.Homology.DerivedCategory.DerivabilityStructureInjectives Mathlib.Algebra.Homology.DerivedCategory.ExactFunctor Mathlib.Algebra.Homology.DerivedCategory.Ext.Basic Mathlib.Algebra.Homology.DerivedCategory.Ext.EnoughInjectives Mathlib.Algebra.Homology.DerivedCategory.Ext.EnoughProjectives Mathlib.Algebra.Homology.DerivedCategory.Ext.ExactSequences Mathlib.Algebra.Homology.DerivedCategory.Ext.ExtClass Mathlib.Algebra.Homology.DerivedCategory.Ext.Linear Mathlib.Algebra.Homology.DerivedCategory.Ext.MapBijective Mathlib.Algebra.Homology.DerivedCategory.Ext.Map Mathlib.Algebra.Homology.DerivedCategory.Ext.TStructure Mathlib.Algebra.Homology.DerivedCategory.Fractions Mathlib.Algebra.Homology.DerivedCategory.FullyFaithful Mathlib.Algebra.Homology.DerivedCategory.HomologySequence Mathlib.Algebra.Homology.DerivedCategory.KInjective Mathlib.Algebra.Homology.DerivedCategory.KProjective Mathlib.Algebra.Homology.DerivedCategory.Linear Mathlib.Algebra.Homology.DerivedCategory.Plus Mathlib.Algebra.Homology.DerivedCategory.RightDerivedFunctorPlus Mathlib.Algebra.Homology.DerivedCategory.ShortExact Mathlib.Algebra.Homology.DerivedCategory.SingleTriangle Mathlib.Algebra.Homology.DerivedCategory.SmallShiftedHom Mathlib.Algebra.Homology.DerivedCategory.TStructure Mathlib.Algebra.Homology.DifferentialObject Mathlib.Algebra.Homology.Double Mathlib.Algebra.Homology.Embedding.AreComplementary Mathlib.Algebra.Homology.Embedding.Boundary Mathlib.Algebra.Homology.Embedding.CochainComplex Mathlib.Algebra.Homology.Embedding.Connect Mathlib.Algebra.Homology.Embedding.ExtendHomology Mathlib.Algebra.Homology.Embedding.ExtendHomotopy Mathlib.Algebra.Homology.Embedding.Extend Mathlib.Algebra.Homology.Embedding.HomEquiv Mathlib.Algebra.Homology.Embedding.IsSupported Mathlib.Algebra.Homology.Embedding.RestrictionHomology Mathlib.Algebra.Homology.Embedding.Restriction Mathlib.Algebra.Homology.Embedding.Splitting 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.EulerCharacteristic Mathlib.Algebra.Homology.Factorizations.Basic Mathlib.Algebra.Homology.Factorizations.CM5a Mathlib.Algebra.Homology.Factorizations.CM5b Mathlib.Algebra.Homology.FullSubcategory Mathlib.Algebra.Homology.Functor Mathlib.Algebra.Homology.GrothendieckAbelian Mathlib.Algebra.Homology.HomologicalBicomplex Mathlib.Algebra.Homology.HomologicalComplexAbelian Mathlib.Algebra.Homology.HomologicalComplexBiprod Mathlib.Algebra.Homology.HomologicalComplexKernels Mathlib.Algebra.Homology.HomologicalComplexLimitsEventuallyConstant Mathlib.Algebra.Homology.HomologicalComplexLimits Mathlib.Algebra.Homology.HomologicalComplex Mathlib.Algebra.Homology.HomologySequenceLemmas Mathlib.Algebra.Homology.HomologySequence Mathlib.Algebra.Homology.HomotopyCategory.Acyclic Mathlib.Algebra.Homology.HomotopyCategory.ChainComplex Mathlib.Algebra.Homology.HomotopyCategory.DegreewiseSplit Mathlib.Algebra.Homology.HomotopyCategory.HomComplexCohomology Mathlib.Algebra.Homology.HomotopyCategory.HomComplexInduction Mathlib.Algebra.Homology.HomotopyCategory.HomComplexShift Mathlib.Algebra.Homology.HomotopyCategory.HomComplexSingle Mathlib.Algebra.Homology.HomotopyCategory.HomComplex Mathlib.Algebra.Homology.HomotopyCategory.HomologicalFunctor Mathlib.Algebra.Homology.HomotopyCategory.KInjective Mathlib.Algebra.Homology.HomotopyCategory.KProjective Mathlib.Algebra.Homology.HomotopyCategory.MappingCocone Mathlib.Algebra.Homology.HomotopyCategory.MappingCone Mathlib.Algebra.Homology.HomotopyCategory.Plus 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.SpectralObject Mathlib.Algebra.Homology.HomotopyCategory.Triangulated Mathlib.Algebra.Homology.HomotopyCategory Mathlib.Algebra.Homology.HomotopyCofiber Mathlib.Algebra.Homology.HomotopyFiber Mathlib.Algebra.Homology.Homotopy Mathlib.Algebra.Homology.ImageToKernel Mathlib.Algebra.Homology.LeftResolution.Basic Mathlib.Algebra.Homology.LeftResolution.Reduced Mathlib.Algebra.Homology.LeftResolution.Transport Mathlib.Algebra.Homology.Linear Mathlib.Algebra.Homology.LocalCohomology Mathlib.Algebra.Homology.Localization Mathlib.Algebra.Homology.ModelCategory.Injective Mathlib.Algebra.Homology.ModelCategory.Lifting Mathlib.Algebra.Homology.Monoidal Mathlib.Algebra.Homology.Opposite Mathlib.Algebra.Homology.Precylinder Mathlib.Algebra.Homology.QuasiIso Mathlib.Algebra.Homology.Refinements Mathlib.Algebra.Homology.ShortComplex.ConcreteCategory Mathlib.Algebra.Homology.ShortComplex.ExactFunctor Mathlib.Algebra.Homology.ShortComplex.HomologicalComplex Mathlib.Algebra.Homology.ShortComplex.ModuleCat Mathlib.Algebra.Homology.SingleHomology Mathlib.Algebra.Homology.Single Mathlib.Algebra.Homology.SpectralObject.Cycles Mathlib.Algebra.Homology.SpectralObject.Differentials Mathlib.Algebra.Homology.SpectralObject.EpiMono Mathlib.Algebra.Homology.SpectralObject.FirstPage Mathlib.Algebra.Homology.SpectralObject.Homology Mathlib.Algebra.Homology.SpectralObject.Page Mathlib.Algebra.Homology.SpectralObject.SpectralSequence Mathlib.Algebra.Homology.SpectralSequence.Basic Mathlib.Algebra.Homology.TotalComplexShift Mathlib.Algebra.Homology.TotalComplexSymmetry Mathlib.Algebra.Homology.TotalComplex Mathlib.Algebra.Module.PID 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.AlgebraicTopology.SimplicialObject.ChainHomotopy Mathlib.AlgebraicTopology.SimplicialSet.AnodyneExtensions.Basic Mathlib.AlgebraicTopology.SimplicialSet.AnodyneExtensions.Inner.Basic Mathlib.AlgebraicTopology.SimplicialSet.AnodyneExtensions.Inner.PushoutProduct Mathlib.AlgebraicTopology.SimplicialSet.AnodyneExtensions.PushoutProduct Mathlib.AlgebraicTopology.SimplicialSet.Homology.Basic Mathlib.AlgebraicTopology.SimplicialSet.Homology.HomologyZero Mathlib.AlgebraicTopology.SimplicialSet.Homology.HomotopyInvariance Mathlib.AlgebraicTopology.SimplicialSet.Homology.MapHomologicalComplex Mathlib.AlgebraicTopology.SimplicialSet.Homology.Nondegenerate Mathlib.AlgebraicTopology.SimplicialSet.Presentable Mathlib.AlgebraicTopology.SingularHomology.Basic Mathlib.AlgebraicTopology.SingularHomology.HomologyZero Mathlib.AlgebraicTopology.SingularHomology.HomotopyInvarianceTopCat Mathlib.AlgebraicTopology.SingularHomology.HomotopyInvariance Mathlib.Analysis.Fourier.FiniteAbelian.PontryaginDuality Mathlib.CategoryTheory.Abelian.Exact Mathlib.CategoryTheory.Abelian.Ext Mathlib.CategoryTheory.Abelian.FreydMitchell Mathlib.CategoryTheory.Abelian.GrothendieckAxioms.Basic Mathlib.CategoryTheory.Abelian.GrothendieckAxioms.Colim Mathlib.CategoryTheory.Abelian.GrothendieckAxioms.Connected Mathlib.CategoryTheory.Abelian.GrothendieckAxioms.FunctorCategory Mathlib.CategoryTheory.Abelian.GrothendieckAxioms.Indization Mathlib.CategoryTheory.Abelian.GrothendieckAxioms.PresheafOfModules Mathlib.CategoryTheory.Abelian.GrothendieckAxioms.SheafOfModules Mathlib.CategoryTheory.Abelian.GrothendieckAxioms.Sheaf Mathlib.CategoryTheory.Abelian.GrothendieckAxioms.Types Mathlib.CategoryTheory.Abelian.GrothendieckCategory.Basic 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.Injective.Basic Mathlib.CategoryTheory.Abelian.Injective.Dimension Mathlib.CategoryTheory.Abelian.Injective.Ext Mathlib.CategoryTheory.Abelian.Injective.Extend Mathlib.CategoryTheory.Abelian.Injective.Resolution Mathlib.CategoryTheory.Abelian.LeftDerived Mathlib.CategoryTheory.Abelian.Projective.Basic Mathlib.CategoryTheory.Abelian.Projective.Dimension Mathlib.CategoryTheory.Abelian.Projective.Ext Mathlib.CategoryTheory.Abelian.Projective.Extend Mathlib.CategoryTheory.Abelian.Projective.Resolution Mathlib.CategoryTheory.Abelian.Pseudoelements Mathlib.CategoryTheory.Abelian.RightDerived Mathlib.CategoryTheory.Abelian.SerreClass.Localization Mathlib.CategoryTheory.Abelian.ShortExact Mathlib.CategoryTheory.Abelian.Subobject Mathlib.CategoryTheory.Abelian.Yoneda Mathlib.CategoryTheory.Adhesive.Subobject Mathlib.CategoryTheory.Adjunction.AdjointFunctorTheorems Mathlib.CategoryTheory.Dialectica.Basic Mathlib.CategoryTheory.Dialectica.Monoidal Mathlib.CategoryTheory.ExtremalEpi Mathlib.CategoryTheory.Functor.KanExtension.Dense Mathlib.CategoryTheory.Functor.ReflectsIso.Exact Mathlib.CategoryTheory.Generator.Abelian Mathlib.CategoryTheory.Generator.Basic Mathlib.CategoryTheory.Generator.HomologicalComplex Mathlib.CategoryTheory.Generator.Indization Mathlib.CategoryTheory.Generator.Preadditive Mathlib.CategoryTheory.Generator.Presheaf Mathlib.CategoryTheory.Generator.Sheaf Mathlib.CategoryTheory.Generator.StrongGenerator Mathlib.CategoryTheory.Generator.Type Mathlib.CategoryTheory.Idempotents.HomologicalComplex Mathlib.CategoryTheory.Limits.FormalCoproducts.ExtraDegeneracy Mathlib.CategoryTheory.Limits.Types.PreservesLimit Mathlib.CategoryTheory.Monoidal.Tor Mathlib.CategoryTheory.MorphismProperty.Ind Mathlib.CategoryTheory.Noetherian Mathlib.CategoryTheory.ObjectProperty.FunctorCategory.PreservesLimits Mathlib.CategoryTheory.ObjectProperty.Ind Mathlib.CategoryTheory.Preadditive.Injective.Resolution Mathlib.CategoryTheory.Preadditive.Projective.Resolution Mathlib.CategoryTheory.Preadditive.Schur Mathlib.CategoryTheory.Presentable.Adjunction Mathlib.CategoryTheory.Presentable.CardinalDirectedPoset Mathlib.CategoryTheory.Presentable.CardinalFilteredPresentation Mathlib.CategoryTheory.Presentable.CardinalPure Mathlib.CategoryTheory.Presentable.Dense Mathlib.CategoryTheory.Presentable.EssentiallyLarge Mathlib.CategoryTheory.Presentable.IsDiscrete Mathlib.CategoryTheory.Presentable.LocallyPresentable Mathlib.CategoryTheory.Presentable.OrthogonalReflection Mathlib.CategoryTheory.Presentable.Presheaf Mathlib.CategoryTheory.Presentable.SharplyLT.Basic Mathlib.CategoryTheory.Presentable.StrongGenerator Mathlib.CategoryTheory.Presentable.Type Mathlib.CategoryTheory.RegularCategory.Basic Mathlib.CategoryTheory.Simple Mathlib.CategoryTheory.Sites.LocalSite Mathlib.CategoryTheory.Sites.Point.Basic Mathlib.CategoryTheory.Sites.Point.Category Mathlib.CategoryTheory.Sites.Point.Comap Mathlib.CategoryTheory.Sites.Point.Conservative Mathlib.CategoryTheory.Sites.Point.IsMonoidalW Mathlib.CategoryTheory.Sites.Point.Map Mathlib.CategoryTheory.Sites.Point.Monoidal Mathlib.CategoryTheory.Sites.Point.OfIsCofiltered Mathlib.CategoryTheory.Sites.Point.Over Mathlib.CategoryTheory.Sites.Point.Presheaf Mathlib.CategoryTheory.Sites.Point.Skyscraper Mathlib.CategoryTheory.Sites.SheafCohomology.Basic Mathlib.CategoryTheory.Sites.SheafCohomology.Cech Mathlib.CategoryTheory.Sites.SheafCohomology.MayerVietoris Mathlib.CategoryTheory.Subfunctor.Subobject Mathlib.CategoryTheory.Subobject.ArtinianObject Mathlib.CategoryTheory.Subobject.Basic Mathlib.CategoryTheory.Subobject.Classifier.Defs Mathlib.CategoryTheory.Subobject.Comma Mathlib.CategoryTheory.Subobject.FactorThru Mathlib.CategoryTheory.Subobject.HasCardinalLT Mathlib.CategoryTheory.Subobject.Lattice Mathlib.CategoryTheory.Subobject.Limits Mathlib.CategoryTheory.Subobject.NoetherianObject Mathlib.CategoryTheory.Subobject.Presheaf Mathlib.CategoryTheory.Subobject.Types Mathlib.CategoryTheory.Subobject.WellPowered Mathlib.CategoryTheory.Topos.Classifier Mathlib.CategoryTheory.Topos.Sheaf Mathlib.Condensed.AB Mathlib.Condensed.Light.AB Mathlib.FieldTheory.Galois.NormalBasis Mathlib.GroupTheory.FiniteAbelian.Basic Mathlib.GroupTheory.FiniteAbelian.Duality Mathlib.NumberTheory.DirichletCharacter.Orthogonality Mathlib.NumberTheory.LSeries.PrimesInAP Mathlib.NumberTheory.MulChar.Duality Mathlib.NumberTheory.NumberField.Cyclotomic.Galois Mathlib.RepresentationTheory.Character Mathlib.RepresentationTheory.Coinvariants Mathlib.RepresentationTheory.FDRep Mathlib.RepresentationTheory.FinGroupCharZero Mathlib.RepresentationTheory.FiniteIndex Mathlib.RepresentationTheory.Homological.ContCohomology.Basic Mathlib.RepresentationTheory.Homological.ContCohomology.Functoriality Mathlib.RepresentationTheory.Homological.ContCohomology.LowDegree 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.Tannaka Mathlib.RingTheory.Depth.Rees Mathlib.RingTheory.Flat.CategoryTheory Mathlib.RingTheory.LocalProperties.InjectiveDimension Mathlib.RingTheory.LocalProperties.ProjectiveDimension Mathlib.RingTheory.Regular.Category Mathlib.RingTheory.Regular.ProjectiveDimension Mathlib.RingTheory.SimpleRing.DivisionRing Mathlib.Topology.Category.Profinite.Nobeling.Induction Mathlib.Topology.Category.Profinite.Nobeling.Successor

1

---

Declarations diff (regex)

+ _root_.CategoryTheory.Subobject.exists_eq_imageSubobject
+ _root_.CategoryTheory.Subobject.exists_mk_eq_imageSubobject
+ _root_.CategoryTheory.Subobject.mk_mono_eq_imageSubobject
+ _root_.CategoryTheory.Subobject.pullback_kernelSubobject
+ _root_.CategoryTheory.Subobject.sup_eq_imageSubobject
+ existsComp
+ existsObjIso
+ exists_comp
+ exists_eq_mk_of_mono
+ exists_le_exists_iff_of_mono
+ exists_le_of_comm
+ exists_pullback_eq_inf_of_mono
+ exists_pullback_le
+ factorThruImage_comp_existsPullbackAdj_counit_app_hom_left
+ full_exists
+ imageObjIso
+ imageSubobject_epi_comp
+ le_pullback_exists
+ le_pullback_of_comm
+ pullback_exists_eq_self_of_mono
+ supIsImage
+ supIsoImage
+ supMonoFactorisation

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

• +36 new declarations
• −0 removed declarations

+CategoryTheory.Limits.equalizerSubobject.congr_simp
+CategoryTheory.Limits.image.isoStrongEpiMono.congr_simp
+CategoryTheory.Limits.imageSubobject_epi_comp
+CategoryTheory.MonoOver.existsComp
+CategoryTheory.MonoOver.existsObjIso
+CategoryTheory.MonoOver.existsObjIso_hom_hom_left
+CategoryTheory.MonoOver.existsObjIso_inv_hom_left
+CategoryTheory.MonoOver.factorThruImage_comp_existsPullbackAdj_counit_app_hom_left
+CategoryTheory.MonoOver.factorThruImage_comp_existsPullbackAdj_counit_app_hom_left_assoc
+CategoryTheory.MonoOver.full_exists
+CategoryTheory.MonoOver.imageObjIso
+CategoryTheory.MonoOver.imageObjIso_hom_hom_left
+CategoryTheory.MonoOver.imageObjIso_inv_hom_left
+CategoryTheory.Subobject.exists_comp
+CategoryTheory.Subobject.exists_eq_imageSubobject
+CategoryTheory.Subobject.exists_eq_mk_of_mono
+CategoryTheory.Subobject.exists_le_exists_iff_of_mono
+CategoryTheory.Subobject.exists_le_of_comm
+CategoryTheory.Subobject.exists_mk_eq_imageSubobject
+CategoryTheory.Subobject.exists_pullback_eq_inf_of_mono
+CategoryTheory.Subobject.exists_pullback_le
+CategoryTheory.Subobject.le_pullback_exists
+CategoryTheory.Subobject.le_pullback_of_comm
+CategoryTheory.Subobject.mk_mono_eq_imageSubobject
+CategoryTheory.Subobject.pullback_exists_eq_self_of_mono
+CategoryTheory.Subobject.pullback_kernelSubobject
+CategoryTheory.Subobject.supIsImage
+CategoryTheory.Subobject.supIsImage_lift
+CategoryTheory.Subobject.supIsoImage
+CategoryTheory.Subobject.supIsoImage_hom
+CategoryTheory.Subobject.supIsoImage_inv
+CategoryTheory.Subobject.supMonoFactorisation
+CategoryTheory.Subobject.supMonoFactorisation_I
+CategoryTheory.Subobject.supMonoFactorisation_e
+CategoryTheory.Subobject.supMonoFactorisation_m
+CategoryTheory.Subobject.sup_eq_imageSubobject

---

Increase in strong tech debt: (relative, absolute) = (1.00, 0.00)

Current number	Change	Type (strong)
5130	1	backward.isDefEq.respectTransparency

No changes to weak technical debt.

Current commit 3438f481ef
Reference commit 9058eaf3aa

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

[mathlib-dependent-issues]

This PR/issue depends on:

• feat(CategoryTheory/Subobject): extend exists and pullback API #42757
  By Dependent Issues (🤖). Happy coding!