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: port CategoryTheory.Localization.Construction #2917

Closed
wants to merge 33 commits into from
Closed

[Merged by Bors] - feat: port CategoryTheory.Localization.Construction #2917

wants to merge 33 commits into from

Commits on Mar 14, 2023

  1. feat: port CategoryTheory.Limits.Shapes.KernelPair

    @joelriou
    joelriou committed Mar 14, 2023
    Configuration menu
    Copy the full SHA
    1fa830f View commit details
    Browse the repository at this point in the history

  2. Initial file copy from mathport

    @joelriou
    joelriou committed Mar 14, 2023
    Configuration menu
    Copy the full SHA
    e1dd851 View commit details
    Browse the repository at this point in the history

  3. automated fixes 

    Mathbin -> Mathlib
fix certain import statements
move "by" to end of line
add import to Mathlib.lean
    @joelriou
    joelriou committed Mar 14, 2023
    Configuration menu
    Copy the full SHA
    c158e24 View commit details
    Browse the repository at this point in the history

  4. it compiles

    @joelriou
    joelriou committed Mar 14, 2023
    Configuration menu
    Copy the full SHA
    10e1265 View commit details
    Browse the repository at this point in the history

  5. added PushoutCocone.IsColimit.desc

    @joelriou
    joelriou committed Mar 14, 2023
    Configuration menu
    Copy the full SHA
    6bc339c View commit details
    Browse the repository at this point in the history

  6. feat: port CategoryTheory.Limits.Shapes.Diagonal

    @joelriou
    joelriou committed Mar 14, 2023
    Configuration menu
    Copy the full SHA
    787dd56 View commit details
    Browse the repository at this point in the history

  7. Initial file copy from mathport

    @joelriou
    joelriou committed Mar 14, 2023
    Configuration menu
    Copy the full SHA
    b41aca4 View commit details
    Browse the repository at this point in the history

  8. automated fixes 

    Mathbin -> Mathlib
fix certain import statements
move "by" to end of line
add import to Mathlib.lean
    @joelriou
    joelriou committed Mar 14, 2023
    Configuration menu
    Copy the full SHA
    d827c86 View commit details
    Browse the repository at this point in the history

  9. Merge remote-tracking branch 'origin/port/CategoryTheory.Limits.Shape… 

    …s.KernelPair' into port/CategoryTheory.Limits.Shapes.Diagonal
    @joelriou
    joelriou committed Mar 14, 2023
    Configuration menu
    Copy the full SHA
    c7388c2 View commit details
    Browse the repository at this point in the history

  10. started working on this file

    @joelriou
    joelriou committed Mar 14, 2023
    Configuration menu
    Copy the full SHA
    ac7f3fc View commit details
    Browse the repository at this point in the history

  11. it should compile

    @joelriou
    joelriou committed Mar 14, 2023
    Configuration menu
    Copy the full SHA
    0acb2e6 View commit details
    Browse the repository at this point in the history

Commits on Mar 15, 2023

  1. feat: port CategoryTheory.MorphismProperty

    @joelriou
    joelriou committed Mar 15, 2023
    Configuration menu
    Copy the full SHA
    259bcf8 View commit details
    Browse the repository at this point in the history

  2. Initial file copy from mathport

    @joelriou
    joelriou committed Mar 15, 2023
    Configuration menu
    Copy the full SHA
    4dbc620 View commit details
    Browse the repository at this point in the history

  3. automated fixes 

    Mathbin -> Mathlib
