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(geometry/manifold): stab at diffeomorphisms #4351

Closed
wants to merge 94 commits into from
Closed

[Merged by Bors] - feat(geometry/manifold): stab at diffeomorphisms #4351

wants to merge 94 commits into from

Commits on Jul 4, 2020

  1. recreated the problem

    @Nicknamen
    Nicknamen committed Jul 4, 2020
    Copy the full SHA
    03df6e2 View commit details
    Browse the repository at this point in the history

Commits on Jul 13, 2020

  1. Proved that continuous functions are an algebra

    @Nicknamen
    Nicknamen committed Jul 13, 2020
    Copy the full SHA
    80b9cab View commit details
    Browse the repository at this point in the history

  2. Merge branch 'master' into continuous_functions_algebra

    @Nicknamen
    Nicknamen committed Jul 13, 2020
    Copy the full SHA
    d8ad078 View commit details
    Browse the repository at this point in the history

  3. Solving a conflict appeared in sheaves

    @Nicknamen
    Nicknamen committed Jul 13, 2020
    Copy the full SHA
    56d2716 View commit details
    Browse the repository at this point in the history

  4. Corrected a mistake in the documentation

    @Nicknamen
    Nicknamen committed Jul 13, 2020
    Copy the full SHA
    da64672 View commit details
    Browse the repository at this point in the history

  5. Solved a DANGEROUS INSTANCE problem

    @Nicknamen
    Nicknamen committed Jul 13, 2020
    Copy the full SHA
    53b8e04 View commit details
    Browse the repository at this point in the history

  6. Forgot to remove #lint

    @Nicknamen
    Nicknamen committed Jul 13, 2020
    Copy the full SHA
    fee8ca8 View commit details
    Browse the repository at this point in the history

  7. Making lint happy

    @Nicknamen
    Nicknamen committed Jul 13, 2020
    Copy the full SHA
    dc6197b View commit details
    Browse the repository at this point in the history

  8. Trying again to make lint happy

    @Nicknamen
    Nicknamen committed Jul 13, 2020
    Copy the full SHA
    b807d94 View commit details
    Browse the repository at this point in the history

Commits on Jul 15, 2020

  1. Algebra structure over continuous bundled functions

    @Nicknamen
    Nicknamen committed Jul 15, 2020
    Copy the full SHA
    4652e8a View commit details
    Browse the repository at this point in the history

  2. Trying to merge

    @Nicknamen
    Nicknamen committed Jul 15, 2020
    Copy the full SHA
    20866d7 View commit details
    Browse the repository at this point in the history

  3. Having problems with the merging

    @Nicknamen
    Nicknamen committed Jul 15, 2020
    Copy the full SHA
    99cee94 View commit details
    Browse the repository at this point in the history

Commits on Jul 16, 2020

  1. Updated the code following smooth manifolds PR

    @Nicknamen
    Nicknamen committed Jul 16, 2020
    Copy the full SHA
    ac6c3ba View commit details
    Browse the repository at this point in the history

  2. Merge branch 'master' into Lie_groups

    @Nicknamen
    Nicknamen committed Jul 16, 2020
    Copy the full SHA
    c8f1304 View commit details
    Browse the repository at this point in the history

  3. Merge branch 'master' into continuous_functions_algebra

    @Nicknamen
    Nicknamen committed Jul 16, 2020
    Copy the full SHA
    f31adad View commit details
    Browse the repository at this point in the history

  4. Merge branch 'continuous_functions_algebra' into continuous_bundled_map

    @Nicknamen
    Nicknamen committed Jul 16, 2020
    Copy the full SHA
    fd3efc7 View commit details
    Browse the repository at this point in the history

  5. Added some documentation

    @Nicknamen
    Nicknamen committed Jul 16, 2020
    Copy the full SHA
    a9bdde6 View commit details
    Browse the repository at this point in the history

  6. Merge branch 'Lie_groups' into smooth_map

    @Nicknamen
    Nicknamen committed Jul 16, 2020
    Copy the full SHA
    1c3e998 View commit details
    Browse the repository at this point in the history

