feat(Topology/Algebra): linearly topologized iff non-archimedean#23758
feat(Topology/Algebra): linearly topologized iff non-archimedean#23758
Conversation
PR summary cceabe754fImport changes exceeding 2%
|
| File | Base Count | Head Count | Change |
|---|---|---|---|
| Mathlib.Topology.Algebra.LinearTopology | 1096 | 1174 | +78 (+7.12%) |
Import changes for all files
| Files | Import difference |
|---|---|
3 filesMathlib.RingTheory.MvPowerSeries.Evaluation Mathlib.RingTheory.MvPowerSeries.Substitution Mathlib.RingTheory.PowerSeries.Evaluation |
4 |
Mathlib.RingTheory.MvPowerSeries.LinearTopology |
9 |
Mathlib.Topology.Algebra.TopologicallyNilpotent |
44 |
Mathlib.Topology.Algebra.LinearTopology |
78 |
Declarations diff
+ _root_.Submodule.isOpen_leAddSubgroup_of_compactSpace
+ _root_.isLinearTopology_iff_exists_submodule_isOpen_subset
+ _root_.isLinearTopology_iff_nonarchimedeanAddGroup_of_compactSpace
+ _root_.isLinearTopology_iff_nonarchimedeanAddGroup_of_finite
+ _root_.isLinearTopology_int_iff_nonarchimedeanAddGroup
+ iff_restrictScalars
+ instance (priority := low) [NonarchimedeanAddGroup M] :
+ instance [NonarchimedeanAddGroup M] : IsLinearTopology ℤ M
+ leAddSubgroup
+ leAddSubgroup_le
+ le_leAddSubgroup_iff
+ mem_leAddSubgroup
+ mem_leAddSubgroup_iff_of_span_eq_top
+ mem_leAddSubgroup_iff_span_le
+ nonarchimedeanAddGroup
+ of_restrictScalars
+ restrictScalars
You can run this locally as follows
## summary with just the declaration names:
./scripts/declarations_diff.sh <optional_commit>
## more verbose report:
./scripts/declarations_diff.sh long <optional_commit>The doc-module for script/declarations_diff.sh contains some details about this script.
No changes to technical debt.
You can run this locally as
./scripts/technical-debt-metrics.sh pr_summary
- The
relativevalue is the weighted sum of the differences with weight given by the inverse of the current value of the statistic. - The
absolutevalue is therelativevalue divided by the total sum of the inverses of the current values (i.e. the weighted average of the differences).
| simpa [p.mapIic.isCompl_iff, Iic.isCompl_iff] using Iic.isCompl_inf_inf_of_isCompl_of_le h₁ h₂ | ||
|
|
||
| variable (R) in | ||
| /-- The largest submodule contained in an additive subgroup of a module. -/ |
There was a problem hiding this comment.
This works, but there is a largest submodule contained in anything that contains 0. The definition here could serve as an mem_iff__forall_smul_mem.
There was a problem hiding this comment.
I don't think that's true? There is no largest subspace contained in the union of two (distinct) lines passing through the origin. Of course you could consider a maximal one, but I'm not sure how useful that is as a general API.
I think the proper generality here would again be that of Bourbaki's "groups with operators", but for now I think I'm happy with this.
I would like a different name though. What about Submodule.core or AddSubgroup.submoduleCore? Is there a more standard name?
There was a problem hiding this comment.
I delete my remark.
There was a problem hiding this comment.
What seems to be true, anyway, is that the supremum of the submodules contained in an add subgroup is actually contained in that add subgroup — and is the largest such thing.
There was a problem hiding this comment.
docs#Subgroup.normalCore is the largest normal subgroup contained in a subgroup, and it's also a similar thing for groups with operators (the operators are the conjugacy operators of the group on itself).
There was a problem hiding this comment.
And if mathlib's existing code serves as a guide for good taste, docs#Subgroup.normalCore is proved in exactly the same way as done here.
| obtain ⟨V, hV⟩ := NonarchimedeanAddGroup.is_nonarchimedean s (hs.mem_nhds h0s) | ||
| exact ⟨V.1.toIntSubmodule, V.2, hV⟩ | ||
|
|
||
| instance [NonarchimedeanAddGroup M] : IsLinearTopology ℤ M := |
There was a problem hiding this comment.
I can't decide whether this or that instance is useful/will add noise to the typeclass inference system. But having two equivalent types that are phrased differently looks annoying to me.
There was a problem hiding this comment.
I think this duplication is essentially unavoidable, and I believe the instance is essentially harmless (note there are no possible loops because IsLinearTopology --> NonarchimedeanAddGroup cannot be an instance).
| refine isLinearTopology_iff_exists_submodule_isOpen_subset.mpr fun s hs h0s ↦ ?_ | ||
| obtain ⟨V, hV⟩ := NonarchimedeanAddGroup.is_nonarchimedean s (hs.mem_nhds h0s) | ||
| exact ⟨V.1.toIntSubmodule, V.2, hV⟩ |
There was a problem hiding this comment.
I would prefer to avoid the lemma isLinearTopology_iff_exists_submodule_isOpen_subset which looks un-idiomatic to me.
(suggestion that can be golfed a little bit.)
| refine isLinearTopology_iff_exists_submodule_isOpen_subset.mpr fun s hs h0s ↦ ?_ | |
| obtain ⟨V, hV⟩ := NonarchimedeanAddGroup.is_nonarchimedean s (hs.mem_nhds h0s) | |
| exact ⟨V.1.toIntSubmodule, V.2, hV⟩ | |
| simp only [isLinearTopology_iff_hasBasis_submodule, hasBasis_iff] | |
| intro s | |
| refine ⟨fun h0s ↦ ?_, fun ⟨V, hV0, hVs⟩ ↦ mem_of_superset hV0 hVs⟩ | |
| obtain ⟨V, hV⟩ := NonarchimedeanAddGroup.is_nonarchimedean s h0s | |
| exact ⟨V.1.toIntSubmodule, (isOpen_iff_mem_nhds.mp V.2) 0 V.zero_mem, hV⟩ |
There was a problem hiding this comment.
The real way to trivialize this lemma and the one above would be to have a proper description of NonarchimedeanGroup in terms of filter bases, which simply doesn't exist at the time being!
Adding the lemmas would be relatively easy, but it might be worth changing the definition as well... although I'm not sure how disturbing this would be for the FLT team...
| lemma of_restrictScalars [Module R S] [IsScalarTower R S M] [Module.Finite R S] | ||
| [IsLinearTopology R M] [ContinuousAdd M] [ContinuousConstSMul S M] : | ||
| IsLinearTopology S M := by | ||
| rw [isLinearTopology_iff_exists_submodule_isOpen_subset] |
There was a problem hiding this comment.
same comment as above, using nhds of zero rather than open sets seems more idiomatic. What would @ADedecker say?
| ext | ||
| simp [Submodule.mem_leAddSubgroup_iff_of_span_eq_top _ hs] | ||
|
|
||
| lemma iff_restrictScalars [Module R S] [IsScalarTower R S M] [Module.Finite R S] |
There was a problem hiding this comment.
There could be an additional iff lemma that builds on the above result for compact modules.
| (fun N : Submodule R M ↦ IsOpen (N : Set M)) (fun N : Submodule R M ↦ (N : Set M)) := | ||
| ⟨fun _ ↦ hasBasis_open_submodule R, fun h ↦ .mk_of_hasBasis R h⟩ | ||
|
|
||
| theorem _root_.isLinearTopology_iff_exists_submodule_isOpen_subset [ContinuousAdd M] : |
There was a problem hiding this comment.
Is this very useful?
There was a problem hiding this comment.
I second Antoine's opinion: in a lot of cases, it is better to use the HasBasis API rather than go back to that explicit statement.
That said, I don't think we can make an argument for not having this lemma at all, since this is not the last time people will look for it. I think the best is to put it here with a comment suggesting to try using the HasBasis version instead.
There was a problem hiding this comment.
Would you be more happy with
IsLinearTopology R M ↔
∀ s ∈ 𝓝 0, ∃ N : Submodule R M, IsOpen (X := M) N ∧ (N : Set M) ⊆ s
I guess my point of introducing this lemma is that the inverse direction (contains open submodule => is neighborhood) is trivial and it is annoying to prove it every time.
| IsLinearTopology R M := by | ||
| rw [isLinearTopology_iff_hasBasis_submodule] at hS ⊢ | ||
| exact hS.to_hasBasis' (fun N hN ↦ ⟨N.restrictScalars R, hN, by simp⟩) (by simp) |
There was a problem hiding this comment.
| IsLinearTopology R M := by | |
| rw [isLinearTopology_iff_hasBasis_submodule] at hS ⊢ | |
| exact hS.to_hasBasis' (fun N hN ↦ ⟨N.restrictScalars R, hN, by simp⟩) (by simp) | |
| IsLinearTopology R M := | |
| .mk_of_hasBasis' R hS.hasBasis_submodule fun N r _ ↦ N.smul_of_tower_mem r |
| (fun N : Submodule R M ↦ IsOpen (N : Set M)) (fun N : Submodule R M ↦ (N : Set M)) := | ||
| ⟨fun _ ↦ hasBasis_open_submodule R, fun h ↦ .mk_of_hasBasis R h⟩ | ||
|
|
||
| theorem _root_.isLinearTopology_iff_exists_submodule_isOpen_subset [ContinuousAdd M] : |
There was a problem hiding this comment.
I second Antoine's opinion: in a lot of cases, it is better to use the HasBasis API rather than go back to that explicit statement.
That said, I don't think we can make an argument for not having this lemma at all, since this is not the last time people will look for it. I think the best is to put it here with a comment suggesting to try using the HasBasis version instead.
| refine isLinearTopology_iff_exists_submodule_isOpen_subset.mpr fun s hs h0s ↦ ?_ | ||
| obtain ⟨V, hV⟩ := NonarchimedeanAddGroup.is_nonarchimedean s (hs.mem_nhds h0s) | ||
| exact ⟨V.1.toIntSubmodule, V.2, hV⟩ |
There was a problem hiding this comment.
The real way to trivialize this lemma and the one above would be to have a proper description of NonarchimedeanGroup in terms of filter bases, which simply doesn't exist at the time being!
Adding the lemmas would be relatively easy, but it might be worth changing the definition as well... although I'm not sure how disturbing this would be for the FLT team...
| obtain ⟨V, hV⟩ := NonarchimedeanAddGroup.is_nonarchimedean s (hs.mem_nhds h0s) | ||
| exact ⟨V.1.toIntSubmodule, V.2, hV⟩ | ||
|
|
||
| instance [NonarchimedeanAddGroup M] : IsLinearTopology ℤ M := |
There was a problem hiding this comment.
I think this duplication is essentially unavoidable, and I believe the instance is essentially harmless (note there are no possible loops because IsLinearTopology --> NonarchimedeanAddGroup cannot be an instance).
|
|
||
| variable [TopologicalSpace R] [CompactSpace R] [ContinuousSMul R M] | ||
|
|
||
| lemma _root_.Submodule.isOpen_leAddSubgroup_of_compactSpace |
There was a problem hiding this comment.
Is there a result about modules over linearly compact algebras which would generalize both this and of_restrictScalars ?
There was a problem hiding this comment.
In another direction: @AntoineChambert-Loir, do you see some lemma about "group with operators" (and some kind of compactness on the operators) which would encompass both this lemma and e.g IsTopologicalGroup.exist_openSubgroup_sub_clopen_nhd_of_one ?
I'm not suggesting that we formalize linearly compact algebras nor groups with operators for the sake of this PR of course, these are mostly potential future additions.
There was a problem hiding this comment.
Tu as le nez creux.
It seems both this result and the one of this PR are precisely particular cases of a similarly stated results for groups with operators, and I'd guess the proofs are the same — how couldn't they? (Does mathlib have groups with operators?)
|
Let me override the proposed automated assignment and assign both Anatole and Antoine, as you have been reviewing this PR already. |
|
This pull request has conflicts, please merge |
...for topological modules over compact rings or
ℤ-finite rings