[Merged by Bors] - feat(CategoryTheory): the Freyd-Mitchell embedding theorem #22222

TwoFX · 2025-02-23T18:34:56Z

Co-authored-by: Jakob von Raumer [email protected]
Co-authored-by: Paul Reichert [email protected]
Co-authored-by: Joël Riou [email protected]

depends on: [Merged by Bors] - feat(CategoryTheory): the category of ind-objects is Grothendieck abelian #21606

This reverts commit 2d7126d.

github-actions · 2025-02-23T18:35:56Z

PR summary 55e2d9d46d

Import changes for modified files

No significant changes to the import graph

Import changes for all files

Files	Import difference
`Mathlib.CategoryTheory.Abelian.FreydMitchell` (new file)	1399

Declarations diff

+ EmbeddingRing
+ faithful_embedding
+ freyd_mitchell
+ full_embedding
+ functor
+ instance : (functor C).Faithful := by
+ instance : (functor C).Full := by
+ instance : Nonempty (AsSmall.{max u v} C) := ⟨0⟩
+ instance : PreservesFiniteColimits (functor C) := by
+ instance : PreservesFiniteLimits (functor C) := by
+ instance : Ring (EmbeddingRing C)
+ preservesFiniteColimits_embedding
+ preservesFiniteLimits_embedding
- instance : PreservesFiniteColimits (embedding F) := by
- instance : PreservesFiniteLimits (embedding F) := by
- instance [Nonempty D] : (embedding F).Faithful
- instance [Nonempty D] [F.Full] : (F ⋙ embedding F).Full

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

mathlib4-dependent-issues-bot · 2025-02-23T19:02:12Z

This PR/issue depends on:

~~[Merged by Bors] - feat(CategoryTheory): the category of ind-objects is Grothendieck abelian #21606~~
By Dependent Issues (🤖). Happy coding!

joelriou · 2025-02-23T19:06:49Z

Mathlib/CategoryTheory/Abelian/FreydMitchell.lean

+Let `C` be an abelian category. We construct a ring `FreydMitchell.EmbeddingRing C` and a functor
+`FreydMitchell.embedding : C ⥤ ModuleCat.{max u v} (EmbeddingRing C)` which is full, faithful and
+exact.
+


Great work! Could you include an outline of the strategy of proof here, in particular the important work on Ind-objects?

I have added an overview of the proof stategy. Is that what you had in mind?

joelriou · 2025-02-23T20:35:20Z

Thanks!

bors merge

Co-authored-by: Jakob von Raumer <[email protected]> Co-authored-by: Paul Reichert <[email protected]> Co-authored-by: Joël Riou <[email protected]> Co-authored-by: Markus Himmel <[email protected]>

mathlib-bors · 2025-02-23T20:45:33Z

Pull request successfully merged into master.

Build succeeded:

