feat(Topology/Algebra/Valued): IsLinearTopology 𝒪[K] K and 𝒪[K] 𝒪[K]#24627
feat(Topology/Algebra/Valued): IsLinearTopology 𝒪[K] K and 𝒪[K] 𝒪[K]#24627
IsLinearTopology 𝒪[K] K and 𝒪[K] 𝒪[K]#24627Conversation
as well as `IsDiscreteValuationRing 𝒪[ℚ_[p]]` `IsLinearTopology ℤ_[p] ℤ_[p]`
PR summary 81ccf8f455Import changes for modified filesNo significant changes to the import graph Import changes for all files
|
|
Looks like you have updated the proofs not to require DVR assumptions, but you have not updated the lemma names to match? If the comment about Qp not being |
|
Thanks, I fixed the name, and expanded the implementation notes to explain why |
Co-authored-by: David Loeffler <d.loeffler.01@cantab.net>
…anprover-community/mathlib4 into pechersky/linear-top-val-ring
Co-authored-by: github-actions[bot] <41898282+github-actions[bot]@users.noreply.github.com>
…anprover-community/mathlib4 into pechersky/linear-top-val-ring
with TODO
Co-authored-by: David Loeffler <d.loeffler.01@cantab.net>
doesn't require Valued
|
This pull request has conflicts, please merge |
|
This PR/issue depends on: |
| simpa [mem_nhds_zero] using hI.mem_nhds I.zero_mem | ||
|
|
||
| instance IsLinearTopology.of_valued' : | ||
| IsLinearTopology 𝒪[K] 𝒪[K] := by |
There was a problem hiding this comment.
Is there a way to make this rely less on the specific defeq of the ring of integers? And more on a predicate that asserts that K is the ring of fractions of some domain 𝒪 (+ suitable hyps, of course)
There was a problem hiding this comment.
Is this comment about IsLinearTopology 𝒪[K] K in particular?
There was a problem hiding this comment.
Not too particular. I'm generally somewhat concerned about API relying on such defeqs. If you think that concern should be dealt with in a separate PR, than I think that's fair.
I'm interested in what you think about this.
There was a problem hiding this comment.
Let me know if the generalization is acceptable.
There was a problem hiding this comment.
I'm happy to merge this for now. But eventually we should transition the API away from 𝒪[K], and state everything in terms of predicates.
…-community/mathlib4 into pechersky/linear-top-val-ring
|
Am I correct that the titular results follows from #23758 and infer instance? |
|
No, unfortunately: In fact, neither of the following synths either: |
| lemma IsLinearTopology.of_isOpenEmbedding {R K : Type*} [CommRing R] [rTop : TopologicalSpace R] | ||
| [ContinuousAdd R] [hl : IsLinearTopology R R] | ||
| [CommRing K] [kTop : TopologicalSpace K] [ContinuousAdd K] -- inferrable from ContinuousAdd R? | ||
| [Algebra R K] (h : IsOpenEmbedding (algebraMap R K)) : | ||
| IsLinearTopology R K := by |
There was a problem hiding this comment.
This looks good to me.
Does #find_home give something useful?
| simpa [mem_nhds_zero] using hI.mem_nhds I.zero_mem | ||
|
|
||
| instance IsLinearTopology.of_valued' : | ||
| IsLinearTopology 𝒪[K] 𝒪[K] := by |
There was a problem hiding this comment.
I'm happy to merge this for now. But eventually we should transition the API away from 𝒪[K], and state everything in terms of predicates.
| variable (K : Type*) {Γ₀ : Type*} [Field K] [LinearOrderedCommGroupWithZero Γ₀] [Valued K Γ₀] | ||
|
|
||
| lemma isOpenEmbedding_algebraMap_integer : | ||
| Topology.IsOpenEmbedding (algebraMap 𝒪[K] K) := |
There was a problem hiding this comment.
Eg results like the ones you add here should probably also generalize away from the defeq ring of integers.
Fair, but what is the predicate that is available to TC search? |
|
Yes something about integral closures, just like in the case of number fields. (And then something about topologies.) |
|
This pull request has conflicts, please merge |
as well as
IsLinearTopology ℤ_[p] ℤ_[p]