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 (Category Theory): redefine and extend mates #13840

Closed
wants to merge 36 commits into from
Closed

[Merged by Bors] - feat (Category Theory): redefine and extend mates #13840

wants to merge 36 commits into from

Commits on Jun 14, 2024

  1. initial draft of revisions/additions to the mates correspondence

    @emilyriehl
    emilyriehl committed Jun 14, 2024
    Configuration menu
    Copy the full SHA
    078b3c7 View commit details
    Browse the repository at this point in the history

  2. forgot to end the section

    @emilyriehl
    emilyriehl committed Jun 14, 2024
    Configuration menu
    Copy the full SHA
    18871c0 View commit details
    Browse the repository at this point in the history

Commits on Jun 15, 2024

  1. Update Mathlib/CategoryTheory/Adjunction/Mates.lean 

    Co-authored-by: github-actions[bot] <41898282+github-actions[bot]@users.noreply.github.com>
    @emilyriehl @github-actions
    emilyriehl and github-actions[bot] authored Jun 15, 2024
    Configuration menu
    Copy the full SHA
    0ce7de1 View commit details
    Browse the repository at this point in the history

  2. Update Mathlib/CategoryTheory/Adjunction/Mates.lean 

    Co-authored-by: Bhavik Mehta <[email protected]>
    @emilyriehl @b-mehta
    emilyriehl and b-mehta authored Jun 15, 2024
    Configuration menu
    Copy the full SHA
    3a56b48 View commit details
    Browse the repository at this point in the history

  3. Update Mathlib/CategoryTheory/Adjunction/Mates.lean 

    Co-authored-by: github-actions[bot] <41898282+github-actions[bot]@users.noreply.github.com>
    @emilyriehl @github-actions
    emilyriehl and github-actions[bot] authored Jun 15, 2024
    Configuration menu
    Copy the full SHA
    14f64a7 View commit details
    Browse the repository at this point in the history

  4. Update Mathlib/CategoryTheory/Adjunction/Mates.lean 

    Co-authored-by: github-actions[bot] <41898282+github-actions[bot]@users.noreply.github.com>
    @emilyriehl @github-actions
    emilyriehl and github-actions[bot] authored Jun 15, 2024
    Configuration menu
    Copy the full SHA
    914dc7b View commit details
    Browse the repository at this point in the history

  5. Update Mathlib/CategoryTheory/Adjunction/Mates.lean 

    Co-authored-by: github-actions[bot] <41898282+github-actions[bot]@users.noreply.github.com>
    @emilyriehl @github-actions
    emilyriehl and github-actions[bot] authored Jun 15, 2024
    Configuration menu
    Copy the full SHA
    aec07a0 View commit details
    Browse the repository at this point in the history

  6. Update Mathlib/CategoryTheory/Adjunction/Mates.lean 

    Co-authored-by: github-actions[bot] <41898282+github-actions[bot]@users.noreply.github.com>
    @emilyriehl @github-actions
    emilyriehl and github-actions[bot] authored Jun 15, 2024
    Configuration menu
    Copy the full SHA
    d6e7096 View commit details
    Browse the repository at this point in the history

  7. suggestions from the PR review

    @emilyriehl
    emilyriehl committed Jun 15, 2024
    Configuration menu
    Copy the full SHA
    57d2736 View commit details
    Browse the repository at this point in the history

Commits on Jun 16, 2024

  1. fixed line overruns

    @emilyriehl
    emilyriehl committed Jun 16, 2024
    Configuration menu
    Copy the full SHA
    9544f73 View commit details
    Browse the repository at this point in the history

  2. fixed := misalignment

    @emilyriehl
    emilyriehl committed Jun 16, 2024
    Configuration menu
    Copy the full SHA
    a5078bc View commit details
    Browse the repository at this point in the history

Commits on Jun 17, 2024

  1. attempt to fix the missing documentation strings lint error

    @emilyriehl
    emilyriehl committed Jun 17, 2024
    Configuration menu
    Copy the full SHA
    d332c18 View commit details
    Browse the repository at this point in the history

