[Merged by Bors] - feat(AlgebraicTopology/SimplexCategory/GeneratorsRelations/EpiMono): epi-mono factorisation in `SimplexCategoryGenRel` by robin-carlier · Pull Request #21743 · leanprover-community/mathlib4

robin-carlier · 2025-02-11T21:22:05Z

We show that every morphism in SimplexCategoryGenRel factors as a P_σ followed by a P_δ.

Part of a series of PR formalising that SimplexCategoryGenRel is equivalent to SimplexCategory.

depends on: [Merged by Bors] - feat(AlgebraicTopology/SimplexCategory/GeneratorsRelations/EpiMono): Morphism properties in SimplexCategoryGenRel #21742

github-actions · 2025-02-11T21:23:00Z

PR summary 48943d0338

Import changes for modified files

No significant changes to the import graph

Import changes for all files

Files	Import difference

Declarations diff

+ exists_P_σ_P_δ_factorization
+ instance : MorphismProperty.HasFactorization P_σ P_δ

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

Co-authored-by: Joël Riou <37772949+joelriou@users.noreply.github.com>

…sure of a property

…es` and eqToHom

robin-carlier · 2025-02-21T16:01:31Z

Thanks a lot @joelriou for taking the time to golf these!

Co-authored-by: Joël Riou <37772949+joelriou@users.noreply.github.com>

joelriou · 2025-02-23T17:57:52Z

Just in case, could you merge again with master?

joelriou · 2025-02-23T18:24:24Z

Thanks!

bors merge

…epi-mono factorisation in `SimplexCategoryGenRel` (#21743) We show that every morphism in `SimplexCategoryGenRel` factors as a `P_σ` followed by a `P_δ`. Part of a series of PR formalising that `SimplexCategoryGenRel` is equivalent to `SimplexCategory`.

mathlib-bors · 2025-02-23T18:42:35Z

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)

…epi-mono factorisation in `SimplexCategoryGenRel` (#21743) We show that every morphism in `SimplexCategoryGenRel` factors as a `P_σ` followed by a `P_δ`. Part of a series of PR formalising that `SimplexCategoryGenRel` is equivalent to `SimplexCategory`.

Initial commit

53a6f43

github-actions Bot added the t-topology Topological spaces, uniform spaces, metric spaces, filters label Feb 11, 2025

This was referenced Feb 11, 2025

[Merged by Bors] - feat(AlgebraicTopology/SimplexCategory/GeneratorsRelations/NormalForms): admissible lists and simplicial insertion #21744

Closed

Tracking issue: definition of simplicial objects by generators and relations. #21749

Open

lake shake

b5404f9

robin-carlier force-pushed the RC_SimplexCategoryGenRel3 branch from 5fcb6f6 to 5e27260 Compare February 11, 2025 21:38

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

joelriou added the t-category-theory Category theory label Feb 12, 2025

robin-carlier and others added 5 commits February 12, 2025 11:58

Apply suggestions from code review

de99346

Co-authored-by: Joël Riou <37772949+joelriou@users.noreply.github.com>

fix build

8307c3e

change namespace

f36825f

mirror names

89e5264

better nat lemmas

0a75491

robin-carlier force-pushed the RC_SimplexCategoryGenRel3 branch from 5e27260 to 789297a Compare February 12, 2025 12:03

robin-carlier added 5 commits February 13, 2025 11:33

change namespace

99c76f2

Initial

92ac6ea

adapt to changes in #21741

1e84b00

adapt namespace change

7679d60

rebase on #21742

ee6df34

robin-carlier force-pushed the RC_SimplexCategoryGenRel3 branch from 789297a to ee6df34 Compare February 13, 2025 10:53

joelriou reviewed Feb 13, 2025

View reviewed changes

Comment thread Mathlib/AlgebraicTopology/SimplexCategory/GeneratorsRelations/EpiMono.lean Outdated

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

joelriou mentioned this pull request Feb 13, 2025

[Merged by Bors] - feat(AlgebraicTopology/SimplexCategory/GeneratorsRelations): the category SimplexCategoryGenRel #21741

Closed

1 task

leanprover-community-bot-assistant added the merge-conflict The PR has a merge conflict with master, and needs manual merging. (this label is managed by a bot) label Feb 14, 2025

feat(CategoryTheory/MorphismProperty/Composition): multiplicative clo…

dced4d2

…sure of a property

robin-carlier mentioned this pull request Feb 14, 2025

[Merged by Bors] - feat(CategoryTheory/MorphismProperty): multiplicative closure of a MorphismProperty #21864

Closed

robin-carlier added 3 commits February 14, 2025 11:50

feat(CategoryTheory/MorphismProperty/Composition): multiplicative clo…

5544494

…sure of a property

chore(CategoryTheory/MorphismProperty/Composition): `ContainsIdentiti…