Commits on Jul 17, 2020

  1. Begun writing smooth_functions

    @Nicknamen
    Nicknamen committed Jul 17, 2020
    Copy the full SHA
    f91678e View commit details
    Browse the repository at this point in the history

  2. Merge branch 'master' into Lie_groups

    @Nicknamen
    Nicknamen committed Jul 17, 2020
    Copy the full SHA
    46af74b View commit details
    Browse the repository at this point in the history

  3. Added some documentation

    @Nicknamen
    Nicknamen committed Jul 17, 2020
    Copy the full SHA
    f5abebf View commit details
    Browse the repository at this point in the history

  4. Trying to show to Wojtek the excessive memory consumption

    @Nicknamen
    Nicknamen committed Jul 17, 2020
    Copy the full SHA
    5288ed0 View commit details
    Browse the repository at this point in the history

Commits on Jul 18, 2020

  1. Merge branch 'master' into continuous_functions_algebra

    @Nicknamen
    Nicknamen committed Jul 18, 2020
    Copy the full SHA
    3f5fa6d View commit details
    Browse the repository at this point in the history

  2. Forgot to save files before last commit.

    @Nicknamen
    Nicknamen committed Jul 18, 2020
    Copy the full SHA
    ee83faa View commit details
    Browse the repository at this point in the history

  3. Merge branch 'master' into continuous_functions_algebra

    @Nicknamen
    Nicknamen committed Jul 18, 2020
    Copy the full SHA
    37a21d4 View commit details
    Browse the repository at this point in the history

  4. Merge branch 'continuous_functions_algebra' into has_continuous_mul

    @Nicknamen
    Nicknamen committed Jul 18, 2020
    Copy the full SHA
    629ad00 View commit details
    Browse the repository at this point in the history

  5. Merge branch 'has_continuous_mul' into continuous_bundled_map

    @Nicknamen
    Nicknamen committed Jul 18, 2020
    Copy the full SHA
    ee812a2 View commit details
    Browse the repository at this point in the history

  6. Added some further documentation

    @Nicknamen
    Nicknamen committed Jul 18, 2020
    Copy the full SHA
    283dd6e View commit details
    Browse the repository at this point in the history

  7. Merge branch 'continuous_bundled_map' into smooth_map

    @Nicknamen
    Nicknamen committed Jul 18, 2020
    Copy the full SHA
    3a3011d View commit details
    Browse the repository at this point in the history

  8. Merge branch 'continuous_bundled_map' into Lie_groups

    @Nicknamen
    Nicknamen committed Jul 18, 2020
    Copy the full SHA
    fcb4714 View commit details
    Browse the repository at this point in the history

  9. Fixed dangerous instance

    @Nicknamen
    Nicknamen committed Jul 18, 2020
    Copy the full SHA
    8e358bc View commit details
    Browse the repository at this point in the history

Commits on Jul 19, 2020

  1. Began implementing the smooth name

    @Nicknamen
    Nicknamen committed Jul 19, 2020
    Copy the full SHA
    a8ef625 View commit details
    Browse the repository at this point in the history

Commits on Jul 20, 2020

  1. halfway through the work on smooth maps

    @Nicknamen
    Nicknamen committed Jul 20, 2020
    Copy the full SHA
    2bfd38d View commit details
    Browse the repository at this point in the history

Commits on Jul 22, 2020

  1. Begun generalizing constructions

    @Nicknamen
    Nicknamen committed Jul 22, 2020
    Copy the full SHA
    81c590d View commit details
    Browse the repository at this point in the history

  2. Merge branch 'master' into Lie_groups

    @Nicknamen
    Nicknamen committed Jul 22, 2020
    Copy the full SHA
    4fd7e93 View commit details
    Browse the repository at this point in the history

Commits on Jul 23, 2020

  1. Ready to PR with help-needed

    @Nicknamen
    Nicknamen committed Jul 23, 2020
    Copy the full SHA
    d99d42e View commit details
    Browse the repository at this point in the history

  2. Merge branch 'master' into Lie_groups

    @Nicknamen
    Nicknamen committed Jul 23, 2020
    Copy the full SHA
    2e49c6e View commit details
    Browse the repository at this point in the history

  3. Adjust a mistake in last merge

    @Nicknamen
    Nicknamen committed Jul 23, 2020
    Copy the full SHA
    9bbf9b3 View commit details
    Browse the repository at this point in the history

