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

feat: the (contravariant) long exact sequence of Ext #15092

Open
wants to merge 169 commits into
base: master
Choose a base branch
from
Open

feat: the (contravariant) long exact sequence of Ext #15092

wants to merge 169 commits into from
+457 −7

Commits on Jun 8, 2024

  1. feat: small types of morphisms in the localized category

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

  2. added compatibilities

    @joelriou
    joelriou committed Jun 8, 2024
    Configuration menu
    Copy the full SHA
    9d5cdc1 View commit details
    Browse the repository at this point in the history

  3. fixed imports

    @joelriou
    joelriou committed Jun 8, 2024
    Configuration menu
    Copy the full SHA
    08077d0 View commit details
    Browse the repository at this point in the history

Commits on Jun 9, 2024

  1. Merge remote-tracking branch 'origin' into has-small-localized-hom

    @joelriou
    joelriou committed Jun 9, 2024
    Configuration menu
    Copy the full SHA
    75e6713 View commit details
    Browse the repository at this point in the history

  2. added note

    @joelriou
    joelriou committed Jun 9, 2024
    Configuration menu
    Copy the full SHA
    88d42d8 View commit details
    Browse the repository at this point in the history

  3. feat: the mapping cone of a monomorphism, up to a quasi-isomorphism

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

  4. updated Mathlib.lean

    @joelriou
    joelriou committed Jun 9, 2024
    Configuration menu
    Copy the full SHA
    467fa14 View commit details
    Browse the repository at this point in the history

  5. wip

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

  6. Update Mathlib/Algebra/Homology/Refinements.lean 

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

  7. removed a sorry

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

Commits on Jun 10, 2024

  1. removed a sorry

    @joelriou
    joelriou committed Jun 10, 2024
    Configuration menu
    Copy the full SHA
    3b5de64 View commit details
    Browse the repository at this point in the history

  2. removed sorries

    @joelriou
    joelriou committed Jun 10, 2024
    Configuration menu
    Copy the full SHA
    89fe3b0 View commit details
    Browse the repository at this point in the history

  3. added docstring

    @joelriou
    joelriou committed Jun 10, 2024
    Configuration menu
    Copy the full SHA
    a0d590b View commit details
    Browse the repository at this point in the history

  4. fixed def/lemma

    @joelriou
    joelriou committed Jun 10, 2024
    Configuration menu
    Copy the full SHA
    872879a View commit details
    Browse the repository at this point in the history

  5. s/refine'/refine/

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

Commits on Jun 11, 2024

  1. feat: the distinguished triangle attached to a short exact sequence o… 

    …f complexes
    @joelriou
    joelriou committed Jun 11, 2024
    Configuration menu
    Copy the full SHA
    683b743 View commit details
    Browse the repository at this point in the history

  2. Merge remote-tracking branch 'origin' into dist-triangle-ses2

    @joelriou
    joelriou committed Jun 11, 2024
    Configuration menu
    Copy the full SHA
    b7d1af2 View commit details
    Browse the repository at this point in the history

Commits on Jun 12, 2024

  1. feat: more API for commutation of functors with shifts

    @joelriou
    joelriou committed Jun 12, 2024
    Configuration menu
    Copy the full SHA
    42f76c1 View commit details
    Browse the repository at this point in the history

  2. Merge remote-tracking branch 'origin/commshift-comp' into dist-triang… 

    …le-ses2
    @joelriou
    joelriou committed Jun 12, 2024
    Configuration menu
    Copy the full SHA
    495efc6 View commit details
    Browse the repository at this point in the history

Commits on Jun 16, 2024

  1. feat(Algebra/Homology) the single complex functor preserves (co)limits

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

  2. Merge remote-tracking branch 'origin' into single-triangle

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

  3. Merge remote-tracking branch 'origin/single-preserves-limits' into si… 

    …ngle-triangle
    @joelriou
    joelriou committed Jun 16, 2024
    Configuration menu
    Copy the full SHA
    d60e280 View commit details
    Browse the repository at this point in the history

  4. feat: the distinguished triangle attached to a short exact sequence

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

Commits on Jun 18, 2024

  1. Merge remote-tracking branch 'origin' into has-small-localized-hom

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

  2. added docstring

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

  3. more API

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

  4. wip

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

  5. Merge remote-tracking branch 'origin/commshift-comp' into has-small-l… 

    …ocalized-shifted-hom
    @joelriou
    joelriou committed Jun 18, 2024
    Configuration menu
    Copy the full SHA
    40b7ed7 View commit details
    Browse the repository at this point in the history

  6. wip

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

  7. removed a sorry

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

  8. removed sorries

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

