Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Jump to bottom

[Merged by Bors] - feat(algebraic_topology): introduce the simplex category #6173

Closed
wants to merge 69 commits into from
Closed

[Merged by Bors] - feat(algebraic_topology): introduce the simplex category #6173

wants to merge 69 commits into from

Commits on Feb 8, 2021

  1. feature(fin): cast_succ_mk and succ_mk simp lemmas

    @semorrison
    semorrison committed Feb 8, 2021
    Configuration menu
    Copy the full SHA
    e982fb9 View commit details
    Browse the repository at this point in the history

  2. more cast lemmas, and fix some doc-strings

    @semorrison
    semorrison committed Feb 8, 2021
    Configuration menu
    Copy the full SHA
    fb2fa5b View commit details
    Browse the repository at this point in the history

  3. broken

    @semorrison
    semorrison committed Feb 8, 2021
    Configuration menu
    Copy the full SHA
    3036326 View commit details
    Browse the repository at this point in the history

  4. Merge branch 'fin_cast_succ_mk' into pred_above

    @semorrison
    semorrison committed Feb 8, 2021
    Configuration menu
    Copy the full SHA
    d3b93fd View commit details
    Browse the repository at this point in the history

  5. hrmm... pred_above is being used differently than I expected

    @semorrison
    semorrison committed Feb 8, 2021
    Configuration menu
    Copy the full SHA
    f83e244 View commit details
    Browse the repository at this point in the history

  6. chore(data/fin): reorder file to group declarations

    @pechersky
    pechersky committed Feb 8, 2021
    Configuration menu
    Copy the full SHA
    0422730 View commit details
    Browse the repository at this point in the history

  7. fix and make proof more robust

    @fpvandoorn
    fpvandoorn committed Feb 8, 2021
    Configuration menu
    Copy the full SHA
    5cd8588 View commit details
    Browse the repository at this point in the history

  8. section titles

    @pechersky
    pechersky committed Feb 8, 2021
    Configuration menu
    Copy the full SHA
    e5372d9 View commit details
    Browse the repository at this point in the history

  9. fix missing simp call

    @pechersky
    pechersky committed Feb 8, 2021
    Configuration menu
    Copy the full SHA
    2b03eb3 View commit details
    Browse the repository at this point in the history

  10. fix rw

    @pechersky
    pechersky committed Feb 8, 2021
    Configuration menu
    Copy the full SHA
    72d0f8c View commit details
    Browse the repository at this point in the history

Commits on Feb 9, 2021

  1. still broken

    @semorrison
    semorrison committed Feb 9, 2021
    Configuration menu
    Copy the full SHA
    8dd5420 View commit details
    Browse the repository at this point in the history

  2. maybe good

    @semorrison
    semorrison committed Feb 9, 2021
    Configuration menu
    Copy the full SHA
    2a54476 View commit details
    Browse the repository at this point in the history

  3. Merge remote-tracking branch 'origin/master' into pred_above

    @semorrison
    semorrison committed Feb 9, 2021
    Configuration menu
    Copy the full SHA
    0641792 View commit details
    Browse the repository at this point in the history

  4. restoring insert_nth

    @semorrison
    semorrison committed Feb 9, 2021
    Configuration menu
    Copy the full SHA
    ecc4d70 View commit details
    Browse the repository at this point in the history

  5. doc-strings

    @semorrison
    semorrison committed Feb 9, 2021
    Configuration menu
    Copy the full SHA
    6ada915 View commit details
    Browse the repository at this point in the history

  6. fix

    @semorrison
    semorrison committed Feb 9, 2021
    Configuration menu
    Copy the full SHA
    2814b97 View commit details
    Browse the repository at this point in the history

  7. merge

    @semorrison
    semorrison committed Feb 9, 2021
    Configuration menu
    Copy the full SHA
    cb8604c View commit details
    Browse the repository at this point in the history

  8. cleanup

    @semorrison
    semorrison committed Feb 9, 2021
    Configuration menu
    Copy the full SHA
    b1b36c9 View commit details
    Browse the repository at this point in the history

  9. update docs

    @semorrison
    semorrison committed Feb 9, 2021
    Configuration menu
    Copy the full SHA
    96cd0d3 View commit details
    Browse the repository at this point in the history

  10. reorg

    @semorrison
    semorrison committed Feb 9, 2021
    Configuration menu
    Copy the full SHA
    aa798e6 View commit details
    Browse the repository at this point in the history

