Lifts along open immersions of K-spaces, and double restrictions #
Bookkeeping for the gluing modules: a K-morphism into the source of an open immersion a : B ⟶ A
is determined by its composite with a (hom_ext_of_comp_eq, open immersions being monomorphisms),
and a K-morphism g : C ⟶ A whose range lies in that of a lifts uniquely through a
(liftAlong, liftAlong_comp, liftAlong_unique; Hom.restrictTo of
Hironaka.AnalyticSpace.Complexification is the case a = ofRestrict). The inclusion
incl₂ A U W : (A | U) | W ⟶ A of a double restriction is an open immersion with range the trace of
W on A (mem_range_toFun_incl₂).
Conventions. A | U is the open subspace restrictOpen; a point of (A | U) | W is a pair of
subtypes, x.1.1 : A. For a = 𝟙 A the lift is g itself; for W = ⊤, incl₂ is ofRestrict up
to the identification of Hironaka.AnalyticSpace.OpenSubspaceLemmas. Not in the sources.
Two K-morphisms into the source of an open immersion agree if they agree after it.
The lift of g : C ⟶ A through the open immersion a : B ⟶ A, when the range of g lies in
the range of a.
Equations
Instances For
Double restrictions #
The inclusion of the double restriction (A | U) | W into A.
Equations
- AnalyticSpace.Glue.incl₂ A U W = CategoryTheory.CategoryStruct.comp ((A.restrictOpen U).ofRestrict W) (A.ofRestrict U)