Hom.HasPullback

Stream: mathlib4

[joseph hua]

In PR #29795 I generalised some theorems related to base change along a morphism. Namely instead of assuming that the category has pullbacks, we just need pullbacks along that morphism to exist. I am wondering if making a typeclass for this is a good idea:

protected class Hom.HasPullback {X Y : C} (f : X ⟶ Y) : Prop where
  hasPullback {W} (g : W ⟶ Y) : HasPullback g f

[Christian Merten]

I think [∀ {W} (g : W ⟶ Y), HasPullback g f] is good enough.

[Kevin Buzzard]

I have not used category theory much in mathlib but I have noticed similar patterns to what Joseph is suggesting before e.g. docs#CategoryTheory.Limits.HasLimitsOfSize is a class, just defined to mean "for all J, (another class)", so why isn't Christian's suggestion an argument against docs#CategoryTheory.Limits.HasLimitsOfSize ?

[Joël Riou]

For convenience, ∀ {W} (g : W ⟶ Y), HasPullback g f could be made into an abbrev.

I would not mind if somebody implemented a change in the design of HasLimitsOfShape and HasLimitsOfSize to make them abbrevs, as long as !bench produces reasonable results...

[joseph hua]

Joël Riou said:

For convenience, ∀ {W} (g : W ⟶ Y), HasPullback g f could be made into an abbrev.

I would not mind if somebody implemented a change in the design of HasLimitsOfShape and HasLimitsOfSize to make them abbrevs, as long as !bench produces reasonable results...

unless there are any objections I will implement the HasPullback instance as an abbrev in the PR

[joseph hua]

Now implemented in #29795