Skip to content

feat: InfinitePlace.Extension API for extensions of infinite places.#24881

Closed
smmercuri wants to merge 3 commits intomasterfrom
smmercuri/InfinitePlaceExtension
Closed

feat: InfinitePlace.Extension API for extensions of infinite places.#24881
smmercuri wants to merge 3 commits intomasterfrom
smmercuri/InfinitePlaceExtension

Conversation

@smmercuri
Copy link
Copy Markdown
Collaborator

@smmercuri smmercuri commented May 14, 2025

If L / K are fields and v : InfinitePlace K, then we define

  • v.Extension L : the subtype of w : InfinitePlace L whose restriction to K matches v.
  • isExtension_or_isExtension_conjugate : if w extends v, then either w.embedding extends v.embedding or conjugate w.embedding extends v.embedding
  • IsLift: class encoding the case where w extends v and w.embedding extends v.embedding.
  • IsConjugateLift: class encoding the case where w extends v and conjugate w.embedding extends v.embedding.

Open in Gitpod

@github-actions
Copy link
Copy Markdown

github-actions bot commented May 14, 2025

PR summary 5e4705b938

Import changes for modified files

No significant changes to the import graph

Import changes for all files
Files Import difference

Declarations diff

+ Extension
+ IsConjugateLift
+ IsConjugateLift.isExtension
+ IsExtension
+ IsExtension.ne
+ IsExtension.not_isExtension_conjugate
+ IsExtension.not_isReal_of_not_isReal
+ IsLift
+ IsLift.isExtension
+ IsMixedExtension
+ IsUnmixedExtension
+ IsUnmixedExtension.isReal_of_isReal
+ conjugate_comp
+ isComplex_of_isComplex
+ isExtension
+ isExtensionEquivSum
+ isExtension_conjugate_of_not_isExtension
+ isExtension_or_isExtension_conjugate
+ isLift_or_isConjugateLift
+ mk_embedding_comp
+ not_isReal
++ isReal

You can run this locally as follows 
## summary with just the declaration names:
./scripts/declarations_diff.sh <optional_commit>

## more verbose report:
./scripts/declarations_diff.sh long <optional_commit>

The doc-module for script/declarations_diff.sh contains some details about this script.

No changes to technical debt.

You can run this locally as

./scripts/technical-debt-metrics.sh pr_summary
  • The relative value is the weighted sum of the differences with weight given by the inverse of the current value of the statistic.
  • The absolute value is the relative value divided by the total sum of the inverses of the current values (i.e. the weighted average of the differences).

@smmercuri smmercuri mentioned this pull request May 14, 2025
Closed
9 tasks
@mathlib4-dependent-issues-bot
Copy link
Copy Markdown
Collaborator

mathlib4-dependent-issues-bot commented May 14, 2025

This PR/issue depends on:

@mathlib4-dependent-issues-bot mathlib4-dependent-issues-bot added the blocked-by-other-PR This PR depends on another PR (this label is automatically managed by a bot) label May 14, 2025
@leanprover-community-bot-assistant
Copy link
Copy Markdown
Collaborator

leanprover-community-bot-assistant commented Jun 4, 2025

This pull request has conflicts, please merge master and resolve them.

@leanprover-community-bot-assistant leanprover-community-bot-assistant added the merge-conflict The PR has a merge conflict with master, and needs manual merging. (this label is managed by a bot) label Jun 4, 2025
@grunweg grunweg added the t-number-theory Number theory (also use t-algebra or t-analysis to specialize) label Aug 4, 2025
@smmercuri smmercuri mentioned this pull request Aug 5, 2025
Closed
1 task
@smmercuri
Copy link
Copy Markdown
Collaborator Author

smmercuri commented Aug 5, 2025

This PR has been migrated to a fork-based workflow: #27978

@smmercuri smmercuri closed this Aug 5, 2025
@YaelDillies YaelDillies deleted the smmercuri/InfinitePlaceExtension branch August 18, 2025 07:25
mathlib-bors bot pushed a commit that referenced this pull request Oct 29, 2025
@smmercuri
feat(InfinitePlace/Ramification): LiesOver class for absolute value…
598a716 
…s and derived results on infinite places (#27978)

If `w` is an absolute value on `L/K` and `v` is an absolute value of `K` then `w.LiesOver v` is the class defining the property that `v` is the restriction of `w` to `K`.

This PR continues the work from #24881.

Original PR: #24881
BeibeiX0 pushed a commit to BeibeiX0/mathlib4 that referenced this pull request Nov 7, 2025
@smmercuri @BeibeiX0
feat(InfinitePlace/Ramification): LiesOver class for absolute value…
59bfd69 
…s and derived results on infinite places (leanprover-community#27978)

If `w` is an absolute value on `L/K` and `v` is an absolute value of `K` then `w.LiesOver v` is the class defining the property that `v` is the restriction of `w` to `K`.

This PR continues the work from leanprover-community#24881.

Original PR: leanprover-community#24881
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 (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) migrated-to-fork 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.

4 participants

@smmercuri @mathlib4-dependent-issues-bot @leanprover-community-bot-assistant @grunweg