Commits on Jul 24, 2020

  1. complete times_cont_mdiff_within_at.prod_map

    @sgouezel
    sgouezel committed Jul 24, 2020
    Copy the full SHA
    4ebee58 View commit details
    Browse the repository at this point in the history

  2. Merge branch 'Lie_groups' into smooth_map

    @Nicknamen
    Nicknamen committed Jul 24, 2020
    Copy the full SHA
    4c62301 View commit details
    Browse the repository at this point in the history

  3. Merge branch 'master' into smooth_map

    @Nicknamen
    Nicknamen committed Jul 24, 2020
    Copy the full SHA
    0dda2b5 View commit details
    Browse the repository at this point in the history

  4. smoothness of projections

    @sgouezel
    sgouezel committed Jul 24, 2020
    Copy the full SHA
    0cedba6 View commit details
    Browse the repository at this point in the history

  5. proof terms

    @sgouezel
    sgouezel committed Jul 24, 2020
    Copy the full SHA
    10142d0 View commit details
    Browse the repository at this point in the history

Commits on Jul 25, 2020

  1. Some progress on smooth maps

    @Nicknamen
    Nicknamen committed Jul 25, 2020
    Copy the full SHA
    a1319a5 View commit details
    Browse the repository at this point in the history

Commits on Jul 26, 2020

  1. Applied most of suggested changes

    @Nicknamen
    Nicknamen committed Jul 26, 2020
    Copy the full SHA
    ddd0b02 View commit details
    Browse the repository at this point in the history

  2. Linter

    @Nicknamen
    Nicknamen committed Jul 26, 2020
    Copy the full SHA
    0a73ef2 View commit details
    Browse the repository at this point in the history

  3. minor changes

    @Nicknamen
    Nicknamen committed Jul 26, 2020
    Copy the full SHA
    485debf View commit details
    Browse the repository at this point in the history

  4. For Patrick: real numbers are a Lie group

    @Nicknamen
    Nicknamen committed Jul 26, 2020
    Copy the full SHA
    726ed6c View commit details
    Browse the repository at this point in the history

Commits on Jul 27, 2020

  1. Merge branch 'master' into Lie_groups

    @Nicknamen
    Nicknamen committed Jul 27, 2020
    Copy the full SHA
    1503909 View commit details
    Browse the repository at this point in the history

  2. Changed folder name

    @Nicknamen
    Nicknamen committed Jul 27, 2020
    Copy the full SHA
    b17d3d5 View commit details
    Browse the repository at this point in the history

  3. fix build

    @sgouezel
    sgouezel committed Jul 27, 2020
    Copy the full SHA
    6a7aeba View commit details
    Browse the repository at this point in the history

  4. Merge remote-tracking branch 'upstream/master' into Lie_groups

    @sgouezel
    sgouezel committed Jul 27, 2020
    Copy the full SHA
    34fd3b9 View commit details
    Browse the repository at this point in the history

  5. Merge branch 'Lie_groups' into smooth_map

    @Nicknamen
    Nicknamen committed Jul 27, 2020
    Copy the full SHA
    0c15a40 View commit details
    Browse the repository at this point in the history

  6. Random commit

    @Nicknamen
    Nicknamen committed Jul 27, 2020
    Copy the full SHA
    2a9c58b View commit details
    Browse the repository at this point in the history

  7. minor changes

    @Nicknamen
    Nicknamen committed Jul 27, 2020
    Copy the full SHA
    92fe915 View commit details
    Browse the repository at this point in the history

  8. streamline some proofs

    @sgouezel
    sgouezel committed Jul 27, 2020
    Copy the full SHA
    652e523 View commit details
    Browse the repository at this point in the history

