Theorems · Definition · category theory

CategoryTheory.ChosenPullbacksAlong.binaryFan

{C : Type u₁} →
  [inst : CategoryTheory.Category.{v₁, u₁} C] →
    {X : C} →
      (Y Z : CategoryTheory.Over X) → [CategoryTheory.ChosenPullbacksAlong Z.hom] → CategoryTheory.Limits.BinaryFan Y Z

The binary fan provided by fst' and snd'.

Defined in: Mathlib.CategoryTheory.LocallyCartesianClosed.Over
Cited by: 0 results in Mathlib
Foundations: Depth 32 from the axioms · uses propext, Classical.choice, Quot.sound
Assumes: CategoryTheory.Category CategoryTheory.ChosenPullbacksAlong

Mathlib docs Source Loogle LeanSearch

Around this declaration

Dashed lines are statement dependencies; solid lines are citations in proofs.

Cites9

Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.

CategoryTheory.Categorystatement and proof · cited by 32,673
CategoryTheory.Overstatement and proof · cited by 935
CategoryTheory.Over.leftstatement · cited by 541
CategoryTheory.Over.homstatement and proof · cited by 370
CategoryTheory.Limits.BinaryFan.mkproof · cited by 112
CategoryTheory.ChosenPullbacksAlongstatement and proof · cited by 73
CategoryTheory.Limits.BinaryFanstatement · cited by 51
CategoryTheory.ChosenPullbacksAlong.fst'proof · cited by 4
CategoryTheory.ChosenPullbacksAlong.snd'proof · cited by 2

Cited by2

Results whose statement or proof uses this declaration.

CategoryTheory.ChosenPullbacksAlong.cartesianMonoidalCategoryOverproof · cited by 49
CategoryTheory.ChosenPullbacksAlong.binaryFanIsBinaryProductstatement and proof · cited by 0