[Merged by Bors] - feat(RingTheory/Perfectoid): define the untilt map and generalize pretilt by jjdishere · Pull Request #21563 · leanprover-community/mathlib4

jjdishere · 2025-02-07T19:41:37Z

In this PR,

we generalize the definition of the pretilt and
define the untilt function from the pretilt of a p-adically complete ring to the ring itself.

The results about pretilt and tilt are kept unchanged as much as possible. They will be generalized in future PRs.

github-actions · 2025-02-07T19:42:33Z

PR summary 9052e95d07

Import changes for modified files

No significant changes to the import graph

Import changes for all files

Files	Import difference
`Mathlib.RingTheory.Perfectoid.Untilt` (new file)	1839

Declarations diff

+ IsHausdorff.eq_iff_smodEq
+ _root_.sub_smodEq_zero
+ exists_smodEq_untiltAux
+ instance : CharP (PreTilt O p) p
+ instance : CommRing (PreTilt O p)
+ instance [Fact p.Prime] [hvp : Fact (v p ≠ 1)] : Field (Tilt K v O hv p)
+ isDomain
+ mk_comp_untilt_eq_coeff_zero
+ mk_out
+ mk_untilt_eq_coeff_zero
+ nontrivial
+ pow_dvd_mul_untiltAux_sub_untiltAux_mul
+ pow_dvd_one_untiltAux_sub_one
+ pow_dvd_untiltAux_sub_untiltAux
+ untilt
+ untiltAux
+ untiltAux_smodEq_untiltFun
+ untiltFun
- instance : CharP (PreTilt K v O hv p) p
- instance : CommRing (PreTilt K v O hv p)
- instance [Fact p.Prime] [Fact (v p ≠ 1)] : Field (Tilt K v O hv p)
- instance [hp : Fact p.Prime] : IsDomain (PreTilt K v O hv p) := by
- instance [hp : Fact p.Prime] [Fact (v p ≠ 1)] : Nontrivial (ModP K v O hv p)

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.

Decrease in tech debt: (relative, absolute) = (3.00, 0.00)

Current number	Change	Type
3363	-3	porting notes

Current commit 9052e95d07
Reference commit c3c9f71b3b

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

Mathlib/RingTheory/Perfection.lean

Co-authored-by: github-actions[bot] <41898282+github-actions[bot]@users.noreply.github.com>

riccardobrasca

Thanks!

bors d+

Mathlib/LinearAlgebra/SModEq.lean

Mathlib/RingTheory/AdicCompletion/Basic.lean

riccardobrasca · 2025-02-14T12:37:15Z

Mathlib/RingTheory/Perfection.lean

-@[nolint unusedArguments]
-def ModP (K : Type u₁) [Field K] (v : Valuation K ℝ≥0) (O : Type u₂) [CommRing O] [Algebra O K]
-    (_ : v.Integers O) (p : ℕ) :=
+def ModP :=


This looks like an improvement to me, but do you know what was the reason for the previous definition?

I'm not sure what the concrete reason is here. All the following sections share the same variables here.

Mathlib/RingTheory/Perfectoid/Untilt.lean

mathlib-bors · 2025-02-14T12:43:25Z

✌️ jjdishere can now approve this pull request. To approve and merge a pull request, simply reply with bors r+. More detailed instructions are available here.

Co-authored-by: Riccardo Brasca <[email protected]>

…b.com/leanprover-community/mathlib4 into jiedong_jiang_integral_perfectoid_psu

jjdishere · 2025-02-20T09:55:34Z

bors r+

