ClopenNaturality.lean`

2 declarations, 0 contain sorry, 0 declared as axioms

Restriction across a proper map

If the preimage of a compact open component is exactly the specified compact open component of the source, the corresponding KK restrictions commute with pushforward. The identity is proved on functions first.

theorem OAI.CoarseAssembly.Analytic.pullback_zeroExtension line 23

theorem OAI.CoarseAssembly.Analytic.restrictComponent_natural line 41

Source documentation

This is the coordinate restriction identity used by the changing finite-component index test. It is derived from the geometric preimage identity, without invoking or assuming a global detection theorem.

theorem restrictComponent_natural (e : A ↪ X) (he : IsOpenEmbedding e)
    (d : B ↪ Y) (hd : IsOpenEmbedding d) (f : CocompactMap X Y) (g : CocompactMap A B)
    (commutes : ∀ a, f (e a) = d (g a))
    (preimage : ∀ x, f x ∈ Set.range d ↔ x ∈ Set.range e) :
    (restrictComponent d hd).comp (pushforward f) =
      (pushforward g).comp (restrictComponent e he) := by
…

Mentions: OAI.CoarseAssembly.Analytic.restrictComponent, OAI.CoarseAssembly.Analytic.pushforward