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.

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

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

Closed
wants to merge 36 commits into from
Closed
Show file tree
Hide file tree
Changes from 35 commits
Commits
Show all changes
36 commits
Select commit Hold shift + click to select a range
078b3c7
initial draft of revisions/additions to the mates correspondence
emilyriehl Jun 14, 2024
18871c0
forgot to end the section
emilyriehl Jun 14, 2024
0ce7de1
Update Mathlib/CategoryTheory/Adjunction/Mates.lean
emilyriehl Jun 15, 2024
3a56b48
Update Mathlib/CategoryTheory/Adjunction/Mates.lean
emilyriehl Jun 15, 2024
14f64a7
Update Mathlib/CategoryTheory/Adjunction/Mates.lean
emilyriehl Jun 15, 2024
914dc7b
Update Mathlib/CategoryTheory/Adjunction/Mates.lean
emilyriehl Jun 15, 2024
aec07a0
Update Mathlib/CategoryTheory/Adjunction/Mates.lean
emilyriehl Jun 15, 2024
d6e7096
Update Mathlib/CategoryTheory/Adjunction/Mates.lean
emilyriehl Jun 15, 2024
57d2736
suggestions from the PR review
emilyriehl Jun 15, 2024
9544f73
fixed line overruns
emilyriehl Jun 16, 2024
a5078bc
fixed := misalignment
emilyriehl Jun 16, 2024
d332c18
attempt to fix the missing documentation strings lint error
emilyriehl Jun 17, 2024
9b2e628
redefined all of transferNatTransSelf as Conjugates
emilyriehl Jun 18, 2024
b847776
renamed terms in files that depend on mates
emilyriehl Jun 18, 2024
92291e9
cut material that has been renamed
emilyriehl Jun 18, 2024
4a7a8a5
cleaned up comments and started a final section
emilyriehl Jun 18, 2024
8d6078f
iterated mates are conjugates
emilyriehl Jun 18, 2024
2ab137b
iterated mates dual
emilyriehl Jun 18, 2024
6ed18ff
reproved expComparison_whiskerLeft
emilyriehl Jun 18, 2024
959da46
fixed proofs for closed functors
emilyriehl Jun 18, 2024
ef76cb3
fixed line overflows
emilyriehl Jun 18, 2024
5e6f6db
Update Mathlib/CategoryTheory/Closed/Functor.lean
emilyriehl Jun 18, 2024
565b337
non-terminal simp
emilyriehl Jun 18, 2024
20c0686
Update Mathlib/CategoryTheory/Closed/Functor.lean
emilyriehl Jun 18, 2024
8e00b56
Update Mathlib/CategoryTheory/Adjunction/Mates.lean
emilyriehl Jun 18, 2024
5b31648
Update Mathlib/CategoryTheory/Adjunction/Mates.lean
emilyriehl Jun 18, 2024
5f6e1ba
Update Mathlib/CategoryTheory/Adjunction/Mates.lean
emilyriehl Jun 18, 2024
5de6876
removed starting capitals
emilyriehl Jun 18, 2024
364057f
dual proofs
emilyriehl Jun 18, 2024
3a9d0f8
two more duals
emilyriehl Jun 19, 2024
f2ad310
conjugateIsoEquiv
emilyriehl Jun 20, 2024
961ed57
subdivided a section and removed unneeded variables
emilyriehl Jun 20, 2024
50f588b
Update Mathlib/CategoryTheory/Adjunction/Mates.lean
emilyriehl Jul 5, 2024
943fee5
consolidation into fewer lines
emilyriehl Jul 5, 2024
80b90d4
added depricated aliases
emilyriehl Jul 9, 2024
a20fcb5
fixed formatting of deprecate tags
emilyriehl Jul 10, 2024
File filter

Filter by extension

Filter by extension

Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
Loading
Loading