Commits on Feb 10, 2021

  1. purge pred_above' and add cast_pred

    @pechersky
    pechersky committed Feb 10, 2021
    Configuration menu
    Copy the full SHA
    0119f6a View commit details
    Browse the repository at this point in the history

  2. Merge remote-tracking branch 'refs/remotes/origin/pred_above' into pr… 

    …ed_above
    @pechersky
    pechersky committed Feb 10, 2021
    Configuration menu
    Copy the full SHA
    d22811e View commit details
    Browse the repository at this point in the history

  3. repurge pred_above'

    @pechersky
    pechersky committed Feb 10, 2021
    Configuration menu
    Copy the full SHA
    fb9eb33 View commit details
    Browse the repository at this point in the history

  4. merge

    @semorrison
    semorrison committed Feb 10, 2021
    Configuration menu
    Copy the full SHA
    d0df714 View commit details
    Browse the repository at this point in the history

  5. Merge branch 'fin_cast_succ_mk' into pred_above

    @semorrison
    semorrison committed Feb 10, 2021
    Configuration menu
    Copy the full SHA
    d74d6e5 View commit details
    Browse the repository at this point in the history

  6. Rob's fix for linarith error

    @semorrison
    semorrison committed Feb 10, 2021
    Configuration menu
    Copy the full SHA
    cd33ed8 View commit details
    Browse the repository at this point in the history

  7. Merge branch 'pred_above' of github.com:leanprover-community/mathlib … 

    …into pred_above
    @semorrison
    semorrison committed Feb 10, 2021
    Configuration menu
    Copy the full SHA
    83cca03 View commit details
    Browse the repository at this point in the history

