Rigidity of the local resolutions over X

Kollár's descent of the centres from the disjoint union of an affine cover — the pieces of the centre agree on the overlaps, (37.2) in [Kol07, Proposition 37, proof] — and the uniqueness of the canonical isomorphisms of the local resolutions [Kol07, Theorem 36, proof]; Włodarczyk's transitions over the overlaps [Wlo09, §4, (3)⇒(4)]. The independence of the local resolution from the embedding, taken as the hypothesis hind : LocalResolutionIndependentOn X bed, says the isomorphism over the base between two local resolutions is UNIQUE. Read at one local resolution against itself, this is RIGIDITY: every automorphism over X of a part of a local resolution over a base open is the identity — the haut hypothesis of isoOver_unique_of_aut (LocalModel.lean), named RigidOver. This module supplies it for the FOUR maps to X that the resolutions carry, each by hind's uniqueness applied to the given automorphism AND to 𝟙:

• PieceEmbedding.rigidOver_toSpaceMap: the parts of a piece's local resolution over ANY open under its base open (toSpaceMap), by the cover argument of transition_unique at one embedding — exists_localTransition_pair E E at each point, then hom_ext_of_cover; with the corollary rigidOver_toSpaceMap_domOpens at O := E.domOpens Q, Q ≤ W (domOpens_mono);
• LocalEmbeddingData.rigidOver_pieceToSpace: the pieces of a gluing datum (pieceToSpace) — transition_unique at i = j;
• LocalEmbeddingData.rigidOver_resolutionOnToSpace: the glued resolutionOn (resolutionOnToSpace) — the uniqueness clause of exists_isoOver_resolutionOn D D;
• BEDanFamStar.ExhaustionGluing.rigidOver_descMap: the exhaustion glue (descMap) — ExhaustionGluing.isoOver_eq_id (LocalModel.lean), repackaged.

The datum-level and resolutionOn-level forms are the rigidity hypotheses of the gluing of the exceptional families (compatClosedSubspaces_pair_of_forall_exists_isoOver, eq_tOver_of_isoOver; CoproductGluedFamilyCompat.lean, ExhaustionChainFamilies.lean); the piece-level and exhaustion-glue forms are stated for completeness and have no user in the library. Not in the sources beyond the remarks cited; bookkeeping.

theorem Hironaka.Manifold.PieceEmbedding.rigidOver_toSpaceMap {𝕜 : Type} [RCLike 𝕜] {X : AnalyticSpace 𝕜} {n : ℕ} {V : Set ↑↑X.toPresheafedSpace} (E : PieceEmbedding 𝕜 n X V) (hV : IsOpen V) (bed : BEDanFamStar 𝕜) (hbed : BEDanFamStar.IsEmbeddedDesing 𝕜 bed) (hind : LocalResolutionIndependentOn X bed) (W : TopologicalSpace.Opens (pieceAmbient 𝕜 E.G).carrier) (hW : IsCompact (closure ↑W)) (O : TopologicalSpace.Opens ↑↑X.toPresheafedSpace) (hO : O ≤ E.domOpens W) : AnalyticSpace.KLocallyRingedSpace.RigidOver (E.toSpaceMap bed W hW) O

The parts of a piece's local resolution are rigid over X ([Kol07, Theorem 36, proof]; [Wlo09, §4, (3)⇒(4)]; with the independence as hind) — every automorphism over X of the part over an open O under the base open is the identity. The argument of transition_unique at ONE embedding: at every point of O the unique local transition of E with itself (exists_localTransition_pair) is what BOTH t and 𝟙 restrict to (restrictOver, isIso_restrictOver, restrictOver_over), and morphisms agreeing on a cover agree (hom_ext_of_cover, comp_eq_of_restrict_eq, restrictOver_comp_restrictIncl).

theorem Hironaka.Manifold.PieceEmbedding.rigidOver_toSpaceMap_domOpens {𝕜 : Type} [RCLike 𝕜] {X : AnalyticSpace 𝕜} {n : ℕ} {V : Set ↑↑X.toPresheafedSpace} (E : PieceEmbedding 𝕜 n X V) (hV : IsOpen V) (bed : BEDanFamStar 𝕜) (hbed : BEDanFamStar.IsEmbeddedDesing 𝕜 bed) (hind : LocalResolutionIndependentOn X bed) (W : TopologicalSpace.Opens (pieceAmbient 𝕜 E.G).carrier) (hW : IsCompact (closure ↑W)) (Q : TopologicalSpace.Opens (pieceAmbient 𝕜 E.G).carrier) (hQ : Q ≤ W) : AnalyticSpace.KLocallyRingedSpace.RigidOver (E.toSpaceMap bed W hW) (E.domOpens Q)

The named form — rigidity over the base open domOpens Q of an ambient open Q ≤ W.

theorem Hironaka.Manifold.LocalEmbeddingData.rigidOver_pieceToSpace {𝕜 : Type} [RCLike 𝕜] {X : AnalyticSpace 𝕜} {U : Set ↑↑X.toPresheafedSpace} (D : LocalEmbeddingData 𝕜 X U) (bed : BEDanFamStar 𝕜) (W : (i : D.ι) → TopologicalSpace.Opens (pieceAmbient 𝕜 (D.embedding i).G).carrier) (hW : ∀ (i : D.ι), IsCompact (closure ↑(W i))) (hbed : BEDanFamStar.IsEmbeddedDesing 𝕜 bed) (hind : LocalResolutionIndependentOn X bed) (i : D.ι) (O : TopologicalSpace.Opens ↑↑X.toPresheafedSpace) (hO : O ≤ D.pieceDom i (W i)) : AnalyticSpace.KLocallyRingedSpace.RigidOver (D.pieceToSpace bed i (W i) ⋯) O

The parts of a datum's pieces are rigid over X (with the independence as hind) — transition_unique at i = j, for the automorphism and for 𝟙.

theorem Hironaka.Manifold.LocalEmbeddingData.rigidOver_resolutionOnToSpace {𝕜 : Type} [RCLike 𝕜] {X : AnalyticSpace 𝕜} {U : Set ↑↑X.toPresheafedSpace} (D : LocalEmbeddingData 𝕜 X U) (bed : BEDanFamStar 𝕜) (hbed : BEDanFamStar.IsEmbeddedDesing 𝕜 bed) (hind : LocalResolutionIndependentOn X bed) (O : TopologicalSpace.Opens ↑↑X.toPresheafedSpace) (hO : ↑O ⊆ U) : AnalyticSpace.KLocallyRingedSpace.RigidOver (D.resolutionOnToSpace bed) O

The parts of the glued resolutionOn are rigid over X (with the independence as hind) — the uniqueness clause of exists_isoOver_resolutionOn D D, for the automorphism and for 𝟙.

theorem Hironaka.Manifold.BEDanFamStar.ExhaustionGluing.rigidOver_descMap {𝕜 : Type} [RCLike 𝕜] (bed : BEDanFamStar 𝕜) (X : AnalyticSpace 𝕜) (Ξ : bed.ExhaustionGluing X) (hbed : IsEmbeddedDesing 𝕜 bed) (hind : LocalResolutionIndependentOn X bed) (O : TopologicalSpace.Opens ↑↑X.toPresheafedSpace) : AnalyticSpace.KLocallyRingedSpace.RigidOver Ξ.glue.descMap O

The parts of the exhaustion glue are rigid over X — ExhaustionGluing.isoOver_eq_id (LocalModel.lean), in the RigidOver spelling.