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(Algebra/Category/ModuleCat): the category of presheaves of modules is abelian #12721

Closed
wants to merge 39 commits into from
Closed

[Merged by Bors] - feat(Algebra/Category/ModuleCat): the category of presheaves of modules is abelian #12721

wants to merge 39 commits into from

Commits on Mar 28, 2024

  1. feat(CategoryTheory): triangulated subcategories

    @joelriou
    joelriou committed Mar 28, 2024
    Configuration menu
    Copy the full SHA
    2865b80 View commit details
    Browse the repository at this point in the history

  2. feat(CategoryTheory/Triangulated): homological functors

    @joelriou
    joelriou committed Mar 28, 2024
    Configuration menu
    Copy the full SHA
    58bd6d3 View commit details
    Browse the repository at this point in the history

  3. fixing Mathlib.lean

    @joelriou
    joelriou committed Mar 28, 2024
    Configuration menu
    Copy the full SHA
    0fa5280 View commit details
    Browse the repository at this point in the history

  4. coding style

    @joelriou
    joelriou committed Mar 28, 2024
    Configuration menu
    Copy the full SHA
    05af53c View commit details
    Browse the repository at this point in the history

Commits on Mar 29, 2024

  1. one more constructor

    @joelriou
    joelriou committed Mar 29, 2024
    Configuration menu
    Copy the full SHA
    6da2115 View commit details
    Browse the repository at this point in the history

  2. feat: the homological functor on the homotopy category of an abelian … 

    …category
    @joelriou
    joelriou committed Mar 29, 2024
    Configuration menu
    Copy the full SHA
    42656e4 View commit details
    Browse the repository at this point in the history

  3. cleaning up

    @joelriou
    joelriou committed Mar 29, 2024
    Configuration menu
    Copy the full SHA
    73051a1 View commit details
    Browse the repository at this point in the history

  4. added docstrings

    @joelriou
    joelriou committed Mar 29, 2024
    Configuration menu
    Copy the full SHA
    bd494bb View commit details
    Browse the repository at this point in the history

Commits on Mar 30, 2024

  1. Merge remote-tracking branch 'origin' into triangulated-subcategory

    @joelriou
    joelriou committed Mar 30, 2024
    Configuration menu
    Copy the full SHA
    7225e05 View commit details
    Browse the repository at this point in the history

  2. followed @TwoFX suggestions

    @joelriou
    joelriou committed Mar 30, 2024
    Configuration menu
    Copy the full SHA
    fa0c448 View commit details
    Browse the repository at this point in the history

  3. replaces sets by predicates

    @joelriou
    joelriou committed Mar 30, 2024
    Configuration menu
    Copy the full SHA
    7e48b5f View commit details
    Browse the repository at this point in the history

  4. fixed coding style

    @joelriou
    joelriou committed Mar 30, 2024
    Configuration menu
    Copy the full SHA
    dd4cd80 View commit details
    Browse the repository at this point in the history

  5. added isIso variants

    @joelriou
    joelriou committed Mar 30, 2024
    Configuration menu
    Copy the full SHA
    f05ab7b View commit details
    Browse the repository at this point in the history

  6. Merge remote-tracking branch 'origin/triangulated-subcategory' into h… 

    …omological-functor
    @joelriou
    joelriou committed Mar 30, 2024
    Configuration menu
    Copy the full SHA
    dbde1b9 View commit details
    Browse the repository at this point in the history

  7. fixed the build

    @joelriou
    joelriou committed Mar 30, 2024
    Configuration menu
    Copy the full SHA
    a07dd2f View commit details
    Browse the repository at this point in the history

  8. Merge remote-tracking branch 'origin/homological-functor' into homoto… 

    …py-category-homological-functor
    @joelriou
    joelriou committed Mar 30, 2024
    Configuration menu
    Copy the full SHA
    7f09d1e View commit details
    Browse the repository at this point in the history

Commits on Mar 31, 2024

  1. Merge remote-tracking branch 'origin' into homotopy-category-homologi… 

    …cal-functor
    @joelriou
    joelriou committed Mar 31, 2024
    Configuration menu
    Copy the full SHA
    280bb5f View commit details
    Browse the repository at this point in the history

Commits on Apr 12, 2024

  1. Merge remote-tracking branch 'origin' into triangulated-subcategory

    @joelriou
    joelriou committed Apr 12, 2024
    Configuration menu
    Copy the full SHA
    5de084d View commit details
    Browse the repository at this point in the history