Commits on Jul 28, 2020

  1. Update src/geometry/algebra/lie_group.lean 

    Co-authored-by: sgouezel <sebastien.gouezel@univ-rennes1.fr>
    @Nicknamen @sgouezel
    Nicknamen and sgouezel committed Jul 28, 2020
    Copy the full SHA
    9c32b00 View commit details
    Browse the repository at this point in the history

  2. Update src/geometry/algebra/lie_group.lean 

    Co-authored-by: sgouezel <sebastien.gouezel@univ-rennes1.fr>
    @Nicknamen @sgouezel
    Nicknamen and sgouezel committed Jul 28, 2020
    Copy the full SHA
    d6eb4ff View commit details
    Browse the repository at this point in the history

  3. Random commit

    @Nicknamen
    Nicknamen committed Jul 28, 2020
    Copy the full SHA
    f2e1b61 View commit details
    Browse the repository at this point in the history

  4. Merge branch 'Lie_groups' of https://github.com/leanprover-community/… 

    …mathlib into Lie_groups
    @Nicknamen
    Nicknamen committed Jul 28, 2020
    Copy the full SHA
    41d4149 View commit details
    Browse the repository at this point in the history

  5. Applied most of suggested changes

    @Nicknamen
    Nicknamen committed Jul 28, 2020
    Copy the full SHA
    3ceb3e9 View commit details
    Browse the repository at this point in the history

Commits on Jul 29, 2020

  1. Applied suggested changes

    @Nicknamen
    Nicknamen committed Jul 29, 2020
    Copy the full SHA
    82f3a0d View commit details
    Browse the repository at this point in the history

Commits on Jul 30, 2020

  1. linter

    @Nicknamen
    Nicknamen committed Jul 30, 2020
    Copy the full SHA
    2a1abc6 View commit details
    Browse the repository at this point in the history

  2. Merge branch 'Lie_groups' into smooth_map

    @Nicknamen
    Nicknamen committed Jul 30, 2020
    Copy the full SHA
    475c401 View commit details
    Browse the repository at this point in the history

  3. Proved smooth functions valued in smooth algebra are algebra

    @Nicknamen
    Nicknamen committed Jul 30, 2020
    Copy the full SHA
    5c95d71 View commit details
    Browse the repository at this point in the history

Commits on Jul 31, 2020

  1. Finished proofs of the PR

    @Nicknamen
    Nicknamen committed Jul 31, 2020
    Copy the full SHA
    4cf09b7 View commit details
    Browse the repository at this point in the history

  2. Merge branch 'master' into smooth_map

    @Nicknamen
    Nicknamen committed Jul 31, 2020
    Copy the full SHA
    8ea7f16 View commit details
    Browse the repository at this point in the history

  3. Reorganized files

    @Nicknamen
    Nicknamen committed Jul 31, 2020
    Copy the full SHA
    0d68a6d View commit details
    Browse the repository at this point in the history

  4. Trying to fix the errors of the merge

    @Nicknamen
    Nicknamen committed Jul 31, 2020
    Copy the full SHA
    4466d90 View commit details
    Browse the repository at this point in the history

  5. Fixed some errors

    @Nicknamen
    Nicknamen committed Jul 31, 2020
    Copy the full SHA
    964085a View commit details
    Browse the repository at this point in the history

  6. Most of Linter

    @Nicknamen
    Nicknamen committed Jul 31, 2020
    Copy the full SHA
    f2b74bd View commit details
    Browse the repository at this point in the history

  7. Solved dangerous instance problem

    @Nicknamen
    Nicknamen committed Jul 31, 2020
    Copy the full SHA
    4fe39f0 View commit details
    Browse the repository at this point in the history

Commits on Aug 1, 2020

  1. Improved notation

    @Nicknamen
    Nicknamen committed Aug 1, 2020
    Copy the full SHA
    e9f9fcb View commit details
    Browse the repository at this point in the history

Commits on Aug 4, 2020

  1. Applied some of the suggested changes

    @Nicknamen
    Nicknamen committed Aug 4, 2020
    Copy the full SHA
    770974c View commit details
    Browse the repository at this point in the history

Commits on Aug 5, 2020

  1. Done some progress

    @Nicknamen
    Nicknamen committed Aug 5, 2020
    Copy the full SHA
    28ee5e9 View commit details
    Browse the repository at this point in the history