Commits on Jun 19, 2024

  1. fixed sorries

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

  2. Update Mathlib/CategoryTheory/Localization/SmallHom.lean 

    Co-authored-by: Andrew Yang <[email protected]>
    @joelriou @erdOne
    joelriou and erdOne authored Jun 19, 2024
    Configuration menu
    Copy the full SHA
    7ee3dfb View commit details
    Browse the repository at this point in the history

  3. wip

    @joelriou
    joelriou committed Jun 19, 2024
    Configuration menu
    Copy the full SHA
    9c91e8d View commit details
    Browse the repository at this point in the history

  4. feat: bijections between morphisms in two localized categories

    @joelriou
    joelriou committed Jun 19, 2024
    Configuration menu
    Copy the full SHA
    83d8c13 View commit details
    Browse the repository at this point in the history

  5. merge with localization-homequiv

    @joelriou
    joelriou committed Jun 19, 2024
    Configuration menu
    Copy the full SHA
    212683a View commit details
    Browse the repository at this point in the history

  6. Merge branch 'localization-homequiv' into has-small-localized-hom

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

  7. whitespace

    @joelriou
    joelriou committed Jun 19, 2024
    Configuration menu
    Copy the full SHA
    69e5969 View commit details
    Browse the repository at this point in the history

  8. Merge branch 'localization-homequiv' into has-small-localized-hom

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

  9. Merge remote-tracking branch 'origin' into has-small-localized-shifte… 

    …d-hom
    @joelriou
    joelriou committed Jun 19, 2024
    Configuration menu
    Copy the full SHA
    a8fcf79 View commit details
    Browse the repository at this point in the history

  10. cleaning up

    @joelriou
    joelriou committed Jun 19, 2024
    Configuration menu
    Copy the full SHA
    40d4490 View commit details
    Browse the repository at this point in the history

  11. Merge remote-tracking branch 'origin/has-small-localized-shifted-hom'… 

    … into small-ext-derived-category
    @joelriou
    joelriou committed Jun 19, 2024
    Configuration menu
    Copy the full SHA
    b62b783 View commit details
    Browse the repository at this point in the history

  12. feat: definition of Ext-groups

    @joelriou
    joelriou committed Jun 19, 2024
    Configuration menu
    Copy the full SHA
    2d3bae9 View commit details
    Browse the repository at this point in the history

  13. wip

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

Commits on Jun 20, 2024

  1. wip

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

  2. better docstring

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

  3. Merge remote-tracking branch 'origin/dist-triangle-ses2' into small-e… 

    …xt-derived-category
    @joelriou
    joelriou committed Jun 20, 2024
    Configuration menu
    Copy the full SHA
    e5c353b View commit details
    Browse the repository at this point in the history

  4. added additive structure

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

  5. added lemma about IsCompatibleWithShift

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

  6. Merge remote-tracking branch 'origin' into small-ext-derived-category

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

  7. remove sorries

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

  8. fixed sorries

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

  9. Merge remote-tracking branch 'origin' into localization-homequiv

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

  10. fixed long line

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

Commits on Jun 22, 2024

  1. Update Mathlib/Algebra/Homology/Single.lean 

    Co-authored-by: Calle Sönne <[email protected]>
    @joelriou @callesonne
    joelriou and callesonne authored Jun 22, 2024
    Configuration menu
    Copy the full SHA
    03a28f0 View commit details
    Browse the repository at this point in the history

  2. Update Mathlib/CategoryTheory/Limits/Preserves/Shapes/Zero.lean 

    Co-authored-by: Calle Sönne <[email protected]>
    @joelriou @callesonne
    joelriou and callesonne authored Jun 22, 2024
    Configuration menu
    Copy the full SHA
    4b47afd View commit details
    Browse the repository at this point in the history

  3. Update Mathlib/CategoryTheory/Limits/Preserves/Shapes/Zero.lean 

    Co-authored-by: Calle Sönne <[email protected]>
    @joelriou @callesonne
    joelriou and callesonne authored Jun 22, 2024
    Configuration menu
    Copy the full SHA
    f9a0d7f View commit details
    Browse the repository at this point in the history

  4. golfing proofs

    @joelriou
    joelriou committed Jun 22, 2024
    Configuration menu
    Copy the full SHA
    e8998eb View commit details
    Browse the repository at this point in the history

  5. fixing the build

    @joelriou
    joelriou committed Jun 22, 2024
    Configuration menu
    Copy the full SHA
    d45bcf7 View commit details
    Browse the repository at this point in the history

