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(algebra/free_algebra): Define a grading #4321

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

feat(algebra/free_algebra): Define a grading #4321

wants to merge 41 commits into from

Commits on Oct 3, 2020

  1. feat(algebra/free_algebra): Add an inductive principle

    @eric-wieser
    eric-wieser committed Oct 3, 2020
    Configuration menu
    Copy the full SHA
    957b483 View commit details
    Browse the repository at this point in the history

  2. chore(algebra/free_algebra): Use a subtype instead of a struct

    @eric-wieser
    eric-wieser committed Oct 3, 2020
    Configuration menu
    Copy the full SHA
    e789702 View commit details
    Browse the repository at this point in the history

  3. chore(algebra/free_algebra): Disable false positive linter

    @eric-wieser
    eric-wieser committed Oct 3, 2020
    Configuration menu
    Copy the full SHA
    87d31ff View commit details
    Browse the repository at this point in the history

  4. chore(algebra/free_algebra): Tidy up coercions

    @eric-wieser
    eric-wieser committed Oct 3, 2020
    Configuration menu
    Copy the full SHA
    778e9db View commit details
    Browse the repository at this point in the history

Commits on Oct 6, 2020

  1. refactor(algebra/free_algebra): Replace most of the code with subalgebra

    @eric-wieser
    eric-wieser committed Oct 6, 2020
    Configuration menu
    Copy the full SHA
    67e8211 View commit details
    Browse the repository at this point in the history

  2. fix(*): remove squeeze_simp

    @eric-wieser
    eric-wieser committed Oct 6, 2020
    Configuration menu
    Copy the full SHA
    28b1893 View commit details
    Browse the repository at this point in the history

Commits on Oct 7, 2020

  1. Merge remote-tracking branch 'origin/master' into eric-wieser/free_al… 

    …gebra-induction
    @eric-wieser
    eric-wieser committed Oct 7, 2020
    Configuration menu
    Copy the full SHA
    ed419ec View commit details
    Browse the repository at this point in the history

  2. chore(*): Tidy the proof

    @eric-wieser
    eric-wieser committed Oct 7, 2020
    Configuration menu
    Copy the full SHA
    d816bfa View commit details
    Browse the repository at this point in the history

  3. Add induction for the exterior algebra too

    @eric-wieser
    eric-wieser committed Oct 7, 2020
    Configuration menu
    Copy the full SHA
    aff1486 View commit details
    Browse the repository at this point in the history

Commits on Oct 12, 2020

  1. feat(data/monoid_algebra): Add missing has_coe_to_fun instance

    @eric-wieser
    eric-wieser committed Oct 12, 2020
    Configuration menu
    Copy the full SHA
    9f22aa6 View commit details
    Browse the repository at this point in the history

  2. feat(algebra/free_algebra): Attempt to define a grading 

    The grading takes the form `free_algebra R X ≃ₐ[R] add_monoid_algebra (free_algebra R X) ℕ`
    @eric-wieser
    eric-wieser committed Oct 12, 2020
    Configuration menu
    Copy the full SHA
    e75b7ef View commit details
    Browse the repository at this point in the history

  3. Death throes of a failed attempt

    @eric-wieser
    eric-wieser committed Oct 12, 2020
    Configuration menu
    Copy the full SHA
    21ca265 View commit details
    Browse the repository at this point in the history

  4. feat(algebra/free_algebra): A few lemmas about grades of free algebras 

    The grading takes the form `free_algebra R X →ₐ[R] add_monoid_algebra (free_algebra R X) ℕ`

It's likely that there are more generic lemmas about grading that can be shared with `tensor_algebra` and friends, but that's left to follow-up work
    @eric-wieser
    eric-wieser committed Oct 12, 2020
    Configuration menu
    Copy the full SHA
    62a77f0 View commit details
    Browse the repository at this point in the history

  5. chore(*): Remove duplication between sum_id and lift

    @eric-wieser
    eric-wieser committed Oct 12, 2020
    Configuration menu
    Copy the full SHA
    fd54b8d View commit details
    Browse the repository at this point in the history

  6. fix(*): Solve merge mistake

    @eric-wieser
    eric-wieser committed Oct 12, 2020
    Configuration menu
    Copy the full SHA
    234ff72 View commit details
    Browse the repository at this point in the history

  7. wip

    @eric-wieser
    eric-wieser committed Oct 12, 2020
    Configuration menu
    Copy the full SHA
    eec3c2b View commit details
    Browse the repository at this point in the history

  8. chore(algebra/monoid_algebra): Replace algebra_map' with `single_(z… 

    …ero|one)_ring_hom`

 `algebra_map'` is now trivially equal to `single_(zero|one)_ring_hom.comp`, so is no longer needed.
    @eric-wieser
    eric-wieser committed Oct 12, 2020
    Configuration menu
    Copy the full SHA
    81aa68b View commit details
    Browse the repository at this point in the history

  9. Merge branch 'eric-wieser/single-hom' into eric-wieser/free_algebra-g… 

    …rading
    @eric-wieser
    eric-wieser committed Oct 12, 2020
    Configuration menu
    Copy the full SHA
    f999d1a View commit details
    Browse the repository at this point in the history

  10. wip

    @eric-wieser
    eric-wieser committed Oct 12, 2020
    Configuration menu
    Copy the full SHA
    abaa760 View commit details
    Browse the repository at this point in the history

  11. wip

    @eric-wieser
    eric-wieser committed Oct 12, 2020
    Configuration menu
    Copy the full SHA
    b63b36c View commit details
    Browse the repository at this point in the history

  12. Merge branch 'eric-wieser/free_algebra-induction' into eric-wieser/fr… 

    …ee_algebra-grading