Commits on Aug 6, 2020

  1. Merge branch 'master' into smooth_map

    @Nicknamen
    Nicknamen committed Aug 6, 2020
    Copy the full SHA
    7a7b852 View commit details
    Browse the repository at this point in the history

  2. Partial progress

    @Nicknamen
    Nicknamen committed Aug 6, 2020
    Copy the full SHA
    31ebd60 View commit details
    Browse the repository at this point in the history

Commits on Aug 9, 2020

  1. Going back

    @Nicknamen
    Nicknamen committed Aug 9, 2020
    Copy the full SHA
    b514761 View commit details
    Browse the repository at this point in the history

  2. Random commit

    @Nicknamen
    Nicknamen committed Aug 9, 2020
    Copy the full SHA
    9a349d2 View commit details
    Browse the repository at this point in the history

  3. Merge branch 'master' into smooth_map

    @Nicknamen
    Nicknamen committed Aug 9, 2020
    Copy the full SHA
    1ccee56 View commit details
    Browse the repository at this point in the history

  4. Random_commit

    @Nicknamen
    Nicknamen committed Aug 9, 2020
    Copy the full SHA
    0f989f6 View commit details
    Browse the repository at this point in the history

  5. Let's PR the easy stuff first

    @Nicknamen
    Nicknamen committed Aug 9, 2020
    Copy the full SHA
    ef30bdb View commit details
    Browse the repository at this point in the history

Commits on Aug 13, 2020

  1. Updated documentation

    @Nicknamen
    Nicknamen committed Aug 13, 2020
    Copy the full SHA
    f07e1f6 View commit details
    Browse the repository at this point in the history

Commits on Aug 16, 2020

  1. Began to generalize to C^n

    @Nicknamen
    Nicknamen committed Aug 16, 2020
    Copy the full SHA
    d3bea89 View commit details
    Browse the repository at this point in the history

  2. Merge branch 'smooth_map' into diffeomorph

    @Nicknamen
    Nicknamen committed Aug 16, 2020
    Copy the full SHA
    2ad5f2c View commit details
    Browse the repository at this point in the history

Commits on Aug 17, 2020

  1. First stab at diffeomorph

    @Nicknamen
    Nicknamen committed Aug 17, 2020
    Copy the full SHA
    c1b1247 View commit details
    Browse the repository at this point in the history

  2. Merge branch 'master' into smooth_map

    @Nicknamen
    Nicknamen committed Aug 17, 2020
    Copy the full SHA
    2e9a515 View commit details
    Browse the repository at this point in the history

  3. Some better idea for generalization

    @Nicknamen
    Nicknamen committed Aug 17, 2020
    Copy the full SHA
    8da7097 View commit details
    Browse the repository at this point in the history

  4. Merge branch 'smooth_map' into diffeomorph

    @Nicknamen
    Nicknamen committed Aug 17, 2020
    Copy the full SHA
    03b9b05 View commit details
    Browse the repository at this point in the history

Commits on Oct 1, 2020

  1. Merge branch 'master' into diffeomorph

    @Nicknamen
    Nicknamen committed Oct 1, 2020
    Copy the full SHA
    5fb264c View commit details
    Browse the repository at this point in the history

  2. Added last basic lemmas and defs

    @Nicknamen
    Nicknamen committed Oct 1, 2020
    Copy the full SHA
    1c66b05 View commit details
    Browse the repository at this point in the history

  3. Linter

    @Nicknamen
    Nicknamen committed Oct 1, 2020
    Copy the full SHA
    ec15949 View commit details
    Browse the repository at this point in the history

Commits on Oct 12, 2020

  1. Applied suggested changes

    @Nicknamen
    Nicknamen committed Oct 12, 2020
    Copy the full SHA
    f5b68ed View commit details
    Browse the repository at this point in the history

  2. Merge branch 'master' into diffeomorph

    @Nicknamen
    Nicknamen committed Oct 12, 2020
    Copy the full SHA
    3490c3d View commit details
    Browse the repository at this point in the history