feat(ModelTheory): add quantifier elimination and reduction to one qu…#8
Open
iosephusferrum wants to merge 452 commits into
Open
Conversation
… under isomorphisms (leanprover-community#41036) This is only the translation of this statement in terms of some `ObjectProperty` in functor categories.
…y#37901) In this PR we define the notion of algebraic cycles on a scheme, and define the pushforward of an algebraic cycle by a quasicompact morhphism. This was originally defined in leanprover-community#26304, but after some refactoring it was decided that it would be best to split this definition into a separate PR. Co-authored-by: Raph-DG <raphaeldouglasgiles@gmail.com>
…r-community#40976) Generalize both interval-version Lebesgue differentiation theorems `LocallyIntegrable.ae_hasDerivAt_integral` and `IntervalIntegrable.ae_hasDerivAt_integral` from real-valued functions `f : ℝ → ℝ` to functions `f : ℝ → E` valued in a Banach space `E`. The existing proof already goes through the vector-valued averaging theorem `VitaliFamily.ae_tendsto_average`, so the only change is replacing scalar multiplication `*` by `•` in the slope computation. This is a prerequisite for leanprover-community#40973. AI usage disclosure: I used Claude Opus 4.8 to implement this and manually tested it with the other PR and my other separate project.
…ommunity#40986) Remove a duplicate lemma and generalize some lemmas to support two different codomains.
…#40919) This can in future replace a similar lemma for `RingQuot`. The old copyright is because this was derived from `Mathlib/Algebra/Star/RingQuot.lean`.
Implement tactic for proving equality of polynomials. This tactic is part of a larger suite (see leanprover-community#30374). Also generalize the preprocessing step for `algebra` so that it always replaces `algebraMap R A r` with `r • 1` instead of only when `R` is `Nat` or `Int`. This was an oversight in `algebra` that broke `polynomial`. - [x] depends on: leanprover-community#31508
…anprover-community#38667) - `OrderHom`s are equivalent to `RelHom`s of `LE` (unlike `OrderEmbedding`/`OrderIso` they aren't defined using it) - Congruence equivs for `OrderEmbedding`/`OrderIso` when the two sides are order-isomorphic. This already exists for `OrderHom`.
…eanprover-community#41041) These probably became non-`noncomputable` with the new compiler.
…1044) This PR updates the Mathlib dependencies.
From flt-regular.
I've put this in mathlib since it can use `Function.Involutive`; it can of course be upstreamed at a later date. Having this generalization encourages downstream code in cslib to be expressed in terms of involutive functions, rather than just `^^^` on bitvectors.
This PR is adds `NSMul`, `NPow`, `ZSMul` and `ZPow` classes for the `nsmul`, `npow`, `zsmul`, `zpow` data fields. This has a few advantages: - If you first declare a `SMul` instance, then you don't need to manually write `nsmul := (· • ·)` and `zsmul := (· • ·)` . For `Pow`, the extra benefit is that inferring the instance is preferred over the default field `npowRecAuto`. So this helps avoid accidental diamonds. - If you first declare a `SMul` instance on a type synonym, then `inferInstanceAs` will infer the `nsmul` field from the `SMul` instance. This makes it easier to avoid diamonds on type synonyms like `Matrix` and `MonoidAlgebra`. - The not-yet-merged instance diamond linter will be able to detect cases where the `NSMul` and `SMul` classes do not agree. In the process of making this PR, I have identified two existing `NPow` diamonds: - In `Mathlib.Algebra.Order.Positive.Field`, there were two conflicting `NPow` instances. - For `Fin`, there are two conflicting `NPow` instances. I have overwritten the one in core lean with the one from mathlib that is more computationally efficient. TODO: the same for `QSMul` and `NNQSMul`.
…-community#38623) We add a multiplicative version of `Finset.HasAntidiagonal`, called `Finset.HasMulAntidiagonal`. This requires some naming changes (since otherwise, for instance, there would be a clash between [Finset.swap_mem_mulAntidiagonal](https://leanprover-community.github.io/mathlib4_docs/Mathlib/Data/Finset/MulAntidiagonal.html#Finset.swap_mem_mulAntidiagonal) and the corresponding lemma in Mathlib.Algebra.Order.Antidiag.Prod). We made the following naming choices: - Since the additive version will be much more commonly used, we still keep `Finset.HasAntidiagonal` for the additive version, and translate `mulAntidiagonal` to `antidiagonal` rather than to `addAntidiagonal`. Note that in particular this affects the API in Mathlib.Data.Finset.MulAntidiagonal, which used `addAntidiagonal`. - We move most of the results in `Mathlib.Algebra.Order.Antidiag.Prod` into the `Has(Mul)Antidiagonal` namespace, so that e.g. `Finset.swap_mem_antidiagonal` and `Finset.HasAntidiagonal.mem_antidiagonal` can co-exist. Note that some deprecation tags (e.g., for Finset.antidiagonal, Finset.antidiagonal.fst_le, ...) are intentionally missing. The reason is that `antidiagonal` and related lemmas are normally used inside an open `Finset` namespace, and since these declarations have moved into `Finset.HasAntidiagonal`, the deprecation causes errors which would require to explicitly add `HasAntidiagonal` in many places. An easier solution is just to open `Finset.HasAntidiagonal`, after which the preexisting code works. Co-authored-by : @xgenereux Co-authored-by: mariainesdff <mariaines.dff@gmail.com>
…ty#41047) The following fails before the PR, works after it ``` example : starRingEnd ℝ = RingHom.id ℝ := by with_reducible_and_instances rfl ``` Co-authored-by: sgouezel <sebastien.gouezel@univ-rennes1.fr>
…ity#40884) This PR adds a few properties about localization with respect to isomorphisms. The lemma `LocalizerMorphism.Derives.isIso` is renamed `isIso_of_isRightDerivedFunctor`, because we shall need the dual lemma in the future.
This PR adds API lemmas about `dcomp` that were previously missing.
Add the isomorphism between `PiLp` over any `Unique` index type and the corresponding individual type. Generalise `PiLp.linearEquiv` to topological vector spaces, then this is straightforward. This will be used in leanprover-community#29077, to yield an equivalence `EuclideanSpace 𝕜 (Fin 1) ≃L[𝕜] 𝕜`.
…gonalComplement_eq_zero` (leanprover-community#40722) leanprover-community#38970 tried to create one, but made a slip (and created a deprecated alias for a declaration that never existed). Correct this oversight. Noticed during leanprover-community/sphere-eversion#143.
…ver-community#41000) Let `C` be an abelian category with enough injectives. In this file, we define a localizer morphism `CochainComplex.Plus.localizerMorphism` (relatively to quasi-isomorphisms) which is given by the (fully faithful) functor `CochainComplex.Plus (InjectiveObject C) ⥤ CochainComplex.Plus C`, and we show that it is a right derivability structure in the sense of Kahn and Maltsiniotis. (The proof proceeds by showing that up to equivalences of categories, this functor is the inclusion of the full subcategory of fibrant objects in the model category `CochainComplex.Plus C`.)
…th_le_length` (leanprover-community#37578) Co-authored-by: Snir Broshi <26556598+SnirBroshi@users.noreply.github.com>
…ogy and groupHomology (leanprover-community#40714) This is another upstreaming PR originated from the [CFT](https://github.com/kbuzzard/ClassFieldTheory) repo, it's a collaborative work from 2025 Clay Summer School on Formalizing Class Field Theory.
…stance (leanprover-community#40914) The instance `Algebra.ofSubring` is a specialization of `Algebra.ofSubsemiring` and is causing diamonds in leanprover-community#40912. Co-authored-by: tb65536 <thomas.l.browning@gmail.com> Co-authored-by: Monica Omar <23701951+themathqueen@users.noreply.github.com>
…text (leanprover-community#41001) This PR fixes the panic in `#click_suggestions` that was reported at https://leanprover.zulipchat.com/#narrow/channel/287929-mathlib4/topic/.23click_suggestions.20doesn.27t.20find.20lemma/near/606231763 There are two separate problems that this PR fixes: 1. The implementation of `#click_suggestion` assumes all metavariables have already been instantiated. This is valid because they are all instantiated at the very beginning. However, this was not done properly, causing the types of free variables to still be able to contain metavariables. 2. The function `viewKAbstractSubExpr` was able to reach its `unreachable!` block. The reason is that `kabstractPositions` calls `instantiateMVars` on the expression `e` but not on the pattern `p`, causing a discrepancy. This is fixed by removing the `instantiateMVars` call. This is fine, because in both of the use cases (`rw??` and `#click_suggestions`), the expressions already have instantiated metavariables at this point.
…leanprover-community#39624) This formula is useful for defining partial derivatives of multivariate power series, see PR leanprover-community#39626.
…eanprover-community#40937) In this file, we introduce the predicate `Cardinal.SharplyLT`. Given two regular cardinals `κ₁ < κ₂`, this condition can be described in different ways (a TFAE lemma will appear in a future PR). Here, we define it by saying that the category `CardinalDirectedPoset κ₁` is `κ₂`-accessible, and we show one of the implications for the future TFAE lemma. (This PR also renames `CardinalFilteredPoset` as `CardinalDirectedPoset`.)
In this PR, we introduce the definition of Reedy structures. From https://github.com/joelriou/reedy which was started at https://www.mittag-leffler.se/activities/formalizing-higher-categories/ Co-authored-by: Aras Ergus <arasergus@posteo.net> Co-authored-by: Nima Rasekh <nima.rasekh@uni-greifswald.de>
…rds the definition of K-sheaf (leanprover-community#40737) this file adds the definition of the set of compacts nhds of a compact, the open nhds of a compact, the open relatively compact nhds of a compact and the compacts inside an open subset. It also adds API related with these sets and the way they interact. In particular there is API related to the induced (as preorder) categories. I neede the dual version of Monotone.final_functor_iff, Joel Riou told me to duplicate the code for now (as the same tactic sequence can prove the dual version) until the automation can deal with that. All these definitions are prerequisite to the definition of K-Sheaves and their link with Sheaves, this will follow in an other PR Co-authored-by: Yannis Monbru <yannis.monbru@orange.fr>
…eanprover-community#40797) Given a bifunctor `F : C₁ ⥤ C₂ ⥤ C₃`, and morphisms `f₁ : X₁ ⟶ Y₁` in `C₁` and `f₂ : X₂ ⟶ Y₂` in `C₂`, one can form a commutative square in the category `C₃`, and the `PushoutObjObj` structure contains the data of a pushout of the top and left maps in this square. Then, `PushoutObjObj.ι` is the induced map from the pushout to the bottom-right object of the square. Until this PR, `PushoutObjObj.ι` was a definition. In this PR, we make it a field of the structure `PushoutObjObj` instead. This allows a better control on the definitional properties of `ι`. This already simplifies proofs in the file `Mathlib/AlgebraicTopology/SimplicialSet/AnodyneExtensions/PushoutProduct.lean` and I plan to take advantage of this in the formalization of the Reedy model category structure https://github.com/joelriou/reedy because in the study of similar structures for trifunctors obtained as compositions of bifunctors, these `ι` will appear as parameters of certain dependent types.
Not exhaustive at all. Inspired by Zulip discussion in https://leanprover.zulipchat.com/#narrow/channel/287929-mathlib4/topic/linter.20requests/with/605217189
These revisions are ignored when doing git blame, providing more helpful output. We populate it with the commits corresponding to - leanprover-community#31786 (move to the module system), - leanprover-community#13166 and leanprover-community#13059 (replacing `refine'` by `refine`). This list is not exhaustive; further commits can be added later.
…d category of a preadditive category (leanprover-community#41294) Define the right Freyd category of a preadditive category `V` as the quotient of `Arrow V` by the right homotopy relation, as well as a fully faithful additive functor `V ⥤ RightFreyd V` (when `V` has a zero object). TODO: If `V` has binary biproduct, then `RightFreyd V` has cokernels. Co-authored-by: morel <sophie.morel@ens-lyon.fr>
This PR golfs some proofs with `grw`, by making use of strict rewriting. This is not exhaustive. I just picked some proofs that could be golfed, to show what can be done with `grw` now.
…ommunity#41315) They were assuming unnecessarily strong hypotheses: weaken them to what was inteded. Co-authored-by: Michael Rothgang <rothgang@math.uni-bonn.de>
…prover-community#39693) Kill TODO in `Mathlib/Combinatorics/Enumerative/Bell.lean` which proves `Nat.bell` as a sum of `Multiset.bell` over partition shapes
…nprover-community#40179) Also allow a few selected suffixes to abbreviations. And make the error messages about suffixes more detailed.
…over-community#40946) To my surprise, `lambdaMetaTelescope` does not use the lambda binder names to give names to the introduced metavariables. As a result, `reorderLambda` would rename all lambda binder names to `x`. This is fixed by only using `forallMetaTelescope` to introduce the metavariables.
leanprover-community#40261) …eying the module system
…ces of `inertiaDeg_eq_inertiaDeg'` (leanprover-community#41320) This PR adds a bit more API for `RingTheory/RamificationInertia/Inertia` in order to remove the last occurances of `inertiaDeg_eq_inertiaDeg'`. Co-authored-by: tb65536 <thomas.l.browning@gmail.com>
refactor the existing proof of weak approximation to the generalized version applied to pairwise inequivalent absolute value
…ions (leanprover-community#41316) Remove duplicate definitions `kernel.congr` (already defined in `kernelIsoOfEq`) and `cokernel.congr` (already defined in `cokernelIsoOfEq`). Co-authored-by: morel <sophie.morel@ens-lyon.fr>
…ity of continuous cohomology (leanprover-community#41309)
…sUnramifiedIn` version (leanprover-community#41323) This PR extracts an `Algebra.IsUnramifiedIn` version of the existence of ramified primes in number fields. Co-authored-by: tb65536 <thomas.l.browning@gmail.com>
…Freyd category has cokernels (leanprover-community#41295) If `V` is a preadditive category with binary biproducts, its right Freyd category (defined in leanprover-community#41294) has cokernels. - [x] depends on: leanprover-community#41292 - [x] depends on: leanprover-community#41294 Co-authored-by: morel <sophie.morel@ens-lyon.fr> Co-authored-by: Joël Riou <37772949+joelriou@users.noreply.github.com>
This PR adds a step to the PR summary bot to make it add the "tech debt" label to PRs that decrease tech debt. This PR was made with the assistance of Claude code Thanks to Felix for this idea. Zulip discussion here [#mathlib4 > Technical Debt Counters @ 💬](https://leanprover.zulipchat.com/#narrow/channel/287929-mathlib4/topic/Technical.20Debt.20Counters/near/601643776)
…1330) This PR updates the Mathlib dependencies.
…r-community#40755) This PR adds the `#click_suggestions` command to `Mathlib.Tactic.Common`, so that it can be used in most mathlib files. To allow this, I reduced the theory imports, since `Mathlib.Tactic.Common` is not supposed to import much theory. The extra import will probably give a minor slowdown, but I think it is worth it.
…ponent of crt for zmod (leanprover-community#40972) The CRT for ZMod on the each components is equivalent to the usual `ZMod.castHom` given by the divisibility property.
…1035) This PR fixes some instance diamonds found by the instance diamond linter (leanprover-community#38781)
leanprover-community#40701) This PR adds `scripts/export_crossrefs.lean`, which exports every declaration tagged with `@[wikidata]`, `@[stacks]`, or `@[kerodon]` (name, file, line, ids) as JSON, and a CI workflow that runs it after each successful master build and publishes the result to https://github.com/leanprover-community/crossref-exports. The CI workflow can also be triggered manually using `workflow_dispatch`. The credentials are provided by a new GitHub app "crossref-exports-app" under the `leanprover-community` organization with secrets set up in the "crossref-exports" repo environment. Co-authored-by: Bryan Gin-ge Chen <bryangingechen@gmail.com>
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.
3