[Merged by Bors] - feat(CategoryTheory): Split equalizers by mckoen · Pull Request #14170 · leanprover-community/mathlib4

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 <kim@tqft.net>

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 <dagurtomas@gmail.com> Co-authored-by: Jack <104791831+mckoen@users.noreply.github.com>

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 <dagurtomas@gmail.com> Co-authored-by: Jack <104791831+mckoen@users.noreply.github.com>

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 <dagurtomas@gmail.com> Co-authored-by: Jack <104791831+mckoen@users.noreply.github.com> Co-authored-by: Joël Riou <joel.riou@universite-paris-saclay.fr>

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 This PR does not pass CI yet. This label is automatically removed once it does. label Jun 27, 2024

github-actions bot removed the awaiting-CI This PR does not pass CI yet. This label is automatically removed once it does. 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 This pull request has been delegated to the PR author (or occasionally another non-maintainer). 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 <kim@tqft.net>

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

Conversation

mckoen commented Jun 26, 2024 • edited Loading Uh oh! There was an error while loading. Please reload this page.

Uh oh!

Uh oh!

github-actions bot commented Jun 26, 2024 • edited Loading Uh oh! There was an error while loading. Please reload this page.

Uh oh!

PR summary acae65ca35

Import changes

Declarations diff

Uh oh!

Uh oh!

dagurtomas Jun 27, 2024

Choose a reason for hiding this comment

Uh oh!

dagurtomas Jun 27, 2024

Choose a reason for hiding this comment

Uh oh!

Uh oh!

kim-em commented Jun 29, 2024

Uh oh!

mathlib-bors bot commented Jun 29, 2024

Uh oh!

mckoen commented Jul 1, 2024

Uh oh!

mathlib-bors bot commented Jul 1, 2024

Uh oh!

mathlib-bors bot commented Jul 1, 2024

Uh oh!

mathlib-bors bot commented Jul 1, 2024

Uh oh!

riccardobrasca commented Jul 2, 2024

Uh oh!

mckoen commented Jul 2, 2024

Uh oh!

riccardobrasca commented Jul 2, 2024

Uh oh!

riccardobrasca commented Jul 2, 2024

Uh oh!

mathlib-bors bot commented Jul 2, 2024

Uh oh!

Reviewers

Assignees

Labels

Projects

Milestone

Development

Uh oh!

5 participants

mckoen commented Jun 26, 2024 •

edited

Loading

github-actions bot commented Jun 26, 2024 •

edited

Loading