Documentation

TauCeti.Topology.Category.TopCat.Fiber

Fibres of morphisms in TopCat #

The fibre TopCat.Hom.fiber p b of a morphism p : E ⟶ B over a point b is the preimage p ⁻¹' {b} with the subspace topology, and TopCat.Hom.fiberι p b is its inclusion into E. A commutative square from p to p', such as a map of fibrations, induces maps between the fibres (CategoryTheory.CommSq.fiberMap), functorially in horizontal composition of squares.

The names and the dot-notation shape follow Mathlib's scheme-theoretic fibres AlgebraicGeometry.Scheme.Hom.fiber and AlgebraicGeometry.Scheme.Hom.fiberι.

source
@[reducible, inline]
abbrev TopCat.Hom.fiber {E B : TopCat} (p : E ⟶ B) (b : ↑B) :
TopCat

The fibre p ⁻¹' {b} of a morphism p : E ⟶ B over a point b, with the subspace topology.

Instances For
    source
    def TopCat.Hom.fiberι {E B : TopCat} (p : E ⟶ B) (b : ↑B) :
    fiber p b ⟶ E

    The inclusion of the fibre of p over b into E.

    Instances For
      source
      @[simp]
      theorem TopCat.Hom.fiberι_apply {E B : TopCat} (p : E ⟶ B) (b : ↑B) (x : ↑(fiber p b)) :
      (CategoryTheory.ConcreteCategory.hom (fiberι p b)) x = ↑x
      source
      @[simp]
      theorem TopCat.Hom.apply_coe_fiber {E B : TopCat} (p : E ⟶ B) (b : ↑B) (x : ↑(fiber p b)) :
      (CategoryTheory.ConcreteCategory.hom p) ↑x = b

      The morphism p sends every point of its fibre over b to b.

      source
      @[simp]
      theorem TopCat.Hom.fiberι_comp {E B : TopCat} (p : E ⟶ B) (b : ↑B) :
      CategoryTheory.CategoryStruct.comp (fiberι p b) p = const b
      source
      @[simp]
      theorem TopCat.Hom.fiberι_comp_assoc {E B : TopCat} (p : E ⟶ B) (b : ↑B) {Z : TopCat} (h : B ⟶ Z) :
      CategoryTheory.CategoryStruct.comp (fiberι p b) (CategoryTheory.CategoryStruct.comp p h) = CategoryTheory.CategoryStruct.comp (const b) h
      source
      theorem TopCat.Hom.finite_fibers_comp {E B X : TopCat} (p : E ⟶ B) (q : B ⟶ X) (hfinp : ∀ (b : ↑B), Finite ↑(⇑(CategoryTheory.ConcreteCategory.hom p) ⁻¹' {b})) (hfinq : ∀ (x : ↑X), Finite ↑(⇑(CategoryTheory.ConcreteCategory.hom q) ⁻¹' {x})) (x : ↑X) :
      Finite ↑(⇑(CategoryTheory.ConcreteCategory.hom (CategoryTheory.CategoryStruct.comp p q)) ⁻¹' {x})

      The composite of two maps with finite fibres has finite fibres.

      source
      def CategoryTheory.CommSq.fiberMap {E B E' B' : TopCat} {p : E ⟶ B} {p' : E' ⟶ B'} {f : E ⟶ E'} {g : B ⟶ B'} (sq : CommSq f p p' g) (b : ↑B) :
      TopCat.Hom.fiber p b ⟶ TopCat.Hom.fiber p' ((ConcreteCategory.hom g) b)

      A map of fibrations, that is, a commutative square from p to p', maps the fibre of p over b to the fibre of p' over g b.

      Instances For
        source
        @[simp]
        theorem CategoryTheory.CommSq.fiberMap_apply_coe {E B E' B' : TopCat} {p : E ⟶ B} {p' : E' ⟶ B'} {f : E ⟶ E'} {g : B ⟶ B'} (sq : CommSq f p p' g) (b : ↑B) (x : ↑(TopCat.Hom.fiber p b)) :
        ↑((ConcreteCategory.hom (sq.fiberMap b)) x) = (ConcreteCategory.hom f) ↑x
        source
        @[simp]
        theorem CategoryTheory.CommSq.fiberMap_comp_fiberι {E B E' B' : TopCat} {p : E ⟶ B} {p' : E' ⟶ B'} {f : E ⟶ E'} {g : B ⟶ B'} (sq : CommSq f p p' g) (b : ↑B) :
        CategoryStruct.comp (sq.fiberMap b) (TopCat.Hom.fiberι p' ((ConcreteCategory.hom g) b)) = CategoryStruct.comp (TopCat.Hom.fiberι p b) f
        source
        @[simp]
        theorem CategoryTheory.CommSq.fiberMap_comp_fiberι_assoc {E B E' B' : TopCat} {p : E ⟶ B} {p' : E' ⟶ B'} {f : E ⟶ E'} {g : B ⟶ B'} (sq : CommSq f p p' g) (b : ↑B) {Z : TopCat} (h : E' ⟶ Z) :
        CategoryStruct.comp (sq.fiberMap b) (CategoryStruct.comp (TopCat.Hom.fiberι p' ((ConcreteCategory.hom g) b)) h) = CategoryStruct.comp (TopCat.Hom.fiberι p b) (CategoryStruct.comp f h)
        source
        @[simp]
        theorem CategoryTheory.CommSq.fiberMap_id {E B : TopCat} {p : E ⟶ B} (sq : CommSq (CategoryStruct.id E) p p (CategoryStruct.id B)) (b : ↑B) :
        sq.fiberMap b = CategoryStruct.id (TopCat.Hom.fiber p b)

        The identity square induces the identity on fibres.

        source
        @[simp]
        theorem CategoryTheory.CommSq.fiberMap_comp_fiberMap {E B E' B' E'' B'' : TopCat} {p : E ⟶ B} {p' : E' ⟶ B'} {p'' : E'' ⟶ B''} {f : E ⟶ E'} {g : B ⟶ B'} {f' : E' ⟶ E''} {g' : B' ⟶ B''} (sq : CommSq f p p' g) (sq' : CommSq f' p' p'' g') (b : ↑B) :
        CategoryStruct.comp (sq.fiberMap b) (sq'.fiberMap ((ConcreteCategory.hom g) b)) = ⋯.fiberMap b

        The composite of the maps on fibres induced by two squares is the map on fibres induced by their horizontal composite. It is stated in this direction so that simp can use it: the middle map p' cannot be recovered from the composite square, as for eqToHom_trans.

        source
        @[simp]
        theorem CategoryTheory.CommSq.fiberMap_comp_fiberMap_assoc {E B E' B' E'' B'' : TopCat} {p : E ⟶ B} {p' : E' ⟶ B'} {p'' : E'' ⟶ B''} {f : E ⟶ E'} {g : B ⟶ B'} {f' : E' ⟶ E''} {g' : B' ⟶ B''} (sq : CommSq f p p' g) (sq' : CommSq f' p' p'' g') (b : ↑B) {Z : TopCat} (h : TopCat.Hom.fiber p'' ((ConcreteCategory.hom g') ((ConcreteCategory.hom g) b)) ⟶ Z) :
        CategoryStruct.comp (sq.fiberMap b) (CategoryStruct.comp (sq'.fiberMap ((ConcreteCategory.hom g) b)) h) = CategoryStruct.comp (⋯.fiberMap b) h

        The composite of the maps on fibres induced by two squares is the map on fibres induced by their horizontal composite. It is stated in this direction so that simp can use it: the middle map p' cannot be recovered from the composite square, as for eqToHom_trans.