Isomorphisms over an open of the target: composition, monotonicity, transport

The predicate f.IsIsoOver V (f restricts to an isomorphism f⁻¹V → V; condition (2) of a resolution in [Hir64, Introduction], clause (2) of [Kol07, Theorem 45]) and its bookkeeping, needed to read off that the resolution morphism is an isomorphism over the simple locus piece by piece:

• Hom.restrictSet_comp: the restriction of a composite is the composite of the restrictions;
• Hom.isIsoOver_of_isOpenImmersion: an open immersion is an isomorphism over every open subset of its range (the point-level criterion isIso_restrictTo_of_bijOn_of_bijective_stalkMap);
• Hom.IsIsoOver.comp: f ≫ g is an isomorphism over V when g is over V and f over g⁻¹V;
• Hom.IsIsoOver.mono: an isomorphism over the open V is one over every open P ⊆ V (the criterion again, from injOn/surjOn/the stalk maps over V);
• Hom.IsIsoOver.of_isIso_restrictSet_comm: IsIsoOver transports along an isomorphism over the base (exists_restrictSet_isIso_of_restrictSet_isIso_of_subset of Hironaka/Resolution/Analytic/Kol07Thm45/AmbientFactorizationTransport.lean).

Routine; used by Hironaka/Resolution/Analytic/Kol07Thm45/Glue/OverIsoReg.lean and Hironaka/Resolution/Analytic/Kol07Thm45/CoproductLevelPair.lean.

theorem AnalyticSpace.KLocallyRingedSpace.Hom.restrictTo_comp {K : Type} [RCLike K] {A B Z : KLocallyRingedSpace K} (f : A ⟶ B) (g : B ⟶ Z) (U : TopologicalSpace.Opens ↑↑A.toPresheafedSpace) (U' : TopologicalSpace.Opens ↑↑B.toPresheafedSpace) (U'' : TopologicalSpace.Opens ↑↑Z.toPresheafedSpace) (hf : ∀ a ∈ U, toFun f a ∈ U') (hg : ∀ b ∈ U', toFun g b ∈ U'') (h : ∀ a ∈ U, toFun (CategoryTheory.CategoryStruct.comp f g) a ∈ U'') : restrictTo (CategoryTheory.CategoryStruct.comp f g) U U'' h = CategoryTheory.CategoryStruct.comp (restrictTo f U U' hf) (restrictTo g U' U'' hg)

The restriction of a composite to opens is the composite of the restrictions: both agree after the open immersion Z|U'' ⟶ Z (Hom.restrictTo_comp_ofRestrict).

theorem AnalyticSpace.Hom.restrictSet_comp {K : Type} [RCLike K] {A B X : AnalyticSpace K} (f : A ⟶ B) (g : B ⟶ X) (V : Set ↑↑X.toPresheafedSpace) : restrictSet (CategoryTheory.CategoryStruct.comp f g) V = CategoryTheory.CategoryStruct.comp (restrictSet f (↑g ⁻¹' V)) (restrictSet g V)

The restriction of a composite is the composite of the restrictions — Hom.restrictTo_comp at the opens openOf (the two spellings of (f ≫ g)⁻¹V are definitionally equal).

theorem AnalyticSpace.Hom.isIsoOver_of_isOpenImmersion {K : Type} [RCLike K] {B X : AnalyticSpace K} (g : B ⟶ X) [hg : AlgebraicGeometry.LocallyRingedSpace.IsOpenImmersion ↑g] {V : Set ↑↑X.toPresheafedSpace} (hV : IsOpen V) (hsub : V ⊆ Set.range (KLocallyRingedSpace.Hom.toFun g)) : IsIsoOver g V

An open immersion is an isomorphism over every open subset of its range: on g⁻¹V → V it is a bijection with bijective stalk maps (isIso_restrictTo_of_bijOn_of_bijective_stalkMap).

theorem AnalyticSpace.Hom.IsIsoOver.comp {K : Type} [RCLike K] {A B X : AnalyticSpace K} {f : A ⟶ B} {g : B ⟶ X} {V : Set ↑↑X.toPresheafedSpace} (hf : IsIsoOver f (↑g ⁻¹' V)) (hg : IsIsoOver g V) : IsIsoOver (CategoryTheory.CategoryStruct.comp f g) V

f ≫ g is an isomorphism over V when g is one over V and f one over g⁻¹V (Hom.restrictSet_comp).

theorem AnalyticSpace.Hom.IsIsoOver.mono {K : Type} [RCLike K] {X Y : AnalyticSpace K} {f : Y ⟶ X} {V P : Set ↑↑X.toPresheafedSpace} (hV : IsOpen V) (hP : IsOpen P) (hPV : P ⊆ V) (h : IsIsoOver f V) : IsIsoOver f P

An isomorphism over the open V is one over every open P ⊆ V: on f⁻¹P → P the map is a bijection (injOn/surjOn over V) with bijective stalk maps (bijective_stalkMap_of_isIso_restrictSet), so the point-level criterion applies.

theorem AnalyticSpace.Hom.IsIsoOver.of_isIso_restrictSet_comm {K : Type} [RCLike K] {X Y Y' : AnalyticSpace K} (f : Y ⟶ X) (f' : Y' ⟶ X) {O P : Set ↑↑X.toPresheafedSpace} (e : Y.restrictSet (KLocallyRingedSpace.Hom.toFun f ⁻¹' O) ⟶ Y'.restrictSet (KLocallyRingedSpace.Hom.toFun f' ⁻¹' O)) (he : CategoryTheory.IsIso e) (hcomm : CategoryTheory.CategoryStruct.comp e (restrictSet f' O) = restrictSet f O) (hP : IsOpen P) (hPO : P ⊆ O) (h : IsIsoOver f' P) : IsIsoOver f P

IsIsoOver transports along an isomorphism over the base: with e : Y|f⁻¹O ≅ Y'|f'⁻¹O over X|O and an open P ⊆ O, f' an isomorphism over P makes f one — f|P = e' ≫ f'|P for the restriction e' of e (exists_restrictSet_isIso_of_restrictSet_isIso_of_subset).