Morphisms over a base: uniqueness under conjugation; the part of a restriction

General facts behind the independence and the gluing of the local resolutions along an exhaustion (resolutionOn_indep, resolutionGlues_of_isEmbeddedDesing of Hironaka/Resolution/Analytic/Kol07Thm45/GluingProperties.lean; the gluing of local desingularizations of [Wlo09, §4, §4.3]):

• CategoryTheory.uniq_of_conj: in any category, if the isomorphisms over a base Z between A' and B' are unique, so are those between A and B for any A ≅ A', B ≅ B' over Z — conjugation by the two identifications is injective and preserves "over Z";
• CategoryTheory.over_of_conj_inv_hom: conjugating a morphism over Z by isomorphisms over Z gives a morphism over Z;
• KLocallyRingedSpace.exists_iso_restrictOpen_restrictOpen_comap: for a K-morphism g : A ⟶ Z and opens U ⊆ A, U' ⊆ Z with g(U) ⊆ U', the part of the restriction A|U over an open O whose preimage lies in U (through g|U ≫ ofRestrict Z U') is the part of A over O, over Z — the identification through which the gluing of the restricted resolutions along an exhaustion reads the isomorphisms of the full glued spaces (it needs only g⁻¹O ⊆ U, not U = g⁻¹U').

The remaining lemmas — conj_conj_inv (conjugating back and forth is the identity), over_comp₃ (a composite of three morphisms over the base is over the base), over_inv_of_over (the inverse of an isomorphism over the base) and conj_over_eq (the structure maps under conjugation) — are the bookkeeping of conjugation and composition over the base.

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

