Documentation

TauCeti.Topology.Category.TopCat.Pullback

Pullbacks in TopCat #

A commutative square of topological spaces whose top horizontal map is an embedding and whose bottom horizontal map is injective is a pullback when the range of the top map is the preimage of the range of the bottom one. This range criterion is useful for geometric constructions presented as embedded open subspaces.

The base change TopCat.pullbackFst g p of a morphism p : E ⟶ B along g : B' ⟶ B has the same fibres as p: its fibre over b' is the fibre of p over g b' (TopCat.Hom.fiberPullbackFstIso).

source
theorem TauCeti.TopCat.isPullback_of_isEmbedding_of_range_eq_preimage {P X Y Z : TopCat} {fst : P ⟶ X} {snd : P ⟶ Y} {f : X ⟶ Z} {g : Y ⟶ Z} (hfst : Topology.IsEmbedding ⇑(CategoryTheory.ConcreteCategory.hom fst)) (hg : Function.Injective ⇑(CategoryTheory.ConcreteCategory.hom g)) (hcomm : CategoryTheory.CategoryStruct.comp fst f = CategoryTheory.CategoryStruct.comp snd g) (hrange : Set.range ⇑(CategoryTheory.ConcreteCategory.hom fst) = ⇑(CategoryTheory.ConcreteCategory.hom f) ⁻¹' Set.range ⇑(CategoryTheory.ConcreteCategory.hom g)) :
CategoryTheory.IsPullback fst snd f g

A commutative square whose top horizontal map is an embedding and whose bottom horizontal map is injective is a pullback when the range of the top map is the preimage of the range of the bottom map.

source
def TopCat.Hom.fiberPullbackFstIso {E B B' : TopCat} (p : E ⟶ B) (g : B' ⟶ B) (b' : ↑B') :
fiber (pullbackFst g p) b' ≅ fiber p ((CategoryTheory.ConcreteCategory.hom g) b')

The fibre of the base change of p along g : B' ⟶ B over b' is the fibre of p over g b'.

Instances For
    source
    @[simp]
    theorem TopCat.Hom.fiberPullbackFstIso_hom_comp_fiberι {E B B' : TopCat} (p : E ⟶ B) (g : B' ⟶ B) (b' : ↑B') :
    CategoryTheory.CategoryStruct.comp (fiberPullbackFstIso p g b').hom (fiberι p ((CategoryTheory.ConcreteCategory.hom g) b')) = CategoryTheory.CategoryStruct.comp (fiberι (pullbackFst g p) b') (pullbackSnd g p)
    source
    @[simp]
    theorem TopCat.Hom.fiberPullbackFstIso_hom_comp_fiberι_assoc {E B B' : TopCat} (p : E ⟶ B) (g : B' ⟶ B) (b' : ↑B') {Z : TopCat} (h : E ⟶ Z) :
    CategoryTheory.CategoryStruct.comp (fiberPullbackFstIso p g b').hom (CategoryTheory.CategoryStruct.comp (fiberι p ((CategoryTheory.ConcreteCategory.hom g) b')) h) = CategoryTheory.CategoryStruct.comp (fiberι (pullbackFst g p) b') (CategoryTheory.CategoryStruct.comp (pullbackSnd g p) h)
    source
    theorem TopCat.Hom.fiberPullbackFstIso_hom_apply_coe {E B B' : TopCat} (p : E ⟶ B) (g : B' ⟶ B) (b' : ↑B') (x : ↑(fiber (pullbackFst g p) b')) :
    ↑((CategoryTheory.ConcreteCategory.hom (fiberPullbackFstIso p g b').hom) x) = (↑↑x).2
    source
    theorem TopCat.Hom.fiberPullbackFstIso_inv_apply_coe {E B B' : TopCat} (p : E ⟶ B) (g : B' ⟶ B) (b' : ↑B') (x : ↑(fiber p ((CategoryTheory.ConcreteCategory.hom g) b'))) :
    ↑((CategoryTheory.ConcreteCategory.hom (fiberPullbackFstIso p g b').inv) x) = ⟨(b', ↑x), ⋯⟩