Skip to content

[Merged by Bors] - feat(RingTheory/AdicCompletion): injectivity/surjectivity of AdicCompletion.lift - #25927

Closed
jjdishere wants to merge 115 commits into
leanprover-community:masterfrom
jjdishere:jiedong_jiang_is_adic_complete
Closed

[Merged by Bors] - feat(RingTheory/AdicCompletion): injectivity/surjectivity of AdicCompletion.lift#25927
jjdishere wants to merge 115 commits into
leanprover-community:masterfrom
jjdishere:jiedong_jiang_is_adic_complete

Conversation

@jjdishere

@jjdishere jjdishere commented Jun 15, 2025

Copy link
Copy Markdown
Collaborator

This PR continues the work from #21582.

Original PR: #21582

jjdishere and others added 30 commits February 3, 2025 20:04
@jjdishere
fix non-finishing simp
4a3cd3f
@jjdishere
finish proof
a7294b3
@jjdishere
delete unused file
acd93bb
@jjdishere
Revert "delete unused file"
7f053c6 
This reverts commit acd93bb.
@jjdishere
reference
3a9a9ab
@jjdishere
comments
54f0f47
@jjdishere
Merge branch 'master' into jiedong_jiang_integral_perfectoid_psu
f1a2d57
@jjdishere
relocate lemmas
6183344
@jjdishere
mk_all
978f6c9
@jjdishere
Update Mathlib/RingTheory/Perfection.lean
78ad72e
@jjdishere
Update Mathlib/RingTheory/Perfection.lean
322c0c6
@jjdishere @github-actions
Update docs/references.bib
6e8f950 
Co-authored-by: github-actions[bot] <41898282+github-actions[bot]@users.noreply.github.com>
@jjdishere
Merge branch 'jiedong_jiang_integral_perfectoid_psu' into jiedong_jia…
5cb0b02 
…ng_fontaine_theta
@jjdishere
Update SModEq.lean
9a7e149
@jjdishere
Merge branch 'jiedong_jiang_integral_perfectoid_psu' into jiedong_jia…
51bf9ad 
…ng_fontaine_theta
@jjdishere @github-actions
Update Mathlib.lean
8bc669b 
Co-authored-by: github-actions[bot] <41898282+github-actions[bot]@users.noreply.github.com>
@jjdishere
fix a typo
bc2ab3b
@jjdishere
Merge branch 'jiedong_jiang_fontaine_theta' of https://github.com/lea…
cfeb701 
…nprover-community/mathlib4 into jiedong_jiang_fontaine_theta
@jjdishere
More api's for adic complete
5c3aa9b
@jjdishere
finish proof
d1c42d0
@jjdishere
relocate lemmas
8648743
@jjdishere
remove other files
943b918
@jjdishere
mk_all
b17507e
@jjdishere
reverse changes in other PR
d77eef4
@jjdishere
Update docs/references.bib
0209d43
@jjdishere
Update docs/references.bib
60a41f4
@jjdishere
add doc string
c2f0240
@jjdishere
Merge branch 'jiedong_jiang_is_adic_complete' of https://github.com/l…
64d8240 
…eanprover-community/mathlib4 into jiedong_jiang_is_adic_complete
@Thmoas-Guan
define transtition map between quotient powers
10b2fb6
@Thmoas-Guan
Update Mathlib.lean
989392e
@mathlib4-merge-conflict-bot mathlib4-merge-conflict-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 Oct 30, 2025
@mathlib4-merge-conflict-bot

mathlib4-merge-conflict-bot commented Oct 30, 2025

Copy link
Copy Markdown
Collaborator

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

@github-actions github-actions 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 Oct 31, 2025
@mathlib4-merge-conflict-bot mathlib4-merge-conflict-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 Nov 1, 2025
@mathlib4-merge-conflict-bot

mathlib4-merge-conflict-bot commented Nov 1, 2025

Copy link
Copy Markdown
Collaborator

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

@github-actions github-actions 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 Nov 2, 2025
riccardobrasca
riccardobrasca reviewed Nov 5, 2025
View reviewed changes

@riccardobrasca riccardobrasca left a comment

Copy link
Copy Markdown
Member

Choose a reason for hiding this comment

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

Can you try to split the PR? I have the impression you do various things, and the PR is quite big.

