Properness over an open of the target

Three general facts behind the properness of the resolution morphism over the members of an open cover ([Wlo09, §4]: "des_V : Ṽ → V is bimeromorphic and proper", checked on the pieces of the gluing; isProperMap_resolutionOnMap of Hironaka/Resolution/Analytic/Kol07Thm45/PieceGlueDatum.lean), stated for plain continuous maps and for K-morphisms:

• isProperMap_of_homeomorph_comp_eq: properness is invariant under conjugation by homeomorphisms of the source and of the target (f = e_B⁻¹ ∘ f' ∘ e_A) — the transport used to read the resolution morphism on the pieces and on the parts over the base opens;
• isProperMap_restrictPreimage_of_cover: a continuous map proper over each member of an open family V i of the target is proper over every U ⊆ ⋃ V i — isProperMap_of_restrictPreimage_cover of Hironaka/AnalyticSpace/CoverLemmas.lean (Mathlib's IsOpenCover.isClosedMap_iff_restrictPreimage) applied to the restriction over U and the cover {U ∩ V i} of U;
• isProperMap_toFun_restrictTo: the restriction g|U : A|U ⟶ B|U' of a K-morphism to opens with U = g⁻¹U' is proper as soon as g is proper over U' (the resolution morphism over an open is such a restriction); isProperMap_toFun_restrictSet for the restriction of the vocabulary.

Routine; used by Hironaka/AnalyticSpace/Glue/OverProper.lean and Hironaka/Resolution/Analytic/Kol07Thm45/ResolutionClauses.lean.

theorem AnalyticSpace.isProperMap_of_homeomorph_comp_eq {A : Type u_1} {B : Type u_2} {A' : Type u_3} {B' : Type u_4} [TopologicalSpace A] [TopologicalSpace B] [TopologicalSpace A'] [TopologicalSpace B'] (eA : A ≃ₜ A') (eB : B ≃ₜ B') {f : A → B} {f' : A' → B'} (hf' : IsProperMap f') (h : ∀ (a : A), eB (f a) = f' (eA a)) : IsProperMap f

Properness is invariant under conjugation by homeomorphisms of the source and of the target: if e_B ∘ f = f' ∘ e_A with f' proper, then f = e_B⁻¹ ∘ f' ∘ e_A is proper (Homeomorph.isProperMap, IsProperMap.comp).

def AnalyticSpace.nestedSubtypeSwap {A : Type u_1} [TopologicalSpace A] (p q : A → Prop) : { a : { a : A // p a } // q ↑a } ≃ₜ { a : { a : A // q a } // p ↑a }

Swapping two nested subtype conditions is a homeomorphism: {a : {a // p a} // q a} ≃ₜ {a : {a // q a} // p a} (both are the points with p ∧ q; the two orders of restricting a map over a set of the target arise in isProperMap_restrictPreimage_of_cover).

Equations

• One or more equations did not get rendered due to their size.

theorem AnalyticSpace.isProperMap_restrictPreimage_of_cover {Y : Type u_5} {X : Type u_6} [TopologicalSpace Y] [TopologicalSpace X] (f : Y → X) (hf : Continuous f) {ι : Type u_7} (V : ι → Set X) (hV : ∀ (i : ι), IsOpen (V i)) (h : ∀ (i : ι), IsProperMap ((V i).restrictPreimage f)) (U : Set X) (hUV : U ⊆ ⋃ (i : ι), V i) : IsProperMap (U.restrictPreimage f)

([Wlo09, §4]: the properness of des_V is checked over the members of the cover {V_i} of V.) A continuous map proper over each member of an open family V i of the target is proper over every U ⊆ ⋃ V i: isProperMap_of_restrictPreimage_cover (Hironaka/AnalyticSpace/CoverLemmas.lean) applied to the restriction f|_U : f⁻¹U → U with the open cover {U ∩ V i} of U; over U ∩ V i the restriction of f|_U is the restriction of f|_{V i} (IsProperMap.restrictPreimage), read through nestedSubtypeSwap.

theorem AnalyticSpace.KLocallyRingedSpace.isProperMap_toFun_restrictTo {K : Type} [RCLike K] {A B : KLocallyRingedSpace K} (g : A ⟶ B) (U : TopologicalSpace.Opens ↑↑A.toPresheafedSpace) (U' : TopologicalSpace.Opens ↑↑B.toPresheafedSpace) (h : ∀ a ∈ U, Hom.toFun g a ∈ U') (hset : ↑U = Hom.toFun g ⁻¹' ↑U') (hp : IsProperMap ((↑U').restrictPreimage (Hom.toFun g))) : IsProperMap (Hom.toFun (Hom.restrictTo g U U' h))

The restriction of a K-morphism to opens is proper when the morphism is proper over the target open: for g : A ⟶ B and opens U = g⁻¹U', the underlying map of g|U : A|U ⟶ B|U' is the restriction U'.restrictPreimage g read through the identification U = g⁻¹U' of the sources (Hom.toFun_restrictTo).

theorem AnalyticSpace.isProperMap_toFun_restrictSet {K : Type} [RCLike K] {X Y : AnalyticSpace K} (f : X ⟶ Y) {V : Set ↑↑Y.toPresheafedSpace} (hV : IsOpen V) (hp : IsProperMap (V.restrictPreimage ↑f)) : IsProperMap ↑(Hom.restrictSet f V)

The restriction f|_{f⁻¹V} : X|f⁻¹V ⟶ Y|V of a morphism of analytic spaces to an OPEN V of the target is proper when f is proper over V (Hom.restrictSet: for an open V the opens of the convention are V and f⁻¹V themselves, openOf_of_isOpen).