Theorems · Definition · category theory

CategoryTheory.PreGaloisCategory.fiberPullbackEquiv

{C : Type u₁} →
  [inst : CategoryTheory.Category.{u₂, u₁} C] →
    (F : CategoryTheory.Functor C FintypeCat) →
      [inst_1 : CategoryTheory.PreGaloisCategory C] →
        [CategoryTheory.PreGaloisCategory.FiberFunctor F] →
          {X A B : C} →
            (f : A ⟶ X) →
              (g : B ⟶ X) →
                (F.obj (CategoryTheory.Limits.pullback f g)).obj ≃
                  { p //
                    (CategoryTheory.ConcreteCategory.hom (F.map f)) p.1 =
                      (CategoryTheory.ConcreteCategory.hom (F.map g)) p.2 }

The fiber of the pullback is the fiber product of the fibers.

Defined in

Mathlib.CategoryTheory.Galois.Basic

Cited by

3 results in Mathlib

Foundations

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

Assumes

CategoryTheory.CategoryCategoryTheory.PreGaloisCategoryCategoryTheory.PreGaloisCategory.FiberFunctor