* origin/master: feat(Polynomial): polynomial sequences are bases for R[X] (#20846) feat: monoidal structure on Hopf algebras (#12011) feat(DiscreteValuationRing): addVal_eq_zero_iff (#21154) refactor(Cache): refactor getPackageDir to not use manually provided package directories (#21817) feat(CategoryTheory): categories of homological complexes have a separator (#20229) chore(Data/Complex): deprecate `Complex.abs` (#21995) feat: uncountable instances for `Ordinal` and isomorphic types (#18547) feat(Data/Set/Card): a few missing lemmas (#22186) feat: discrete topological spaces are 0-manifolds (#22105) feat(Data/Matroid/Loop): matroid loops (#22045) feat(SetTheory/Ordinal/Nimber/Field): Nimber division (#19066) feat(LinearAlgebra/Pi): add `pi_proj` and `pi_proj_comp` (#22162) feat(Data/Matroid/Circuit): matroid cocircuits (#21692) feat(Topology/Compactification/OnePoint): generalize instance (#22179) feat(Combinatorics/SimpleGraph): takeUntil properties (#21250) feat(Tactic): `pnat_to_nat` and `enat_to_nat` tactics (#21602) refactor: move `Polynomial.coeffs` and related results (#22225) chore: add AlgHom.ker_coe_equiv, resolve porting notes and erws (#22019) refactor(Order/Category): `ConcreteCategory` instance for `\omegaCPO` (#21478) feat(CategoryTheory): Grothendieck categories have a coseparator (#22224) feat: tweak calc widget (#22170) feat(CategoryTheory): the Freyd-Mitchell embedding theorem (#22222) chore(CategoryTheory): turn more `simp` into `simps!` (#22223) feat(CategoryTheory): the category of ind-objects is Grothendieck abelian (#21606) feat(AlgebraicTopology/SimplexCategory/GeneratorsRelations/EpiMono): epi-mono factorisation in `SimplexCategoryGenRel` (#21743) chore(CategoryTheory/DiscreteCategory): turn `simp` to `simps!` (#22217) feat(Analysis/Asymptotics): exponential growth of a sequence (#21178) feat(CategoryTheory): sigmaConst preserves monomorphisms (#21599) feat(RingTheory/Cotangent): `liftBaseChange` is injective for localizations (#21037) chore(CategoryTheory): fix incorrect name (#22210) feat(CategoryTheory): `IsPullback` version of 'pullback of iso is iso' (#22211) feat(CategoryTheory): pullbacks in functor categories (#22209) feat(CategoryTheory): detecting limit cones over connected diagrams (#22192) feat(LinearAlgebra): add theorems for injective/surjective/bijective compositions of bilinear maps (#21491)

Co-authored-by: Jakob von Raumer <[email protected]> Co-authored-by: Paul Reichert <[email protected]> Co-authored-by: Joël Riou <[email protected]> Co-authored-by: Markus Himmel <[email protected]>

TwoFX added 30 commits January 26, 2025 11:32

Bad start

3c87dcb

WIP

f4a3c79

nothing

2d7126d

feat: group objects

b2d6f6b

Revert "nothing"

6ad4df4

This reverts commit 2d7126d.

Mathlib.lean

a790055

Switch to PreservesFiniteProducts

f36a814

Additional group stuff

d121ea8

CommGrp

4ddcb9d

Additional group stuff

ef5a5d6

Cleanup

f8fe688

WIP

eab57ef

Okay

5682836

WIP

c1b92de

Done

97bdbca

Fix

1cf5d22

Merge remote-tracking branch 'origin/master' into fme-197-more

8959ad6

Merge remote-tracking branch 'origin/master' into fme-197

2172134

Add forgetful functor

93b6633

Import

10f6445

Compatibility

0d20720

Fix namespace

b1c3eee

Move to separate file

2fe34b5

Merge branch 'fme-197' into fme-197-more

ef38b43

Fix

6da6e17

Add forgetful functor

527b8c9

Fix

4e118dd

Merge branch 'fme-197-more' into fme-199

9c42bc2

Cleanup

22b12d2

Fix implicitness

d575b25

TwoFX added 8 commits February 22, 2025 11:59

Docs

0abcc2d

Merge branch 'tothefinish' into fme-204

443f60c

Update 1000.yaml

6330cd3

Update comment in Pseudoelements.lean

ff3622f

Comment

5021923

Fix

0500131

Busywork

96146bc

Typo

6063df1

TwoFX changed the title ~~Fme 204~~ feat(CategoryTheory): the Freyd-Mitchell embedding theorem Feb 23, 2025

github-actions bot added the large-import Automatically added label for PRs with a significant increase in transitive imports label Feb 23, 2025

github-actions bot added the t-category-theory Category theory label Feb 23, 2025

mathlib4-dependent-issues-bot added the blocked-by-other-PR This PR depends on another PR to Mathlib (this label is automatically managed by a bot) label Feb 23, 2025

Merge remote-tracking branch 'origin/master' into fme-204

ed5ef10

mathlib4-dependent-issues-bot removed the blocked-by-other-PR This PR depends on another PR to Mathlib (this label is automatically managed by a bot) label Feb 23, 2025

github-actions bot removed the large-import Automatically added label for PRs with a significant increase in transitive imports label Feb 23, 2025

joelriou reviewed Feb 23, 2025

View reviewed changes

joelriou added the awaiting-author A reviewer has asked the author a question or requested changes label Feb 23, 2025

add overview

55e2d9d

TwoFX removed the awaiting-author A reviewer has asked the author a question or requested changes label Feb 23, 2025

leanprover-community-mathlib4-bot added the ready-to-merge This PR has been sent to bors. label Feb 23, 2025

mathlib-bors bot changed the title ~~feat(CategoryTheory): the Freyd-Mitchell embedding theorem~~ [Merged by Bors] - feat(CategoryTheory): the Freyd-Mitchell embedding theorem Feb 23, 2025

mathlib-bors bot closed this Feb 23, 2025

mathlib-bors bot deleted the fme-204 branch February 23, 2025 20:45

Provide feedback

Saved searches

Use saved searches to filter your results more quickly

[Merged by Bors] - feat(CategoryTheory): the Freyd-Mitchell embedding theorem #22222

[Merged by Bors] - feat(CategoryTheory): the Freyd-Mitchell embedding theorem #22222

TwoFX commented Feb 23, 2025 •

edited

Loading

github-actions bot commented Feb 23, 2025 •

edited

Loading

Declarations diff

mathlib4-dependent-issues-bot commented Feb 23, 2025

joelriou Feb 23, 2025

TwoFX Feb 23, 2025

joelriou commented Feb 23, 2025

mathlib-bors bot commented Feb 23, 2025

[Merged by Bors] - feat(CategoryTheory): the Freyd-Mitchell embedding theorem #22222

[Merged by Bors] - feat(CategoryTheory): the Freyd-Mitchell embedding theorem #22222

Conversation

TwoFX commented Feb 23, 2025 • edited Loading

github-actions bot commented Feb 23, 2025 • edited Loading

PR summary 55e2d9d46d

Import changes for modified files

Declarations diff

mathlib4-dependent-issues-bot commented Feb 23, 2025

joelriou Feb 23, 2025

Choose a reason for hiding this comment

TwoFX Feb 23, 2025

Choose a reason for hiding this comment

joelriou commented Feb 23, 2025

mathlib-bors bot commented Feb 23, 2025

TwoFX commented Feb 23, 2025 •

edited

Loading

github-actions bot commented Feb 23, 2025 •

edited

Loading