fix certain import statements
move "by" to end of line
add import to Mathlib.lean
    @joelriou
    joelriou committed Mar 15, 2023
    Configuration menu
    Copy the full SHA
    f7010f9 View commit details
    Browse the repository at this point in the history

  4. added set_option maxHeartbeats 400000

    @joelriou
    joelriou committed Mar 15, 2023
    Configuration menu
    Copy the full SHA
    f2cb46d View commit details
    Browse the repository at this point in the history

  5. Merge remote-tracking branch 'origin/port/CategoryTheory.Limits.Shape… 

    …s.Diagonal' into port/CategoryTheory.MorphismProperty
    @joelriou
    joelriou committed Mar 15, 2023
    Configuration menu
    Copy the full SHA
    eac970e View commit details
    Browse the repository at this point in the history

  6. added set_option maxHeartbeats 400000 in

    @joelriou
    joelriou committed Mar 15, 2023
    Configuration menu
    Copy the full SHA
    82a9980 View commit details
    Browse the repository at this point in the history

  7. Merge remote-tracking branch 'origin/port/CategoryTheory.Limits.Shape… 

    …s.Diagonal' into port/CategoryTheory.MorphismProperty
    @joelriou
    joelriou committed Mar 15, 2023
    Configuration menu
    Copy the full SHA
    411ddc5 View commit details
    Browse the repository at this point in the history

  8. started working on this file

    @joelriou
    joelriou committed Mar 15, 2023
    Configuration menu
    Copy the full SHA
    bdb0072 View commit details
    Browse the repository at this point in the history

  9. removed last sorry

    @joelriou
    joelriou committed Mar 15, 2023
    Configuration menu
    Copy the full SHA
    0a60829 View commit details
    Browse the repository at this point in the history

  10. feat: port CategoryTheory.Localization.Construction

    @joelriou
    joelriou committed Mar 15, 2023
    Configuration menu
    Copy the full SHA
    94b9625 View commit details
    Browse the repository at this point in the history

  11. Initial file copy from mathport

    @joelriou
    joelriou committed Mar 15, 2023
    Configuration menu
    Copy the full SHA
    ccc4933 View commit details
    Browse the repository at this point in the history

  12. automated fixes 

    Mathbin -> Mathlib
fix certain import statements
move "by" to end of line
add import to Mathlib.lean
    @joelriou
    joelriou committed Mar 15, 2023
    Configuration menu
    Copy the full SHA
    f8a440e View commit details
    Browse the repository at this point in the history

  13. Merge remote-tracking branch 'origin/port/CategoryTheory.MorphismProp… 

    …erty' into port/CategoryTheory.Localization.Construction
    @joelriou
    joelriou committed Mar 15, 2023
    Configuration menu
    Copy the full SHA
    e6b6420 View commit details
    Browse the repository at this point in the history

  14. it compiles

    @joelriou
    joelriou committed Mar 15, 2023
    Configuration menu
    Copy the full SHA
    131bdb2 View commit details
    Browse the repository at this point in the history

  15. shortened a proof

    @joelriou
    joelriou committed Mar 15, 2023
    Configuration menu
    Copy the full SHA
    58fb61e View commit details
    Browse the repository at this point in the history

Commits on Mar 22, 2023

  1. Merge remote-tracking branch 'origin' into port/CategoryTheory.Locali… 

    …zation.Construction
    @joelriou
    joelriou committed Mar 22, 2023
    Configuration menu
    Copy the full SHA
    4d93db8 View commit details
    Browse the repository at this point in the history

Commits on Mar 24, 2023

  1. Merge branch 'master' into port/CategoryTheory.Localization.Construction

    @Parcly-Taxel
    Parcly-Taxel committed Mar 24, 2023
    Configuration menu
    Copy the full SHA
    f58926f View commit details
    Browse the repository at this point in the history

  2. Merge branch 'master' into port/CategoryTheory.Localization.Construction

    @Parcly-Taxel
    Parcly-Taxel committed Mar 24, 2023
    Configuration menu
    Copy the full SHA
    7a39495 View commit details
    Browse the repository at this point in the history

  3. oops

    @Parcly-Taxel
    Parcly-Taxel committed Mar 24, 2023
    Configuration menu
    Copy the full SHA
    6c1a788 View commit details
    Browse the repository at this point in the history

  4. Restore extra definitions

    @Parcly-Taxel
    Parcly-Taxel committed Mar 24, 2023
    Configuration menu
    Copy the full SHA
    db5ae50 View commit details
    Browse the repository at this point in the history

  5. porting note

    @ChrisHughes24
    ChrisHughes24 committed Mar 24, 2023
    Configuration menu
    Copy the full SHA
    de0c515 View commit details
    Browse the repository at this point in the history

  6. indentation

    @ChrisHughes24
    ChrisHughes24 committed Mar 24, 2023
    Configuration menu
    Copy the full SHA
    01bbd22 View commit details
    Browse the repository at this point in the history