Gluing data for K-spaces along transition isomorphisms #
A family of K-local-ringed spaces Y i, open subsets W i j ⊆ Y i with W i i = ⊤,
K-morphisms t i j : Y i | W i j ⟶ Y j | W j i with t i i = 𝟙, mapping the points of
W i j ∩ W i k into W j k, and satisfying the cocycle condition as morphisms on the triple
overlaps (KGlueCore, KGlueData), define gluing data for locally ringed spaces in Mathlib's sense
(LocallyRingedSpace.GlueData, KGlueData.toLRSGlueData): the pieces V (i, j) = Y i | W i j, the
open immersions f i j = ofRestrict, the transitions t i j, and the transitions t' i j k on the
pullbacks V (i, j) ×_{U i} V (i, k), obtained by conjugating the restricted transition maps
tRes i j k : Y i | (W i j ⊓ W i k) ⟶ Y j | (W j k ⊓ W j i) through the canonical isomorphisms of
the pullbacks with the meets (pbIso). Mathlib has a pointwise constructor only for topological
gluing (TopCat.GlueData.mk'); this is its analogue for K-spaces, after the pattern of
AlgebraicGeometry.Scheme.Cover.gluedCover.
Conventions. The cocycle condition is required for the restricted maps tRes, which are defined
from the t i j by the universal property of the open immersions
(LocallyRingedSpace.IsOpenImmersion.lift); it is proved in practice by cancelling the monomorphism
ofRestrict and using the pointwise identities. The pullback pullback (f i j) (f i k) is
identified with Y i | (W i j ⊓ W i k) by pbIso, whose inverse is the pair of inclusions of the
meet into the two open subsets. A single piece has W = ⊤, t = 𝟙, and the glued space is the
piece; disjoint pieces (W i j = ⊥ for i ≠ j) have empty transitions, and the glued space is the
disjoint union.
This is the categorical input of the gluing of local complexifications into a complexification (the
theorem of Bruhat and Whitney [BW59, Proposition 1], cited by Hironaka in Hir64, Ch. 0, §1, p. 120,
footnote 7; the cocycle on a neighbourhood follows the pattern of the proof of Car57, §3,
Proposition 2), and of the gluing of local resolutions over a base
(Hironaka.AnalyticSpace.Glue.Over). The glued K-space is built in
Hironaka.AnalyticSpace.Glue.KSpace.
The inclusion of opens composed with the open immersion of the larger open is the open immersion of the smaller one.
The inclusion of opens composed with the open immersion of the larger open is the open immersion of the smaller one.
Gluing data for K-spaces along transition morphisms of open subsets (isomorphisms once the
cocycle identity of KGlueData holds): the pieces, the open subsets, the transitions with their
compatibility on points.
- J : Type u
The index type.
- Y : self.J → KLocallyRingedSpace K
The pieces.
- W (i a✝ : self.J) : TopologicalSpace.Opens ↑↑(self.Y i).toPresheafedSpace
The transition
K-morphisms.- t_id (i : self.J) : self.t i i = CategoryTheory.CategoryStruct.id ((self.Y i).restrictOpen (self.W i i))
- t_inter (i j k : self.J) (x : ↑↑((self.Y i).restrictOpen (self.W i j)).toPresheafedSpace) : ↑x ∈ self.W i k → ↑(KLocallyRingedSpace.Hom.toFun (self.t i j) x) ∈ self.W j k
Instances For
The restricted transition followed by the inclusion of the meet into W j i is the inclusion
into W i j followed by the transition.
The points of the pullback of V (i, j) and V (i, k) land in the meet W i j ⊓ W i k.
From the pullback of V (i, j) and V (i, k) over Y i to the meet
Y i | (W i j ⊓ W i k).
Equations
- One or more equations did not get rendered due to their size.
Instances For
From the meet to the pullback: the pair of inclusions.
Equations
- D.resToPb i j k = CategoryTheory.Limits.pullback.lift ↑((D.Y i).restrictOpenIncl ⋯) ↑((D.Y i).restrictOpenIncl ⋯) ⋯
Instances For
The pullback of two pieces over Y i is the meet of their opens.
Equations
Instances For
Gluing data with the cocycle condition on the restricted transitions.
- Y : self.J → KLocallyRingedSpace K
- t_id (i : self.J) : self.t i i = CategoryTheory.CategoryStruct.id ((self.Y i).restrictOpen (self.W i i))
- t_inter (i j k : self.J) (x : ↑↑((self.Y i).restrictOpen (self.W i j)).toPresheafedSpace) : ↑x ∈ self.W i k → ↑(KLocallyRingedSpace.Hom.toFun (self.t i j) x) ∈ self.W j k
- cocycle (i j k : self.J) : CategoryTheory.CategoryStruct.comp (self.tRes i j k) (CategoryTheory.CategoryStruct.comp (self.tRes j k i) (self.tRes k i j)) = CategoryTheory.CategoryStruct.id ((self.Y i).restrictOpen (self.W i j ⊓ self.W i k))
Instances For
The transition on the pullbacks: the restricted transition, conjugated by the identifications of the pullbacks with the meets.
Equations
- D.t' i j k = CategoryTheory.CategoryStruct.comp (D.pbIso i j k).hom (CategoryTheory.CategoryStruct.comp (↑(D.tRes i j k)) (D.pbIso j k i).inv)
Instances For
The gluing data in Mathlib's categorical form.
Equations
- One or more equations did not get rendered due to their size.
Instances For
The gluing data of locally ringed spaces.
Equations
- D.toLRSGlueData = { toGlueData := D.toGlueData, f_open := ⋯ }