[Merged by Bors] - refactor(Topology/Category): add CompHausLike.Limits #13905
Conversation
This file contains 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
PR summary 644c692821Import changesNo significant changes to the import graph
|
2 tasks
leanprover-community-mathlib4-bot
added
the
blocked-by-other-PR
This was referenced Jun 17, 2024
dagurtomas
added
awaiting-review
t-category-theory
dagurtomas
commented
Jun 19, 2024
dagurtomas
commented
Jun 19, 2024
dagurtomas
added
awaiting-CI
and removed
blocked-by-other-PR
|
This PR/issue depends on: |
This will allow us to write `n.toNat` instead of `ENat.toNat n`
We derive the inequality between the harmonic and geometric mean as a consequence of AM-GM for positive real valued functions from a `Finset`. We state a weighted as well as the classical version.
This is one in a series of PRs rewriting most checks from `lint-style.py` in Lean. This PR moves the check for copyright headers and authors: the check has been rewritten anew (and is hopefully simpler to understand now); this has made it stricter in various places. The necessary adjustments have been made in #13212 and #13247. This PR also adds a `nolints` file for text-based linters.
…es (#13545) We define the strict bicategory of based categories. Its objects are categories equipped with a functor to some fixed base-category. The strict bicategory of fibered categories will later be built on top of this one. Co-authored-by: Paul Lezeau [[email protected]](mailto:[email protected])
…14018) This PR adds the `SpecialFunctions/Log/ENNRealLog.lean` file where we define `log` as an extension of the logarithm of a positive real to the extended nonnegative reals `ℝ≥0∞`. The function takes values in the extended reals `EReal`, with `log 0 = ⊥` and `log ⊤ = ⊤`. Co-authored with @D-Thomine.
left and right unitor functors for product of categories Co-authored-by: Shanghe Chen <[email protected]>
Co-authored-by: Joël Riou <[email protected]>
We show that `Module.Finite` is preserved under localizations and that if a module is finite after localizing at a spanning set of elements of the ring, it is finite.
This reduces the long pole.
The `cc` tactic is a high-cost tactic, so I restored `cc` tactics only if a proof can be reduced significantly. I made sure that `cc` tactic works on in the all changed proofs except when the other specification changes in Lean 4 changes a goal. Co-authored-by: Pol'tta / Miyahara Kō <[email protected]>
- Add `slope_neg_fun` - Add `ConvexOn.slope_mono` and `ConcaveOn.slope_anti` in a new separate section called `slope` Co-authored-by: Lorenzo Luccioli <[email protected]>
The `subsingleton` tactic tries to close equality goals by arguing that the underlying type is a subsingleton type. It might be via a `Subsingleton` instance (via `Subsingleton.elim`), but it also handles some cases where morally the types are subsingletons; for example, it can prove that two `BEq` instances are equal if they both have `LawfulBEq` instances. For heterogeneous equality, it tries the `HEq` version of proof irrelevance. This tactic avoids the issue where ```lean example (α : Sort _) (x y : α) : x = y := by apply Subsingleton.elim ``` is a "proof" that every type is trivial. Changing this to `by subsingleton` prevents it from assigning the universe level metavariable in `Sort _` to `0`. This tactic can accept a list of instances `subsingleton [inst1, inst2, ...]` to do something like `have := inst1; have := inst2; ...; subsingleton`, but it elaborates them in a lenient way (like `simp` arguments), and they can even be universe polymorphic. For example, `subsingleton [CharP.CharOne.subsingleton]` is allowed even though the type of `CharP.CharOne.subsingleton` is `Subsingleton ?R` with a number of pending instance problems. This PR also eliminates a number of uses of `Subsingleton.elim`, either by switching a `congr` to `congr!` or by using this new tactic.
- [x] depends on: #13503
Extends `convert_to` to be able to operate on any location. When converting the type of a local hypothesis, new congruence goals come first. Suggested [on Zulip](https://leanprover.zulipchat.com/#narrow/stream/239415-metaprogramming-.2F-tactics/topic/.60convert_to.20at.60.20.2F.20non-definitional.20.60change.60/near/447601320).
…functor, then the unit is an isomorphism. (#14017) This PR proves that to show that the unit of an adjunction `L ⊣ R` is an isomorphism (i.e. that L is fully faithful), it is enough to give an arbitrary isomorphism `L ⋙ R ≅ 𝟭 C`, and the dual result. To do this, we give a general way to transport (co)monad structures on functors along isomorphisms of functors.
…rder` (#14121) We don't want to import the order hierarchy without really needing it.
For an alternating form $B : M \times M \to R$ and $a, b, c \in M$ with $a + b+ c = 0$, we have $B(a, b) = B(b, c)$. This can be used to prove the same property of Wronskian: see #14243. Co-authored-by: Seewoo Lee <[email protected]>
We can avoid importing `Algebra.Order.Group.Defs` in `Data.Rat.Lemmas` if we use `Nat` versions of some lemmas and slightly modify one proof.
We shouldn't import the whole order hierarchy when we want ring instances on products.
We shouldn't need to import ordered algebraic classes for basic properties of pointwise multiplication of sets.
We can just specialize to the results about `Nat` and avoid importing `Algebra.Order.Ring.Nat`.
…ousOn_eval₂` (#13532) Also use it to weaken TC assumptions in `ContinuousMultilinearMap.continuous_eval`.
Splitting `Prime.lean` into `Defs`, `Basic`. The split aims at separation of defs and needed lemmas from everything else. With this split 13/18 Mathlib modules no longer import the whole `Prime.lean`. `Prime/Defs.lean` is about half the size. Motivation is a circular dependency that would prevent me from adding a lemma to `Prime.lean`. https://leanprover.zulipchat.com/#narrow/stream/287929-mathlib4/topic/split.20Nat.2FPrime.2Elean
|
(Sorry if everyone got github notifications for some unrelated commit, I was merging master and messed up...) |
jcommelin
reviewed
Jul 2, 2024
|
bors d+ |
|
✌️ dagurtomas can now approve this pull request. To approve and merge a pull request, simply reply with |
|
Thanks! bors merge |
mathlib-bors bot
added a commit
that referenced
this pull request
Jul 2, 2024
This is the first part of the refactor of CompHaus and friends (adding the new API which will eventually be used to redefine the categories of compact Hausdorff spaces, see #12930) Co-authored-by: Yury G. Kudryashov <[email protected]> Co-authored-by: Ralf Stephan <[email protected]> Co-authored-by: Kim Morrison <[email protected]> Co-authored-by: dagurtomas <[email protected]> Co-authored-by: grunweg <[email protected]> Co-authored-by: Dagur Tómas Ásgeirsson <[email protected]> Co-authored-by: James Sundstrom <[email protected]> Co-authored-by: leanprover-community-mathlib4-bot <[email protected]> Co-authored-by: Christian Merten <[email protected]> Co-authored-by: Joël Riou <[email protected]> Co-authored-by: Ruben Van de Velde <[email protected]> Co-authored-by: Peter Nelson <[email protected]> Co-authored-by: Jireh Loreaux <[email protected]> Co-authored-by: Pietro Monticone <[email protected]> Co-authored-by: Herman Chau <[email protected]> Co-authored-by: Kyle Miller <[email protected]> Co-authored-by: Seewoo Lee <[email protected]>
|
Pull request successfully merged into master. Build succeeded: |
mathlib-bors
bot
changed the title
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment
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.
This is the first part of the refactor of CompHaus and friends (adding the new API which will eventually be used to redefine the categories of compact Hausdorff spaces, see #12930)