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: quantale homomorphisms #19291

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

feat: quantale homomorphisms #19291

wants to merge 103 commits into from
+237 −6

Commits on Sep 24, 2024

  1. Basic definition of quantale.

    @PieterCuijpers
    PieterCuijpers committed Sep 24, 2024
    Configuration menu
    Copy the full SHA
    455a748 View commit details
    Browse the repository at this point in the history

Commits on Sep 30, 2024

  1. Rephrased some text and todo's

    @PieterCuijpers
    PieterCuijpers committed Sep 30, 2024
    Configuration menu
    Copy the full SHA
    a60b10f View commit details
    Browse the repository at this point in the history

  2. Updated using lake exe mk_all

    @PieterCuijpers
    PieterCuijpers committed Sep 30, 2024
    Configuration menu
    Copy the full SHA
    c488a7d View commit details
    Browse the repository at this point in the history

  3. Linter corrections

    @PieterCuijpers
    PieterCuijpers committed Sep 30, 2024
    Configuration menu
    Copy the full SHA
    33a33c9 View commit details
    Browse the repository at this point in the history

  4. Linter corrections (docstrings)

    @PieterCuijpers
    PieterCuijpers committed Sep 30, 2024
    Configuration menu
    Copy the full SHA
    7913f82 View commit details
    Browse the repository at this point in the history

  5. Update Mathlib/Order/Quantale.lean 

    Different bullet style

Co-authored-by: Jireh Loreaux <[email protected]>
    @PieterCuijpers @j-loreaux
    PieterCuijpers and j-loreaux authored Sep 30, 2024
    Configuration menu
    Copy the full SHA
    0f08888 View commit details
    Browse the repository at this point in the history

  6. Update Mathlib/Order/Quantale.lean 

    Style change, including 'left'

Co-authored-by: Jireh Loreaux <[email protected]>
    @PieterCuijpers @j-loreaux
    PieterCuijpers and j-loreaux authored Sep 30, 2024
    Configuration menu
    Copy the full SHA
    1190a65 View commit details
    Browse the repository at this point in the history

  7. Style updates

    @PieterCuijpers
    PieterCuijpers committed Sep 30, 2024
    Configuration menu
    Copy the full SHA
    b623b56 View commit details
    Browse the repository at this point in the history

  8. Made peace with using CompleteLattice as the basis of a quantale defi… 

    …nition.
    @PieterCuijpers
    PieterCuijpers committed Sep 30, 2024
    Configuration menu
    Copy the full SHA
    15babb8 View commit details
    Browse the repository at this point in the history

Commits on Oct 1, 2024

  1. scoping the residulation notation

    @PieterCuijpers
    PieterCuijpers committed Oct 1, 2024
    Configuration menu
    Copy the full SHA
    50a1500 View commit details
    Browse the repository at this point in the history

Commits on Oct 2, 2024

  1. Implemented "to_additive" variants, and classes for all special quant… 

    …ale properties.
    @PieterCuijpers
    PieterCuijpers committed Oct 2, 2024
    Configuration menu
    Copy the full SHA
    1ec5d12 View commit details
    Browse the repository at this point in the history

Commits on Oct 3, 2024

  1. Small textual changes in comments.

    @PieterCuijpers
    PieterCuijpers committed Oct 3, 2024
    Configuration menu
    Copy the full SHA
    2734c4a View commit details
    Browse the repository at this point in the history

  2. Extracted "IdemSemigroup" and updated IdemSemiring definition in Klee… 

    …ne.lean to remedy clash on ádd_idem'.
    @PieterCuijpers
    PieterCuijpers committed Oct 3, 2024
    Configuration menu
    Copy the full SHA
    af98150 View commit details
    Browse the repository at this point in the history

  3. Found a better way to derive IdemSemiring from IdemSemigroup

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

  4. Style updates to Idem.lean

    @PieterCuijpers
    PieterCuijpers committed Oct 3, 2024
    Configuration menu
    Copy the full SHA
    120eafe View commit details
    Browse the repository at this point in the history

  5. Small edits

    @PieterCuijpers
    PieterCuijpers committed Oct 3, 2024
    Configuration menu
    Copy the full SHA
    03e05ad View commit details
    Browse the repository at this point in the history

  6. Update

    @PieterCuijpers
    PieterCuijpers committed Oct 3, 2024
    Configuration menu
    Copy the full SHA
    b8c27e8 View commit details
    Browse the repository at this point in the history

  7. Style. Added missing docstring

    @PieterCuijpers
    PieterCuijpers committed Oct 3, 2024
    Configuration menu
    Copy the full SHA
    27a9144 View commit details
    Browse the repository at this point in the history

  8. Residuation notation only on multiplicative quantale for the time being.

    @PieterCuijpers
    PieterCuijpers committed Oct 3, 2024
    Configuration menu
    Copy the full SHA
    1551fe7 View commit details
    Browse the repository at this point in the history