Commits on Jun 23, 2024

  1. Merge remote-tracking branch 'origin' into localization-homequiv

    @joelriou
    joelriou committed Jun 23, 2024
    Configuration menu
    Copy the full SHA
    1d71033 View commit details
    Browse the repository at this point in the history

  2. removed duplicate Iso.homEquiv

    @joelriou
    joelriou committed Jun 23, 2024
    Configuration menu
    Copy the full SHA
    bb61444 View commit details
    Browse the repository at this point in the history

  3. Merge remote-tracking branch 'origin/localization-homequiv' into has-… 

    …small-localized-hom
    @joelriou
    joelriou committed Jun 23, 2024
    Configuration menu
    Copy the full SHA
    1141dfb View commit details
    Browse the repository at this point in the history

  4. fixing the build

    @joelriou
    joelriou committed Jun 23, 2024
    Configuration menu
    Copy the full SHA
    2f8d8c8 View commit details
    Browse the repository at this point in the history

  5. Merge remote-tracking branch 'origin/has-small-localized-hom' into ha… 

    …s-small-localized-shifted-hom
    @joelriou
    joelriou committed Jun 23, 2024
    Configuration menu
    Copy the full SHA
    05ba03d View commit details
    Browse the repository at this point in the history

Commits on Jun 24, 2024

  1. added preservesLimitsOfSize variants

    @joelriou
    joelriou committed Jun 24, 2024
    Configuration menu
    Copy the full SHA
    5b005a5 View commit details
    Browse the repository at this point in the history

  2. added converse statements

    @joelriou
    joelriou committed Jun 24, 2024
    Configuration menu
    Copy the full SHA
    7f136b5 View commit details
    Browse the repository at this point in the history

  3. fixing the build

    @joelriou
    joelriou committed Jun 24, 2024
    Configuration menu
    Copy the full SHA
    2f5b840 View commit details
    Browse the repository at this point in the history

  4. Merge remote-tracking branch 'origin/single-preserves-limits' into si… 

    …ngle-triangle
    @joelriou
    joelriou committed Jun 24, 2024
    Configuration menu
    Copy the full SHA
    2ad8c94 View commit details
    Browse the repository at this point in the history

  5. Merge remote-tracking branch 'origin' into has-small-localized-hom

    @joelriou
    joelriou committed Jun 24, 2024
    Configuration menu
    Copy the full SHA
    d3dda4b View commit details
    Browse the repository at this point in the history

  6. Merge remote-tracking branch 'origin' into has-small-localized-hom

    @joelriou
    joelriou committed Jun 24, 2024
    Configuration menu
    Copy the full SHA
    ed23d53 View commit details
    Browse the repository at this point in the history

Commits on Jun 25, 2024

  1. Merge remote-tracking branch 'origin' into has-small-localized-hom

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

  2. reverted unnecessary change

    @joelriou
    joelriou committed Jun 25, 2024
    Configuration menu
    Copy the full SHA
    051d129 View commit details
    Browse the repository at this point in the history

  3. Merge remote-tracking branch 'origin' into dist-triangle-ses2

    @joelriou
    joelriou committed Jun 25, 2024
    Configuration menu
    Copy the full SHA
    a109e48 View commit details
    Browse the repository at this point in the history

  4. Merge remote-tracking branch 'origin/has-small-localized-hom' into ha… 

    …s-small-localized-shifted-hom
    @joelriou
    joelriou committed Jun 25, 2024
    Configuration menu
    Copy the full SHA
    ce64078 View commit details
    Browse the repository at this point in the history

  5. Merge remote-tracking branch 'origin' into has-small-localized-shifte… 

    …d-hom
    @joelriou
    joelriou committed Jun 25, 2024
    Configuration menu
    Copy the full SHA
    aa05936 View commit details
    Browse the repository at this point in the history

Commits on Jun 29, 2024

  1. Merge remote-tracking branch 'origin' into dist-triangle-ses2

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

  2. Merge remote-tracking branch 'origin' into has-small-localized-hom

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

  3. Merge remote-tracking branch 'origin' into has-small-localized-shifte… 

    …d-hom
    @joelriou
    joelriou committed Jun 29, 2024
    Configuration menu
    Copy the full SHA
    f30af05 View commit details
    Browse the repository at this point in the history

