[joelriou]

If A is a monoidal category, we introduce a property of objects ObjectProperty.flat : ObjectProperty A which is satisfied by objects X : A such that both functors tensorLeft X : A ⥤ A and tensorRight X : A ⥤ A are exact (i.e. preserve both finite limits and finite colimits).

Moreover, if A is an abelian category, we introduce a typeclass Abelian.HasFunctorialFlatResolution A which says that objects in A admit a functorial epimorphism from a flat object.

---

• depends on: [Merged by Bors] - chore(CategoryTheory): deprecate leftExactFunctor #45418
• depends on: [Merged by Bors] - feat(CategoryTheory): stability under retracts of the preservation of (co)limits #45417

[github-actions]

PR summary 0ddb4253a1

Import changes for modified files

No significant changes to the import graph

Import changes for all files

Files	Import difference
Mathlib.CategoryTheory.Abelian.Flat.Basic (new file)	1155

---

Declarations diff (regex)

+ HasFunctorialFlatResolution
+ HasFunctorialFlatResolution.mk
+ exactFunctor.preservesFiniteColimits
+ exactFunctor.preservesFiniteLimits
+ flat
+ flat_eq_min
+ instance : (flat (A := A)).IsClosedUnderIsomorphisms := by
+ instance : (flat (A := A)).IsMonoidal
+ instance : (flat (A := A)).IsStableUnderRetracts := by
+ instance {D : Type*} [Category* D] (F : D ⥤ C) : (P.inverseImage F).IsStableUnderRetracts
+ instance {P₁ P₂ : ObjectProperty C} [P₁.IsStableUnderRetracts] [P₂.IsStableUnderRetracts] :
+ tensorLeft
+ tensorRight
- instance : (exactFunctor C D).IsClosedUnderIsomorphisms := by

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

• +14 new declarations
• −0 removed declarations

+CategoryTheory.Abelian.HasFunctorialFlatResolution
+CategoryTheory.Abelian.HasFunctorialFlatResolution.mk
+CategoryTheory.ObjectProperty.IsStableUnderRetracts.instInverseImage
+CategoryTheory.ObjectProperty.flat
+CategoryTheory.ObjectProperty.flat.instIsClosedUnderIsomorphisms
+CategoryTheory.ObjectProperty.flat.instIsMonoidal
+CategoryTheory.ObjectProperty.flat.instIsStableUnderRetracts
+CategoryTheory.ObjectProperty.flat.tensorLeft
+CategoryTheory.ObjectProperty.flat.tensorRight
+CategoryTheory.ObjectProperty.flat_eq_min
+CategoryTheory.ObjectProperty.instIsStableUnderRetractsMin
+CategoryTheory.exactFunctor.preservesFiniteColimits
+CategoryTheory.exactFunctor.preservesFiniteLimits
+CategoryTheory.instIsStableUnderRetractsFunctorExactFunctor

---

No changes to strong technical debt.
No changes to weak technical debt.

Current commit 0ddb4253a1
Reference commit f9738e46d3

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

[mathlib-dependent-issues]

This PR/issue depends on:

• [Merged by Bors] - chore(CategoryTheory): deprecate leftExactFunctor #45418
• [Merged by Bors] - feat(CategoryTheory): stability under retracts of the preservation of (co)limits #45417
  By Dependent Issues (🤖). Happy coding!

[robin-carlier]

Is there a way to keep good dot notation while scoping this name to something else than barely ObjectProperty? Maybe ObjectProperty.Monoidal.flat?

There is a notion of "flat functors" as well, and ObjectProperty.flat could equally be the object property of such functors.