Sync upstream mathlib4 (2026-05-10, +65 commits)#2
Merged
Conversation
… if `P` is (#39114) From Proetale.
…dyne morphisms (#37869) Defines inner fibrations, inner anodyne morphisms, and immediate results.
…`CommSemiring` (#39112)
…group is a Galois group (#39093) This PR proves `IsGaloisGroup (⊤ : Subgroup G) A B ↔ IsGaloisGroup G A B`. Co-authored-by: tb65536 <thomas.l.browning@gmail.com>
This PR adds the feature to `to_dual` and `to_additive` that you can now locally modify the name translation dictionary. With this change, we run the risk of having the automated translations being harder to predict. For this reason, the changes to the dictionary do not persisted through imports. Instead, the change lasts until the end of the file (though it ignores sections). See https://leanprover.zulipchat.com/#narrow/channel/287929-mathlib4/topic/Order.20dual.20tactic/near/580834166
…7441) Don't be so restrictive about the shape of morphism theorems Right now, `fun_prop` has a problem with a bundled morphism `Foo α` that coerces to `α → α → α` . The coerced function has two arguments and there is an unnecessary restriction about this. This PR lifts that restriction. [Zulip discussion](https://leanprover.zulipchat.com/#narrow/channel/287929-mathlib4/topic/.60fun_prop.60.20in.20.60FunLike.60.20with.20multiple.20arguments/with/582731349) Co-authored-by: Tomas Skrivan <tomass@sidefx.com> Co-authored-by: Jon Eugster <eugster.jon@gmail.com>
We split this file into a `Basic` file with only the basic results on `Order.cof`, and an `Ordinal` file for the interactions with ordinals. This avoids an import cycle in a subsequent PR. The module docstrings were rewritten, but no theorems were changed.
…o_additive tactic (#38525) This PR adds the pair "conGen", "AddConGen" to the additive tactic and capitalizes the second of some pairs that should have been.
Adding some basic lemmas for the cardinality of an order type. Co-authored-by: YanYablonovskiy <yablonovskiy.yan@gmail.com>
…ConditionallyCompleteLattice` (#38854) Usually a primed version of a sup/inf theorem is like the unprimed version but for `ConditionallyCompleteLinearOrderBot` which can remove `Nonempty` assumptions. `ciSup_mono'` is different from its unprimed version and it's missing `ConditionallyCompleteLattice` versions. We add these and rename `ciSup_mono'` to `ciSup_mono_of_forall_exists'`.
…s of `iSup_exists`/`iSup_and` (#38857) For `iSup_exists` we can only get `≤` in `ConditionallyCompleteLattice`, and equality in `ConditionallyCompleteLinearOrderBot`.
…eLinearOrderBot` versions of `csSup_union`/`csSup_inter_le`/`csSup_insert` (#38858) `ConditionallyCompleteLinearOrderBot` lets us drop all the `Set.Nonempty` assumptions.
We prove that `toZ` is strictly monotonic, and golf/deprecate other theorems in this file using this.
…IsBotZeroClass` (#39062) To be used in the CGT repo.
…` + def lemmas (#37171) - Generallise `le_induction` from `Prop` to `Sort*` and rename to `leInduction` - Add a few lemmas - Simplify proofs using `lia` - Move `inductionOn'_add_one` [Zulip 💬](https://leanprover.zulipchat.com/#narrow/channel/287929-mathlib4/topic/Add.20note.20to.20help.20search.20similar.20thms/near/535331432)
`Finset` version of lemmas already existing for `Set`.
Adds `Finset.filter_powersetCard_subset` and derives `Finset.card_filter_powersetCard_subset` from it. The hypothesis `s.card ≤ n` is necessary: without it, natural subtraction silently gives `Nat.choose k 0 = 1 ≠ 0`. Co-authored-by: Malte Jackisch <jackisch@zib.de> Co-authored-by: Christoph Spiegel <christophspiegel.berlin@gmail.com>
…and use it everywhere (#38414)
This can be used as e.g. ```lean induction n using stepInduction 3 with | base n hn => ... | step n ih => ... ``` The test file's examples are from a term project I did for an NUS module taught by Olivier Danvy himself. Co-authored-by: Parcly Taxel <reddeloostw@gmail.com>
Generalize a result by removing an unnecessary hypothesis. Also simplifies the proof. Co-authored-by: NoahW314 <noahwalker3.14@gmail.com>
Renames `Pi.prod` to `Function.prod` in order to allow for dot notation to work in the non-dependent case. Co-authored-by: pre-commit-ci-lite[bot] <117423508+pre-commit-ci-lite[bot]@users.noreply.github.com>
The definitions in this file don't give any useful def-eqs, so we opt to not expose them.
Co-authored-by: sgouezel <sebastien.gouezel@univ-rennes1.fr>
…IsCommComonObj (#38314) ## Summary Two symmetric-monoidal coherence results: 1. `MonoidalCategory.tensorμ_braid_swap` (in `Monoidal/Braided/Basic.lean`) — canonical rearrangement `tensorμ A A Y Y` intertwines the braiding on `A ⊗ Y` with the pair of braidings on `A` and `Y`. Sibling of `CategoryTheory.MonObj.mul_braiding`. 2. Tensor-product instance for `IsCommComonObj` (in `Monoidal/CommComon_.lean`): if `A, B` carry commutative comonoid structures in a symmetric monoidal category, so does `A ⊗ B`. Fills a gap alongside the existing `instCommComonObjUnit` and `instIsCommComonObjOfCartesian`. ## Downstream consumer The `IsCommComonObj` tensor-product instance is load-bearing for an external library (markovcat, formalising Fritz–Klingler Markov categories). Co-authored-by: Pedro Cortes <pedrocortes.pc@outlook.com>
Ideally we would have only one spelling of this, but in the meantime we should at least have a lemma to transport between the two spellings.
…o_mul_le_add_of_sq_eq_mul` (#38093) The equality `r^2 = a * b` in the hypothesis can be weakened to `r^2 ≤ a * b`. The implementation requires adding an appropriate `ZeroLEOneClass` instance.
…splitting (#38954)
We add the class of algebras that are locally (on the geometric source) standard open immersions. This will be used to define ind-Zariski algebras, which are an important tool to study ind-étale algebras. From Proetale.
… simplicity of A_5 (#38670) Now that #36524 has been merged, we can deprecate the old proof of simplicity of A_5. Co-authored-by: tb65536 <thomas.l.browning@gmail.com>
The torsion subgroup is the whole group if and only if the group is torsion. Co-authored-by: tb65536 <thomas.l.browning@gmail.com>
…ries (#38998) This PR adds basic API for constructing precylinder or pre-path objects in full subcategories and study left/right homotopies in full subcategories.
…#39124) For some reason Lean likes it much better when we explicitly tell it `W`, even though it can be figured out through elaboration. Typeclass inference goes off on a completely unnecessary wild goose chase before this figuring-out is done, for some reason.
We show that the functor from the Verdier quotient `A/(A ⊓ B)` to `C/B` is fully faithful when `A` is a `B`-right- or left-localizing triangulated subcategory in the sense of Verdier.
Provide the `InnerProductSpace 𝕜 PUnit` instance. From MeanFourier
…7831) If `s ⊆ t` then `s.card = ∑ i ∈ t, if i ∈ s then 1 else 0`.
This PR merges the case split and removes duplicated proofs in `Int.mem_divisorsAntidiag`.
Co-authored-by: pre-commit-ci-lite[bot] <117423508+pre-commit-ci-lite[bot]@users.noreply.github.com>
This is put in a new file because it needs combined import from Topology/ENat and Topology/ENNReal, and the existing Topoloty/ENNReal/Lemmas file is pretty deep in the tree so I don't want to increase the import to it. AI usage disclosure: the statement were verified by Aristotle. The proof was completely rewritten by me.
If `Φ : LocalizerMorphism W₁ W₂`, the typeclass `Φ.IsInduced` says that `W₂.inverseImage Φ.functor = W₁`.
Add antiperiodicity and periodicity theorems for complex sinh/cosh/tanh from AlexKontorovich/PrimeNumberTheoremAnd
Proves the classical identity expressing the modular discriminant as a combination of Eisenstein series:
$$\Delta = \frac{E_4^3 - E_6^2}{1728}.$$
The work was done as part of the Sphere packing project. This PR was done with the help of Claude Code.
(Resubmission of #37789 with a renamed branch; earlier dependency work has been merged via #37979.)
…ow_const_nhds_zero (#39030) Specialises `Filter.Tendsto.rpow_const` to base `→ 0`. The strict `0 < p` (rather than `0 ≤ p` from the parent) is needed to identify `0 ^ p` with `0`. Refactors the one in-tree call site (`ZetaAsymp.term_tsum_of_lt`). Co-authored-by: Sebastian Pokutta <23001135+pokutta@users.noreply.github.com> Co-authored-by: Christoph Spiegel <christophspiegel.berlin@gmail.com>
![cursor[bot]](https://avatars.githubusercontent.com/in/1210556?s=60&v=4){kind=small}
There was a problem hiding this comment.
Cursor Bugbot has reviewed your changes and found 1 potential issue.
❌ Bugbot Autofix is OFF. To automatically fix reported issues with cloud agents, enable autofix in the Cursor dashboard.
Reviewed by Cursor Bugbot for commit 6b495b4. Configure here.
|
|
||
| @[simp] | ||
| theorem normalClosure_eq_bot_iff : normalClosure s = ⊥ ↔ s ⊆ {1} := by | ||
| rw [eq_bot_iff, ← normalClosure_subset_iff, coe_bot] |
There was a problem hiding this comment.
Missing @[to_additive] on new subgroup lemma
Low Severity
The new normalClosure_eq_bot_iff lemma is missing the @[to_additive] attribute. Every surrounding lemma in this section (normalClosure_subset_iff, normalClosure_mono, normalClosure_eq_iInf, normalClosure_eq_self, normalClosure_idempotent) carries @[to_additive] to auto-generate the AddSubgroup version. Without it, the additive counterpart AddSubgroup.normalClosure_eq_bot_iff won't exist, breaking the expected API symmetry between Subgroup and AddSubgroup.
Reviewed by Cursor Bugbot for commit 6b495b4. Configure here.
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.
Automated daily sync from
leanprover-community/mathlib4@master.706bea155cb08b692c202d4080da25c88fb8030aAuto-merges to
masteronceCI (self-hosted)passes. Regenerateddaily until merged or until a conflict appears.
Note
Medium Risk
Medium risk due to broad upstream changes touching core algebra/category theory APIs (e.g.
Pi.prod→Function.prod, localization aliases, new typeclass instances), which may subtly affect downstream proofs and simp behavior.Overview
Syncs upstream mathlib with new substantial additions in homological algebra, algebraic geometry, and simplicial sets: introduces
HomologicalComplex.homotopyFiber/path objects, definesScheme.Hom.finrankfor finite flat morphisms (with local constancy/surjectivity/isomorphism criteria), and adds inner fibrations/inner anodyne extensions plus related horn-filling utilities.Includes wide API/simp refactors: replaces many uses/definitions of
Pi.prodwithFunction.prod(and deprecatesPi.prodaliases), relocates/standardizesLocalizedModule.Away/IsLocalizedModule.Away, adds newIsEquivalenceinstances and Guitart exact composition lemmas, and makes numerous small lemma/generalization tweaks (e.g. new simp lemmas, generalized assumptions, and proof-automation cleanups).Reviewed by Cursor Bugbot for commit 6b495b4. Bugbot is set up for automated code reviews on this repo. Configure here.