Commits on Apr 18, 2024

  1. Merge remote-tracking branch 'origin' into triangulated-subcategory

    @joelriou
    joelriou committed Apr 18, 2024
    Configuration menu
    Copy the full SHA
    d5c8df7 View commit details
    Browse the repository at this point in the history

  2. fixing names

    @joelriou
    joelriou committed Apr 18, 2024
    Configuration menu
    Copy the full SHA
    8d93376 View commit details
    Browse the repository at this point in the history

  3. fixed def of isoClosure

    @joelriou
    joelriou committed Apr 18, 2024
    Configuration menu
    Copy the full SHA
    447e037 View commit details
    Browse the repository at this point in the history

  4. fixed names

    @joelriou
    joelriou committed Apr 18, 2024
    Configuration menu
    Copy the full SHA
    79edf14 View commit details
    Browse the repository at this point in the history

  5. Merge remote-tracking branch 'origin/triangulated-subcategory' into h… 

    …omological-functor
    @joelriou
    joelriou committed Apr 18, 2024
    Configuration menu
    Copy the full SHA
    4f5cd42 View commit details
    Browse the repository at this point in the history

  6. Merge remote-tracking branch 'origin/homological-functor' into homoto… 

    …py-category-homological-functor
    @joelriou
    joelriou committed Apr 18, 2024
    Configuration menu
    Copy the full SHA
    14e636f View commit details
    Browse the repository at this point in the history

Commits on Apr 30, 2024

  1. Merge remote-tracking branch 'origin' into homotopy-category-homologi… 

    …cal-functor
    @joelriou
    joelriou committed Apr 30, 2024
    Configuration menu
    Copy the full SHA
    73fd877 View commit details
    Browse the repository at this point in the history

  2. typo

    @joelriou
    joelriou committed Apr 30, 2024
    Configuration menu
    Copy the full SHA
    f355a73 View commit details
    Browse the repository at this point in the history

Commits on May 6, 2024

  1. feat(Algebra/Category/ModuleCat): the category of preheaves of module… 

    …s has colimits
    @joelriou
    joelriou committed May 6, 2024
    Configuration menu
    Copy the full SHA
    7c81f56 View commit details
    Browse the repository at this point in the history

  2. fixes

    @joelriou
    joelriou committed May 6, 2024
    Configuration menu
    Copy the full SHA
    d60cab1 View commit details
    Browse the repository at this point in the history

  3. one sorry left

    @joelriou
    joelriou committed May 6, 2024
    Configuration menu
    Copy the full SHA
    e7900a9 View commit details
    Browse the repository at this point in the history

  4. finished the proof

    @joelriou
    joelriou committed May 6, 2024
    Configuration menu
    Copy the full SHA
    e22a2e3 View commit details
    Browse the repository at this point in the history

Commits on May 7, 2024

  1. created file

    @joelriou
    joelriou committed May 7, 2024
    Configuration menu
    Copy the full SHA
    2e709ee View commit details
    Browse the repository at this point in the history

  2. Merge remote-tracking branch 'origin/homotopy-category-homological-fu… 

    …nctor' into modulecat-presheaf-abelian
    @joelriou
    joelriou committed May 7, 2024
    Configuration menu
    Copy the full SHA
    426e59f View commit details
    Browse the repository at this point in the history

  3. obtained abelian instance

    @joelriou
    joelriou committed May 7, 2024
    Configuration menu
    Copy the full SHA
    166238c View commit details
    Browse the repository at this point in the history

Commits on May 8, 2024

  1. Merge remote-tracking branch 'origin' into homotopy-category-homologi… 

    …cal-functor
    @joelriou
    joelriou committed May 8, 2024
    Configuration menu
    Copy the full SHA
    bbc50bf View commit details
    Browse the repository at this point in the history

Commits on May 9, 2024

  1. Merge remote-tracking branch 'origin' into homotopy-category-homologi… 

    …cal-functor
    @joelriou
    joelriou committed May 9, 2024
    Configuration menu
    Copy the full SHA
    118dc36 View commit details
    Browse the repository at this point in the history

  2. shortened names

    @joelriou
    joelriou committed May 9, 2024
    Configuration menu
    Copy the full SHA
    406d7bb View commit details
    Browse the repository at this point in the history

Commits on May 10, 2024

  1. Merge remote-tracking branch 'origin/homotopy-category-homological-fu… 

    …nctor' into modulecat-presheaf-abelian
    @joelriou
    joelriou committed May 10, 2024
    Configuration menu
    Copy the full SHA
    61e7d48 View commit details
    Browse the repository at this point in the history

Commits on May 13, 2024

  1. Merge remote-tracking branch 'origin' into modulecat-presheaf-abelian

    @joelriou
    joelriou committed May 13, 2024
    Configuration menu
    Copy the full SHA
    bfa64f7 View commit details
    Browse the repository at this point in the history

  2. fixing the build

    @joelriou
    joelriou committed May 13, 2024
    Configuration menu
    Copy the full SHA
    757e593 View commit details
    Browse the repository at this point in the history