Uniform structures and boundedness #5
Conversation
|
For the record: this involved some set manipulation help from Reid Barton (see Zulip on June 9th at 16:30). |
src/adic_space.lean
Outdated
|
|
||
| section topological_ring | ||
|
|
||
| variables (R : Type*) [comm_ring R] [topological_space R] [comm_ring R] [topological_ring R] |
There was a problem hiding this comment.
You have [comm_ring R] twice.
src/adic_space.lean
Outdated
| -- Following is copy-pasted from t2_space class. | ||
| -- We need to think whether we could directly use that class | ||
| definition is_hausdorff (α : Type*) [topological_space α] : Prop := | ||
| ∀x y, x ≠ y → ∃u v : set α, is_open u ∧ is_open v ∧ x ∈ u ∧ y ∈ v ∧ u ∩ v = ∅ |
There was a problem hiding this comment.
I would prefer uppercase for the open subsets. But of course that is only a matter of notation. Also, does it make sense to use opens X in this case?
src/adic_space.lean
Outdated
|
|
||
| def nhd_zero := (nhds (0 : R)).sets | ||
| variable {R} | ||
| lemma nhd_zero_symmetric {V : set R} : V ∈ nhd_zero R → (λ a, -a) '' V ∈ nhd_zero R := |
There was a problem hiding this comment.
This doesn't use the ring structure, right? Should we just prove it for additive topological groups?
src/adic_space.lean
Outdated
| definition is_bounded | ||
| (B : set R) : Prop := ∀ U ∈ nhd_zero R, ∃ V ∈ nhd_zero R, ∀ v ∈ V, ∀ b ∈ B, v*b ∈ U | ||
|
|
||
| def power_set (r : R) : set R := set.range (λ n : ℕ, r^n) |
There was a problem hiding this comment.
This sounds a lot like "powerset" from basic set theory. Is it an idea to call this merely powers? Otherwise, I think it is good to at least include a user comment
/-- power_set r is the subset of the ring R consisting of all powers of r -/
There was a problem hiding this comment.
Kenny calls them powers in his ring theory stuff I think (we localise at the multiplicative set powers f IIRC)
src/adic_space.lean
Outdated
|
|
||
| -- Schol= : "Recall that a topological ring R is Tate if it contains an | ||
| -- open and bounded subring R0 ⊂ R and a topologically nilpotent unit pi ∈ R; such elements are | ||
| -- called pseudo-uniformizers."" | ||
| -- called pseudo-uni7formizers."" |
There was a problem hiding this comment.
Schol= -> Scholze as well (this was my fault)
src/adic_space.lean
Outdated
| -- Type implicit or explicit. | ||
| variables (R : Type) [comm_ring R] [topological_space R] [comm_ring R] [topological_ring R] | ||
| variables {A : Type} [comm_ring A] [topological_space A] [comm_ring A] [topological_ring A] | ||
|
|
There was a problem hiding this comment.
Did you mean to have comm_ring twice in these definitions?
src/adic_space.lean
Outdated
| refl := begin simp, intros i H r, exact mem_of_nhds H end, | ||
| symm := sorry, | ||
| comp := sorry } | ||
|
|
There was a problem hiding this comment.
Patrick I'm rather relieved you've stepped in here to unravel the uniform spaces and filters. But what are these sorrys?
src/adic_space.lean
Outdated
| -- type class resolution issues | ||
| definition power_bounded_subring := {r : R // is_power_bounded r} | ||
| definition power_bounded_subring_set := {r : R | is_power_bounded r} | ||
|
|
There was a problem hiding this comment.
Is this definitely what we're supposed to be doing? Chris Hughes seemed to be advocating the standard CS "asymmetric" approach where one of these types is deemed to be the "best" one and should be used if at all possible, and coercions should handle all the others.
src/adic_space.lean
Outdated
| end | ||
|
|
||
|
|
||
| instance toplogical_ring.to_uniform_space : uniform_space R := |
There was a problem hiding this comment.
Is this going to create a diamond-like problem for the type class system? We now have topological_ring → topological_space and now also the composition topological_ring → uniform_space → topological_space. I don't think they are defeq. Is this a problem?
src/adic_space.lean
Outdated
| def nhd_zero := (nhds (0 : R)).sets | ||
| variable {R} | ||
| lemma nhd_zero_symmetric {V : set R} : V ∈ nhd_zero R → (λ a, -a) '' V ∈ nhd_zero R := | ||
| begin |
There was a problem hiding this comment.
Do you think there's a simpler proof just saying "neg is continuous"?
src/adic_space.lean
Outdated
|
|
||
| instance toplogical_ring.to_uniform_space : uniform_space R := | ||
| uniform_space.of_core { | ||
| uniformity := (⨅ U ∈ nhd_zero R, principal {p : R×R | p.2 - p.1 ∈ U}), |
There was a problem hiding this comment.
It says in the docstring of uniform_space that a topological group has a uniform structure. Do you think this might already be proved in mathlib? If so, we could just apply it to the underlying additive group of R, right?
src/adic_space.lean
Outdated
| variable (R) | ||
| /-- Wedhorn Definition 5.31 page 38 -/ | ||
| definition is_complete : Prop := is_hausdorff R ∧ ∀ {f:filter R}, cauchy f → ∃x, f ≤ nhds x | ||
|
|
There was a problem hiding this comment.
Do you think the definition of Cauchy in mathlib coincides with the definition in Wedhorn? Wedhorn's definition relies on the topological group structure.
|
I've completely redone the uniform space stuff. Now it is defined for commutative topological groups and gives back the original topology. I also addressed the minor comments. It should be ready for merge. |
The main point of this PR is to define the uniform structure on topological rings. This allows to unsorry the definition of
is_complete. It defines basic boundedness properties.