Commits on Feb 11, 2021

  1. fix error

    @pechersky
    pechersky committed Feb 11, 2021
    Configuration menu
    Copy the full SHA
    32c61c3 View commit details
    Browse the repository at this point in the history

  2. remove evil second instance of has_zero

    @semorrison
    semorrison committed Feb 11, 2021
    Configuration menu
    Copy the full SHA
    79276b0 View commit details
    Browse the repository at this point in the history

  3. feat(data/fin): pred_above_monotone

    @semorrison
    semorrison committed Feb 11, 2021
    Configuration menu
    Copy the full SHA
    af09a1e View commit details
    Browse the repository at this point in the history

  4. feat(simplex_category): introduce the simplex category

    @semorrison
    semorrison committed Feb 11, 2021
    Configuration menu
    Copy the full SHA
    5aeb62b View commit details
    Browse the repository at this point in the history

  5. feat(simplex_category): introduce the simplex category

    @semorrison
    semorrison committed Feb 11, 2021
    Configuration menu
    Copy the full SHA
    5a6b795 View commit details
    Browse the repository at this point in the history

  6. restore simp lemma

    @semorrison
    semorrison committed Feb 11, 2021
    Configuration menu
    Copy the full SHA
    f38cb6f View commit details
    Browse the repository at this point in the history

  7. fixes

    @semorrison
    semorrison committed Feb 11, 2021
    Configuration menu
    Copy the full SHA
    56aad54 View commit details
    Browse the repository at this point in the history

  8. linting

    @semorrison
    semorrison committed Feb 11, 2021
    Configuration menu
    Copy the full SHA
    41f765a View commit details
    Browse the repository at this point in the history

  9. Merge branch 'succ_above_monotone' into simplex_category

    @semorrison
    semorrison committed Feb 11, 2021
    Configuration menu
    Copy the full SHA
    f601768 View commit details
    Browse the repository at this point in the history

  10. cast_pred simp lemmas

    @pechersky
    pechersky committed Feb 11, 2021
    Configuration menu
    Copy the full SHA
    8c923b6 View commit details
    Browse the repository at this point in the history

  11. cast_pred mention in module docstring

    @pechersky
    pechersky committed Feb 11, 2021
    Configuration menu
    Copy the full SHA
    b11d13d View commit details
    Browse the repository at this point in the history

  12. Merge remote-tracking branch 'origin/pred_above' into succ_above_mono… 

    …tone
    @pechersky
    pechersky committed Feb 11, 2021
    Configuration menu
    Copy the full SHA
    3b047a3 View commit details
    Browse the repository at this point in the history

  13. cast_pred_monotone

    @pechersky
    pechersky committed Feb 11, 2021
    Configuration menu
    Copy the full SHA
    c7973d0 View commit details
    Browse the repository at this point in the history

  14. pred_above_left_monotone

    @pechersky
    pechersky committed Feb 11, 2021
    Configuration menu
    Copy the full SHA
    a698bb9 View commit details
    Browse the repository at this point in the history

  15. Update src/data/fin.lean 

    Co-authored-by: Yakov Pechersky <pechersky@users.noreply.github.com>
    @semorrison @pechersky
    semorrison and pechersky committed Feb 11, 2021
    Configuration menu
    Copy the full SHA
    6a00a0b View commit details
    Browse the repository at this point in the history

  16. Merge remote-tracking branch 'origin/pred_above' into succ_above_mono… 

    …tone
    @semorrison
    semorrison committed Feb 11, 2021
    Configuration menu
    Copy the full SHA
    9684d1c View commit details
    Browse the repository at this point in the history

  17. Merge branch 'succ_above_monotone' of github.com:leanprover-community… 

    …/mathlib into succ_above_monotone
    @semorrison
    semorrison committed Feb 11, 2021
    Configuration menu
    Copy the full SHA
    20c5b8e View commit details
    Browse the repository at this point in the history

  18. Merge remote-tracking branch 'origin/master' into succ_above_monotone

    @semorrison
    semorrison committed Feb 11, 2021
    Configuration menu
    Copy the full SHA
    2b3a816 View commit details
    Browse the repository at this point in the history

  19. Merge branch 'succ_above_monotone' into simplex_category

    @semorrison
    semorrison committed Feb 11, 2021
    Configuration menu
    Copy the full SHA
    8f31531 View commit details
    Browse the repository at this point in the history

Commits on Feb 12, 2021

  1. use category_theory.skeletal

    @semorrison
    semorrison committed Feb 12, 2021
    Configuration menu
    Copy the full SHA
    44f43a7 View commit details
    Browse the repository at this point in the history

  2. fix

    @semorrison
    semorrison committed Feb 12, 2021
    Configuration menu
    Copy the full SHA
    2be9ebf View commit details
    Browse the repository at this point in the history

  3. fill in sorry

    @semorrison
    semorrison committed Feb 12, 2021
    Configuration menu
    Copy the full SHA
    19e67af View commit details
    Browse the repository at this point in the history

  4. linting

    @semorrison
    semorrison committed Feb 12, 2021
    Configuration menu
    Copy the full SHA
    f4f9e6d View commit details
    Browse the repository at this point in the history

Commits on Feb 13, 2021

  1. merge

    @semorrison
    semorrison committed Feb 13, 2021
    Configuration menu
    Copy the full SHA
    22c7c5f View commit details
    Browse the repository at this point in the history

  2. Merge branch 'pred_above' into succ_above_monotone

    @semorrison
    semorrison committed Feb 13, 2021
    Configuration menu
    Copy the full SHA
    13d2e7e View commit details
    Browse the repository at this point in the history

  3. Merge branch 'succ_above_monotone' into simplex_category

    @semorrison
    semorrison committed Feb 13, 2021
    Configuration menu
    Copy the full SHA
    93760b5 View commit details
    Browse the repository at this point in the history