Commits on Oct 4, 2024

  1. Added to_additive on left_residuation notation. (Test to see if there… 

    … still is a problem with the doc-string?)
    @PieterCuijpers
    PieterCuijpers committed Oct 4, 2024
    Configuration menu
    Copy the full SHA
    547941a View commit details
    Browse the repository at this point in the history

  2. Separated additive and multiplicative notations for left- and right r… 

    …esiduation to solve doc-string problem in to_additive.
    @PieterCuijpers
    PieterCuijpers committed Oct 4, 2024
    Configuration menu
    Copy the full SHA
    3e9b865 View commit details
    Browse the repository at this point in the history

  3. Made Quantale definition dependent on Semigroup - this seems to simpl… 

    …ify all derived classes. Turned IsIntegral into a mix-in, removed Comm- and Idem- classes as they are now moved to semigroups.
    @PieterCuijpers
    PieterCuijpers committed Oct 4, 2024
    Configuration menu
    Copy the full SHA
    47e3aa2 View commit details
    Browse the repository at this point in the history

  4. Update

    @PieterCuijpers
    PieterCuijpers committed Oct 4, 2024
    Configuration menu
    Copy the full SHA
    0f080dc View commit details
    Browse the repository at this point in the history

  5. Updated ToAdditive.Frontend to undo unnecessary changes.

    @PieterCuijpers
    PieterCuijpers committed Oct 4, 2024
    Configuration menu
    Copy the full SHA
    4a75852 View commit details
    Browse the repository at this point in the history

Commits on Oct 22, 2024

  1. IsIntegral into Quantale namespace

    @PieterCuijpers
    PieterCuijpers committed Oct 22, 2024
    Configuration menu
    Copy the full SHA
    206c5e4 View commit details
    Browse the repository at this point in the history

  2. IsIdem in Semigroup namespace

    @PieterCuijpers
    PieterCuijpers committed Oct 22, 2024
    Configuration menu
    Copy the full SHA
    7723983 View commit details
    Browse the repository at this point in the history

