Functoriality of the resolution for isomorphisms of open subspaces #
Kollár's resolution functor commutes with smooth morphisms [Kol07, Theorem 45(5)], through the
functoriality half of the proof of Theorem 36 (transport the local embedding along the
isomorphism, then the canonical isomorphism) [Kol07, Theorem 36, proof]; Włodarczyk's canonical
desingularization is functorial with respect to local analytic isomorphisms
[Wlo09, Theorem 2.0.1(3)] (the gluing commutes with them, [Wlo09, §4, (3)⇒(4)]). An isomorphism
φ : X|U ≅ Y|V of open subspaces of reduced spaces lifts to an isomorphism
ψ : R(X)|Π_X⁻¹U ≅ R(Y)|Π_Y⁻¹V with Π_Y|V ∘ ψ = φ ∘ Π_X|U — clause (5) of
exists_functorial_resolution (ResolutionAssembly.lean).
The argument (untwisted over X). R(Y)|Π_Y⁻¹V is viewed as a space over X through
Π_Y|V ≫ φ⁻¹ ≫ (X|U → X) (resolutionOverMap), so that the gluing of local isomorphisms over X,
exists_isIso_over_of_cover, glues LOCAL isomorphisms on a cover of U
(exists_localIsoOver_resolution) with UNIQUENESS from the triviality of the automorphisms of
R(X) over X (resolution_isoOver_eq_id; LocalModel.lean). The local isomorphism at x ∈ U:
a piece embedding F' of Y near φ x over an open O' ⊆ V, the restriction φ' := φ|O', the
transported embedding F'ᵗ := F'.transportAlongIso φ', ONE ambient open W; the local models
(exists_localModel) of R(X) at F'ᵗ and of R(Y) at F' are parts of the SAME local
resolution (same ambient, same ideal), whose maps to X and to Y differ by φ'
(comp_localResolutionToPiece_transportAlongIso); Q := φ(P) makes the two parts the same open
(toFun_restrictIsoTo_mem_imageOpen_iff,
Hironaka/Resolution/Analytic/Kol07Thm45/RestrictIsoOpen.lean). The independence of the local
resolution enters for X and for Y (hind, hindY).
Uniqueness of the lift (resolution_lift_unique). Two lifts ψ, ψ' of the same φ differ
by the automorphism ψ ≫ ψ'⁻¹ of R(X)|Π_X⁻¹U, which lies over X|U (cancel the isomorphism
φ), hence is the identity by resolution_isoOver_eq_id. So the lift is unique, and the lifts
respect identities and composition
(ResolutionAssignment.LiftsLocalIsomorphisms.lift_id_restrictSet,
ResolutionAssignment.LiftsLocalIsomorphisms.lift_comp_restrictSet, which use only the uniqueness
in the statement).
Not in the sources beyond the statements cited; bookkeeping.
The twist algebra of the local isomorphism, in any category: the
Y-side local model sY, the identification βinv of the part of R(Y)|V over P (through φ⁻¹)
with the part of R(Y) over φ(P), and the structure maps related by Π_{F'ᵗ} ≫ φ' = Π_{F'} and
φ' ≫ (Y|O' → Y|V) = (X|φ⁻¹O' → X|U) ≫ φ give: the part of the common local resolution over the
X-open, mapped to X, is the composite inv sY ≫ βinv followed by the view over X through
φ⁻¹ — the inverse of φ is cancelled after the monomorphism Y|V → Y.
The final square, in any category: the glued isomorphism s over X between the parts
over U (read through the identifications h1, h2 ≫ ofBt of the parts with the restrictions),
followed by Π_Y|V, is Π_X|U followed by φ — after cancelling φ⁻¹ and the monomorphism
X|U → X.
The automorphism ψ ≫ ψ'⁻¹ lies over the base, in any category: if ψ and ψ' both lie
over the monomorphism φ (ψ ≫ r_Y = r ≫ φ, ψ' ≫ r_Y = r ≫ φ), then (ψ ≫ ψ'⁻¹) ≫ r = r.
Conjugating an endomorphism over the base, in any category: if α ≫ r = r,
r ≫ oX = oA ≫ π and e : A ≅ A' lies over R (e.hom ≫ oA' = oA, e.inv ≫ oA = oA'), then
the conjugate e.inv ≫ α ≫ e.hom lies over X through oA' ≫ π.
An endomorphism whose conjugate by an isomorphism is the identity is the identity.
Two morphisms ψ, ψ' with ψ ≫ ψ'⁻¹ = 𝟙 are equal.
The image of the preimage of S lies in S.
The image is monotone.
A space over Y|V viewed over X through φ⁻¹: for Π : R → Y, the
part R|Π⁻¹V maps to X by Π|V ≫ φ⁻¹ ≫ (X|U → X).
Equations
- One or more equations did not get rendered due to their size.
Instances For
The part of R|Π⁻¹V over P through φ⁻¹ is the part of R over
φ(P): the open immersion (R|Π⁻¹V)|_{…} → R|Π⁻¹V → R has range the part of R over the image
open φ(P).
The part of R(Y) over V, viewed over X through φ⁻¹: Π_Y|V followed by the
inverse of φ : X|U ≅ Y|V and the open immersion X|U → X.
Equations
- One or more equations did not get rendered due to their size.
Instances For
Unfolding lemma: the view over X is the generic Hom.overMap at Π_Y.
The local isomorphism over φ, on the gluings: at every x ∈ U a small open P ∋ x,
P ⊆ U, and an isomorphism over X from the part of the glued space of X over P to the part
of the glued space of Y over V (viewed over X through φ⁻¹) over P — the local models
(exists_localModel, LocalModel.lean) of both sides at the same local resolution (F' of Y
near φ x over
O' ⊆ V, transported along φ' := φ|O' to X), identified through
Π_{F'ᵗ} ≫ φ' = Π_{F'} (comp_localResolutionToPiece_transportAlongIso) at Q := φ(P), and the
part of R(Y)|V over P read as the part of R(Y) over Q (range_ofRestrict_comp_overMap).
R(X) has no non-trivial automorphism over X on any part (X reduced, under hbed and
the independence hind) — ExhaustionGluing.isoOver_eq_id (LocalModel.lean) on the resolution
(resolutionPair_eq_of_glues).
The lift of an isomorphism of open subspaces is unique (X reduced, under hbed and the
independence hind): two isomorphisms ψ, ψ' : R(X)|Π_X⁻¹U ≅ R(Y)|Π_Y⁻¹V over the same
isomorphism φ : X|U ≅ Y|V are equal — ψ ≫ ψ'⁻¹ is an automorphism of R(X)|Π_X⁻¹U over
X|U (comp_inv_over_of_over), read on the part over U in the Opens.comap spelling, hence the
identity (resolution_isoOver_eq_id).
The local isomorphism over φ on the resolutions (X, Y reduced, under hbed and the
independences hind, hindY; φ an isomorphism of the open subspaces X|U ≅ Y|V, x ∈ U):
ExhaustionGluing.exists_localIsoOver for the chosen gluings of X and of Y
(resolutionPair_eq_of_glues).
The functoriality for isomorphisms of open subspaces (clause (5) of
exists_functorial_resolution; [Kol07, Theorem 45(5)] through [Kol07, Theorem 36, proof];
[Wlo09, Theorem 2.0.1(3)]), with the independence of the local resolution for X and for Y as
the hypotheses hind, hindY: an isomorphism φ : X|U ≅ Y|V of open subspaces of reduced spaces
lifts to an isomorphism ψ of the resolutions over U and V with Π_Y|V ∘ ψ = φ ∘ Π_X|U — the
local isomorphisms exists_localIsoOver_resolution on a cover of U, unique by
resolution_isoOver_eq_id and isoOver_unique_of_aut, glued by exists_isIso_over_of_cover over
X, read into the restrictions.
The lifts of isomorphisms between open subspaces respect composition: for a resolution
assignment R lifting local analytic isomorphisms (uniquely, LiftsLocalIsomorphisms), the lift
of a composite φ₁ ≫ φ₂ of isomorphisms X|U ≅ Y|V ≅ Z|W between open subspaces of inputs is the
composite of the lifts — ψ₁ ≫ ψ₂ lies over φ₁ ≫ φ₂, and the lift is the only morphism over
it.
The lifts of isomorphisms between open subspaces respect identities: for a resolution
assignment R lifting local analytic isomorphisms (uniquely, LiftsLocalIsomorphisms), the lift
of the identity of X|U is the identity.