Commits on Jun 30, 2024

  1. Merge remote-tracking branch 'origin/has-small-localized-hom' into sm… 

    …all-ext-derived-category
    @joelriou
    joelriou committed Jun 30, 2024
    Configuration menu
    Copy the full SHA
    600a8c9 View commit details
    Browse the repository at this point in the history

  2. Merge remote-tracking branch 'origin/has-small-localized-shifted-hom'… 

    … into small-ext-derived-category
    @joelriou
    joelriou committed Jun 30, 2024
    Configuration menu
    Copy the full SHA
    b4bdf07 View commit details
    Browse the repository at this point in the history

  3. Merge remote-tracking branch 'origin/dist-triangle-ses2' into small-e… 

    …xt-derived-category
    @joelriou
    joelriou committed Jun 30, 2024
    Configuration menu
    Copy the full SHA
    d69ef8e View commit details
    Browse the repository at this point in the history

  4. removed duplicate lemmas

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

Commits on Jul 1, 2024

  1. Merge remote-tracking branch 'origin' into single-triangle

    @joelriou
    joelriou committed Jul 1, 2024
    Configuration menu
    Copy the full SHA
    aa4a9df View commit details
    Browse the repository at this point in the history

  2. Merge remote-tracking branch 'origin/single-triangle' into small-ext-… 

    …derived-category
    @joelriou
    joelriou committed Jul 1, 2024
    Configuration menu
    Copy the full SHA
    6fe2a03 View commit details
    Browse the repository at this point in the history

  3. fixing the build

    @joelriou
    joelriou committed Jul 1, 2024
    Configuration menu
    Copy the full SHA
    3e944a4 View commit details
    Browse the repository at this point in the history

Commits on Jul 4, 2024

  1. Merge remote-tracking branch 'origin' into small-ext-derived-category

    @joelriou
    joelriou committed Jul 4, 2024
    Configuration menu
    Copy the full SHA
    ba7c74b View commit details
    Browse the repository at this point in the history

Commits on Jul 5, 2024

  1. Merge remote-tracking branch 'origin' into small-ext-derived-category

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

  2. fixing the build

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

  3. Merge remote-tracking branch 'origin' into small-ext-derived-category

    @joelriou
    joelriou committed Jul 5, 2024
    Configuration menu
    Copy the full SHA
    35226d6 View commit details
    Browse the repository at this point in the history

  4. fixing the build

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

Commits on Jul 7, 2024

  1. removed AddCommGroup instance

    @joelriou
    joelriou committed Jul 7, 2024
    Configuration menu
    Copy the full SHA
    3c4c026 View commit details
    Browse the repository at this point in the history

  2. Merge remote-tracking branch 'origin' into small-ext-derived-category… 

    …-addcommgroup
    @joelriou
    joelriou committed Jul 7, 2024
    Configuration menu
    Copy the full SHA
    eb4bdbd View commit details
    Browse the repository at this point in the history

  3. wip

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

  4. wip

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

  5. wip

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

  6. Merge remote-tracking branch 'origin' into small-ext-derived-category… 

    …-addcommgroup
    @joelriou
    joelriou committed Jul 7, 2024
    Configuration menu
    Copy the full SHA
    d3ae9b7 View commit details
    Browse the repository at this point in the history

  7. Update Mathlib/Algebra/Homology/DerivedCategory/Ext.lean 

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

  8. added docstring

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

  9. better docstring

    @joelriou
    joelriou committed Jul 7, 2024
    Configuration menu
    Copy the full SHA
    4894c9f View commit details
    Browse the repository at this point in the history

