Skip to content
This repository has been archived by the owner on Jul 24, 2024. It is now read-only.

[Merged by Bors] - feat(category_theory/path_category): canonical quotient of a path category #13159

Closed
wants to merge 8 commits into from
Closed

[Merged by Bors] - feat(category_theory/path_category): canonical quotient of a path category #13159

wants to merge 8 commits into from

Conversation

kim-em
Copy link
Collaborator

@kim-em kim-em commented Apr 4, 2022

This isn't particularly interesting in itself. I'm thinking of it as a warm-up to quasi-strict monoidal categories. :-)

Open in Gitpod

@kim-em kim-em requested a review from dwarn April 4, 2022 05:01
@kim-em kim-em added the awaiting-CI The author would like to see what CI has to say before doing more work. label Apr 4, 2022
@github-actions github-actions bot removed the awaiting-CI The author would like to see what CI has to say before doing more work. label Apr 4, 2022
@dwarn
Copy link
Collaborator

dwarn commented Apr 4, 2022

Maybe it's not worth the added generality, but doesn't most of this work also for other functors F : C => D in place of path_composition? I mean, F.map f = F.map g determines a congruence relation on C and the quotient has a faithful functor to D, which is an equivalence if F is full and essentially surjective. (Indeed, this should be part of an equivalence between congruence relations on C and full, essentially surjective functors out of C)

@bryangingechen bryangingechen added the awaiting-review The author would like community review of the PR label Apr 5, 2022
@jcommelin jcommelin added awaiting-author A reviewer has asked the author a question or requested changes and removed awaiting-review The author would like community review of the PR labels Apr 9, 2022
@jcommelin
Copy link
Member

LGTM, but see @dwarn's comment above. Happy to merge this as is.

@kim-em
Copy link
Collaborator Author

kim-em commented Apr 13, 2022

Okay, I don't seem to be getting to this generalization, so I've just added a TODO comment for it to be done later.

@kim-em kim-em added awaiting-review The author would like community review of the PR and removed awaiting-author A reviewer has asked the author a question or requested changes labels Apr 13, 2022
@jcommelin
Copy link
Member

Thanks 🎉

bors merge