Commits on Oct 29, 2024

  1. Update Mathlib/Algebra/Group/IsIdem.lean 

    Co-authored-by: Yaël Dillies <[email protected]>
    @PieterCuijpers @YaelDillies
    PieterCuijpers and YaelDillies authored Oct 29, 2024
    Configuration menu
    Copy the full SHA
    a81f90e View commit details
    Browse the repository at this point in the history

  2. Update Mathlib/Algebra/Group/IsIdem.lean 

    Co-authored-by: Yaël Dillies <[email protected]>
    @PieterCuijpers @YaelDillies
    PieterCuijpers and YaelDillies authored Oct 29, 2024
    Configuration menu
    Copy the full SHA
    70d0f50 View commit details
    Browse the repository at this point in the history

  3. Update Mathlib/Algebra/Group/IsIdem.lean 

    Co-authored-by: Yaël Dillies <[email protected]>
    @PieterCuijpers @YaelDillies
    PieterCuijpers and YaelDillies authored Oct 29, 2024
    Configuration menu
    Copy the full SHA
    c23bd96 View commit details
    Browse the repository at this point in the history

  4. Update Mathlib/Algebra/Group/IsIdem.lean 

    Co-authored-by: Yaël Dillies <[email protected]>
    @PieterCuijpers @YaelDillies
    PieterCuijpers and YaelDillies authored Oct 29, 2024
    Configuration menu
    Copy the full SHA
    338f754 View commit details
    Browse the repository at this point in the history

  5. Update Mathlib/Algebra/Group/IsIdem.lean 

    Co-authored-by: Yaël Dillies <[email protected]>
    @PieterCuijpers @YaelDillies
    PieterCuijpers and YaelDillies authored Oct 29, 2024
    Configuration menu
    Copy the full SHA
    8397c31 View commit details
    Browse the repository at this point in the history

  6. Update Mathlib/Algebra/Order/Kleene.lean 

    Co-authored-by: Yaël Dillies <[email protected]>
    @PieterCuijpers @YaelDillies
    PieterCuijpers and YaelDillies authored Oct 29, 2024
    Configuration menu
    Copy the full SHA
    8e4e77b View commit details
    Browse the repository at this point in the history

  7. Update Mathlib/Order/Quantale.lean 

    Co-authored-by: Yaël Dillies <[email protected]>
    @PieterCuijpers @YaelDillies
    PieterCuijpers and YaelDillies authored Oct 29, 2024
    Configuration menu
    Copy the full SHA
    a673241 View commit details
    Browse the repository at this point in the history

  8. Update Mathlib/Order/Quantale.lean 

    Co-authored-by: Yaël Dillies <[email protected]>
    @PieterCuijpers @YaelDillies
    PieterCuijpers and YaelDillies authored Oct 29, 2024
    Configuration menu
    Copy the full SHA
    3ccf5f3 View commit details
    Browse the repository at this point in the history

  9. Update Mathlib/Order/Quantale.lean 

    Co-authored-by: Yaël Dillies <[email protected]>
    @PieterCuijpers @YaelDillies
    PieterCuijpers and YaelDillies authored Oct 29, 2024
    Configuration menu
    Copy the full SHA
    ca29e95 View commit details
    Browse the repository at this point in the history

  10. Update Mathlib/Order/Quantale.lean 

    Co-authored-by: Yaël Dillies <[email protected]>
    @PieterCuijpers @YaelDillies
    PieterCuijpers and YaelDillies authored Oct 29, 2024
    Configuration menu
    Copy the full SHA
    8f2416b View commit details
    Browse the repository at this point in the history

  11. Moved Quantales to Algebra/Order and fixed the implementation of left… 

    …Residual and rightResidual notation for AddQuantales (to_additive does not work there).
    @PieterCuijpers
    PieterCuijpers committed Oct 29, 2024
    Configuration menu
    Copy the full SHA
    cb533ec View commit details
    Browse the repository at this point in the history

  12. Update library

    @PieterCuijpers
    PieterCuijpers committed Oct 29, 2024
    Configuration menu
    Copy the full SHA
    1e1595d View commit details
    Browse the repository at this point in the history

  13. Struggles to resolve an not-understood error...

    @PieterCuijpers
    PieterCuijpers committed Oct 29, 2024
    Configuration menu
    Copy the full SHA
    9082b68 View commit details
    Browse the repository at this point in the history

  14. Correct Quantale.lean, but unresolved error in settings somewhere.

    @PieterCuijpers
    PieterCuijpers committed Oct 29, 2024
    Configuration menu
    Copy the full SHA
    6d1141e View commit details
    Browse the repository at this point in the history

  15. Merge conflicts resolved

    @PieterCuijpers
    PieterCuijpers committed Oct 29, 2024
    Configuration menu
    Copy the full SHA
    db7ada1 View commit details
    Browse the repository at this point in the history

  16. Fixed left- rightResiduation notation, also for AddQuantale (workarou… 

    …nd - since to_additive was giving trouble)
    @PieterCuijpers
    PieterCuijpers committed Oct 29, 2024
    Configuration menu
    Copy the full SHA
    80e96f3 View commit details
    Browse the repository at this point in the history

  17. Merge branch 'PieterCuijpers_Quantales' of https://github.com/leanpro… 

    …ver-community/mathlib4 into PieterCuijpers_Quantales
    @PieterCuijpers
    PieterCuijpers committed Oct 29, 2024
    Configuration menu
    Copy the full SHA
    803078c View commit details
    Browse the repository at this point in the history

  18. Lake-manifest was corrupted. Now fixed.

    @PieterCuijpers
    PieterCuijpers committed Oct 29, 2024
    Configuration menu
    Copy the full SHA
    c602733 View commit details
    Browse the repository at this point in the history

  19. Moved Quantale.lean to Algebra/Order

    @PieterCuijpers
    PieterCuijpers committed Oct 29, 2024
    Configuration menu
    Copy the full SHA
    e7799fd View commit details
    Browse the repository at this point in the history

  20. Update

    @PieterCuijpers
    PieterCuijpers committed Oct 29, 2024
    Configuration menu
    Copy the full SHA
    96ed693 View commit details
    Browse the repository at this point in the history

