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 e3514f12e382a8ef8f0d2b8822ed9b792bcaf838.

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