Comment thread Mathlib/RingTheory/AdicCompletion/Algebra.lean Outdated
Comment thread Mathlib/RingTheory/AdicCompletion/Basic.lean Outdated
Comment thread Mathlib/RingTheory/AdicCompletion/Basic.lean Outdated
@jjdishere

jjdishere commented Nov 5, 2025 •
edited
Loading

Copy link
Copy Markdown
Collaborator Author

Can you try to split the PR? I have the impression you do various things, and the PR is quite big.

@riccardobrasca OK, I have split the PR into 4 smaller PRs.

  1. Showing that .of is injective/surjective if and only if IsHausdorff/IsPrecomplete, define .ofLinearEquiv. (the current one)
  2. Using 1, define IsAdicComplete.lift and show its universal properties. ([Merged by Bors] - feat(RingTheory/AdicCompletion): universal property of IsAdicComplete #31295)
  3. Generalizing 2 to a version that only takes M/I^ a n as input instead of M/I^n for every n. ([Merged by Bors] - feat(RingTheory/AdicCompletion): generalize universal property of IsAdicComplete #31296)
  4. Copying everything from the module version to the ring version. ([Merged by Bors] - feat(RingTheory/AdicCompletion): IsAdicComplete.lift APIs for RingHoms #31298)

The only disadvantage is that each of these PRs depends on the previous one linearly... It would be a long queue.

@jjdishere jjdishere mentioned this pull request Nov 5, 2025
Closed
1 task
erdOne
erdOne reviewed Nov 5, 2025
View reviewed changes
Comment thread Mathlib/RingTheory/AdicCompletion/Basic.lean Outdated
@jjdishere jjdishere changed the title feat(RingTheory/AdicCompletion): more APIs for IsAdicComplete feat(RingTheory/AdicCompletion): injectivity/surjectivity of AdicCompletion.lift Nov 6, 2025
@riccardobrasca

riccardobrasca commented Nov 6, 2025

Copy link
Copy Markdown
Member

Thanks!

bors merge

@ghost ghost added the ready-to-merge This PR has been sent to bors. label Nov 6, 2025
mathlib-bors Bot pushed a commit that referenced this pull request Nov 6, 2025
@jjdishere @kckennylau cirno
feat(RingTheory/AdicCompletion): injectivity/surjectivity of `AdicCom…
2ea7c11 
…pletion.lift` (#25927)

This PR continues the work from #21582.

Original PR: #21582

Co-authored-by: Jiedong Jiang <emailboxofjjd@163.com>
Co-authored-by: Kenny Lau <kc_kennylau@yahoo.com.hk>
Co-authored-by: jjdishere <emailboxofjjd@163.com>
Co-authored-by: cirno <cirno@shiguna.moe>
@mathlib-bors

mathlib-bors Bot commented Nov 6, 2025

Copy link
Copy Markdown
Contributor

Pull request successfully merged into master.

Build succeeded:

@mathlib-bors mathlib-bors Bot changed the title feat(RingTheory/AdicCompletion): injectivity/surjectivity of AdicCompletion.lift [Merged by Bors] - feat(RingTheory/AdicCompletion): injectivity/surjectivity of AdicCompletion.lift Nov 6, 2025
@mathlib-bors mathlib-bors Bot closed this Nov 6, 2025
@jjdishere jjdishere mentioned this pull request Nov 18, 2025
Closed
1 task
mathlib-bors Bot pushed a commit that referenced this pull request Nov 19, 2025
@jjdishere
feat(RingTheory/AdicCompletion): IsAdicComplete.lift APIs for `Ring…
2a03d8a 
…Homs` (#31298)

In this PR, we build every API of the module version `IsAdicComplete.lift` for the ring version `IsAdicComplete.liftRingHom`. Mainly copying APIs in #25927, #31295, #31296.
This would be used in #26388.

Co-authored-by: Jiedong Jiang <emailboxofjjd@163.com>
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment

Reviewers

@riccardobrasca riccardobrasca riccardobrasca left review comments
@erdOne erdOne erdOne left review comments
@chrisflav chrisflav Awaiting requested review from chrisflav

Assignees

@erdOne erdOne

@mariainesdff mariainesdff

Labels

ready-to-merge This PR has been sent to bors. t-ring-theory Ring theory

Projects

None yet

Milestone

No milestone

Development

Successfully merging this pull request may close these issues.

8 participants

@jjdishere @mathlib4-merge-conflict-bot @riccardobrasca @erdOne @grunweg @mariainesdff @Thmoas-Guan @kckennylau