Commits on Jul 8, 2024

  1. wip

    @joelriou
    joelriou committed Jul 8, 2024
    Configuration menu
    Copy the full SHA
    2eca969 View commit details
    Browse the repository at this point in the history

  2. wip

    @joelriou
    joelriou committed Jul 8, 2024
    Configuration menu
    Copy the full SHA
    828d0c4 View commit details
    Browse the repository at this point in the history

  3. wip

    @joelriou
    joelriou committed Jul 8, 2024
    Configuration menu
    Copy the full SHA
    308e483 View commit details
    Browse the repository at this point in the history

  4. Update Mathlib/Algebra/Homology/DerivedCategory/Ext.lean 

    Co-authored-by: Julian-Kuelshammer <[email protected]>
    @joelriou @Julian-Kuelshammer
    joelriou and Julian-Kuelshammer authored Jul 8, 2024
    Configuration menu
    Copy the full SHA
    69ce8aa View commit details
    Browse the repository at this point in the history

  5. wip

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

  6. pleasing lint

    @joelriou
    joelriou committed Jul 8, 2024
    Configuration menu
    Copy the full SHA
    672d68b View commit details
    Browse the repository at this point in the history

  7. wip

    @joelriou
    joelriou committed Jul 8, 2024
    Configuration menu
    Copy the full SHA
    5a8d6e0 View commit details
    Browse the repository at this point in the history

  8. feat: more API for Function.Exact

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

  9. relation between Function.Exact and ShortComplex.Exact

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

Commits on Jul 10, 2024

  1. Merge remote-tracking branch 'origin' into small-ext-derived-category… 

    …-addcommgroup
    @joelriou
    joelriou committed Jul 10, 2024
    Configuration menu
    Copy the full SHA
    ef3ae72 View commit details
    Browse the repository at this point in the history

  2. Merge remote-tracking branch 'origin' into function-exact-addequiv

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

  3. reorganized the file Algebra.Exact

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

  4. Merge remote-tracking branch 'origin/small-ext-derived-category-addco… 

    …mmgroup' into ext-covariant-sequence
    @joelriou
    joelriou committed Jul 10, 2024
    Configuration menu
    Copy the full SHA
    55ba28f View commit details
    Browse the repository at this point in the history

  5. Update Mathlib/Algebra/Exact.lean 

    Co-authored-by: Riccardo Brasca <[email protected]>
    @joelriou @riccardobrasca
    joelriou and riccardobrasca authored Jul 10, 2024
    Configuration menu
    Copy the full SHA
    259568d View commit details
    Browse the repository at this point in the history

  6. used coercion instead to .toAddMonoidHom

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

  7. Merge remote-tracking branch 'origin/function-exact-addequiv' into ex… 

    …t-covariant-sequence
    @joelriou
    joelriou committed Jul 10, 2024
    Configuration menu
    Copy the full SHA
    ccff800 View commit details
    Browse the repository at this point in the history

  8. fixing the build

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

  9. added docstrings

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

Commits on Jul 16, 2024

  1. Merge remote-tracking branch 'origin' into ext-covariant-sequence

    @joelriou
    joelriou committed Jul 16, 2024
    Configuration menu
    Copy the full SHA
    174e0b0 View commit details
    Browse the repository at this point in the history

  2. feat: the Ext class of a short exact sequence

    @joelriou
    joelriou committed Jul 16, 2024
    Configuration menu
    Copy the full SHA
    a713a36 View commit details
    Browse the repository at this point in the history

Commits on Jul 17, 2024

  1. using local notations

    @joelriou
    joelriou committed Jul 17, 2024
    Configuration menu
    Copy the full SHA
    0730ec9 View commit details
    Browse the repository at this point in the history

Commits on Jul 18, 2024

  1. removed postcomp/precomp, unnecessary here

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

  2. Merge remote-tracking branch 'origin' into ext-class-of-short-exact

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

  3. Merge remote-tracking branch 'origin' into ext-covariant-sequence

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

  4. added bilinearComp

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

Commits on Jul 22, 2024

  1. Merge remote-tracking branch 'origin' into ext-class-of-short-exact

    @joelriou
    joelriou committed Jul 22, 2024
    Configuration menu
    Copy the full SHA
    9509a9f View commit details
    Browse the repository at this point in the history

  2. split files

    @joelriou
    joelriou committed Jul 22, 2024
    Configuration menu
    Copy the full SHA
    596b658 View commit details
    Browse the repository at this point in the history

  3. fixing imports

    @joelriou
    joelriou committed Jul 22, 2024
    Configuration menu
    Copy the full SHA
    469b443 View commit details
    Browse the repository at this point in the history

Commits on Jul 23, 2024

  1. Merge remote-tracking branch 'origin' into ext-class-of-short-exact

    @joelriou
    joelriou committed Jul 23, 2024
    Configuration menu
    Copy the full SHA
    4339010 View commit details
    Browse the repository at this point in the history

  2. Merge remote-tracking branch 'origin/ext-class-of-short-exact' into e… 

    …xt-covariant-sequence
    @joelriou
    joelriou committed Jul 23, 2024
    Configuration menu
    Copy the full SHA
    2f313c7 View commit details
    Browse the repository at this point in the history

  3. fixing the build

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