Commits on Oct 31, 2024

  1. Merge remote-tracking branch 'origin' into PieterCuijpers_Quantales

    @PieterCuijpers
    PieterCuijpers committed Oct 31, 2024
    Configuration menu
    Copy the full SHA
    dc50f88 View commit details
    Browse the repository at this point in the history

  2. Corrected bibtex references

    @PieterCuijpers
    PieterCuijpers committed Oct 31, 2024
    Configuration menu
    Copy the full SHA
    c72a23f View commit details
    Browse the repository at this point in the history

  3. Update docs/references.bib 

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

  4. Typo in introduction text

    @PieterCuijpers
    PieterCuijpers committed Oct 31, 2024
    Configuration menu
    Copy the full SHA
    2f0ddb0 View commit details
    Browse the repository at this point in the history

  5. First definition of QuantaleHom and OneQuantaleHom

    @PieterCuijpers
    PieterCuijpers committed Oct 31, 2024
    Configuration menu
    Copy the full SHA
    a38d957 View commit details
    Browse the repository at this point in the history

  6. Attempt to add LaxQuantaleHom. 

    Not yet finished due to a missing SubadditiveHom (while SubadditiveHomClass is defined).
    @PieterCuijpers
    PieterCuijpers committed Oct 31, 2024
    Configuration menu
    Copy the full SHA
    1a85bc0 View commit details
    Browse the repository at this point in the history

Commits on Nov 1, 2024

  1. Typo 

    Co-authored-by: Yaël Dillies <[email protected]>
    @PieterCuijpers @YaelDillies
    PieterCuijpers and YaelDillies authored Nov 1, 2024
    Configuration menu
    Copy the full SHA
    ea22c9a View commit details
    Browse the repository at this point in the history

  2. Merge remote-tracking branch 'origin' into PieterCuijpers_Quantales

    @PieterCuijpers
    PieterCuijpers committed Nov 1, 2024
    Configuration menu
    Copy the full SHA
    0eb1511 View commit details
    Browse the repository at this point in the history

  3. Merge branch 'PieterCuijpers_Quantales' into PieterCuijpers_Quantales… 

    …_Homomorphism
    @PieterCuijpers
    PieterCuijpers committed Nov 1, 2024
    Configuration menu
    Copy the full SHA
    e312d98 View commit details
    Browse the repository at this point in the history

  4. Improved definition (following Algebra.Group.Hom.Defs as an example) … 

    …and added basic coercion theorems.
    @PieterCuijpers
    PieterCuijpers committed Nov 1, 2024
    Configuration menu
    Copy the full SHA
    aaa58b0 View commit details
    Browse the repository at this point in the history

  5. Added OneQuantaleHom

    @PieterCuijpers
    PieterCuijpers committed Nov 1, 2024
    Configuration menu
    Copy the full SHA
    b359e2a View commit details
    Browse the repository at this point in the history

  6. Cleaned up a bit of notation, leaving out notation for non-unital qua… 

    …ntales to favour simpler notation for unital quantales - in line with monoid notations.
    @PieterCuijpers
    PieterCuijpers committed Nov 1, 2024
    Configuration menu
    Copy the full SHA
    0fe63c1 View commit details
    Browse the repository at this point in the history

  7. Theorem: every ordered monoid isomorphism is a unital quantale homomo… 

    …rphism
    @PieterCuijpers
    PieterCuijpers committed Nov 1, 2024
    Configuration menu
    Copy the full SHA
    8c9c4ea View commit details
    Browse the repository at this point in the history

  8. Made a start on a lax homomorphism document.

    @PieterCuijpers
    PieterCuijpers committed Nov 1, 2024
    Configuration menu
    Copy the full SHA
    f65082f View commit details
    Browse the repository at this point in the history

