PAT test#1
Merged
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.)
![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 feeff90. 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 normalClosure_eq_bot_iff
Low Severity
The new normalClosure_eq_bot_iff lemma is missing the @[to_additive] attribute. Every neighboring lemma in this section (normalClosure_subset_iff, normalClosure_mono, normalClosure_eq_iInf) carries @[to_additive], so the additive counterpart (AddSubgroup.normalClosure equal to ⊥ iff s ⊆ {0}) won't be auto-generated, breaking the pattern established by the surrounding API.
Reviewed by Cursor Bugbot for commit feeff90. 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.
diagnostic
Note
Medium Risk
Touches many core Mathlib files with new category-theory/algebraic-topology/algebraic-geometry constructions and several API migrations (
Pi.prod→Function.prod,IsLocalizedModule.Awaymove), so downstream breakage risk is moderate despite mostly additive changes.Overview
Adds substantial new theory in several areas. Introduces
HomologicalComplex.homotopyFiber/HasHomotopyFiberand a dual path object construction (via opposites), plus supporting lemmas/instances inHomotopyCofiber/Opposite.Expands algebraic geometry and simplicial-set infrastructure. Adds
Scheme.Hom.finrankfor finite flat (locally finitely presented) morphisms with local-constancy/surjectivity/iso characterizations, and addsSSet.innerFibrations+innerAnodyneExtensions(with small object argument setup) alongside new simplicial utilities (δ₀Iter/σ₀Iter, boundary face inclusions/hom_ext, horn lifting helpers).API cleanups and compatibility shims. Replaces many uses of
Pi.prodwithFunction.prod(deprecatingPi.prodaliases), movesIsLocalizedModule.Away/LocalizedModule.Awaydefinitions intoLocalizedModule/Basicand deprecates the oldAwaymodule, and adds numerous small lemmas/instances/refactors across algebra/order/list/int/category theory (e.g. newLocalizerMorphism.IsInduced+inv,initialize_simps_projectionson several bundled categories, new periodicity lemmas forsinh/cosh/tanh).Reviewed by Cursor Bugbot for commit feeff90. Bugbot is set up for automated code reviews on this repo. Configure here.