ValuationSpectrum.IsLimitSheaf
Mathematical summary.
For every open V ⊆ Spa(A,A⁺) and every open cover V = ⋃ᵢ Uᵢ, sections are separated, compatible families glue, and the restriction map 𝒪(V) → ∏ᵢ 𝒪(Uᵢ) is a topological embedding. This is the all-open topological sheaf condition used in the paper.
Original Lean docstring
The genuine all-open structure presheaf is a sheaf of topological rings
(bundled; Wedhorn Remark 8.20 for the projective-limit presheaf): separation and
gluing of the underlying ring presheaf for every open cover of every open, and
the topological-embedding condition for every open cover. The cover index lives in the
ring's universe (covers in use are (sub)types of RationalLocData A-data; larger
index types factor through their ranges).
Used in the paper for: Appendix A (all-open sheaf condition); Appendix: all-open sheaf condition
structure IsLimitSheaf (A : Type u) [CommRing A] [TopologicalSpace A]
[IsTopologicalRing A] [PlusSubring A] [IsHuberRing A]
[HasLocLiftPowerBounded A] : Prop where
/-- Separation: sections agreeing on a cover agree. -/
injective : ∀ {V : Opens ↥(Spa A A⁺)} {ι : Type u} {U : ι → Opens ↥(Spa A A⁺)}
(hle : ∀ i, U i ≤ V)
(_ : (V : Set ↥(Spa A A⁺)) ⊆ ⋃ i, (U i : Set ↥(Spa A A⁺)))
{x y : ↥(limitSections V)},
(∀ i, limitRestrict (hle i) x = limitRestrict (hle i) y) → x = y
/-- Gluing: compatible families glue. -/
glue : ∀ {V : Opens ↥(Spa A A⁺)} {ι : Type u} {U : ι → Opens ↥(Spa A A⁺)}
(hle : ∀ i, U i ≤ V)
(_ : (V : Set ↥(Spa A A⁺)) ⊆ ⋃ i, (U i : Set ↥(Spa A A⁺)))
(s : ∀ i, ↥(limitSections (U i))),
(∀ i j, limitRestrict (inf_le_left (a := U i) (b := U j)) (s i) =
limitRestrict (inf_le_right (a := U i) (b := U j)) (s j)) →
∃ x : ↥(limitSections V), ∀ i, limitRestrict (hle i) x = s i
/-- The restriction into the product over any open cover is a topological embedding. -/
isEmbedding : ∀ {V : Opens ↥(Spa A A⁺)} {ι : Type u} {U : ι → Opens ↥(Spa A A⁺)}
(hle : ∀ i, U i ≤ V)
(_ : (V : Set ↥(Spa A A⁺)) ⊆ ⋃ i, (U i : Set ↥(Spa A A⁺))),
Topology.IsEmbedding (limitRestrictProd hle)
/-- **C3+C4**: the finite rational-cover criterion implies that the genuine all-open