Commits on Nov 4, 2024

  1. Update Mathlib/Algebra/Group/IsIdem.lean 

    Co-authored-by: Yaël Dillies <[email protected]>
    @PieterCuijpers @YaelDillies
    PieterCuijpers and YaelDillies authored Nov 4, 2024
    Configuration menu
    Copy the full SHA
    f6279c8 View commit details
    Browse the repository at this point in the history

  2. Update Mathlib/Algebra/Group/IsIdem.lean 

    Co-authored-by: Yaël Dillies <[email protected]>
    @PieterCuijpers @YaelDillies
    PieterCuijpers and YaelDillies authored Nov 4, 2024
    Configuration menu
    Copy the full SHA
    4cf572f View commit details
    Browse the repository at this point in the history

  3. Update Mathlib/Algebra/Group/IsIdem.lean 

    Co-authored-by: Yaël Dillies <[email protected]>
    @PieterCuijpers @YaelDillies
    PieterCuijpers and YaelDillies authored Nov 4, 2024
    Configuration menu
    Copy the full SHA
    7f482d5 View commit details
    Browse the repository at this point in the history

  4. Update Mathlib/Algebra/Order/Kleene.lean 

    Co-authored-by: Yaël Dillies <[email protected]>
    @PieterCuijpers @YaelDillies
    PieterCuijpers and YaelDillies authored Nov 4, 2024
    Configuration menu
    Copy the full SHA
    cbc174e View commit details
    Browse the repository at this point in the history

  5. Update Mathlib/Algebra/Order/Quantale.lean 

    Co-authored-by: Yaël Dillies <[email protected]>
    @PieterCuijpers @YaelDillies
    PieterCuijpers and YaelDillies authored Nov 4, 2024
    Configuration menu
    Copy the full SHA
    73c85fa View commit details
    Browse the repository at this point in the history

  6. Update Mathlib/Algebra/Order/Quantale.lean 

    Co-authored-by: Yaël Dillies <[email protected]>
    @PieterCuijpers @YaelDillies
    PieterCuijpers and YaelDillies authored Nov 4, 2024
    Configuration menu
    Copy the full SHA
    2f972bc View commit details
    Browse the repository at this point in the history

  7. Update Mathlib/Algebra/Order/Kleene.lean 

    Co-authored-by: Yaël Dillies <[email protected]>
    @PieterCuijpers @YaelDillies
    PieterCuijpers and YaelDillies authored Nov 4, 2024
    Configuration menu
    Copy the full SHA
    f453afb View commit details
    Browse the repository at this point in the history

  8. Updated everything to use Type* i.s.o. Type _

    @PieterCuijpers
    PieterCuijpers committed Nov 4, 2024
    Configuration menu
    Copy the full SHA
    4fc415d View commit details
    Browse the repository at this point in the history

Commits on Nov 5, 2024

  1. Added basic theorems for iSup, sup, monotonicity of the semigroup ope… 

    …rator, and residuation
    @PieterCuijpers
    PieterCuijpers committed Nov 5, 2024
    Configuration menu
    Copy the full SHA
    0ee4973 View commit details
    Browse the repository at this point in the history

Commits on Nov 7, 2024

  1. Apply suggestions from code review 

    Co-authored-by: github-actions[bot] <41898282+github-actions[bot]@users.noreply.github.com>