@github-actions github-actions bot added ready-to-merge All that is left is for bors to build and merge this PR. (Remember you need to say `bors r+`.) and removed awaiting-review The author would like community review of the PR labels Apr 21, 2022
bors bot pushed a commit that referenced this pull request Apr 21, 2022
@kim-em
feat(category_theory/path_category): canonical quotient of a path cat…
82ef19a 
…egory (#13159)




Co-authored-by: Scott Morrison <scott.morrison@gmail.com>
@bors
Copy link

bors bot commented Apr 21, 2022

Pull request successfully merged into master.

Build succeeded:

@bors bors bot changed the title feat(category_theory/path_category): canonical quotient of a path category [Merged by Bors] - feat(category_theory/path_category): canonical quotient of a path category Apr 21, 2022
@bors bors bot closed this Apr 21, 2022
@bors bors bot deleted the semorrison/presented_category branch April 21, 2022 14:17
Julian added a commit that referenced this pull request Apr 21, 2022
@Julian
Merge remote-tracking branch 'origin/master' into torsion-free-groups
eb3119e 
* origin/master: (394 commits)
  feat(data/set/[basic|prod]): make `×ˢ` bind more strongly, and define `mem.out` (#13422)
  feat(order/basic): Simple shortcut lemmas (#13421)
  chore(number_theory/dioph): Cleanup (#13403)
  feat(analysis/normed_space/exponential): ring homomorphisms are preserved by the exponential (#13402)
  feat(algebraic_geometry/projective_spectrum): degree zero part of a localized ring (#13398)
  feat(set_theory/cardinal): A set of cardinals is small iff it's bounded (#13373)
  feat(data/polynomial/{derivative, iterated_deriv}): reduce assumptions (#13368)
  feat(algebra/monoid_algebra/grading): Use the new graded_algebra API (#13360)
  feat(algebra/group/to_additive): let @[to_additive] mimic alias’s docstrings (#13330)
  feat(set_theory/cofinality): Basic fundamental sequences (#13326)
  feat(special_functions/pow): continuity of real to complex power (#13244)
  feat(group_theory/torsion): extension closedness, and torsion scalars in modules (#13172)
  feat(category_theory/path_category): canonical quotient of a path category (#13159)
  refactor(number_theory/padics/padic_norm): Switch nat and rat definitions (#12454)
  feat(analysis/normed): more lemmas about the sup norm on pi types and matrices (#13536)
  fix(category_theory/monoidal): improve hygiene in coherence tactic (#13507)
  feat(src/number_theory/cyclotomic/discriminant): add discr_prime_pow_ne_two (#13465)
  chore(algebra/group/type_tags): missing simp lemmas (#13553)
  feat(measure_theory): allow measurability to prove ae_strongly_measurable (#13427)
  refactor(algebra/hom/group): generalize a few lemmas to `monoid_hom_class` (#13447)
  chore(data/list/cycle): Add basic `simp` lemmas + minor golfing (#13533)
  feat(algebra/hom/non_unital_alg): introduce notation for non-unital algebra homomorphisms (#13470)
  chore(algebra/group/defs): Declare `field_simps` attribute earlier (#13543)
  feat(analysis/normed/normed_field): add `one_le_(nn)norm_one` for nontrivial normed rings (#13556)
  refactor(analysis/calculus/cont_diff): reorder the file (#13468)
  move(set_theory/*): Organize in folders (#13530)
  chore(number_theory/zsqrtd/basic): simplify le_total proof (#13555)
  feat(group_theory/perm/basic): Iterating a permutation is the same as taking a power (#13554)
  feat(data/real/sqrt): `sqrt x < y ↔ x < y^2` (#13546)
  feat(algebra/hom/group and *): introduce `mul_hom M N` notation `M →ₙ* N` (#13526)
  feat(group_theory/schreier): Schreier's lemma in terms of `group.fg` and `group.rank` (#13361)
  feat(linear_algebra/trace): dual_tensor_hom is an equivalence + basis-free characterization of the trace (#10372)
  feat(order/filter/basic): allow functions between different types in lemmas about [co]map by a constant function (#13542)
  feat(data/finset/basic): simp `to_finset_eq_empty` (#13531)
  feat(topology/algebra/algebra): ℚ-scalar multiplication is continuous (#13458)
  chore(model_theory/encoding): Improve the encoding of terms  (#13532)
  feat(topology/separation): Finite sets in T2 spaces (#12845)
  feat(analysis/inner_product_space/gram_schmidt_ortho): Gram-Schmidt Orthogonalization and Orthonormalization (#12857)
  chore(algebra/big_operators/fin): golf finset.prod_range (#13535)
  chore(analysis/normed_space/star): make an argument explicit (#13523)
  feat(*): `op_op_op_comm` lemmas (#13528)
  chore(data/real/nnreal): add commuted version of `nnreal.mul_finset_sup` (#13512)
  chore(*/matrix): order `m` and `n` alphabetically (#13510)
  feat(analysis/calculus/specific_functions): trivial extra lemmas (#13516)
  feat(analysis): lemmas about nnnorm and nndist (#13498)
  feat(data/int/basic): add lemma `int.abs_le_one_iff` (#13513)
  feat(category_theory/limits): add characteristic predicate for zero objects (#13511)
  feat(order/filter/n_ary): Add lemma equating map₂ to map on the product (#13490)
  fix(analysis/locally_convex/balanced_hull_core): minimize import (#13450)
  feat(order/cover): define `wcovby` (#13424)
  ...
Sign up for free to subscribe to this conversation on GitHub. Already have an account? Sign in.
Reviewers

@dwarn dwarn Awaiting requested review from dwarn

Assignees
No one assigned
Labels
ready-to-merge All that is left is for bors to build and merge this PR. (Remember you need to say `bors r+`.)
Projects
None yet
Milestone
No milestone
Development

Successfully merging this pull request may close these issues.
4 participants
@kim-em @dwarn @jcommelin @bryangingechen