Theorems · Inductive type · general topology

TopCat.GlueData

Type (u_1 + 1)

A family of gluing data consists of 1. An index type J 2. An object U i for each i : J. 3. An object V i j for each i j : J. (Note that this is J × J → TopCat rather than J → J → TopCat to connect to the limits library easier.) 4. An open embedding f i j : V i j ⟶ U i for each i j : ι. 5. A transition map t i j : V i j ⟶ V j i for each i j : ι. such that 6. f i i is an isomorphism. 7. t i i is the identity. 8. V i j ×[U i] V i k ⟶ V i j ⟶ V j i factors through V j k ×[U j] V j i ⟶ V j i via some t' : V i j ×[U i] V i k ⟶ V j k ×[U j] V j i. (This merely means that V i j ∩ V i k ⊆ t i j ⁻¹' (V j i ∩ V j k).) 9. t' i j k ≫ t' j k i ≫ t' k i j = 𝟙 _. We can then glue the topological spaces U i together by identifying V i j with V j i, such that the U i's are open subspaces of the glued space. Most of the times it would be easier to use the constructor TopCat.GlueData.mk' where the conditions are stated in a less categorical way.

Defined in

Mathlib.Topology.Gluing

Cited by

17 results in Mathlib

Foundations

Depth 0 from the axioms · uses no axioms