feat: topology on ring of finite adeles. #13703
Closed
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 b105d1063fImport changesNo significant changes to the import graph
|
![github-actions[bot]](https://avatars.githubusercontent.com/in/15368?s=60&v=4){kind=small}
leanprover-community-mathlib4-bot
added
the
blocked-by-other-PR
kbuzzard
added
awaiting-review
t-number-theory
Remove tactics that do not seem to affect any goal, as reported by the linter.
doc: Minor improvement Mention equivRealProdCLM (=The natural continuous linear equiv from ℂ to ℝ × ℝ) prominently in the list of functions defined in Analysis/Complex/Basic.lean. For a better overview, list the functions in a table rather than a bullet point list.
…14115) - Add `StieltjesFunction.const` and `StieltjesFunction.add` - Add lemmas `const_apply` and `add_apply` - Add instances `AddCommMonoid StieltjesFunction` and `Module ℝ≥0 StieltjesFunction` - Add lemmas `measure_const`, `measure_add` and `measure_smul` - Cleanup
…on`} with `induction` and `cases` (#14132) Spit from #12605, which picked up some conflicts here. Co-authored-by: negiizhao [[email protected]](mailto:[email protected])
…13845) + Create a new file for materials about bivariate polynomials developed using `R[X][X]` rather than `MvPolynomial`. Introduce `evalEval` for evaluation at a point (x,y) on the plane, and use it in Affine.lean and Jacobian.lean. + Move the notations `R[X][Y]` and `Y` from `EllipticCurve/Afffine.lean` to the new file. + Add two lemmas in `Affine.lean` that relates `negPolynomial` and `polynomialY`, and two trivial lemmas `some_ne_zero` and `some_eq_some_iff`. + Prove two affine formulas `addX_eq_subX_sub` and `addY_sub_negY` which are crucial for the development of division polynomials. + Golf the definition of addition of rational points and subsequent lemmas, including two proofs in `Group.lean`. + Remove `eval_polynomial(X,Y)` lemmas in favor of bivariate polynomial lemma `map_mapRingHom_eval_map_eval`; add a lemma `Equation.map`. Co-authored-by: Junyan Xu <[email protected]>
…uced by multiplication for submodules (#12498) ... used in the definition of linearly disjointness. Let `R` be a commutative ring, `S` be an `R`-algebra (not necessarily commutative). Let `M` and `N` be `R`-submodules in `S`. - `Submodule.mulMap`: the natural `R`-linear map `M ⊗[R] N →ₗ[R] S` induced by the multiplication in `S`, whose image is `M * N` (`Submodule.mulMap_range`). - `Submodule.mulMap'`: the natural map `M ⊗[R] N →ₗ[R] M * N` induced by multiplication in `S`, which is surjective (`Submodule.mulMap'_surjective`). - `Submodule.lTensorOne`, `Submodule.rTensorOne`: the natural isomorphism between `i(R) ⊗[R] N` and `N`, resp. `M ⊗[R] i(R)` and `M`, induced by multiplication in `S`, here `i : R → S` is the structure map. They generalize `TensorProduct.lid` and `TensorProduct.rid`, as `i(R)` is not necessarily isomorphic to `R`. Note that we use `⊥ : Subalgebra R S` instead of `1 : Submodule R S`, since the map `R →ₗ[R] (1 : Submodule R S)` is not defined directly in mathlib yet. - `Submodule.mulLeftMap`: if `m : ι → M` is a family of elements, then there is an `R`-linear map from `ι →₀ N` to `S` which maps `{ n_i }` to the sum of `m_i * n_i`. - `Submodule.mulRightMap`: if `n : ι → N` is a family of elements, then there is an `R`-linear map from `ι →₀ M` to `S` which maps `{ m_i }` to the sum of `m_i * n_i`.
It had become an incoherent grab-bag of results, which I've moved to more suitable places over the last few months.
+ `equiv_iff_eq_of_Z_eq`: if a point has two representations in Jacobian coordinates with the same, nonzero Z-coordinate, then the two representations are equal. + `nonsingular_iff_of_Z_ne_zero`: a lemma deleted in an earlier PR for no reason, now restored. + `addXYZ_self`: if the addition (not doubling) formula is applied to a point representative and itself, the result is (0,0,0). + `addXYZ_neg`: the addition formula applied to a point representative and its negation yields a representative of the point at infinity. + two trivial lemmas `fromAffine_ne_zero` and `comp_fin3`. + a series of `map` lemmas showing the addition and doubling formulas in Jacobian coordinates commute with ring homomorphisms. Co-authored-by: Junyan Xu <[email protected]>
These names were all over the place and there were missing versions.
This PR adds `TopologicalSemiring` and `TopologicalRing` instances on `C(α, β)`, and also gives explicit names to various related instances on `C(α, β)`.
…ble (#14002) `Algebra.TensorProduct.mul` was getting unfolded downstream. We make it `irreducible` to prevent this at the cost of a small number of `unseal mul in`'s, `dsimp`'s, and `with_unfolding_all`'s.
…rom cycleOf. (#13145) cycleOf can be defined using only a decidability condition, rather than the current finiteness condition (from which decidability can be inferred). This commit removes this dependency on finiteness. Co-authored-by: Wrenna Robson <[email protected]>
* From the Sobolev inequality project Co-authored-by: Heather Macbeth [email protected]
…e` for `Fin` (#9814) Redefine the BoundedOrder and Lattice on `Fin (n + 1)` so that they are defined for `Fin n`. Co-authored-by: Wrenna Robson <[email protected]>
This is exhaustive, with the exception of one goal where the `continuity` proof is seemingly not about continuity at all... We tag two lemmas with `fun_prop` which were continuity lemmas. In some cases, this speeds up proofs significantly; we also resolve two porting notes about continuity not applying.
- [x] Add `add_sub_cancel_right` - [x] Add `right_distrib_of_nneg` - [x] Add `left_distrib_of_nneg` - [x] Add `le_iff_le_forall_real_gt` Co-authored-by: @D-Thomine
…oint a` automatically (#13673) These are needed for the specialized tactic `cfc_tac` to work well. This tactic is used for proving side goals related to the continuous functional calculus. Some of the `safe` attributes are not technically safe (i.e. they might turn a provable goal into an unprovable one), but I would claim that in those cases, it's not really reasonable to expect automation to work anyway.
…ercion results (#13838) Added several RCLike to real coercion results to support the result that eigenvalues of a hermitian matrix belong to the real spectrum of that matrix, and included this result. Co-Authored by @j-loreaux Co-authored-by: Eric Wieser <[email protected]> Co-authored-by: JonBannon <[email protected]> Co-authored-by: Jireh Loreaux <[email protected]>
This PR creates a new file with the machinery for transferring matroid structures between types. The most important definitions are `Matroid.map`, which pushes a `M : Matroid α` along `f : α → β` to give an `N : Matroid β`, and `Matroid.comap`, which pulls `N : Matroid β` back along `f : α → β` to get an `M : Matroid α`. The former requires `f` to be injective on the ground set of `M`, but the latter doesn't. The original decision to define matroids with an embedded ground set within a type rather than just a structure on a type came with tradeoffs, and it is in places like this that they show up the most. For this reason, the file also defines several variants of `map` where the range/domain of the function in question is a coerced set rather than a type. There is nothing mathematically interesting going on with these definitions, and maps and comaps are not central to matroid theory in actual research, but they are very useful in making formalization painless, as they save the work of painstakingly checking matroid axioms in many cases. They will be used in future PRs to define things like direct sums and linearly representable matroids.
|
bleurgh, git nightmare. Making a new PR (#14176 , same material) because it's easier than learning how to fix this one. |
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.
Use
SubmodulesRingBasisto put a topology on the finite adeles.