Theorems · Definition · category theory

CategoryTheory.Grothendieck.Hom.fiber

{C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    {F : CategoryTheory.Functor C CategoryTheory.Cat} →
      {X Y : CategoryTheory.Grothendieck F} → (self : X.Hom Y) → (F.map self.base).toFunctor.obj X.fiber ⟶ Y.fiber

The morphism from the pushforward to the source fiber object to the target fiber object.

Defined in

Mathlib.CategoryTheory.Grothendieck

Cited by

26 results in Mathlib

Foundations

Depth 35 from the axioms · uses propext, Classical.choice, Quot.sound

Assumes

CategoryTheory.Category