refactor(perfectoid_space): beautification #34
Conversation
|
|
||
| namespace sheaf_of_topological_rings | ||
|
|
||
| instance topological_space {X : Type*} [topological_space X] (𝒪X : sheaf_of_topological_rings X) | ||
| instance topological_space {X : Type u} [topological_space X] (𝒪X : sheaf_of_topological_rings X) |
There was a problem hiding this comment.
Why those changes from Type* to Type u? Is it faster to elaborate?
There was a problem hiding this comment.
I don't know anymore... but I guess it doesn't hurt.
| @@ -76,16 +80,16 @@ A morphism in 𝒞 is a map of top spaces, an f-map of presheaves, such that the | |||
| map on the stalks pulls one valuation back to the other. | |||
| -/ | |||
|
|
|||
| instance presheaf_of_rings.comm_ring {X : Type*} [topological_space X] | |||
| instance presheaf_of_rings.comm_ring {X : Type u} [topological_space X] | |||
There was a problem hiding this comment.
Why is all this in adic_space.lean? I feel like this file should be split a lot
There was a problem hiding this comment.
Let's do that in a follow-up PR.
src/adic_space.lean
Outdated
| noncomputable def 𝒞.Spa (A : Huber_pair) : 𝒞 (Spa A) := | ||
| { F := Spa.presheaf_of_topological_rings A, | ||
| valuation := λ x, Spv.mk (Spa.presheaf.stalk_valuation x) } | ||
| noncomputable def 𝒞.Spa (A : Huber_pair) : 𝒞 (spa A) := |
There was a problem hiding this comment.
Sure. I just needed a name and McC was short.
| (F : presheaf_of_topological_rings X) (U : opens X) : comm_ring (F U) := | ||
| F.Fring U | ||
|
|
||
| structure presheaf_of_rings.f_map | ||
| {X : Type*} [topological_space X] {Y : Type*} [topological_space Y] | ||
| {X : Type u} [topological_space X] {Y : Type u} [topological_space Y] | ||
| (F : presheaf_of_rings X) (G : presheaf_of_rings Y) := |
There was a problem hiding this comment.
So this is an actual change in our code right? We're going down to one universe. Was this forced upon us by other choices? My instinct would be to use one universe when it was convenient but not worry otherwise. I am still unclear about all of this. From a mathematical perspective it still seems absurd to come up with two topological spaces in different universes -- but these CS people know a whole lot more about writing libraries than us.
There was a problem hiding this comment.
Aah, right. This change was made because we were surprised that Huber_pair depended on three universe variables 😃
| and (an equivalence class of) valuations on the stalks (which are required to be local rings). | ||
| Wedhorn calls this category `𝒱`.-/ | ||
| structure CLVRS := | ||
| (space : Type) -- change this to (Type u) to enable universes |
There was a problem hiding this comment.
I think computer scientists would be equally unhappy with that name though. Should we call it something long and stupid, or maybe even comp_loc_val_ringed_space or something?
| @@ -14,42 +14,42 @@ import for_mathlib.sheaves.stalk_of_rings -- for defining valuations on stalks | |||
|
|
|||
| variable {A : Huber_pair} | |||
|
|
|||
| open topological_space valuation Spv Spa | |||
| open topological_space valuation Spv spa | |||
|
|
|||
There was a problem hiding this comment.
Does the actual name of this file need to be changed? I want to call it "A<T/s>" because that's what it's about.
There was a problem hiding this comment.
Let's do that in another PR
No description provided.