Documentation

Mathlib.CategoryTheory.FiberedCategory.Fiber

Fibers of a functors #

In this file we define, for a functor p : š’³ ℤ š’“, the fiber categories Fiber p S for every S : š’® as follows

For any category C equipped with a functor F : C ℤ š’³ such that F ā‹™ p is constant at S, we define a functor inducedFunctor : C ℤ Fiber p S that F factors through.

def CategoryTheory.Functor.Fiber {š’® : Type u₁} {š’³ : Type uā‚‚} [Category.{v₁, u₁} š’®] [Category.{vā‚‚, uā‚‚} š’³] (p : Functor š’³ š’®) (S : š’®) :
Type uā‚‚

Fiber p S is the type of elements of š’³ mapping to S via p.

Equations
Instances For
    instance CategoryTheory.Functor.Fiber.fiberCategory {š’® : Type u₁} {š’³ : Type uā‚‚} [Category.{v₁, u₁} š’®] [Category.{vā‚‚, uā‚‚} š’³] {p : Functor š’³ š’®} {S : š’®} :

    Fiber p S has the structure of a category with morphisms being those lying over šŸ™ S.

    Equations
    def CategoryTheory.Functor.Fiber.fiberInclusion {š’® : Type u₁} {š’³ : Type uā‚‚} [Category.{v₁, u₁} š’®] [Category.{vā‚‚, uā‚‚} š’³] {p : Functor š’³ š’®} {S : š’®} :
    Functor (p.Fiber S) š’³

    The functor including Fiber p S into š’³.

    Equations
    Instances For
      instance CategoryTheory.Functor.Fiber.instIsHomLiftIdMapFiberInclusion {š’® : Type u₁} {š’³ : Type uā‚‚} [Category.{v₁, u₁} š’®] [Category.{vā‚‚, uā‚‚} š’³] {p : Functor š’³ š’®} {S : š’®} {a b : p.Fiber S} (φ : a ⟶ b) :
      theorem CategoryTheory.Functor.Fiber.hom_ext {š’® : Type u₁} {š’³ : Type uā‚‚} [Category.{v₁, u₁} š’®] [Category.{vā‚‚, uā‚‚} š’³] {p : Functor š’³ š’®} {S : š’®} {a b : p.Fiber S} {φ ψ : a ⟶ b} (h : fiberInclusion.map φ = fiberInclusion.map ψ) :
      φ = ψ
      instance CategoryTheory.Functor.Fiber.instFaithfulFiberInclusion {š’® : Type u₁} {š’³ : Type uā‚‚} [Category.{v₁, u₁} š’®] [Category.{vā‚‚, uā‚‚} š’³] {p : Functor š’³ š’®} {S : š’®} :
      def CategoryTheory.Functor.Fiber.fiberInclusionCompIsoConst {š’® : Type u₁} {š’³ : Type uā‚‚} [Category.{v₁, u₁} š’®] [Category.{vā‚‚, uā‚‚} š’³] {p : Functor š’³ š’®} {S : š’®} :

      For fixed S : š’® this is the natural isomorphism between fiberInclusion ā‹™ p and the constant function valued at S.

      Equations
      Instances For
        @[simp]
        theorem CategoryTheory.Functor.Fiber.fiberInclusionCompIsoConst_hom_app {š’® : Type u₁} {š’³ : Type uā‚‚} [Category.{v₁, u₁} š’®] [Category.{vā‚‚, uā‚‚} š’³] {p : Functor š’³ š’®} {S : š’®} (X : p.Fiber S) :
        @[simp]
        theorem CategoryTheory.Functor.Fiber.fiberInclusionCompIsoConst_inv_app {š’® : Type u₁} {š’³ : Type uā‚‚} [Category.{v₁, u₁} š’®] [Category.{vā‚‚, uā‚‚} š’³] {p : Functor š’³ š’®} {S : š’®} (X : p.Fiber S) :
        theorem CategoryTheory.Functor.Fiber.fiberInclusion_comp_eq_const {š’® : Type u₁} {š’³ : Type uā‚‚} [Category.{v₁, u₁} š’®] [Category.{vā‚‚, uā‚‚} š’³] {p : Functor š’³ š’®} {S : š’®} :
        def CategoryTheory.Functor.Fiber.mk {š’® : Type u₁} {š’³ : Type uā‚‚} [Category.{v₁, u₁} š’®] [Category.{vā‚‚, uā‚‚} š’³] {p : Functor š’³ š’®} {S : š’®} {a : š’³} (ha : p.obj a = S) :
        p.Fiber S

        The object of the fiber over S corresponding to a a : š’³ such that p(a) = S.

        Equations
        Instances For
          @[simp]
          theorem CategoryTheory.Functor.Fiber.fiberInclusion_mk {š’® : Type u₁} {š’³ : Type uā‚‚} [Category.{v₁, u₁} š’®] [Category.{vā‚‚, uā‚‚} š’³] {p : Functor š’³ š’®} {S : š’®} {a : š’³} (ha : p.obj a = S) :
          def CategoryTheory.Functor.Fiber.homMk {š’® : Type u₁} {š’³ : Type uā‚‚} [Category.{v₁, u₁} š’®] [Category.{vā‚‚, uā‚‚} š’³] (p : Functor š’³ š’®) (S : š’®) {a b : š’³} (φ : a ⟶ b) [p.IsHomLift (CategoryStruct.id S) φ] :
          mk ⋯ ⟶ mk ⋯

          The morphism in the fiber over S corresponding to a morphism in š’³ lifting šŸ™ S.

          Equations
          Instances For
            @[simp]
            theorem CategoryTheory.Functor.Fiber.fiberInclusion_homMk {š’® : Type u₁} {š’³ : Type uā‚‚} [Category.{v₁, u₁} š’®] [Category.{vā‚‚, uā‚‚} š’³] (p : Functor š’³ š’®) (S : š’®) {a b : š’³} (φ : a ⟶ b) [p.IsHomLift (CategoryStruct.id S) φ] :
            fiberInclusion.map (homMk p S φ) = φ
            @[simp]
            theorem CategoryTheory.Functor.Fiber.homMk_id {š’® : Type u₁} {š’³ : Type uā‚‚} [Category.{v₁, u₁} š’®] [Category.{vā‚‚, uā‚‚} š’³] (p : Functor š’³ š’®) (S : š’®) (a : š’³) [p.IsHomLift (CategoryStruct.id S) (CategoryStruct.id a)] :
            @[simp]
            theorem CategoryTheory.Functor.Fiber.homMk_comp {š’® : Type u₁} {š’³ : Type uā‚‚} [Category.{v₁, u₁} š’®] [Category.{vā‚‚, uā‚‚} š’³] {p : Functor š’³ š’®} {S : š’®} {a b c : š’³} (φ : a ⟶ b) (ψ : b ⟶ c) [p.IsHomLift (CategoryStruct.id S) φ] [p.IsHomLift (CategoryStruct.id S) ψ] :
            CategoryStruct.comp (homMk p S φ) (homMk p S ψ) = homMk p S (CategoryStruct.comp φ ψ)
            def CategoryTheory.Functor.Fiber.inducedFunctor {š’® : Type u₁} {š’³ : Type uā‚‚} [Category.{v₁, u₁} š’®] [Category.{vā‚‚, uā‚‚} š’³] {p : Functor š’³ š’®} {S : š’®} {C : Type uā‚ƒ} [Category.{vā‚ƒ, uā‚ƒ} C] {F : Functor C š’³} (hF : F.comp p = (const C).obj S) :
            Functor C (p.Fiber S)

            Given a functor F : C ℤ š’³ such that F ā‹™ p is constant at some S : š’®, then we get an induced functor C ℤ Fiber p S that F factors through.

            Equations
            Instances For
              @[simp]
              theorem CategoryTheory.Functor.Fiber.inducedFunctor_map {š’® : Type u₁} {š’³ : Type uā‚‚} [Category.{v₁, u₁} š’®] [Category.{vā‚‚, uā‚‚} š’³] {p : Functor š’³ š’®} {S : š’®} {C : Type uā‚ƒ} [Category.{vā‚ƒ, uā‚ƒ} C] {F : Functor C š’³} (hF : F.comp p = (const C).obj S) {X Y : C} (f : X ⟶ Y) :
              def CategoryTheory.Functor.Fiber.inducedFunctorCompIsoSelf {š’® : Type u₁} {š’³ : Type uā‚‚} [Category.{v₁, u₁} š’®] [Category.{vā‚‚, uā‚‚} š’³] {p : Functor š’³ š’®} {S : š’®} {C : Type uā‚ƒ} [Category.{vā‚ƒ, uā‚ƒ} C] {F : Functor C š’³} (hF : F.comp p = (const C).obj S) :

              Given a functor F : C ℤ š’³ such that F ā‹™ p is constant at some S : š’®, then we get a natural isomorphism between inducedFunctor _ ā‹™ fiberInclusion and F.

              Equations
              Instances For
                @[simp]
                theorem CategoryTheory.Functor.Fiber.inducedFunctorCompIsoSelf_inv_app {š’® : Type u₁} {š’³ : Type uā‚‚} [Category.{v₁, u₁} š’®] [Category.{vā‚‚, uā‚‚} š’³] {p : Functor š’³ š’®} {S : š’®} {C : Type uā‚ƒ} [Category.{vā‚ƒ, uā‚ƒ} C] {F : Functor C š’³} (hF : F.comp p = (const C).obj S) (X : C) :
                @[simp]
                theorem CategoryTheory.Functor.Fiber.inducedFunctorCompIsoSelf_hom_app {š’® : Type u₁} {š’³ : Type uā‚‚} [Category.{v₁, u₁} š’®] [Category.{vā‚‚, uā‚‚} š’³] {p : Functor š’³ š’®} {S : š’®} {C : Type uā‚ƒ} [Category.{vā‚ƒ, uā‚ƒ} C] {F : Functor C š’³} (hF : F.comp p = (const C).obj S) (X : C) :
                theorem CategoryTheory.Functor.Fiber.inducedFunctor_comp {š’® : Type u₁} {š’³ : Type uā‚‚} [Category.{v₁, u₁} š’®] [Category.{vā‚‚, uā‚‚} š’³] {p : Functor š’³ š’®} {S : š’®} {C : Type uā‚ƒ} [Category.{vā‚ƒ, uā‚ƒ} C] {F : Functor C š’³} (hF : F.comp p = (const C).obj S) :