Commits on Jul 24, 2024

  1. feat: the contravariant long exact sequence of Ext

    @joelriou
    joelriou committed Jul 24, 2024
    Configuration menu
    Copy the full SHA
    2a50812 View commit details
    Browse the repository at this point in the history

  2. one sorry left

    @joelriou
    joelriou committed Jul 24, 2024
    Configuration menu
    Copy the full SHA
    e209c53 View commit details
    Browse the repository at this point in the history

  3. Merge remote-tracking branch 'origin' into ext-class-of-short-exact

    @joelriou
    joelriou committed Jul 24, 2024
    Configuration menu
    Copy the full SHA
    0d4714e View commit details
    Browse the repository at this point in the history

  4. Merge remote-tracking branch 'origin/ext-class-of-short-exact' into e… 

    …xt-covariant-sequence
    @joelriou
    joelriou committed Jul 24, 2024
    Configuration menu
    Copy the full SHA
    be5f646 View commit details
    Browse the repository at this point in the history

  5. fixing the build

    @joelriou
    joelriou committed Jul 24, 2024
    Configuration menu
    Copy the full SHA
    1256a79 View commit details
    Browse the repository at this point in the history

  6. Merge remote-tracking branch 'origin/ext-class-of-short-exact' into e… 

    …xt-covariant-sequence
    @joelriou
    joelriou committed Jul 24, 2024
    Configuration menu
    Copy the full SHA
    3a28d99 View commit details
    Browse the repository at this point in the history

  7. Merge remote-tracking branch 'origin/ext-covariant-sequence' into ext… 

    …-contravariant-sequence
    @joelriou
    joelriou committed Jul 24, 2024
    Configuration menu
    Copy the full SHA
    2b79187 View commit details
    Browse the repository at this point in the history

  8. removed sorries

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

  9. little cleaning up

    @joelriou
    joelriou committed Jul 24, 2024
    Configuration menu
    Copy the full SHA
    f8a85fd View commit details
    Browse the repository at this point in the history

  10. Merge remote-tracking branch 'origin' into ext-contravariant-sequence

    @joelriou
    joelriou committed Jul 24, 2024
    Configuration menu
    Copy the full SHA
    0a3a035 View commit details
    Browse the repository at this point in the history

Commits on Jul 28, 2024

  1. Merge remote-tracking branch 'origin' into ext-class-of-short-exact

    @joelriou
    joelriou committed Jul 28, 2024
    Configuration menu
    Copy the full SHA
    8f2270c View commit details
    Browse the repository at this point in the history

  2. Merge remote-tracking branch 'origin/ext-class-of-short-exact' into e… 

    …xt-covariant-sequence
    @joelriou
    joelriou committed Jul 28, 2024
    Configuration menu
    Copy the full SHA
    efecba0 View commit details
    Browse the repository at this point in the history

  3. Merge remote-tracking branch 'origin/ext-covariant-sequence' into ext… 

    …-contravariant-sequence
    @joelriou
    joelriou committed Jul 28, 2024
    Configuration menu
    Copy the full SHA
    0279f09 View commit details
    Browse the repository at this point in the history

Commits on Jul 31, 2024

  1. Merge remote-tracking branch 'origin' into ext-class-of-short-exact

    @joelriou
    joelriou committed Jul 31, 2024
    Configuration menu
    Copy the full SHA
    fadf10e View commit details
    Browse the repository at this point in the history

Commits on Aug 1, 2024

  1. Merge remote-tracking branch 'origin/ext-class-of-short-exact' into e… 

    …xt-covariant-sequence
    @joelriou
    joelriou committed Aug 1, 2024
    Configuration menu
    Copy the full SHA
    71b8cd8 View commit details
    Browse the repository at this point in the history

Commits on Aug 8, 2024

  1. Merge remote-tracking branch 'origin' into ext-class-of-short-exact

    @joelriou
    joelriou committed Aug 8, 2024
    Configuration menu
    Copy the full SHA
    18946e7 View commit details
    Browse the repository at this point in the history

Commits on Aug 9, 2024

  1. Merge remote-tracking branch 'origin' into ext-class-of-short-exact

    @joelriou
    joelriou committed Aug 9, 2024
    Configuration menu
    Copy the full SHA
    8a8287a View commit details
    Browse the repository at this point in the history