theorem CategoryTheory.uniq_of_conj {C : Type u_1} [Category.{u_2, u_1} C] {A A' B B' Z : C} (πA : A ⟶ Z) (πA' : A' ⟶ Z) (πB : B ⟶ Z) (πB' : B' ⟶ Z) (a : A ≅ A') (b : B ≅ B') (ha : CategoryStruct.comp a.hom πA' = πA) (hb : CategoryStruct.comp b.hom πB' = πB) (huniq : ∀ (s s' : A' ⟶ B'), IsIso s → IsIso s' → CategoryStruct.comp s πB' = πA' → CategoryStruct.comp s' πB' = πA' → s = s') (s s' : A ⟶ B) (hs : IsIso s) (hs' : IsIso s') (hc : CategoryStruct.comp s πB = πA) (hc' : CategoryStruct.comp s' πB = πA) : s = s'

Uniqueness of the morphisms over a base transports along isomorphisms over the base: with a : A ≅ A', b : B ≅ B' over Z (a.hom ≫ πA' = πA, b.hom ≫ πB' = πB), two isomorphisms s s' : A ⟶ B over Z conjugate to isomorphisms a.inv ≫ s ≫ b.hom over Z from A' to B', which agree by hypothesis; cancelling the isomorphisms gives s = s'.

theorem CategoryTheory.over_of_conj_inv_hom {C : Type u_1} [Category.{u_2, u_1} C] {A A' B B' Z : C} (a : A ≅ A') (b : B ≅ B') (pA : A ⟶ Z) (pA' : A' ⟶ Z) (pB : B ⟶ Z) (pB' : B' ⟶ Z) (ha : CategoryStruct.comp a.inv pA = pA') (hb : CategoryStruct.comp b.hom pB' = pB) (s : A ⟶ B) (hs : pA = CategoryStruct.comp s pB) : pA' = CategoryStruct.comp (CategoryStruct.comp a.inv (CategoryStruct.comp s b.hom)) pB'

Conjugating a morphism over a base by isomorphisms over the base gives a morphism over the base: pA' = (a.inv ≫ s ≫ b.hom) ≫ pB' from pA = s ≫ pB, a.inv ≫ pA = pA' and b.hom ≫ pB' = pB.

theorem CategoryTheory.conj_conj_inv {C : Type u_1} [Category.{u_2, u_1} C] {A A' B B' : C} (a : A ≅ A') (b : B ≅ B') (f : A ⟶ B) : CategoryStruct.comp a.hom (CategoryStruct.comp (CategoryStruct.comp a.inv (CategoryStruct.comp f b.hom)) b.inv) = f

Conjugating back and forth is the identity: a.hom ≫ (a.inv ≫ f ≫ b.hom) ≫ b.inv = f.

theorem CategoryTheory.over_comp₃ {C : Type u_1} [Category.{u_2, u_1} C] {A B C' D YA YB YC YD Z : C} (e : A ⟶ B) (t : B ⟶ C') (f : C' ⟶ D) (ofA : A ⟶ YA) (ofB : B ⟶ YB) (ofC : C' ⟶ YC) (ofD : D ⟶ YD) (pA : YA ⟶ Z) (pB : YB ⟶ Z) (pC : YC ⟶ Z) (pD : YD ⟶ Z) (he : CategoryStruct.comp ofA pA = CategoryStruct.comp (CategoryStruct.comp e ofB) pB) (ht : CategoryStruct.comp ofB pB = CategoryStruct.comp (CategoryStruct.comp t ofC) pC) (hf : CategoryStruct.comp ofC pC = CategoryStruct.comp (CategoryStruct.comp f ofD) pD) : CategoryStruct.comp ofA pA = CategoryStruct.comp (CategoryStruct.comp (CategoryStruct.comp e (CategoryStruct.comp t f)) ofD) pD

A composite of three morphisms over a base, each over the base in the "restricted" form ofR ≫ p = (e ≫ ofR') ≫ p', is over the base.

theorem CategoryTheory.over_inv_of_over {C : Type u_1} [Category.{u_2, u_1} C] {A A' Y Y' Z : C} (α : A ⟶ A') [IsIso α] (ofR : A ⟶ Y) (ofR' : A' ⟶ Y') (p : Y ⟶ Z) (p' : Y' ⟶ Z) (h : CategoryStruct.comp ofR p = CategoryStruct.comp (CategoryStruct.comp α ofR') p') : CategoryStruct.comp ofR' p' = CategoryStruct.comp (CategoryStruct.comp (inv α) ofR) p

The inverse of an isomorphism over a base (restricted form) is over the base.

theorem CategoryTheory.conj_over_eq {C : Type u_1} [Category.{u_2, u_1} C] {A A' B B' Y Y' Z : C} (a : A ⟶ A') (s : A' ⟶ B') (b : B' ⟶ B) (ofA : A ⟶ Y) (ofA' : A' ⟶ Y) (ofB : B ⟶ Y') (ofB' : B' ⟶ Y') (p : Y ⟶ Z) (p' : Y' ⟶ Z) (ha : CategoryStruct.comp a ofA' = ofA) (hb : CategoryStruct.comp b ofB = ofB') (hs : CategoryStruct.comp ofA' p = CategoryStruct.comp (CategoryStruct.comp s ofB') p') : CategoryStruct.comp (CategoryStruct.comp a (CategoryStruct.comp s b)) (CategoryStruct.comp ofB p') = CategoryStruct.comp ofA p

A morphism over a base, conjugated by two identifications over the base, followed by the target's structure map, is the source's structure map: (a ≫ s ≫ b) ≫ ofB ≫ p' = ofA ≫ p.

theorem AnalyticSpace.KLocallyRingedSpace.exists_iso_restrictOpen_restrictOpen_comap {K : Type} [RCLike K] {A Z : KLocallyRingedSpace K} (g : A ⟶ Z) (U : TopologicalSpace.Opens ↑↑A.toPresheafedSpace) (U' : TopologicalSpace.Opens ↑↑Z.toPresheafedSpace) (h : ∀ a ∈ U, Hom.toFun g a ∈ U') (O : TopologicalSpace.Opens ↑↑Z.toPresheafedSpace) (hOU : ∀ (a : ↑↑A.toPresheafedSpace), Hom.toFun g a ∈ O → a ∈ U) : ∃ (e : (A.restrictOpen U).restrictOpen ((TopologicalSpace.Opens.comap { toFun := Hom.toFun (CategoryTheory.CategoryStruct.comp (Hom.restrictTo g U U' h) (Z.ofRestrict U')), continuous_toFun := ⋯ }) O) ⟶ A.restrictOpen ((TopologicalSpace.Opens.comap { toFun := Hom.toFun g, continuous_toFun := ⋯ }) O)), CategoryTheory.IsIso e ∧ CategoryTheory.CategoryStruct.comp ((A.restrictOpen U).ofRestrict ((TopologicalSpace.Opens.comap { toFun := Hom.toFun (CategoryTheory.CategoryStruct.comp (Hom.restrictTo g U U' h) (Z.ofRestrict U')), continuous_toFun := ⋯ }) O)) (CategoryTheory.CategoryStruct.comp (Hom.restrictTo g U U' h) (Z.ofRestrict U')) = CategoryTheory.CategoryStruct.comp (CategoryTheory.CategoryStruct.comp e (A.ofRestrict ((TopologicalSpace.Opens.comap { toFun := Hom.toFun g, continuous_toFun := ⋯ }) O))) g

The part of the restriction g|U : A|U ⟶ Z|U' over an open O with g⁻¹O ⊆ U is the part of A over O, over Z: the two open immersions (A|U)|_{(g|U)⁻¹O} ⟶ A|U ⟶ A and A|g⁻¹O ⟶ A have the same range (isoOfRangeEq).