Maps and homotopies out of pushouts in TopCat #
Let P = Z ∪_a Y be a pushout square in TopCat, with maps i : B → Y, a : B → Z,
j : Y → P and k : Z → P. Continuous maps out of P are determined by their restrictions to
Y and to Z. Since the unit interval I is locally compact, the cylinder I × P is again a
pushout: a map out of I × P is glued from maps out of I × Y and I × Z which agree along a,
as the uncurried form of the map P → C(I, W) glued from the curried ones. In particular,
homotopies between maps out of P are glued from homotopies on Y and on Z.
Conversely, a space covered by a closed subspace A and finitely many closed pieces B k, any two
of which meet only inside A, is the pushout of A and the coproduct of the B k along the parts
S k where they meet A. This recognizes a space built by attaching finitely many closed pieces,
such as cells or handles, without passing through a quotient. Without the covering hypothesis, a
map out of such a pushout which restricts to closed embeddings on A and on finitely many pieces
B k, any two of which meet only inside A, and meeting A only along the S k, is still a
closed embedding.
Main declarations #
CategoryTheory.IsPushout.continuousMap_ext: continuous maps out of a pushout agree when they agree on both legs.CategoryTheory.IsPushout.cylinderDesc: the map out of the cylinderI × Pglued from compatible maps out ofI × YandI × Z.CategoryTheory.IsPushout.homotopyDesc: the homotopy between maps out ofPglued from compatible homotopies of their restrictions toYand toZ.TopCat.sigmaCylinderDesc: the map out of the cylinderI × ∐ⱼ F jglued from maps out of the cylindersI × F j.TopCat.exists_glue_of_isClosedEmbedding: maps out of the pieces of a finite closed cover which agree on the overlaps glue to a map out of the whole space.CategoryTheory.IsPushout.of_isClosedEmbedding: a cover by a closed subspace and finitely many closed pieces meeting it along prescribed subspaces is a pushout square.TauCeti.TopCat.range_union_iUnion_range_of_isPushout_sigma,TauCeti.TopCat.exists_eq_inl_or_exists_eq_inr_of_isPushout_sigma: every point of a pushout ofLand⨆ᵢ D icomes fromLor from one of theD i.TauCeti.TopCat.injective_of_isPushout_sigma_of_comp,TauCeti.TopCat.isClosedEmbedding_of_isPushout_sigma_of_comp: a map out of the pushout ofLand⨆ᵢ D ialong⨆ᵢ A irestricting to injective maps (resp. closed embeddings) onLand on theD i, with the images of any twoD imeeting only inside the image ofLand each meeting it only alongA i, is injective (resp. a closed embedding).
The pointwise form of the commutativity of a pushout square in TopCat.
Two continuous maps out of a pushout in TopCat agree as soon as they agree on both legs.
The map out of the cylinder I × P on a pushout P = Z ∪_a Y glued from maps
F : I × Y → W and G : I × Z → W which agree along the attaching map. Since I is locally
compact, it is the uncurried map out of P glued from the curried maps into C(I, W); this is the
form in which homotopies are glued on P.
Instances For
On the cylinder over Y, the glued map CategoryTheory.IsPushout.cylinderDesc is F.
On the cylinder over Z, the glued map CategoryTheory.IsPushout.cylinderDesc is G.
A slice of the glued map CategoryTheory.IsPushout.cylinderDesc is the map out of P which
agrees with the corresponding slices of F and G on both legs.
The homotopy between two maps out of a pushout P = Z ∪_a Y glued from homotopies of their
restrictions to Y and to Z which agree along the attaching map.
Instances For
On Y, the glued homotopy CategoryTheory.IsPushout.homotopyDesc is HY.
On Z, the glued homotopy CategoryTheory.IsPushout.homotopyDesc is HZ.
Every point of a coproduct in TopCat lies in the image of one of the coprojections.
The map I × ∐ⱼ F j → W which is C j on the cylinder I × F j: the uncurried form of the
map ∐ⱼ F j → C(I, W) glued from the curried maps.
Instances For
Gluing along a finite closed cover. Let X be covered by the ranges of a closed embedding
i : A ⟶ X and of finitely many closed embeddings j k : B k ⟶ X, any two of which meet only
inside the range of i. Maps a : A ⟶ Y and b k : B k ⟶ Y which agree wherever i meets
j k glue to a map X ⟶ Y restricting to a along i and to b k along j k.
A finite closed cover is a pushout. Let X be covered by the ranges of a closed embedding
i : A ⟶ X and of finitely many closed embeddings j k : B k ⟶ X, any two of which meet only
inside the range of i. Suppose that i meets each j k exactly along S k: the squares
g k ≫ i = m k ≫ j k commute, and every point i a = j k b comes from a point s of S k with
g k s = a and m k s = b. Then X is the pushout of A and ∐ₖ B k along ∐ₖ S k.
For instance, a space which is the union of a closed subspace and finitely many disjoint closed handles, each meeting the subspace in its attaching region, is obtained by attaching the handles.
Every point of a pushout of L and ⨆ᵢ D i comes from L or from one of the D i.
Every point of a pushout of L and ⨆ᵢ D i is the image of a point of L or of one of the
D i. This is the pointwise form of
TauCeti.TopCat.range_union_iUnion_range_of_isPushout_sigma.
Let P be the pushout of L and ⨆ᵢ D i along ⨆ᵢ A i, and let φ : P ⟶ X restrict to
injective maps g on L and χ i on the D i, with the ranges of any two χ i meeting only
inside the range of g. If every point of D i carried by χ i into the range of g lies in the
range of j i, then φ is injective.
Let P be the pushout of L and ⨆ᵢ D i along ⨆ᵢ A i, for finitely many i, and let
φ : P ⟶ X restrict to closed embeddings g on L and χ i on the D i, with the ranges of
any two χ i meeting only inside the range of g. If every point of D i carried by χ i into
the range of g lies in the range of j i, then φ is a closed embedding.