Commits on Aug 12, 2024

  1. Merge remote-tracking branch 'origin' into ext-class-of-short-exact

    @joelriou
    joelriou committed Aug 12, 2024
    Configuration menu
    Copy the full SHA
    47f7d38 View commit details
    Browse the repository at this point in the history

Commits on Aug 13, 2024

  1. Merge remote-tracking branch 'origin' into ext-class-of-short-exact

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

  2. fixing the build

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

  3. Merge remote-tracking branch 'origin/ext-class-of-short-exact' into e… 

    …xt-covariant-sequence
    @joelriou
    joelriou committed Aug 13, 2024
    Configuration menu
    Copy the full SHA
    700a656 View commit details
    Browse the repository at this point in the history

  4. fixing the build

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

  5. Merge remote-tracking branch 'origin/ext-covariant-sequence' into ext… 

    …-contravariant-sequence
    @joelriou
    joelriou committed Aug 13, 2024
    Configuration menu
    Copy the full SHA
    2f1c8bd View commit details
    Browse the repository at this point in the history

  6. fixing the build

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

Commits on Aug 27, 2024

  1. Merge remote-tracking branch 'origin' into ext-covariant-sequence

    @joelriou
    joelriou committed Aug 27, 2024
    Configuration menu
    Copy the full SHA
    746c87e View commit details
    Browse the repository at this point in the history

  2. better docstring

    @joelriou
    joelriou committed Aug 27, 2024
    Configuration menu
    Copy the full SHA
    884be87 View commit details
    Browse the repository at this point in the history

  3. Merge remote-tracking branch 'origin/ext-covariant-sequence' into ext… 

    …-contravariant-sequence
    @joelriou
    joelriou committed Aug 27, 2024
    Configuration menu
    Copy the full SHA
    833e1cd View commit details
    Browse the repository at this point in the history

Commits on Aug 29, 2024

  1. Merge remote-tracking branch 'origin' into ext-covariant-sequence

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

Commits on Sep 26, 2024

  1. Merge branch 'master' into ext-covariant-sequence-merge

    @dagurtomas
    dagurtomas committed Sep 26, 2024
    Configuration menu
    Copy the full SHA
    ffc9523 View commit details
    Browse the repository at this point in the history

  2. add docstrings

    @dagurtomas
    dagurtomas committed Sep 26, 2024
    Configuration menu
    Copy the full SHA
    6a8b133 View commit details
    Browse the repository at this point in the history

  3. Merge remote-tracking branch 'origin/ext-covariant-sequence' into ext… 

    …-contravariant-sequence
    @joelriou
    joelriou committed Sep 26, 2024
    Configuration menu
    Copy the full SHA
    270351d View commit details
    Browse the repository at this point in the history

  4. added docstrings

    @joelriou
    joelriou committed Sep 26, 2024
    Configuration menu
    Copy the full SHA
    f4ffaec View commit details
    Browse the repository at this point in the history

  5. Merge remote-tracking branch 'origin' into ext-contravariant-sequence

    @joelriou
    joelriou committed Sep 26, 2024
    Configuration menu
    Copy the full SHA
    dd2c3c6 View commit details
    Browse the repository at this point in the history

  6. Merge remote-tracking branch 'origin' into ext-contravariant-sequence

    @joelriou
    joelriou committed Sep 26, 2024
    Configuration menu
    Copy the full SHA
    ff53acc View commit details
    Browse the repository at this point in the history

  7. fixing the build

    @joelriou
    joelriou committed Sep 26, 2024
    Configuration menu
    Copy the full SHA
    3ee187c View commit details
    Browse the repository at this point in the history

Commits on Oct 8, 2024

  1. Merge remote-tracking branch 'origin' into ext-contravariant-sequence

    @joelriou
    joelriou committed Oct 8, 2024
    Configuration menu
    Copy the full SHA
    90ca20b View commit details
    Browse the repository at this point in the history

  2. feat(CategoryTheory/Shift): shifted morphisms in the opposite category

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

  3. added blank line

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

  4. Merge remote-tracking branch 'origin/shifted-hom-opposite' into ext-c… 

    …ontravariant-sequence
    @joelriou
    joelriou committed Oct 8, 2024
    Configuration menu
    Copy the full SHA
    f5091dd View commit details
    Browse the repository at this point in the history