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

Avoiding Algebra K (adicCompletion L w) diamond #230

Open
kbuzzard opened this issue Nov 25, 2024 · 2 comments
Open

Avoiding Algebra K (adicCompletion L w) diamond #230

kbuzzard opened this issue Nov 25, 2024 · 2 comments
Assignees
@YaelDillies

Comments

@kbuzzard
Copy link
Collaborator

If K,L are number fields, L is a K-algebra, and w is a nonzero prime of the integers of L, then right now mathlib provides a SMul K (adicCompletion L w) instance but not an Algebra K (adicCompletion L w) instance, so one has to tread carefully to avoid diamonds. This is a sorry in DedekindDomain/FiniteAdeleRing/BaseChange.lean but should be fixed in mathlib.

@YaelDillies is working on this.
@YaelDillies YaelDillies mentioned this issue Nov 25, 2024
Closed
@github-project-automation github-project-automation bot moved this to Unclaimed in FLT Project Dec 1, 2024
@kbuzzard
Copy link
Collaborator Author

kbuzzard commented Dec 1, 2024

@YaelDillies can you claim this?

@YaelDillies
Copy link
Contributor

claim

@kbuzzard kbuzzard moved this from Unclaimed to Claimed in FLT Project Dec 1, 2024
mathlib-bors bot pushed a commit to leanprover-community/mathlib4 that referenced this issue Dec 8, 2024
@YaelDillies
chore(AdicCompletion): generalise algebra instance to separate rings (#…
31530f3 
…19466)

In the existing instance `Algebra R (AdicCompletion I R)`, `R` appears three times: On the left, on the right, and in `I : Ideal R`. The left occurrence can be generalised to a ring `S` such that `R` is a `S`-algebra.

Closes ImperialCollegeLondon/FLT/issues/230.

From FLT
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Assignees

@YaelDillies YaelDillies

Labels
None yet
Projects
FLT Project
Status: Claimed
Milestone
No milestone
2 participants
@YaelDillies @kbuzzard