Skip to content

[Merged by Bors] - feat: roots have non-zero length wrt the canonical form of a finite crystallographic root pairing#19645

Closed
ocfnash wants to merge 2 commits intomasterfrom
ocfnash/root_ne_zero
Closed

[Merged by Bors] - feat: roots have non-zero length wrt the canonical form of a finite crystallographic root pairing#19645
ocfnash wants to merge 2 commits intomasterfrom
ocfnash/root_ne_zero

Conversation

@ocfnash
Copy link
Copy Markdown
Contributor

@ocfnash ocfnash commented Nov 30, 2024 •
edited
Loading

We also relocate some other unrelated lemmas in order to relax the assumptions on their scalars, and add fill out some loosely-related API.

The only mathematical result is RootPairing.rootForm_apply_root_self_ne_zero.

Open in Gitpod

@ocfnash
feat: roots have non-zero length wrt the canonical form of a finite c…
fc7f608 
…rystallographic root pairing

We also relocate some other unrelated lemmas in order to relax the assumptions on their scalars.
@ocfnash ocfnash added the t-algebra Algebra (groups, rings, fields, etc) label Nov 30, 2024
@github-actions
Copy link
Copy Markdown

github-actions bot commented Nov 30, 2024 •
edited
Loading

PR summary 1f63783884

Import changes for modified files

No significant changes to the import graph

Import changes for all files
Files Import difference

Declarations diff

+ IsCrystallographic.flip
+ coPolarization_apply_eq_zero_iff
+ corootForm_apply_apply
+ corootForm_apply_coroot_self_ne_zero
+ flip_comp_polarization_eq_rootForm
+ instance : EquivLike (PerfectPairing R M N) M (Dual R N)
+ instance : LinearEquivClass (PerfectPairing R M N) R M (Dual R N)
+ polarization_apply_eq_zero_iff
+ rootForm_apply_root_self_ne_zero
+ self_comp_coPolarization_eq_corootForm

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).

@ocfnash
Copy link
Copy Markdown
Contributor Author

ocfnash commented Nov 30, 2024 •
edited
Loading

This should allow us to generalise the key result RootPairing.finrank_corootSpan_eq to allow for any integral domain of characteristic zero (rather than just ordered rings).

OTOH we need to assume P.IsCrystallographic. I do not see a common generalisation of ordered scalars and crystallographic so in order to unify the work we may wish to introduce a typeclass definition which states that P.RootForm (P.root i) (P.root i) ≠ 0 (or perhaps something more general) and then create instances lemmas for finite root pairings over ordered scalars, as well as crystallographic root pairings over characteristic-zero integral domains.

Edit: probably the thing to explore is how far one can get just by assuming RootPairing.pairing takes values in an ordered subring. I'll explore this if I have time.

@ocfnash ocfnash requested a review from jcommelin November 30, 2024 22:02
@ocfnash ocfnash force-pushed the ocfnash/root_ne_zero branch from d1f4162 to 1f63783 Compare December 1, 2024 16:40
@ocfnash ocfnash added the awaiting-CI This PR does not pass CI yet. This label is automatically removed once it does. label Dec 1, 2024
@github-actions github-actions bot removed the awaiting-CI This PR does not pass CI yet. This label is automatically removed once it does. label Dec 1, 2024
jcommelin
jcommelin reviewed Dec 2, 2024
View reviewed changes
Copy link
Copy Markdown
Member

@jcommelin jcommelin left a comment

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Thanks 🎉

bors merge

@ghost ghost added the ready-to-merge This PR has been sent to bors. label Dec 2, 2024
mathlib-bors bot pushed a commit that referenced this pull request Dec 2, 2024
@ocfnash
feat: roots have non-zero length wrt the canonical form of a finite c…
62a0adf 
…rystallographic root pairing (#19645)

We also relocate some other unrelated lemmas in order to relax the assumptions on their scalars, and add fill out some loosely-related API.

The only mathematical result is `RootPairing.rootForm_apply_root_self_ne_zero`.
@mathlib-bors
Copy link
Copy Markdown
Contributor

mathlib-bors bot commented Dec 2, 2024

Pull request successfully merged into master.

Build succeeded:

@mathlib-bors mathlib-bors bot changed the title feat: roots have non-zero length wrt the canonical form of a finite crystallographic root pairing [Merged by Bors] - feat: roots have non-zero length wrt the canonical form of a finite crystallographic root pairing Dec 2, 2024
@mathlib-bors mathlib-bors bot closed this Dec 2, 2024
@mathlib-bors mathlib-bors bot deleted the ocfnash/root_ne_zero branch December 2, 2024 13:44
@ocfnash ocfnash mentioned this pull request Dec 3, 2024
Closed
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment

Reviewers

@jcommelin jcommelin jcommelin left review comments

@ScottCarnahan ScottCarnahan Awaiting requested review from ScottCarnahan

Assignees

No one assigned

Labels

ready-to-merge This PR has been sent to bors. t-algebra Algebra (groups, rings, fields, etc)

Projects

None yet

Milestone

No milestone

Development

Successfully merging this pull request may close these issues.

2 participants

@ocfnash @jcommelin