Theorems · Theorem · category theory

CategoryTheory.PreGaloisCategory.fiberPullbackEquiv_symm_fst_apply

∀ {C : Type u₁} [inst : CategoryTheory.Category.{u₂, u₁} C] (F : CategoryTheory.Functor C FintypeCat)
  [inst_1 : CategoryTheory.PreGaloisCategory C] [inst_2 : CategoryTheory.PreGaloisCategory.FiberFunctor F] {X A B : C}
  {f : A ⟶ X} {g : B ⟶ X} (a : (F.obj A).obj) (b : (F.obj B).obj)
  (h : (CategoryTheory.ConcreteCategory.hom (F.map f)) a = (CategoryTheory.ConcreteCategory.hom (F.map g)) b),
  (CategoryTheory.ConcreteCategory.hom (F.map (CategoryTheory.Limits.pullback.fst f g)))
      ((CategoryTheory.PreGaloisCategory.fiberPullbackEquiv F f g).symm ⟨(a, b), h⟩) =
    a

Defined in

Mathlib.CategoryTheory.Galois.Basic

Cited by

1 results in Mathlib

Foundations

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

Assumes

CategoryTheory.CategoryCategoryTheory.PreGaloisCategoryCategoryTheory.PreGaloisCategory.FiberFunctor