Theorems · Theorem · category theory

CategoryTheory.regularTopology.parallelPair_pullback_initial

∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] {X B : C} (π : X ⟶ B)
  (c : CategoryTheory.Limits.PullbackCone π π) (hc : CategoryTheory.Limits.IsLimit c),
  (CategoryTheory.Limits.parallelPair (CategoryTheory.ObjectProperty.homMk (CategoryTheory.Over.homMk c.fst ⋯)).op
      (CategoryTheory.ObjectProperty.homMk (CategoryTheory.Over.homMk c.snd ⋯)).op).Initial

Defined in

Mathlib.CategoryTheory.Sites.Coherent.RegularSheaves

Cited by

0 results in Mathlib

Foundations

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

Assumes

CategoryTheory.Category