Commits on Feb 17, 2021

  1. merge

    @semorrison
    semorrison committed Feb 17, 2021
    Configuration menu
    Copy the full SHA
    71a1357 View commit details
    Browse the repository at this point in the history

  2. Merge branch 'succ_above_monotone' into simplex_category

    @semorrison
    semorrison committed Feb 17, 2021
    Configuration menu
    Copy the full SHA
    418a6dc View commit details
    Browse the repository at this point in the history

  3. move to algebraic_topology/ per jcommelin's suggestion

    @semorrison
    semorrison committed Feb 17, 2021
    Configuration menu
    Copy the full SHA
    16a06fa View commit details
    Browse the repository at this point in the history

  4. remove unnecessary instance name

    @semorrison
    semorrison committed Feb 17, 2021
    Configuration menu
    Copy the full SHA
    9aa6253 View commit details
    Browse the repository at this point in the history

  5. oops, bad merge

    @semorrison
    semorrison committed Feb 17, 2021
    Configuration menu
    Copy the full SHA
    f3c89bf View commit details
    Browse the repository at this point in the history

  6. Merge branch 'succ_above_monotone' into simplex_category

    @semorrison
    semorrison committed Feb 17, 2021
    Configuration menu
    Copy the full SHA
    be7a36c View commit details
    Browse the repository at this point in the history

Commits on Feb 18, 2021

  1. cleanup

    @semorrison
    semorrison committed Feb 18, 2021
    Configuration menu
    Copy the full SHA
    80514da View commit details
    Browse the repository at this point in the history

  2. Merge remote-tracking branch 'origin/master' into simplex_category

    @semorrison
    semorrison committed Feb 18, 2021
    Configuration menu
    Copy the full SHA
    8d5d3f6 View commit details
    Browse the repository at this point in the history

Commits on Feb 23, 2021

  1. Merge remote-tracking branch 'origin/master' into simplex_category

    @semorrison
    semorrison committed Feb 23, 2021
    Configuration menu
    Copy the full SHA
    5c1eac8 View commit details
    Browse the repository at this point in the history

  2. fixes

    @semorrison
    semorrison committed Feb 23, 2021
    Configuration menu
    Copy the full SHA
    f260687 View commit details
    Browse the repository at this point in the history

Commits on Feb 24, 2021

  1. replace some non-terminal simps with suffices

    @jcommelin
    jcommelin committed Feb 24, 2021
    Configuration menu
    Copy the full SHA
    e0f4ea4 View commit details
    Browse the repository at this point in the history

Commits on Feb 25, 2021

  1. finish removing non-terminal simps?

    @semorrison
    semorrison committed Feb 25, 2021
    Configuration menu
    Copy the full SHA
    d374b96 View commit details
    Browse the repository at this point in the history

  2. Merge remote-tracking branch 'origin/master' into simplex_category

    @semorrison
    semorrison committed Feb 25, 2021
    Configuration menu
    Copy the full SHA
    115cf2b View commit details
    Browse the repository at this point in the history

  3. Apply b-mehta's suggestions from code review 

    Co-authored-by: Bhavik Mehta <bhavikmehta8@gmail.com>
    @semorrison @b-mehta
    semorrison and b-mehta committed Feb 25, 2021
    Configuration menu
    Copy the full SHA
    aaef009 View commit details
    Browse the repository at this point in the history

  4. lint

    @semorrison
    semorrison committed Feb 25, 2021
    Configuration menu
    Copy the full SHA
    314f511 View commit details
    Browse the repository at this point in the history

Commits on Feb 26, 2021

  1. Apply suggestions from code review

    @jcommelin
    jcommelin committed Feb 26, 2021
    Configuration menu
    Copy the full SHA
    81a92a3 View commit details
    Browse the repository at this point in the history