Theorems · Theorem · category theory

CategoryTheory.MorphismProperty.Over.pullback_obj_hom

∀ {T : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} T] (P Q : CategoryTheory.MorphismProperty T)
  [inst_1 : Q.IsMultiplicative] {X Y : T} (f : X ⟶ Y) [inst_2 : P.HasPullbacksAlong f]
  [inst_3 : P.IsStableUnderBaseChangeAlong f] [inst_4 : Q.IsStableUnderBaseChange] (A : P.Over Q Y),
  ((CategoryTheory.MorphismProperty.Over.pullback P Q f).obj A).hom = CategoryTheory.Limits.pullback.snd A.hom f

Defined in: Mathlib.CategoryTheory.MorphismProperty.OverAdjunction
Cited by: 0 results in Mathlib
Foundations: Depth 68 from the axioms · uses propext, Classical.choice, Quot.sound
Assumes: CategoryTheory.Category CategoryTheory.MorphismProperty.IsMultiplicative CategoryTheory.MorphismProperty.HasPullbacksAlong CategoryTheory.MorphismProperty.IsStableUnderBaseChangeAlong CategoryTheory.MorphismProperty.IsStableUnderBaseChange

Mathlib docs Source Loogle LeanSearch

Around this declaration

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

Cites20

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
Quiver.Homstatement and proof · cited by 32,603
CategoryTheory.Functor.objstatement and proof · cited by 19,642
Top.topstatement · cited by 9,680
CategoryTheory.Functor.idstatement · cited by 3,333
CategoryTheory.Discretestatement · cited by 2,447
CategoryTheory.MorphismPropertystatement and proof · cited by 2,179
CategoryTheory.Comma.leftstatement · cited by 886
CategoryTheory.Limits.pullbackstatement · cited by 864
CategoryTheory.Functor.fromPUnitstatement · cited by 769
CategoryTheory.Comma.rightstatement · cited by 727
CategoryTheory.Limits.pullback.sndstatement · cited by 637

Cited by0

Results whose statement or proof uses this declaration.

Nothing cites this yet.