Mathlib Map

Theorems · Theorem · category theory

CategoryTheory.Limits.hasPullback_symmetry

∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {X Y Z : C} (f : X ⟶ Z) (g : Y ⟶ Z)
  [CategoryTheory.Limits.HasPullback f g], CategoryTheory.Limits.HasPullback g f

Making this a global instance would make the typeclass search go in an infinite loop.

Defined in
Mathlib.CategoryTheory.Limits.Shapes.Pullback.HasPullback
Cited by
22 results in Mathlib
Foundations
Depth 35 from the axioms · uses propext, Classical.choice, Quot.sound
Assumes
CategoryTheory.CategoryCategoryTheory.Limits.HasPullback
Mathlib docsSourceLoogleLeanSearch

Around this declaration

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

CategoryTheory.Limits.pullbackSymmetry · cited by 61Limits.pullbackSymmetryCategoryTheory.Limits.pullbackSymmetry_hom_comp_fst · cited by 18Limits.pullbackSymmetry_h…CategoryTheory.Limits.pullbackSymmetry_hom_comp_snd · cited by 13Limits.pullbackSymmetry_h…CategoryTheory.Limits.pullbackSymmetry_hom_comp_fst_assoc · cited by 12Limits.pullbackSymmetry_h…CategoryTheory.Limits.pullbackSymmetry_hom_comp_snd_assoc · cited by 11Limits.pullbackSymmetry_h…CategoryTheory.Limits.pullbackSymmetry_inv_comp_fst · cited by 5Limits.pullbackSymmetry_i…CategoryTheory.Limits.pullbackSymmetry_inv_comp_snd · cited by 3Limits.pullbackSymmetry_i…CategoryTheory.Limits.pullbackSymmetry_inv_comp_snd_assoc · cited by 3Limits.pullbackSymmetry_i…CategoryTheory.Limits.hasPullback_symmetry_of_hasPullbacksAlong · cited by 2Limits.hasPullback_symmet…AlgebraicGeometry.Scheme.Pullback.gluedLiftPullbackMap_fst · cited by 1Pullback.gluedLiftPullbac…CategoryTheory.GlueData.t'_comp_eq_pullbackSymmetry · cited by 1GlueData.t'_comp_eq_pullb…CategoryTheory.GlueData.t'_iij · cited by 1GlueData.t'_iijAlgebraicGeometry.Scheme.Pullback.gluedLiftPullbackMap_fst_assoc · cited by 0Pullback.gluedLiftPullbac…CategoryTheory.GlueData.t'_comp_eq_pullbackSymmetry_assoc · cited by 0GlueData.t'_comp_eq_pullb…CategoryTheory.GlueData.t'_inv · cited by 0GlueData.t'_invCategoryTheory.Category · cited by 32673CategoryTheory.CategoryQuiver.Hom · cited by 32603Quiver.HomCategoryTheory.Limits.pullback.fst · cited by 639pullback.fstCategoryTheory.Limits.pullback.snd · cited by 637pullback.sndCategoryTheory.Limits.HasPullback · cited by 434Limits.HasPullbackCategoryTheory.Limits.PullbackCone.mk · cited by 203PullbackCone.mkCategoryTheory.Limits.pullback.condition · cited by 122pullback.conditionCategoryTheory.Limits.pullbackIsPullback · cited by 14Limits.pullbackIsPullbackCategoryTheory.Limits.PullbackCone.flipIsLimit · cited by 6PullbackCone.flipIsLimitCategoryTheory.Limits.PullbackCone.flip · cited by 5PullbackCone.flipLimits.hasPullback_symmetryCITED BYCITES

Cites10

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

Cited by23

Results whose statement or proof uses this declaration.