feat(RingTheory/AdicCompletion): more APIs for IsAdicComplete

[jjdishere]

In this PR, we establish more APIs for IsAdicComplete.

1. Instead of checking the definition in IsPrecomplete (starting with a compatible sequence in M), we build APIs to lift elements (or maps) from compatible sequences in M ⧸ I ^ n • ⊤.
2. We also build APIs to lift a sequence of LinearMaps to LinearMap and a sequence of RingHoms to RingHom directly.
3. Since I * ⊤ is not definitionally equal to I, we build special APIs for the M = R case, enabling one to use R ⧸ I ^ n instead of R ⧸ I ^ n • ⊤.
4. We generalize the compatible sequence from defined on every M ⧸ I ^ n • ⊤ to only defined on M ⧸ I ^ a n • ⊤ for a strictly increasing sequence a n. (I would use the case a n = n + 1 in feat(RingTheory/Perfectoid): Fontaine's theta map and the de Rham period rings #21564 )

---

[mergify]

⚠️ The sha of the head commit of this PR conflicts with #21564. Mergify cannot evaluate rules on this PR. ⚠️

[github-actions]

PR summary c13c0b4820

Import changes for modified files

No significant changes to the import graph

Import changes for all files

Files	Import difference

---

Declarations diff

+ _root_.isHausdorff_iff
+ _root_.isPrecomplete_iff
+ eq_iff_smodEq
+ eq_iff_smodEq'
+ eq_iff_smodEq_of_strictMono
+ eq_iff_smodEq_of_strictMono'
+ eq_of_smodEq
+ eq_of_smodEq'
+ eq_one
+ eq_zero
+ eq_zero'
+ exists_pow_dvd
+ factor_eq_factor
+ function_of_eq_factorPow
+ function_of_eq_factorPow'
+ haus
+ limLinearMap
+ limRingHom
+ map_add
+ map_add'
+ map_mul
+ map_smul
+ mkQ_comp_limLinearMap
+ mk_comp_limRingHom
+ mk_limLinearMap
+ mk_limRingHom
+ of_SModEq_succ
+ of_eq_factorPow
+ of_eq_factorPow'
+ of_eq_factorPowSucc
+ of_eq_factorPowSucc'
+ prec
+ quotEquivOfEq_eq_factor
++ _
- IsHausdorff.eq_iff_smodEq
- IsHausdorff.haus
- IsPrecomplete.prec
- isHausdorff_iff
- isPrecomplete_iff

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

[riccardobrasca]

I had to stop at some point, but already a couple of comments.

[riccardobrasca]

Wouldn't be faster to prove that I ^ n • ⊤ = I ^ n (this is probably already there) and rw this? Or there is some type theoretic issue I don't see?

[riccardobrasca]

I am a bit skeptical that this lemma is not a special case of AdicCompletion.lift. Of course there is the same problem as above, and I am not against having a primed version to handle the case M = R, but the that is the standard formulation of the universal property.

[riccardobrasca]

I mean, you are expressing the universal property in the relevant category of algebras, right?

[jjdishere]

I mean, you are expressing the universal property in the relevant category of algebras, right?

Thank you for your careful review! These lemmas are used in the construction limRingHom (at line 355) and limLinearMap (at line 404). (Maybe I should rename them into liftRingHom and liftLinearMap) They are formulated in a way very similar to AdicCompletion.lift, which expresses the universal property of adic-completeness. They are formulated using the property IsAdicComplete instead of an explicit construction AdicCompletion.

For this map_add lemma, I found that it can be stated without any condition on N except for [Add N]. So I wrote down this general form here.

What do you think about these lemmas here? @riccardobrasca

[riccardobrasca]

Ah sorry, I didn't realize AdicCompletion.lift is only about the completion. Then I agree we want this. Why not calling it IsAdicComplete.lift? Putting aside for a moment the ring map version, I think you can just copy the API, and the names, of AdicCompletion.lift (I think we cannot remove it since the completion is not always complete).

[jjdishere]

Thank you for your advice! I'll rename it as IsAdicComplete.lift and copy APIs for it and names from AdicCompletion.lift. I think I would also leave several original lemmas unchanged since there are also cases people would like to construct single elements instead of a whole linear map using the universal property.

[riccardobrasca]

Yeah, if they're more general why not keeping them. Can you please add a comment saying where the "usual" universal property is? Also, IsAdicComplete.lift and AdicCompletion.lift should have comments relating them. here a reference for a completion that is not complete.

[jjdishere]

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