def

ValuationSpectrum.limitRestrict

Mathematical summary.

For an inclusion W ⊆ V, limitRestrict is the restriction homomorphism 𝒪_X(V) → 𝒪_X(W). A rational subdomain contained in W is also contained in V, so the map simply reindexes the compatible family and forgets the other coordinates.

The mathematical summary is editorial text for this paper. The declaration below is extracted verbatim from the pinned source.

Original Lean docstring

Restriction 𝒪_X(V) → 𝒪_X(W) for W ≤ V: reindex the compatible family along
RationalIndex.mono.

Used in the paper for: Appendix A (restriction on arbitrary opens); Appendix: restriction between arbitrary opens

def limitRestrict {V W : TopologicalSpace.Opens ↥(Spa A A⁺)} (h : W ≤ V) :
    ↥(limitSections V) →+* ↥(limitSections W) where
  toFun x := ⟨fun i => (x : ∀ j : RationalIndex V, presheafValue j.D) (i.mono h),
    fun i j hij => x.2 (i.mono h) (j.mono h) hij⟩
  map_one' := rfl
  map_mul' _ _ := rfl
  map_zero' := rfl
  map_add' _ _ := rfl

Pinned source: Adic spaces/StructurePresheafLimit.lean:218–225
Commit 0a0d2be4c1104e5f52dc147cd28f1fec59fec6a3.

View this pinned source on GitHub. The declaration above is also embedded here so that the paper remains independent of branch movement.