Co-authored-by: Yaël Dillies <[email protected]>
    @PieterCuijpers @github-actions @YaelDillies
    3 people authored Nov 7, 2024
    Configuration menu
    Copy the full SHA
    bc155ea View commit details
    Browse the repository at this point in the history

  2. Processed comments and cleaned up use of implicit variables

    @PieterCuijpers
    PieterCuijpers committed Nov 7, 2024
    Configuration menu
    Copy the full SHA
    4f7564f View commit details
    Browse the repository at this point in the history

  3. Merge branch 'PieterCuijpers_Quantales', remote-tracking branch 'orig… 

    …in' into PieterCuijpers_Quantales_Homomorphism
    @PieterCuijpers
    PieterCuijpers committed Nov 7, 2024
    Configuration menu
    Copy the full SHA
    e64091f View commit details
    Browse the repository at this point in the history

  4. Merge remote-tracking branch 'origin' into PieterCuijpers_Quantales

    @PieterCuijpers
    PieterCuijpers committed Nov 7, 2024
    Configuration menu
    Copy the full SHA
    5c2f66b View commit details
    Browse the repository at this point in the history

  5. Merge branch 'PieterCuijpers_Quantales', remote-tracking branch 'orig… 

    …in' into PieterCuijpers_Quantales_Homomorphism
    @PieterCuijpers
    PieterCuijpers committed Nov 7, 2024
    Configuration menu
    Copy the full SHA
    75061bd View commit details
    Browse the repository at this point in the history

  6. Fixed problem with existing monotonicity theorems on ordered monoid b… 

    …y proving instances of MulLeftMono and MulRightMono.
    @PieterCuijpers
    PieterCuijpers committed Nov 7, 2024
    Configuration menu
    Copy the full SHA
    5d04d47 View commit details
    Browse the repository at this point in the history

  7. Made instances to classed defined in Ordered Monoid theory to deal wi… 

    …th monotonicity, instead of defining them directly.
    @PieterCuijpers
    PieterCuijpers committed Nov 7, 2024
    Configuration menu
    Copy the full SHA
    0e45960 View commit details
    Browse the repository at this point in the history

  8. Apply suggestions from code review 

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

  9. Removed unnecessary comment.

    @PieterCuijpers
    PieterCuijpers committed Nov 7, 2024
    Configuration menu
    Copy the full SHA
    910a712 View commit details
    Browse the repository at this point in the history

Commits on Nov 8, 2024

  1. Updated comments

    @PieterCuijpers
    PieterCuijpers committed Nov 8, 2024
    Configuration menu
    Copy the full SHA
    afdeacd View commit details
    Browse the repository at this point in the history

  2. Merge remote-tracking branch 'origin' into PieterCuijpers_Quantales

    @PieterCuijpers
    PieterCuijpers committed Nov 8, 2024
    Configuration menu
    Copy the full SHA
    b70701f View commit details
    Browse the repository at this point in the history

  3. Merge branch 'PieterCuijpers_Quantales' into PieterCuijpers_Quantales… 

    …_Homomorphism
    @PieterCuijpers
    PieterCuijpers committed Nov 8, 2024
    Configuration menu
    Copy the full SHA
    81ffa5a View commit details
    Browse the repository at this point in the history

  4. Small error correction after merge

    @PieterCuijpers
    PieterCuijpers committed Nov 8, 2024
    Configuration menu
    Copy the full SHA
    90f6b6f View commit details
    Browse the repository at this point in the history

