chore(RingTheory): adapt Perfectoid field draft to current master (revival) - #20
Open
sfingali wants to merge 7490 commits into
Open
chore(RingTheory): adapt Perfectoid field draft to current master (revival)#20sfingali wants to merge 7490 commits into
sfingali wants to merge 7490 commits into
Conversation
…-community#41573) This PR fixes the `Presieve.pullback` docstring, which said the pullback of `R` along `f : X ⟶ Y` consists of all `g : Z ⟶ X` such that `f ≫ g` is in `R`; the definition uses `R (g ≫ f)`, and `f ≫ g` is not even well-typed, so the docstring now says `g ≫ f`. Follow-up to [leanprover-community#40527 (feat(CategoryTheory/Sites): pushforward and pullback of presieves)](leanprover-community#40527). 🤖 Prepared with Claude Code
…1901) This PR updates the Mathlib dependencies.
This PR fixes four docstring typos in `Mathlib/AlgebraicTopology/SimplicialSet/`: "simplcial" → "simplicial" in `Nonsingular.iso`, the broken code reference `s : X : N` → `s : X.N` (plus a missing final period) in `N.toSemiSimplexCategory`, a stray trailing semicolon in `stdSimplex.fullyFaithful`, and "the colimit of the its monogenous subcomplexes" → "the colimit of its monogenous subcomplexes" in `isColimitCoconeN`. Follow-up to [leanprover-community#40254 (feat(AlgebraicTopology): nonsingular simplicial set is colimit of standard simplices)](leanprover-community#40254). 🤖 Prepared with Claude Code
…ty#41581) This PR makes three cosmetic fixes in `Mathlib/AlgebraicTopology/Reedy/Basic.lean`: replace the ASCII `<-` with `←` in the proof of `degHom_comp_le_right`, fix the grammar typo "degree of a morphisms" in the docstring of `degHom`, and delete the unused `universe u` declaration. Follow-up to [leanprover-community#41141 (feat(AlgebraicTopology): Reedy structures)](leanprover-community#41141). 🤖 Prepared with Claude Code
I am happy to remove some nolints for you!
…et (leanprover-community#41160) This PR adds: ```lean theorem det_eq_birdDet {n : Nat} (A : Array R) (hA : A.size = n * n) : Matrix.det (Matrix.ofArray (m := n) (n := n) A hA) = birdDet n A ``` showing that Bird's determinant algorithm computes `Matrix.det`. The PR also adds: - `BirdDet.Spec.birdDet` - an alternative implementation of Bird's algorithm that's stated in terms of `Matrix` instead of `Array`. Co-authored-by: Oliver Nash <github@olivernash.org> Co-authored-by: Oliver Nash <7734364+ocfnash@users.noreply.github.com> Co-authored-by: Johan Commelin <johan@commelin.net>
…40911) This closely mirrors `Mathlib/RingTheory/Ideal/GoingDown.lean` by defining an analogous predicate `Algebra.HasGoingUp` and proving basic properties. It includes: - `Algebra.HasGoingUp.iff_specializingMap_primeSpectrumComap`: going up is equivalent to specializations lifting along `Spec S → Spec R`. - `Algebra.HasGoingUp.of_isIntegral`: integral algebras satisfy going up. - `Ideal.exists_ltSeries_of_hasGoingUp`: a generalization of `exists_ideal_over_prime_of_isIntegral_of_isPrime` from `Mathlib/RingTheory/Ideal/GoingUp.lean` to chains of arbitrary length. This was previously an explicitly marked `TODO`.
… and differentiable (leanprover-community#41027) This will be used to prove that the Levi-Civita connection is smooth. From the path towards the Levi-Civita connection and Riemannian geometry.
…stabilises (leanprover-community#38488) ...and does so in a bounded number of steps (which is why this is Finset-specific). In a later PR, I'll add this for endofunctions on a fintype, as well as add a Set.Finite version.
Update the documentation for consistency, and to contrast with `codRestrict` which is prevalent.
…edgeFinset_inf` (leanprover-community#41789) Unlike `edgeFinset_sup`, `edgeFinset_inf` only accepts `Fintype` instances for `G` and `H` and not their inf, relying on the [`fintypeEdgeSetInf`](https://leanprover-community.github.io/mathlib4_docs/Mathlib/Combinatorics/SimpleGraph/Basic.html#SimpleGraph.fintypeEdgeSetInf) instance providing it. This means the theorem can't be used with a different `Fintype (G₁ ⊓ G₂).edgeSet`.
…is (leanprover-community#41582) This PR removes the `p₁ ≠ p₂` hypothesis from `Sphere.center_mem_affineSpan_pair_iff_isDiameter`: the iff also holds when the points coincide (both sides then say `p₁ = s.center`), and the neighbouring `isDiameter_iff_*` lemmas carry no distinctness hypotheses. The degenerate case is handled by a one-line `simp`. Follow-up to [leanprover-community#41143 (feat(Geometry/Euclidean/Sphere): lemmas about points on a sphere)](leanprover-community#41143). 🤖 Prepared with Claude Code
…nprover-community#41837) Add an adaptation note to `set_option` for `rightUnitor_inv_left_snd` to mark that the option is required to avoid changing auto-generated lemma signatures. This is important so that a (future follow-up to) `scripts/rm_set_option.py` doesn't automatically delete it, otherwise it would break the build for that CI workflow. See [this Zulip thread](https://leanprover.zulipchat.com/#narrow/channel/287929-mathlib4/topic/4.2E33.2E0-rc1.20Multiple.20.60respectTransparency.60-related.20issues/near/611153200).
Regex search ←\w. Replace `rw [←a, ...]` with `rw [← a, ...]` etc. I check the replacements in tactic file are unproblematic Co-authored-by: Batixx <s59fpern@uni-bonn.de>
…braic number (leanprover-community#41605) This PR defines the absolute height of an algebraic number. The proof that this definition does not depend on the choice of ambient number field is in leanprover-community#41606, but it would be nice to have this definition in mathlib earlier for statements in a downstream repo. Co-authored-by: tb65536 <thomas.l.browning@gmail.com>
…idations (leanprover-community#41825) The `post_steps` "verify that everything was available in the cache" step reads the cache back with the PR branch's own `lake exe cache get`, while CI writes it with master's `cache` binary. For fork PRs those are different binaries, so a PR that changes the cache tool's key space (e.g. a `rootHashGeneration` bump in a toolchain bump) reads a different key space than the one the cache was written under and misses every file, hard-failing a build whose cache is in fact correct. Make the verify step warn-and-continue on such a miss, but only when it is an expected key-space invalidation: the build is a fork PR (`github.event.pull_request.head.repo.fork`, the same signal that sends the write path to master's binary) and this PR's `Cache/` differs from master's. Every non-fork build (master, bors, dev branches) reads and writes with one binary, so a miss there is a hard failure, as is an unchanged `Cache/` or an unavailable baseline.
…meomorph` (leanprover-community#41045) This is a continuation of leanprover-community#39084.
…anprover-community#31187) Define the L-function of a modular form (showing it is meromorphic on C and agrees with the naive Dirichlet series for `re s` large).
…nprover-community#41897) This PR fixes a typo in the name of a recently added theorem. Co-authored-by: tb65536 <thomas.l.browning@gmail.com>
…Ring` (leanprover-community#41969) In this PR we generalize projective dimension results about `ModuleCat` to `Ring`, also adding a better doc.
…eanprover-community#40500) Construct `Spec` as a functor from `R`-Hopf algebras to group schemes over `Spec R`, show it is full and faithful and has affine group schemes as essential image. From Toric, FLT Co-authored-by: Andrew Yang <the.erd.one@gmail.com> Co-authored-by: Michał Mrugała <kiolterino@gmail.com> Co-authored-by: Christian Merten <christian@merten.dev>
… in its support (leanprover-community#40288) API for FreeAbelianGroup, a can rw as a sum over the elements in its support
…noetherian ring when the index is finite (leanprover-community#40205) This is a split of leanprover-community#36507 which includes `isEmptyEquiv`, `optionEquivLeft` and `finSuccEquiv`. We use `finSuccEquiv` to show multivariable power series ring over a noetherian ring is a noetherian ring when the index is finite.
…-community#42300) This is in preparation for disallowing `NormedSpace` in `Analysis.Seminorm`.
…ear in the type (leanprover-community#42228) This PR fixes a bug in `to_dual`/`to_additive` that makes it impossible to use it on a structure where a universe level doesn't appear in its type.
…leanprover-community#42303) This PR adds a universe annotation in `algΓAlgSpecAdjunction`, which was seemingly forgotten. This speeds it up by more that 10x. In the rest of the file, the universe is already specified everywhere. For an explanation of why a universe metavariable can cause such an enormous slowdown, see leanprover/lean4#10414
…representations (leanprover-community#42151) Add a missing surjectivity lemma `surjective_or_eq_zero` for irreducible representations, parallel to the existing `injective_or_eq_zero` `bijective_or_eq_zero`.
…f instead of aesop (leanprover-community#41870) The file speeds up by 25%, with significant impact on readability.
…munity#41876) This PR adds the config option `linter.style.header.license` to the header linter. This allows downstream projects to use the linter on their projects even if they need to specify a different license or a different filename for the license.
…-community#42006) Replace the `CommRing` instance with `Ring`.
…orsion free to faithful smul (leanprover-community#41379) This PR removes some `IsDomain` assumptions by generalizing `Module.IsTorsionFree` to `FaithfulSMul`. (As @SnirBroshi pointed out in the comments, this is not quite a generalization when the top ring is the zero ring, but this never arises in practice). Co-authored-by: tb65536 <thomas.l.browning@gmail.com>
…community#42229) After [batteries#1927](leanprover-community/batteries#1927) is merged: - [x] Merge leanprover-community/mathlib4:master - [x] Edit the lakefile to point to leanprover-community/batteries:main - [x] Run lake update batteries - [ ] Wait for CI and merge Co-authored-by: mathlib-nightly-testing[bot] <mathlib-nightly-testing[bot]@users.noreply.github.com>
add field docstrings (docBlame linter)
add the Mathlib.lean import
add field docstrings (docBlame linter)
style: remove spaces before semicolons in quoted docstrings
Wedhorn, Rem. 7.30 (pp. 62-63): R(T/s) = R(T ∪ {s}/s); R(T/s) is open for
s a unit; the intersection of rational subsets is rational (one direction;
the reverse needs ordered-group cancellation and is noted in the project).
Revival of leanprover-community#26389 (co-author): fixes the API drift (structure syntax, IsUniformAddGroup/IsTopologicalDivisionRing renames, universe levels). Compiles against master; the 13 sorries are the remaining mathematical work (val_p_lt_1, IsTopologicalNilpotent, the Tilt instance, the alg-closed iff).
Scholze, Lemma 3.2 (p. 15) first half: v(p) < 1 from the pseudo-uniformizer condition (p ∈ (π^p) for a non-unit π ∈ 𝒪). Stated with the class's own valuation (ValuedPerfectoidField); the ∃-valuation form would need the equivalence-of-valuations machinery (noted). Also: fix the remaining API drift in the draft (universe binder, def-not-instance for ofFiniteDimensional, Tilt arg order). 13 sorries left, all annotated.
… parked on ValueGroup₀ bridge) Sketch + annotation in the docstring; the bridge needs the value-group API. val_p_lt_1 and IsTopologicalNilpotent are proved and kernel-verified.
…ld green Revival state: val_p_lt_1 proved (kernel-verified), IsTopologicalNilpotent defined, topologicallyNilpotent_of_val_lt_one stated (proof parked on the ValueGroup₀ bridge, annotated). 10 annotated sorries remain.
The ValueGroup₀/restrict bridge: embedding_restrict + restrict_lt_iff_lt_embedding + NNReal.tendsto_pow_atTop_nhds_zero_of_lt_one. Kernel-verified.
…nally removed in the block edit)
…n — the ∃-valuation bridge via choose_spec
This file contains hidden or bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment
20 participants
Add this suggestion to a batch that can be applied as a single commit.This suggestion is invalid because no changes were made to the code.Suggestions cannot be applied while the pull request is closed.Suggestions cannot be applied while viewing a subset of changes.Only one suggestion per line can be applied in a batch.Add this suggestion to a batch that can be applied as a single commit.Applying suggestions on deleted lines is not supported.You must change the existing code in this line in order to create a valid suggestion.Outdated suggestions cannot be applied.This suggestion has been applied or marked resolved.Suggestions cannot be applied from pending reviews.Suggestions cannot be applied on multi-line comments.Suggestions cannot be applied while the pull request is queued to merge.Suggestion cannot be applied right now. Please check back later.
Revival of leanprover-community#26389 (as discussed — co-authoring).
What this does: adapts
Perfectoid.leanto the current master API so it compiles again:structure S extends P : Prop→structure S : Prop extends P(new syntax)UniformAddGroup→IsUniformAddGroup,TopologicalDivisionRing→IsTopologicalDivisionRing: Type extendsclasses𝒪[K]notation and theValuedfield names verified against current master (no changes needed)State: compiles against master, 13
sorrys remain — the mathematical work:valuedPerfectoidField.is_topological_valuationIsTopologicalNilpotent,val_p_lt_1Tiltfield instancePerfectoidField.isAlgClosed_iff_isAlgClosed_tiltProposal: I take the sorries in order (starting with
val_p_lt_1and the Frobenius-surjectivity API), you review. Happy to push directly to your branch instead if you prefer.