Zulip Chat Archive

Stream: maths

Topic: cover with property


view this post on Zulip Johan Commelin (May 01 2019 at 07:10):

In the definition of adic_space we have:

(Hlocally_affinoid :  (I : Type u) (U : I  opens X) (Hcover : set.Union (λ i, (U i).1) = set.univ)
  (R : I  Huber_pair.{u}),
   i : I, nonempty (𝒞.equiv (𝒞.Spa (R i)) (𝒞.restrict (U i) locally_ringed_valued_space.to_𝒞)))

https://github.com/leanprover-community/lean-perfectoid-spaces/blob/master/src/adic_space.lean#L402
On the other hand, in the definition of perfectoid_space we have

(perfectoid_cover :  x : X,  (U : opens X) (A : Huber_pair) [perfectoid_ring A],
(x  U)  (𝒞.Spa A) _𝒞 (locally_ringed_valued_space.to_𝒞.restrict U))

https://github.com/leanprover-community/lean-perfectoid-spaces/blob/master/src/perfectoid_space.lean#L28

Both express the condition that there exists a cover of the space by open subsets satisfying some condition. However, they are phrased a bit differently. Are there reasons to prefer one over the other? Does mathlib already have some sort of preference/standard here?

view this post on Zulip Kevin Buzzard (May 01 2019 at 07:14):

To clarify a bit: I guess we want to say, on two occasions, that our topological space XX is covered by open sets each of which has a nice property; the first time we say "there's a random type II and a map from II to the set of open subsets of XX such that the union of the image sets is XX"; the second time we say xXUX\forall x\in X\, \exists U\subseteq X open with xUx\in U and UU nice.


Last updated: May 10 2021 at 06:13 UTC