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(AlgebraicGeometry/EllipticCurve/Group): compute range of baseChange #10142

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

feat(AlgebraicGeometry/EllipticCurve/Group): compute range of baseChange #10142

wants to merge 18 commits into from
+421 −212

Conversation

Multramate
Copy link
Collaborator

@Multramate Multramate commented Jan 31, 2024 •
edited by alreadydone
Loading

@Multramate
Refactor base change for ring homomorphisms
a3c6b48
@Multramate
Rename baseChange to map
a40af5d
@Multramate
Merge remote-tracking branch 'origin/master' into EllipticCurve.Map
46d07ac
@Multramate
Fix merge error
4b8189b
@Multramate
Revert notation
55d723f
@Multramate
Rearrange map_baseChange lemmas
642c344
@Multramate
Relocate universes
d878f75
@Multramate
Define DistribMulAction.fixedSubgroup
5d20a5b
@Multramate
Define homomorphisms of subgroups induced by homomorphisms of groups
4804a83
@Multramate
Merge branch 'DistribMulAction.fixedSubgroup' into MonoidHom.fixedSub…
3abab1f 
…groupMap
@Multramate
Define homomorphisms of fixed subgroups induced by homomorphisms of g…
eb8e8ef 
…roups
@Multramate
Rename DistribMulAction.fixedSubgroup to FixedPoints.subgroup
2b345b7
@Multramate
Merge branch 'DistribMulAction.fixedSubgroup' into MonoidHom.fixedSub…
e27c235 
…groupMap
@Multramate
Merge branch 'MonoidHom.fixedSubgroupMap' into EllipticCurve.DistribM…
0b2063f 
…ulAction
@Multramate
Compute range of baseChange
63d5dac
@Multramate Multramate added blocked-by-other-PR This PR depends on another PR to Mathlib (this label is automatically managed by a bot) awaiting-review awaiting-CI t-number-theory Number theory (also use t-algebra or t-analysis to specialize) t-algebraic-geometry Algebraic geometry labels Jan 31, 2024
@leanprover-community-mathlib4-bot
Copy link
Collaborator

leanprover-community-mathlib4-bot commented Jan 31, 2024 •
edited
Loading

This PR/issue depends on:

@alreadydone
Copy link
Contributor

Why does this PR need to change so much existing material? Can you separate out the refactoring from the new material?

@Multramate
Copy link
Collaborator Author

Why does this PR need to change so much existing material? Can you separate out the refactoring from the new material?

Oh whoops. This is supposed to depend on another PR that I forgot to include in the list of dependencies. The other PR was meant to change all the names to reflect the distinction between map and baseChange

@leanprover-community-mathlib4-bot leanprover-community-mathlib4-bot added the merge-conflict The PR has a merge conflict with master, and needs manual merging. (this label is managed by a bot) label Feb 1, 2024
@leanprover-community-mathlib4-bot leanprover-community-mathlib4-bot removed the merge-conflict The PR has a merge conflict with master, and needs manual merging. (this label is managed by a bot) label Feb 1, 2024
@leanprover-community-mathlib4-bot leanprover-community-mathlib4-bot added the merge-conflict The PR has a merge conflict with master, and needs manual merging. (this label is managed by a bot) label Feb 19, 2024
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Reviewers
No reviews
Assignees
No one assigned
Labels
blocked-by-other-PR This PR depends on another PR to Mathlib (this label is automatically managed by a bot) merge-conflict The PR has a merge conflict with master, and needs manual merging. (this label is managed by a bot) t-algebraic-geometry Algebraic geometry t-number-theory Number theory (also use t-algebra or t-analysis to specialize)
Projects
None yet
Milestone
No milestone
Development

Successfully merging this pull request may close these issues.
5 participants
@Multramate @leanprover-community-mathlib4-bot @alreadydone @kim-em @YaelDillies