def
ValuationSpectrum.limitSections
Mathematical summary.
For an open V ⊆ Spa(A,A⁺), limitSections V is the ring of compatible families (x_D), with x_D ∈ A⟨T_D/s_D⟩, indexed by all rational subdomains R(D) ⊆ V. Compatibility is imposed along every rational containment. It is therefore the concrete projective limit defining 𝒪_X(V), equipped with the projective-limit topology.
Original Lean docstring
The compatible families: elements of the product of the completed rational
localizations over RationalIndex V whose coordinates are intertwined by the canonical
restriction maps. This is Wedhorn's projective limit𝒪_X(V) = lim_{R(T/s) ⊆ V} A⟨T/s⟩ in its concrete model.
Used in the paper for: Appendix A (sections on an arbitrary open); Appendix: sections on an arbitrary open
def limitSections (V : TopologicalSpace.Opens ↥(Spa A A⁺)) :
Subring (∀ i : RationalIndex V, presheafValue i.D) where
carrier := {x | ∀ (i j : RationalIndex V)
(h : rationalOpen j.D.T j.D.s ⊆ rationalOpen i.D.T i.D.s),
restrictionMap i.D j.D h (x i) = x j}
one_mem' := fun i j h => by
show restrictionMapHom i.D j.D h 1 = 1
exact map_one _
mul_mem' := fun {x y} hx hy i j h => by
show restrictionMapHom i.D j.D h (x i * y i) = x j * y j
rw [map_mul]
exact congrArg₂ (· * ·) (hx i j h) (hy i j h)
zero_mem' := fun i j h => by
show restrictionMapHom i.D j.D h 0 = 0
exact map_zero _
add_mem' := fun {x y} hx hy i j h => by
show restrictionMapHom i.D j.D h (x i + y i) = x j + y j
rw [map_add]
exact congrArg₂ (· + ·) (hx i j h) (hy i j h)
neg_mem' := fun {x} hx i j h => by
show restrictionMapHom i.D j.D h (-x i) = -x j
rw [map_neg]
exact congrArg Neg.neg (hx i j h)