[Merged by Bors] - feat(CategoryTheory): Split equalizers #14170

mckoen · 2024-06-26T21:18:59Z

Defines what it means for a triple of morphisms f g : X ⟶ Y, ι : W ⟶ X to be a split equalizer. In addition, shows that every split equalizer is an equalizer and absolute.

This dualises everything in Mathlib.CategoryTheory.Limits.Shapes.SplitCoequalizer.

This contribution was created as part of the AIM workshop "Formalizing Algebraic Geometry" in June 2024.

github-actions · 2024-06-26T21:19:36Z

PR summary acae65ca35

Import changes

No significant changes to the import graph

Declarations diff

+ HasSplitEqualizer
+ HasSplitEqualizer.equalizerOfSplit
+ HasSplitEqualizer.equalizerι
+ HasSplitEqualizer.isSplitEqualizer
+ IsSplitEqualizer
+ IsSplitEqualizer.asFork
+ IsSplitEqualizer.asFork_ι
+ IsSplitEqualizer.isEqualizer
+ IsSplitEqualizer.map
+ instance (priority := 1) hasEqualizer_of_hasSplitEqualizer [HasSplitEqualizer f g] :
+ instance {X : C} : Inhabited (IsSplitEqualizer (𝟙 X) (𝟙 X) (𝟙 X))
+ map_is_cosplit_pair

You can run this locally as follows

## summary with just the declaration names:
./scripts/no_lost_declarations.sh short <optional_commit>

## more verbose report:
./scripts/no_lost_declarations.sh <optional_commit>

Mathlib/CategoryTheory/Limits/Shapes/SplitEqualizer.lean

dagurtomas · 2024-06-27T09:00:56Z

Mathlib/CategoryTheory/Limits/Shapes/SplitEqualizer.lean

+  HasSplitEqualizer (G.map f) (G.map g)
+
+/-- Get the equalizer object from the typeclass `IsCosplitPair`. -/
+noncomputable def HasSplitEqualizer.equalizerOfCosplit [HasSplitEqualizer f g] : C :=


This def should be called HasSplitEqualizer.equalizer or something like that, as it has nothing to do with CosplitPair. I guess it's adapted from the other file, in which case that should be changed too.

Ok, I changed this name to HasSplitEqualizer.equalizerOfSplit, and didn't touch it in the other file. The Split in the name in the other file doesn't refer to Functor.IsSplitPair, hence we shouldn't use `Cosplit here.

Mathlib/CategoryTheory/Limits/Shapes/SplitEqualizer.lean

kim-em · 2024-06-29T07:06:16Z

bors d+

mathlib-bors · 2024-06-29T07:06:18Z

✌️ mckoen can now approve this pull request. To approve and merge a pull request, simply reply with bors r+. More detailed instructions are available here.

Co-authored-by: Kim Morrison <[email protected]>

mckoen · 2024-07-01T18:13:10Z

bors merge