f2456b6

…es` and eqToHom

Initial commit

cbb8abc

joelriou reviewed Feb 21, 2025

View reviewed changes

Comment thread Mathlib/AlgebraicTopology/SimplexCategory/GeneratorsRelations/EpiMono.lean Outdated

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

Apply suggestions from code review

bf4595d

Co-authored-by: Joël Riou <37772949+joelriou@users.noreply.github.com>

robin-carlier added awaiting-CI This PR does not pass CI yet. This label is automatically removed once it does. and removed awaiting-author A reviewer has asked the author a question or requested changes. labels Feb 21, 2025

github-actions Bot removed the awaiting-CI This PR does not pass CI yet. This label is automatically removed once it does. label Feb 21, 2025

joelriou reviewed Feb 22, 2025

View reviewed changes

Comment thread Mathlib/AlgebraicTopology/SimplexCategory/GeneratorsRelations/EpiMono.lean Outdated

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

robin-carlier added 3 commits February 23, 2025 15:45

Golf a bit more the proofs

63bfbba

more golf

06223ae

micro golf

8c043d1

robin-carlier added awaiting-CI This PR does not pass CI yet. This label is automatically removed once it does. and removed awaiting-author A reviewer has asked the author a question or requested changes. labels Feb 23, 2025

github-actions Bot removed the awaiting-CI This PR does not pass CI yet. This label is automatically removed once it does. label Feb 23, 2025

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

Merge branch 'master' into RC_SimplexCategoryGenRel3

48943d0

robin-carlier added awaiting-CI This PR does not pass CI yet. This label is automatically removed once it does. and removed awaiting-author A reviewer has asked the author a question or requested changes. labels Feb 23, 2025

github-actions Bot removed the awaiting-CI This PR does not pass CI yet. This label is automatically removed once it does. label Feb 23, 2025

ghost added the ready-to-merge This PR has been sent to bors. label Feb 23, 2025

mathlib-bors Bot closed this Feb 23, 2025

mathlib-bors Bot deleted the RC_SimplexCategoryGenRel3 branch February 23, 2025 18:42

Navigation Menu

Uh oh!

[Merged by Bors] - feat(AlgebraicTopology/SimplexCategory/GeneratorsRelations/EpiMono): epi-mono factorisation in `SimplexCategoryGenRel` - #21743

[Merged by Bors] - feat(AlgebraicTopology/SimplexCategory/GeneratorsRelations/EpiMono): epi-mono factorisation in `SimplexCategoryGenRel`#21743
robin-carlier wants to merge 128 commits into
masterfrom
RC_SimplexCategoryGenRel3

robin-carlier commented Feb 11, 2025 •

edited

Loading

Uh oh!

github-actions Bot commented Feb 11, 2025 •

edited

Loading

Uh oh!

Uh oh!

Uh oh!

robin-carlier commented Feb 21, 2025

Uh oh!

Uh oh!

joelriou commented Feb 23, 2025

Uh oh!

joelriou commented Feb 23, 2025

Uh oh!

mathlib-bors Bot commented Feb 23, 2025

Uh oh!

Reviewers

Assignees

Labels

Projects

Milestone

Development

Uh oh!

6 participants

Uh oh!

Conversation

robin-carlier commented Feb 11, 2025 • edited Loading Uh oh! There was an error while loading. Please reload this page.

Uh oh!

Uh oh!

github-actions Bot commented Feb 11, 2025 • edited Loading Uh oh! There was an error while loading. Please reload this page.

Uh oh!

PR summary 48943d0338

Import changes for modified files

Declarations diff

Uh oh!

Uh oh!

Uh oh!

robin-carlier commented Feb 21, 2025

Uh oh!

Uh oh!

joelriou commented Feb 23, 2025

Uh oh!

joelriou commented Feb 23, 2025

Uh oh!

mathlib-bors Bot commented Feb 23, 2025

Uh oh!

Reviewers

Assignees

Labels

Projects

Milestone

Development

Uh oh!

6 participants

robin-carlier commented Feb 11, 2025 •

edited

Loading

github-actions Bot commented Feb 11, 2025 •

edited

Loading