Commits on Jun 18, 2024

  1. redefined all of transferNatTransSelf as Conjugates

    @emilyriehl
    emilyriehl committed Jun 18, 2024
    Configuration menu
    Copy the full SHA
    9b2e628 View commit details
    Browse the repository at this point in the history

  2. renamed terms in files that depend on mates

    @emilyriehl
    emilyriehl committed Jun 18, 2024
    Configuration menu
    Copy the full SHA
    b847776 View commit details
    Browse the repository at this point in the history

  3. cut material that has been renamed

    @emilyriehl
    emilyriehl committed Jun 18, 2024
    Configuration menu
    Copy the full SHA
    92291e9 View commit details
    Browse the repository at this point in the history

  4. cleaned up comments and started a final section

    @emilyriehl
    emilyriehl committed Jun 18, 2024
    Configuration menu
    Copy the full SHA
    4a7a8a5 View commit details
    Browse the repository at this point in the history

  5. iterated mates are conjugates

    @emilyriehl
    emilyriehl committed Jun 18, 2024
    Configuration menu
    Copy the full SHA
    8d6078f View commit details
    Browse the repository at this point in the history

  6. iterated mates dual

    @emilyriehl
    emilyriehl committed Jun 18, 2024
    Configuration menu
    Copy the full SHA
    2ab137b View commit details
    Browse the repository at this point in the history

  7. reproved expComparison_whiskerLeft

    @emilyriehl
    emilyriehl committed Jun 18, 2024
    Configuration menu
    Copy the full SHA
    6ed18ff View commit details
    Browse the repository at this point in the history

  8. fixed proofs for closed functors

    @emilyriehl
    emilyriehl committed Jun 18, 2024
    Configuration menu
    Copy the full SHA
    959da46 View commit details
    Browse the repository at this point in the history

  9. fixed line overflows

    @emilyriehl
    emilyriehl committed Jun 18, 2024
    Configuration menu
    Copy the full SHA
    ef76cb3 View commit details
    Browse the repository at this point in the history

  10. Update Mathlib/CategoryTheory/Closed/Functor.lean 

    Co-authored-by: github-actions[bot] <41898282+github-actions[bot]@users.noreply.github.com>
    @emilyriehl @github-actions
    emilyriehl and github-actions[bot] authored Jun 18, 2024
    Configuration menu
    Copy the full SHA
    5e6f6db View commit details
    Browse the repository at this point in the history

  11. non-terminal simp

    @emilyriehl
    emilyriehl committed Jun 18, 2024
    Configuration menu
    Copy the full SHA
    565b337 View commit details
    Browse the repository at this point in the history

  12. Update Mathlib/CategoryTheory/Closed/Functor.lean 

    Co-authored-by: Joël Riou <[email protected]>
    @emilyriehl @joelriou
    emilyriehl and joelriou authored Jun 18, 2024
    Configuration menu
    Copy the full SHA
    20c0686 View commit details
    Browse the repository at this point in the history

  13. Update Mathlib/CategoryTheory/Adjunction/Mates.lean 

    Co-authored-by: Joël Riou <[email protected]>
    @emilyriehl @joelriou
    emilyriehl and joelriou authored Jun 18, 2024
    Configuration menu
    Copy the full SHA
    8e00b56 View commit details
    Browse the repository at this point in the history

  14. Update Mathlib/CategoryTheory/Adjunction/Mates.lean 

    Co-authored-by: Joël Riou <[email protected]>
    @emilyriehl @joelriou
    emilyriehl and joelriou authored Jun 18, 2024
    Configuration menu
    Copy the full SHA
    5b31648 View commit details
    Browse the repository at this point in the history

  15. Update Mathlib/CategoryTheory/Adjunction/Mates.lean 

    Co-authored-by: github-actions[bot] <41898282+github-actions[bot]@users.noreply.github.com>
    @emilyriehl @github-actions
    emilyriehl and github-actions[bot] authored Jun 18, 2024
    Configuration menu
    Copy the full SHA
    5f6e1ba View commit details
    Browse the repository at this point in the history

  16. removed starting capitals

    @emilyriehl
    emilyriehl committed Jun 18, 2024
    Configuration menu
    Copy the full SHA
    5de6876 View commit details
    Browse the repository at this point in the history

  17. dual proofs

    @emilyriehl
    emilyriehl committed Jun 18, 2024
    Configuration menu
    Copy the full SHA
    364057f View commit details
    Browse the repository at this point in the history

Commits on Jun 19, 2024

  1. two more duals

    @emilyriehl
    emilyriehl committed Jun 19, 2024
    Configuration menu
    Copy the full SHA
    3a9d0f8 View commit details
    Browse the repository at this point in the history

Commits on Jun 20, 2024

  1. conjugateIsoEquiv

    @emilyriehl
    emilyriehl committed Jun 20, 2024
    Configuration menu
    Copy the full SHA
    f2ad310 View commit details
    Browse the repository at this point in the history

  2. subdivided a section and removed unneeded variables

    @emilyriehl
    emilyriehl committed Jun 20, 2024
    Configuration menu
    Copy the full SHA
    961ed57 View commit details
    Browse the repository at this point in the history

Commits on Jul 5, 2024

  1. Update Mathlib/CategoryTheory/Adjunction/Mates.lean 

    Co-authored-by: Dagur Tómas Ásgeirsson <[email protected]>
    @emilyriehl @dagurtomas
    emilyriehl and dagurtomas authored Jul 5, 2024
    Configuration menu
    Copy the full SHA
    50f588b View commit details
    Browse the repository at this point in the history

  2. consolidation into fewer lines

    @emilyriehl
    emilyriehl committed Jul 5, 2024
    Configuration menu
    Copy the full SHA
    943fee5 View commit details
    Browse the repository at this point in the history

Commits on Jul 9, 2024

  1. added depricated aliases

    @emilyriehl
    emilyriehl committed Jul 9, 2024
    Configuration menu
    Copy the full SHA
    80b90d4 View commit details
    Browse the repository at this point in the history

Commits on Jul 10, 2024

  1. fixed formatting of deprecate tags

    @emilyriehl
    emilyriehl committed Jul 10, 2024
    Configuration menu
    Copy the full SHA
    a20fcb5 View commit details
    Browse the repository at this point in the history