Defines what it means for a triple of morphisms `f g : X ⟶ Y`, `ι : W ⟶ X` to be a split equalizer. In addition, shows that every split equalizer is an equalizer and absolute. This dualises everything in [Mathlib.CategoryTheory.Limits.Shapes.SplitCoequalizer](https://leanprover-community.github.io/mathlib4_docs/Mathlib/CategoryTheory/Limits/Shapes/SplitCoequalizer.html). This contribution was created as part of the AIM workshop "Formalizing Algebraic Geometry" in June 2024. Co-authored-by: dagurtomas <[email protected]> Co-authored-by: Jack <[email protected]>

mathlib-bors · 2024-07-01T18:42:26Z

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

Defines what it means for a triple of morphisms `f g : X ⟶ Y`, `ι : W ⟶ X` to be a split equalizer. In addition, shows that every split equalizer is an equalizer and absolute. This dualises everything in [Mathlib.CategoryTheory.Limits.Shapes.SplitCoequalizer](https://leanprover-community.github.io/mathlib4_docs/Mathlib/CategoryTheory/Limits/Shapes/SplitCoequalizer.html). This contribution was created as part of the AIM workshop "Formalizing Algebraic Geometry" in June 2024. Co-authored-by: dagurtomas <[email protected]> Co-authored-by: Jack <[email protected]>

mathlib-bors · 2024-07-01T19:46:36Z

Build failed (retrying...):

Build

mathlib-bors · 2024-07-01T20:09:26Z

Canceled.

riccardobrasca · 2024-07-02T15:54:17Z

What is the situation with this PR?

mckoen · 2024-07-02T16:19:30Z

What is the situation with this PR?

I'm not sure, I thought it was okay to merge but it was cancelled for some reason. I'm not very familiar with Bors so maybe I did something wrong

riccardobrasca · 2024-07-02T16:52:50Z

Something failed, can you merge master and see what's wrong?

riccardobrasca · 2024-07-02T19:11:58Z

Thanks!

bors merge

Defines what it means for a triple of morphisms `f g : X ⟶ Y`, `ι : W ⟶ X` to be a split equalizer. In addition, shows that every split equalizer is an equalizer and absolute. This dualises everything in [Mathlib.CategoryTheory.Limits.Shapes.SplitCoequalizer](https://leanprover-community.github.io/mathlib4_docs/Mathlib/CategoryTheory/Limits/Shapes/SplitCoequalizer.html). This contribution was created as part of the AIM workshop "Formalizing Algebraic Geometry" in June 2024. Co-authored-by: dagurtomas <[email protected]> Co-authored-by: Jack <[email protected]> Co-authored-by: Joël Riou <[email protected]>

mathlib-bors · 2024-07-02T19:29:02Z

Pull request successfully merged into master.

Build succeeded:

mckoen added 2 commits June 26, 2024 13:48

splitequalizer

4b47e20

change split to cosplit

e299989

mckoen added the t-category-theory Category theory label Jun 26, 2024

github-actions bot added the new-contributor This PR was made by a contributor with at most 5 merged PRs. Welcome to the community! label Jun 26, 2024

mckoen changed the title ~~feat(CategoryTheory): Split Equalizers~~ feat(CategoryTheory): Split equalizers Jun 26, 2024

add to mathlib.lean

25b042c

mckoen mentioned this pull request Jun 26, 2024

[Merged by Bors] - feat(CategoryTheory): Special equalizers associated to a comonad #14171

Closed

1 task

mckoen added the awaiting-review label Jun 26, 2024

joelriou added the t-algebraic-geometry Algebraic geometry label Jun 26, 2024

dagurtomas reviewed Jun 27, 2024

View reviewed changes

Mathlib/CategoryTheory/Limits/Shapes/SplitEqualizer.lean Outdated Show resolved Hide resolved

dagurtomas reviewed Jun 27, 2024

View reviewed changes

remove @s

c9de176

dagurtomas approved these changes Jun 27, 2024

View reviewed changes

dagurtomas added the awaiting-CI label Jun 27, 2024

github-actions bot removed the awaiting-CI label Jun 27, 2024

mckoen added the workshop-AIM-AG-2024 This PR is associated with the 2024 AIM workshop on formalization of algebraic geometry label Jun 28, 2024

This was referenced Jun 28, 2024

[Merged by Bors] - feat(CategoryTheory): (co)limits in the category of coalgebras #14236

Closed

[Merged by Bors] - feat(CategoryTheory): Beck's comonadicity theorem #14238

Closed

kim-em reviewed Jun 29, 2024

View reviewed changes

Mathlib/CategoryTheory/Limits/Shapes/SplitEqualizer.lean Outdated Show resolved Hide resolved

github-actions bot added delegated and removed awaiting-review labels Jun 29, 2024

mckoen and others added 2 commits July 1, 2024 17:52

Update Mathlib/CategoryTheory/Limits/Shapes/SplitEqualizer.lean

b54940d

Co-authored-by: Kim Morrison <[email protected]>

Update SplitCoequalizer.lean

f09736e

Merge remote-tracking branch 'origin' into mckoen/AIM_comonadicity

f6ffb9b

riccardobrasca added the awaiting-author A reviewer has asked the author a question or requested changes label Jul 2, 2024

Merge branch 'master' into mckoen/AIM_comonadicity

acae65c

github-actions bot added ready-to-merge This PR has been sent to bors. and removed awaiting-author A reviewer has asked the author a question or requested changes labels Jul 2, 2024

mathlib-bors bot changed the title ~~feat(CategoryTheory): Split equalizers~~ [Merged by Bors] - feat(CategoryTheory): Split equalizers Jul 2, 2024

mathlib-bors bot closed this Jul 2, 2024

mathlib-bors bot deleted the mckoen/AIM_comonadicity branch July 2, 2024 19:29

adomani mentioned this pull request Aug 1, 2024

feat: MiM PR report #15355

Open

Provide feedback

Saved searches

Use saved searches to filter your results more quickly

[Merged by Bors] - feat(CategoryTheory): Split equalizers #14170

[Merged by Bors] - feat(CategoryTheory): Split equalizers #14170

mckoen commented Jun 26, 2024 •

edited

Loading

github-actions bot commented Jun 26, 2024 •

edited

Loading

Declarations diff

dagurtomas Jun 27, 2024

dagurtomas Jun 27, 2024

kim-em commented Jun 29, 2024

mathlib-bors bot commented Jun 29, 2024

mckoen commented Jul 1, 2024

mathlib-bors bot commented Jul 1, 2024

mathlib-bors bot commented Jul 1, 2024

mathlib-bors bot commented Jul 1, 2024

riccardobrasca commented Jul 2, 2024

mckoen commented Jul 2, 2024

riccardobrasca commented Jul 2, 2024

riccardobrasca commented Jul 2, 2024

mathlib-bors bot commented Jul 2, 2024

[Merged by Bors] - feat(CategoryTheory): Split equalizers #14170

[Merged by Bors] - feat(CategoryTheory): Split equalizers #14170

Conversation

mckoen commented Jun 26, 2024 • edited Loading

github-actions bot commented Jun 26, 2024 • edited Loading

PR summary acae65ca35

Import changes

Declarations diff

dagurtomas Jun 27, 2024

Choose a reason for hiding this comment

dagurtomas Jun 27, 2024

Choose a reason for hiding this comment

kim-em commented Jun 29, 2024

mathlib-bors bot commented Jun 29, 2024

mckoen commented Jul 1, 2024

mathlib-bors bot commented Jul 1, 2024

mathlib-bors bot commented Jul 1, 2024

mathlib-bors bot commented Jul 1, 2024

riccardobrasca commented Jul 2, 2024

mckoen commented Jul 2, 2024

riccardobrasca commented Jul 2, 2024

riccardobrasca commented Jul 2, 2024

mathlib-bors bot commented Jul 2, 2024

mckoen commented Jun 26, 2024 •

edited

Loading

github-actions bot commented Jun 26, 2024 •

edited

Loading