# Conflicts:
#	src/algebra/free_algebra.lean
    @eric-wieser
    eric-wieser committed Oct 12, 2020
    Configuration menu
    Copy the full SHA
    e5b725e View commit details
    Browse the repository at this point in the history

  13. Revert unrelated changes

    @eric-wieser
    eric-wieser committed Oct 12, 2020
    Configuration menu
    Copy the full SHA
    b702aab View commit details
    Browse the repository at this point in the history

  14. Merge branch 'master' of github.com:leanprover-community/mathlib into… 

    … eric-wieser/free_algebra-grading
    @eric-wieser
    eric-wieser committed Oct 12, 2020
    Configuration menu
    Copy the full SHA
    51900f9 View commit details
    Browse the repository at this point in the history

  15. Fix bad merge

    @eric-wieser
    eric-wieser committed Oct 12, 2020
    Configuration menu
    Copy the full SHA
    5489c46 View commit details
    Browse the repository at this point in the history

Commits on Oct 13, 2020

  1. Merge remote-tracking branch 'origin/master' into eric-wieser/free_al… 

    …gebra-grading
    @eric-wieser
    eric-wieser committed Oct 13, 2020
    Configuration menu
    Copy the full SHA
    3ce401d View commit details
    Browse the repository at this point in the history

  2. wip

    @eric-wieser
    eric-wieser committed Oct 13, 2020
    Configuration menu
    Copy the full SHA
    38d3e48 View commit details
    Browse the repository at this point in the history

  3. feat(algebra/algebra/basic): Add map_finsupp_(sum|prod) to `alg_(ho… 

    …m|equiv)`
    @eric-wieser
    eric-wieser committed Oct 13, 2020
    Configuration menu
    Copy the full SHA
    082ca79 View commit details
    Browse the repository at this point in the history

  4. Merge branch 'eric-wieser/alg_hom.map_finsupp_sum' into eric-wieser/f… 

    …ree_algebra-grading
    @eric-wieser
    eric-wieser committed Oct 13, 2020
    Configuration menu
    Copy the full SHA
    99b4ac1 View commit details
    Browse the repository at this point in the history

  5. Cleanup some more

    @eric-wieser
    eric-wieser committed Oct 13, 2020
    Configuration menu
    Copy the full SHA
    303117d View commit details
    Browse the repository at this point in the history

  6. feat(algebra/algebra/basic): Add map_finsupp_(sum|prod) to `alg_(ho… 

    …m|equiv)`
    @eric-wieser
    eric-wieser committed Oct 13, 2020
    Configuration menu
    Copy the full SHA
    40b1eb8 View commit details
    Browse the repository at this point in the history

  7. Merge branch 'eric-wieser/alg_hom.map_finsupp_sum' into eric-wieser/f… 

    …ree_algebra-grading
    @eric-wieser
    eric-wieser committed Oct 13, 2020
    Configuration menu
    Copy the full SHA
    1a5eaa9 View commit details
    Browse the repository at this point in the history

  8. Fix the proof

    @eric-wieser
    eric-wieser committed Oct 13, 2020
    Configuration menu
    Copy the full SHA
    06e16f5 View commit details
    Browse the repository at this point in the history

Commits on Oct 19, 2020

  1. Merge remote-tracking branch 'origin/master' into eric-wieser/free_al… 

    …gebra-grading
    @eric-wieser
    eric-wieser committed Oct 19, 2020
    Configuration menu
    Copy the full SHA
    9c41969 View commit details
    Browse the repository at this point in the history

  2. Cleanup the proofs

    @eric-wieser
    eric-wieser committed Oct 19, 2020
    Configuration menu
    Copy the full SHA
    2d979c3 View commit details
    Browse the repository at this point in the history

Commits on Oct 20, 2020

  1. Merge remote-tracking branch 'origin/master' into eric-wieser/free_al… 

    …gebra-grading
    @eric-wieser
    eric-wieser committed Oct 20, 2020
    Configuration menu
    Copy the full SHA
    bee9b3c View commit details
    Browse the repository at this point in the history

  2. Update src/algebra/monoid_algebra.lean

    @eric-wieser
    eric-wieser committed Oct 20, 2020
    Configuration menu
    Copy the full SHA
    caaa54d View commit details
    Browse the repository at this point in the history

Commits on Oct 26, 2020

  1. Merge remote-tracking branch 'origin/master' into eric-wieser/free_al… 

    …gebra-grading
    @eric-wieser
    eric-wieser committed Oct 26, 2020
    Configuration menu
    Copy the full SHA
    33f38c7 View commit details
    Browse the repository at this point in the history

  2. wip

    @eric-wieser
    eric-wieser committed Oct 26, 2020
    Configuration menu
    Copy the full SHA
    db82059 View commit details
    Browse the repository at this point in the history

Commits on Oct 28, 2020

  1. Merge branch 'master' of github.com:leanprover-community/mathlib into… 

    … eric-wieser/free_algebra-grading
    @eric-wieser
    eric-wieser committed Oct 28, 2020
    Configuration menu
    Copy the full SHA
    986ed3c View commit details
    Browse the repository at this point in the history

  2. fix(*): adjust for changed lemmas

    @eric-wieser
    eric-wieser committed Oct 28, 2020
    Configuration menu
    Copy the full SHA
    1d0b9c9 View commit details
    Browse the repository at this point in the history

Commits on Dec 4, 2020

  1. Merge branch 'master' into eric-wieser/free_algebra-grading

    @eric-wieser
    eric-wieser committed Dec 4, 2020
    Configuration menu
    Copy the full SHA
    7c58060 View commit details
    Browse the repository at this point in the history