Commits on Nov 11, 2024

  1. Removed HomClass definitions, in-line with Mathlib.Algebra.Order.Hom.… 

    …Monoid (#10544)
    @PieterCuijpers
    PieterCuijpers committed Nov 11, 2024
    Configuration menu
    Copy the full SHA
    42e849e View commit details
    Browse the repository at this point in the history

  2. Updated comments

    @PieterCuijpers
    PieterCuijpers committed Nov 11, 2024
    Configuration menu
    Copy the full SHA
    5d8e0be View commit details
    Browse the repository at this point in the history

Commits on Nov 20, 2024

  1. Merge remote-tracking branch 'origin' into PieterCuijpers_Quantales_H… 

    …omomorphism
    @PieterCuijpers
    PieterCuijpers committed Nov 20, 2024
    Configuration menu
    Copy the full SHA
    ba025f8 View commit details
    Browse the repository at this point in the history

  2. Running into some doubts regarding Mathlib.Algebra.Order.Hom.Monoid w… 

    …hile implementing AddQuantaleHom.
    @PieterCuijpers
    PieterCuijpers committed Nov 20, 2024
    Configuration menu
    Copy the full SHA
    03c4b15 View commit details
    Browse the repository at this point in the history

  3. Merge remote-tracking branch 'origin' into PieterCuijpers_Quantales_H… 

    …omomorphism
    @PieterCuijpers
    PieterCuijpers committed Nov 20, 2024
    Configuration menu
    Copy the full SHA
    56d7d15 View commit details
    Browse the repository at this point in the history

  4. Delete Mathlib/Algebra/Group/IsIdem.lean 

    Don't know what went wrong on the merge. But now it's gone.
    @PieterCuijpers
    PieterCuijpers authored Nov 20, 2024
    Configuration menu
    Copy the full SHA
    ac623f0 View commit details
    Browse the repository at this point in the history

  5. Restored Kleene as well

    @PieterCuijpers
    PieterCuijpers committed Nov 20, 2024
    Configuration menu
    Copy the full SHA
    27f739e View commit details
    Browse the repository at this point in the history

  6. Update Mathlib.lean 

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

  7. Moved problem of defining QuantaleIso as OrderMulIso to a different f… 

    …ile.

Added QuantaleHom definitions.

Note that the doc_strings speak of `AddQuantale` and `Quantale` in anticipation of the variable_alias.
    @PieterCuijpers
    PieterCuijpers committed Nov 20, 2024
    Configuration menu
    Copy the full SHA
    0b7645d View commit details
    Browse the repository at this point in the history

  8. Morphisms only should preserve sSup, not the entire complete lattice.

    @PieterCuijpers
    PieterCuijpers committed Nov 20, 2024
    Configuration menu
    Copy the full SHA
    2c4c8d8 View commit details
    Browse the repository at this point in the history

  9. Added standard? coercion theorems - not sure which ones need to be … 

    …there...
    @PieterCuijpers
    PieterCuijpers committed Nov 20, 2024
    Configuration menu
    Copy the full SHA
    a7eb6cc View commit details
    Browse the repository at this point in the history

  10. Adapted definition of OrderMonoidIso to apply to OrderMul in general.… 

    … (Renaming to OrderMulIso should be considered.)
    @PieterCuijpers
    PieterCuijpers committed Nov 20, 2024
    Configuration menu
    Copy the full SHA
    57b01f3 View commit details
    Browse the repository at this point in the history

  11. Started showing that OrderMulIso is a QuantaleHom (in particular an s… 

    …SupHom)
    @PieterCuijpers
    PieterCuijpers committed Nov 20, 2024
    Configuration menu
    Copy the full SHA
    5631270 View commit details
    Browse the repository at this point in the history

Commits on Nov 21, 2024

  1. Updated OrderMonoidIso theorems to not depend on MulOneClass but only… 

    … on Mul. Added proof that any OrderMonoidIso is a QuantaleHom
    @PieterCuijpers
    PieterCuijpers committed Nov 21, 2024
    Configuration menu
    Copy the full SHA
    9de5f05 View commit details
    Browse the repository at this point in the history

  2. Regenerated the import all files.

    @PieterCuijpers
    PieterCuijpers committed Nov 21, 2024
    Configuration menu
    Copy the full SHA
    6adb04d View commit details
    Browse the repository at this point in the history

  3. Merge remote-tracking branch 'origin' into PieterCuijpers_Quantales_H… 

    …omomorphism
    @PieterCuijpers
    PieterCuijpers committed Nov 21, 2024
    Configuration menu
    Copy the full SHA
    5201d35 View commit details
    Browse the repository at this point in the history

Commits on Nov 22, 2024

  1. Removed OneQuantaleHom definitions for the time being to get a cleane… 

    …r PR.

Added a number of theorems inspired by MonoidHom, but frankly I don't understand what I'm doing there yet.
    @PieterCuijpers
    PieterCuijpers committed Nov 22, 2024
    Configuration menu
    Copy the full SHA
    f42ed4d View commit details
    Browse the repository at this point in the history

  2. Added two forgotten doc_strings

    @PieterCuijpers
    PieterCuijpers committed Nov 22, 2024
    Configuration menu
    Copy the full SHA
    e29a83b View commit details
    Browse the repository at this point in the history

  3. Comment 'todo'

    @PieterCuijpers
    PieterCuijpers committed Nov 22, 2024
    Configuration menu
    Copy the full SHA
    fc8c7c1 View commit details
    Browse the repository at this point in the history

Commits on Nov 23, 2024

  1. A minus was missing before the toOrderHom docstring

    @PieterCuijpers
    PieterCuijpers committed Nov 23, 2024
    Configuration menu
    Copy the full SHA
    7e23b01 View commit details
    Browse the repository at this point in the history

  2. Merge remote-tracking branch 'origin' into PieterCuijpers_Quantales_H… 

    …omomorphism
    @PieterCuijpers
    PieterCuijpers committed Nov 23, 2024
    Configuration menu
    Copy the full SHA
    5189bc2 View commit details
    Browse the repository at this point in the history