…tilt (#21563) In this PR, 1. we generalize the definition of the pretilt and 2. define the untilt function from the pretilt of a p-adically complete ring to the ring itself. The results about pretilt and tilt are kept unchanged as much as possible. They will be generalized in future PRs. Co-authored-by: Jiang Jiedong <[email protected]>

mathlib-bors · 2025-02-20T10:21:50Z

This PR was included in a batch that was canceled, it will be automatically retried

…tilt (#21563) In this PR, 1. we generalize the definition of the pretilt and 2. define the untilt function from the pretilt of a p-adically complete ring to the ring itself. The results about pretilt and tilt are kept unchanged as much as possible. They will be generalized in future PRs. Co-authored-by: Jiang Jiedong <[email protected]>

mathlib-bors · 2025-02-20T11:11:00Z

Pull request successfully merged into master.

Build succeeded:

* origin/master: (823 commits) chore(Computability): fix naming of lemmas about Sum.inl, Sum.inr, Sum.casesOn (#22156) feat: `Fintype Ordering` (#22154) chore: more renamings to fit the naming convention (#22148) feat(CategoryTheory): any monomorphism in a Grothendieck abelian category is a transfinite composition of pushouts of monomorphisms in a small family (#22157) chore: rename `{Continuous., continuous_}sum_map` to `sumMap` (#22155) chore: remove initial space followed by `-/` (#22158) chore: make arg in HeightOneSpectrum.valuation explicit (#22139) feat(Data/List): `List.maximum` is monotone (#22091) chore(Combinatorics/SimpleGraph): extract WalkDecomp from Walk (#21981) feat: if a monoid M acts, then so does (s : S) with [SubmonoidClass S M] (#21123) chore: backport changes to `getElem` lemmas (#22146) feat(CategoryTheory): generating monomorphisms in Grothendieck abelian categories (#22150) feat: rename variables to fit doc (#22143) feat(CategoryTheory): IsDetecting.isIso_iff_of_mono (#22135) feat(CategoryTheory): truncations of transfinite compositions (#22149) chore: simplify a proof (#22134) feat(CategoryTheory): monomorphisms are stable under coproducts in Grothendieck abelian categories (#22133) feat(Order): Set.Ici.isSuccLimit_coe (#22103) chore(Analysis/Convex/Normed): split into smaller files (#22015) feat(Algebra/Algebra/Lie): max nilpotent ideal <= radical (#22140) refactor(LinearIndependent): refactor to use LinearIndepOn (#21886) chore: rename some more `Foo.sum_elim` -> `sumElim` (#22130) chore: rename Injective.sum_elim and friends (#22129) chore: fix naming oversight from #22070 (#22128) chore: fix spelling mistakes (#22136) feat(RingTheory/Ideal/Quotient): define transtition map between ring or module quotient by powers of ideal (#21900) fix: initialize_simps_projections print warning when projection data already exists (#20339) chore: rename ContMDiff.sum_{elim,map} (#22131) feat(CategoryTheory): characterization of injective objects in terms of lifting properties (#22104) chore(Lean,Tactic): un-indent some doc-strings (#22118) feat(Algebra/MvPolynomial): add `comp` versions of rename lemmas (#21259) chose: add deprecation (#22124) feat(CategoryTheory/Abelian/GrothendieckCategory): computing colimits in Subobject (#22123) feat(CategoryTheory/Subobject): hasCardinalLT_of_mono (#22122) feat: add `DenseRange.piMap` (#22114) feat(Algebra/Algebra/Lie): define the maximal nilpotent ideal of Lie algebras (#22061) chore(Data/Finset): don't import algebra when defining `Finset.card` (#21866) feat: a function on a discrete space is smooth (#22113) feat: commutative group objects in additive categories (#21521) style(Geometry/Manifold): remove superfluous indentation in doc-strings (#22117) chore: rename PushNeg.lean to Push.lean (#22108) feat: add Is{Open,Closed}Embedding.sum_elim (#22070) feat(RingTheory/Perfectoid): define the untilt map and generalize pretilt (#21563) feature(Topology/Algebra/Module/WeakBilin): Linear map from F into the topological dual of E with the weak topology (#21078) feat(CategoryTheory/Abelian): the exact sequence attached to a pushout square (#22110) chore(ChartedSpace.lean): group constructions together (#22107) feat(CategoryTheory/MorphismProperty): more basic API (#22099) chore(Data/Fintype): split `Fintype/Card.lean` (#21840) chore(SetTheory/Cardinal/Cofinality): make `IsStrongLimit` into a structure (#21971) feat(Combinatorics/SimpleGraph): Add a theorem about cliques in induced subgraphs (#20705) ...

jjdishere added 8 commits February 3, 2025 20:04

fix non-finishing simp

4a3cd3f

finish proof

a7294b3

delete unused file

acd93bb

reference

3a9a9ab

comments

54f0f47

Merge branch 'master' into jiedong_jiang_integral_perfectoid_psu

f1a2d57

relocate lemmas

6183344

mk_all

978f6c9

jjdishere added t-number-theory Number theory (also use t-algebra or t-analysis to specialize) t-algebra Algebra (groups, rings, fields, etc) labels Feb 7, 2025

jjdishere commented Feb 7, 2025

View reviewed changes

Mathlib/RingTheory/Perfection.lean Outdated Show resolved Hide resolved

Update Mathlib/RingTheory/Perfection.lean

78ad72e

jjdishere commented Feb 7, 2025

View reviewed changes

Mathlib/RingTheory/Perfection.lean Outdated Show resolved Hide resolved

jjdishere and others added 3 commits February 8, 2025 03:43

Update Mathlib/RingTheory/Perfection.lean

322c0c6

Update docs/references.bib

6e8f950

Co-authored-by: github-actions[bot] <41898282+github-actions[bot]@users.noreply.github.com>

Update SModEq.lean

9a7e149

This was referenced Feb 7, 2025

feat(RingTheory/Perfectoid): Fontaine's theta map and the de Rham period rings #21564

Closed

Tracking issue: The Tilting Equivalence of Perfectoid Fields #18696

Open

riccardobrasca self-assigned this Feb 14, 2025

riccardobrasca approved these changes Feb 14, 2025

View reviewed changes

ghost added the delegated This pull request has been delegated to the PR author (or occasionally another non-maintainer). label Feb 14, 2025

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 Feb 17, 2025

jjdishere and others added 6 commits February 20, 2025 16:53

Update Mathlib/RingTheory/Perfectoid/Untilt.lean

aaad7ff

Co-authored-by: Riccardo Brasca <[email protected]>

Update Mathlib/RingTheory/Perfectoid/Untilt.lean

182ad9c

Co-authored-by: Riccardo Brasca <[email protected]>

Update Mathlib/RingTheory/Perfectoid/Untilt.lean

9b777c4

Co-authored-by: Riccardo Brasca <[email protected]>

fix

a3602c0

Merge branch 'jiedong_jiang_integral_perfectoid_psu' of https://githu…

4de5ee4

…b.com/leanprover-community/mathlib4 into jiedong_jiang_integral_perfectoid_psu

Merge branch 'master' into jiedong_jiang_integral_perfectoid_psu

b438bd5

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 Feb 20, 2025

fix perfection

9052e95

mathlib-bors bot changed the title ~~feat(RingTheory/Perfectoid): define the untilt map and generalize pretilt~~ [Merged by Bors] - feat(RingTheory/Perfectoid): define the untilt map and generalize pretilt Feb 20, 2025

mathlib-bors bot closed this Feb 20, 2025

mathlib-bors bot deleted the jiedong_jiang_integral_perfectoid_psu branch February 20, 2025 11:11

Provide feedback

Saved searches

Use saved searches to filter your results more quickly

[Merged by Bors] - feat(RingTheory/Perfectoid): define the untilt map and generalize pretilt#21563

[Merged by Bors] - feat(RingTheory/Perfectoid): define the untilt map and generalize pretilt#21563
jjdishere wants to merge 19 commits intomasterfrom
jiedong_jiang_integral_perfectoid_psu

jjdishere commented Feb 7, 2025 •

edited

Loading

Uh oh!

github-actions bot commented Feb 7, 2025 •

edited

Loading

Declarations diff

Uh oh!

Uh oh!

Uh oh!

riccardobrasca left a comment

Uh oh!

Uh oh!

Uh oh!

riccardobrasca Feb 14, 2025

Uh oh!

jjdishere Feb 20, 2025

Uh oh!

Uh oh!

Uh oh!

Uh oh!

Uh oh!

mathlib-bors bot commented Feb 14, 2025

Uh oh!

jjdishere commented Feb 20, 2025

Uh oh!

mathlib-bors bot commented Feb 20, 2025

Uh oh!

mathlib-bors bot commented Feb 20, 2025

Uh oh!

Reviewers

Assignees

Labels

Projects

Milestone

Development

Uh oh!

3 participants

Conversation

jjdishere commented Feb 7, 2025 • edited Loading Uh oh! There was an error while loading. Please reload this page.

Uh oh!

Uh oh!

github-actions bot commented Feb 7, 2025 • edited Loading Uh oh! There was an error while loading. Please reload this page.

Uh oh!

PR summary 9052e95d07

Import changes for modified files

Declarations diff

Uh oh!

Uh oh!

Uh oh!

riccardobrasca left a comment

Choose a reason for hiding this comment

Uh oh!

Uh oh!

Uh oh!

riccardobrasca Feb 14, 2025

Choose a reason for hiding this comment

Uh oh!

jjdishere Feb 20, 2025

Choose a reason for hiding this comment

Uh oh!

Uh oh!

Uh oh!

Uh oh!

Uh oh!

mathlib-bors bot commented Feb 14, 2025

Uh oh!

jjdishere commented Feb 20, 2025

Uh oh!

mathlib-bors bot commented Feb 20, 2025

Uh oh!

mathlib-bors bot commented Feb 20, 2025

Uh oh!

Reviewers

Assignees

Labels

Projects

Milestone

Development

Uh oh!

3 participants

jjdishere commented Feb 7, 2025 •

edited

Loading

github-actions bot commented Feb 7, 2025 •

edited

Loading