Chosen pullbacks

Given two morphisms f₁ : X₁ ⟶ S and f₂ : X₂ ⟶ S, we introduce a structure ChosenPullback f₁ f₂ which contains the data of pullback of f₁ and f₂.

TODO

• relate this to ChosenPullbacksAlong which is defined in LocallyCartesianClosed.ChosenPullbacksAlong.

structure CategoryTheory.Limits.ChosenPullback {C : Type u} [Category.{v, u} C] {X₁ X₂ S : C} (f₁ : X₁ ⟶ S) (f₂ : X₂ ⟶ S) : Type (max u v)

Given two morphisms f₁ : X₁ ⟶ S and f₂ : X₂ ⟶ S, this is the choice of a pullback of f₁ and f₂.

• pullback : C

  the pullback

• p₁ : self.pullback ⟶ X₁

  the first projection

• p₂ : self.pullback ⟶ X₂

  the second projection

• condition : CategoryStruct.comp self.p₁ f₁ = CategoryStruct.comp self.p₂ f₂
• isLimit : IsLimit (PullbackCone.mk self.p₁ self.p₂ ⋯)

  pullback is a pullback of f₁ and f₂

• p : self.pullback ⟶ S

  the projection pullback ⟶ S

• hp₁ : CategoryStruct.comp self.p₁ f₁ = self.p

theorem CategoryTheory.Limits.ChosenPullback.condition_assoc {C : Type u} [Category.{v, u} C] {X₁ X₂ S : C} {f₁ : X₁ ⟶ S} {f₂ : X₂ ⟶ S} (self : ChosenPullback f₁ f₂) {Z : C} (h : S ⟶ Z) : CategoryStruct.comp self.p₁ (CategoryStruct.comp f₁ h) = CategoryStruct.comp self.p₂ (CategoryStruct.comp f₂ h)

theorem CategoryTheory.Limits.ChosenPullback.isPullback {C : Type u} [Category.{v, u} C] {X₁ X₂ S : C} {f₁ : X₁ ⟶ S} {f₂ : X₂ ⟶ S} (h : ChosenPullback f₁ f₂) : IsPullback h.p₁ h.p₂ f₁ f₂

@[simp]

theorem CategoryTheory.Limits.ChosenPullback.hp₁_assoc {C : Type u} [Category.{v, u} C] {X₁ X₂ S : C} {f₁ : X₁ ⟶ S} {f₂ : X₂ ⟶ S} (self : ChosenPullback f₁ f₂) {Z : C} (h : S ⟶ Z) : CategoryStruct.comp self.p₁ (CategoryStruct.comp f₁ h) = CategoryStruct.comp self.p h

@[simp]

theorem CategoryTheory.Limits.ChosenPullback.hp₂ {C : Type u} [Category.{v, u} C] {X₁ X₂ S : C} {f₁ : X₁ ⟶ S} {f₂ : X₂ ⟶ S} (h : ChosenPullback f₁ f₂) : CategoryStruct.comp h.p₂ f₂ = h.p

@[simp]

theorem CategoryTheory.Limits.ChosenPullback.hp₂_assoc {C : Type u} [Category.{v, u} C] {X₁ X₂ S : C} {f₁ : X₁ ⟶ S} {f₂ : X₂ ⟶ S} (h : ChosenPullback f₁ f₂) {Z : C} (h✝ : S ⟶ Z) : CategoryStruct.comp h.p₂ (CategoryStruct.comp f₂ h✝) = CategoryStruct.comp h.p h✝

theorem CategoryTheory.Limits.ChosenPullback.hom_ext {C : Type u} [Category.{v, u} C] {X₁ X₂ S : C} {f₁ : X₁ ⟶ S} {f₂ : X₂ ⟶ S} (h : ChosenPullback f₁ f₂) {Y : C} {f g : Y ⟶ h.pullback} (h₁ : CategoryStruct.comp f h.p₁ = CategoryStruct.comp g h.p₁) (h₂ : CategoryStruct.comp f h.p₂ = CategoryStruct.comp g h.p₂) : f = g

theorem CategoryTheory.Limits.ChosenPullback.hom_ext_iff {C : Type u} [Category.{v, u} C] {X₁ X₂ S : C} {f₁ : X₁ ⟶ S} {f₂ : X₂ ⟶ S} {h : ChosenPullback f₁ f₂} {Y : C} {f g : Y ⟶ h.pullback} : f = g ↔ CategoryStruct.comp f h.p₁ = CategoryStruct.comp g h.p₁ ∧ CategoryStruct.comp f h.p₂ = CategoryStruct.comp g h.p₂

structure CategoryTheory.Limits.ChosenPullback.LiftStruct {C : Type u} [Category.{v, u} C] {X₁ X₂ S : C} {f₁ : X₁ ⟶ S} {f₂ : X₂ ⟶ S} (h : ChosenPullback f₁ f₂) {Y : C} (g₁ : Y ⟶ X₁) (g₂ : Y ⟶ X₂) (b : Y ⟶ S) : Type v

Given f₁ : X₁ ⟶ S, f₂ : X₂ ⟶ S, h : ChosenPullback f₁ f₂ and morphisms g₁ : Y ⟶ X₁, g₂ : Y ⟶ X₂ and b : Y ⟶ S, this structure contains a morphism Y ⟶ h.pullback such that f ≫ h.p₁ = g₁, f ≫ h.p₂ = g₂ and f ≫ h.p = b. (This is nonempty only when g₁ ≫ f₁ = g₂ ≫ f₂ = b.)

• f : Y ⟶ h.pullback

  a lifting to the pullback

• f_p₁ : CategoryStruct.comp self.f h.p₁ = g₁
• f_p₂ : CategoryStruct.comp self.f h.p₂ = g₂
• f_p : CategoryStruct.comp self.f h.p = b

@[simp]

theorem CategoryTheory.Limits.ChosenPullback.LiftStruct.f_p₂_assoc {C : Type u} [Category.{v, u} C] {X₁ X₂ S : C} {f₁ : X₁ ⟶ S} {f₂ : X₂ ⟶ S} {h : ChosenPullback f₁ f₂} {Y : C} {g₁ : Y ⟶ X₁} {g₂ : Y ⟶ X₂} {b : Y ⟶ S} (self : h.LiftStruct g₁ g₂ b) {Z : C} (h✝ : X₂ ⟶ Z) : CategoryStruct.comp self.f (CategoryStruct.comp h.p₂ h✝) = CategoryStruct.comp g₂ h✝

@[simp]

theorem CategoryTheory.Limits.ChosenPullback.LiftStruct.f_p_assoc {C : Type u} [Category.{v, u} C] {X₁ X₂ S : C} {f₁ : X₁ ⟶ S} {f₂ : X₂ ⟶ S} {h : ChosenPullback f₁ f₂} {Y : C} {g₁ : Y ⟶ X₁} {g₂ : Y ⟶ X₂} {b : Y ⟶ S} (self : h.LiftStruct g₁ g₂ b) {Z : C} (h✝ : S ⟶ Z) : CategoryStruct.comp self.f (CategoryStruct.comp h.p h✝) = CategoryStruct.comp b h✝

@[simp]

theorem CategoryTheory.Limits.ChosenPullback.LiftStruct.f_p₁_assoc {C : Type u} [Category.{v, u} C] {X₁ X₂ S : C} {f₁ : X₁ ⟶ S} {f₂ : X₂ ⟶ S} {h : ChosenPullback f₁ f₂} {Y : C} {g₁ : Y ⟶ X₁} {g₂ : Y ⟶ X₂} {b : Y ⟶ S} (self : h.LiftStruct g₁ g₂ b) {Z : C} (h✝ : X₁ ⟶ Z) : CategoryStruct.comp self.f (CategoryStruct.comp h.p₁ h✝) = CategoryStruct.comp g₁ h✝

theorem CategoryTheory.Limits.ChosenPullback.LiftStruct.w {C : Type u} [Category.{v, u} C] {X₁ X₂ S : C} {f₁ : X₁ ⟶ S} {f₂ : X₂ ⟶ S} {h : ChosenPullback f₁ f₂} {Y : C} {g₁ : Y ⟶ X₁} {g₂ : Y ⟶ X₂} {b : Y ⟶ S} (l : h.LiftStruct g₁ g₂ b) : CategoryStruct.comp g₁ f₁ = CategoryStruct.comp g₂ f₂

theorem CategoryTheory.Limits.ChosenPullback.LiftStruct.w_assoc {C : Type u} [Category.{v, u} C] {X₁ X₂ S : C} {f₁ : X₁ ⟶ S} {f₂ : X₂ ⟶ S} {h : ChosenPullback f₁ f₂} {Y : C} {g₁ : Y ⟶ X₁} {g₂ : Y ⟶ X₂} {b : Y ⟶ S} (l : h.LiftStruct g₁ g₂ b) {Z : C} (h✝ : S ⟶ Z) : CategoryStruct.comp g₁ (CategoryStruct.comp f₁ h✝) = CategoryStruct.comp g₂ (CategoryStruct.comp f₂ h✝)

instance CategoryTheory.Limits.ChosenPullback.LiftStruct.instSubsingleton {C : Type u} [Category.{v, u} C] {X₁ X₂ S : C} {f₁ : X₁ ⟶ S} {f₂ : X₂ ⟶ S} {h : ChosenPullback f₁ f₂} {Y : C} {g₁ : Y ⟶ X₁} {g₂ : Y ⟶ X₂} {b : Y ⟶ S} : Subsingleton (h.LiftStruct g₁ g₂ b)

theorem CategoryTheory.Limits.ChosenPullback.LiftStruct.nonempty {C : Type u} [Category.{v, u} C] {X₁ X₂ S : C} {f₁ : X₁ ⟶ S} {f₂ : X₂ ⟶ S} {h : ChosenPullback f₁ f₂} {Y : C} {g₁ : Y ⟶ X₁} {g₂ : Y ⟶ X₂} {b : Y ⟶ S} (w : CategoryStruct.comp g₁ f₁ = CategoryStruct.comp g₂ f₂) (hf₁ : CategoryStruct.comp g₁ f₁ = b) : Nonempty (h.LiftStruct g₁ g₂ b)

@[reducible, inline]

abbrev CategoryTheory.Limits.ChosenPullback.Diagonal {C : Type u} [Category.{v, u} C] {X S : C} {f : X ⟶ S} (h : ChosenPullback f f) : Type v

Given f : X ⟶ S and h : ChosenPullback f f, this is the type of morphisms l : X ⟶ h.pullback that are equal to the diagonal map.

instance CategoryTheory.Limits.ChosenPullback.instNonemptyDiagonal {C : Type u} [Category.{v, u} C] {X S : C} {f : X ⟶ S} (h : ChosenPullback f f) : Nonempty h.Diagonal

structure CategoryTheory.Limits.ChosenPullback₃ {C : Type u} [Category.{v, u} C] {X₁ X₂ X₃ S : C} {f₁ : X₁ ⟶ S} {f₂ : X₂ ⟶ S} {f₃ : X₃ ⟶ S} (h₁₂ : ChosenPullback f₁ f₂) (h₂₃ : ChosenPullback f₂ f₃) (h₁₃ : ChosenPullback f₁ f₃) : Type (max u v)

Given three morphisms f₁ : X₁ ⟶ S, f₂ : X₂ ⟶ S and f₃ : X₃ ⟶ S, and chosen pullbacks for (f₁, f₂), (f₂, f₃) and (f₁, f₃), this structure contains the data of a wide pullback of the three morphisms f₁, f₂ and f₃.

• chosenPullback : ChosenPullback h₁₂.p₂ h₂₃.p₁

  A chosen pullback of h₁₂.pullback and h₂₃.pullback over X₂.

• p : self.chosenPullback.pullback ⟶ S

  The projection from the wide pullback of (f₁, f₂, f₃) to S.

• p₁ : self.chosenPullback.pullback ⟶ X₁

  The projection from the wide pullback of (f₁, f₂, f₃) to X₁.

• p₃ : self.chosenPullback.pullback ⟶ X₃

  The projection from the wide pullback of (f₁, f₂, f₃) to X₃.

• l : h₁₃.LiftStruct self.p₁ self.p₃ self.p

  A morphism from the wide pullback (f₁, f₂, f₃) to the pullback of f₁ and f₃ that is compatible with projections.

• hp₁ : CategoryStruct.comp self.chosenPullback.p₁ h₁₂.p₁ = self.p₁
• hp₃ : CategoryStruct.comp self.chosenPullback.p₂ h₂₃.p₂ = self.p₃

@[reducible, inline]

abbrev CategoryTheory.Limits.ChosenPullback₃.pullback {C : Type u} [Category.{v, u} C] {X₁ X₂ X₃ S : C} {f₁ : X₁ ⟶ S} {f₂ : X₂ ⟶ S} {f₃ : X₃ ⟶ S} {h₁₂ : ChosenPullback f₁ f₂} {h₂₃ : ChosenPullback f₂ f₃} {h₁₃ : ChosenPullback f₁ f₃} (h : ChosenPullback₃ h₁₂ h₂₃ h₁₃) : C

The chosen wide pullback of (f₁, f₂, f₃).

def CategoryTheory.Limits.ChosenPullback₃.p₁₃ {C : Type u} [Category.{v, u} C] {X₁ X₂ X₃ S : C} {f₁ : X₁ ⟶ S} {f₂ : X₂ ⟶ S} {f₃ : X₃ ⟶ S} {h₁₂ : ChosenPullback f₁ f₂} {h₂₃ : ChosenPullback f₂ f₃} {h₁₃ : ChosenPullback f₁ f₃} (h : ChosenPullback₃ h₁₂ h₂₃ h₁₃) : h.pullback ⟶ h₁₃.pullback

The projection from the wide pullback of (f₁, f₂, f₃) to the pullback of f₁ and f₃.

def CategoryTheory.Limits.ChosenPullback₃.p₁₂ {C : Type u} [Category.{v, u} C] {X₁ X₂ X₃ S : C} {f₁ : X₁ ⟶ S} {f₂ : X₂ ⟶ S} {f₃ : X₃ ⟶ S} {h₁₂ : ChosenPullback f₁ f₂} {h₂₃ : ChosenPullback f₂ f₃} {h₁₃ : ChosenPullback f₁ f₃} (h : ChosenPullback₃ h₁₂ h₂₃ h₁₃) : h.pullback ⟶ h₁₂.pullback

The projection from the wide pullback of (f₁, f₂, f₃) to the pullback of f₁ and f₂.

def CategoryTheory.Limits.ChosenPullback₃.p₂₃ {C : Type u} [Category.{v, u} C] {X₁ X₂ X₃ S : C} {f₁ : X₁ ⟶ S} {f₂ : X₂ ⟶ S} {f₃ : X₃ ⟶ S} {h₁₂ : ChosenPullback f₁ f₂} {h₂₃ : ChosenPullback f₂ f₃} {h₁₃ : ChosenPullback f₁ f₃} (h : ChosenPullback₃ h₁₂ h₂₃ h₁₃) : h.pullback ⟶ h₂₃.pullback

The projection from the wide pullback of (f₁, f₂, f₃) to the pullback of f₂ and f₃.

def CategoryTheory.Limits.ChosenPullback₃.p₂ {C : Type u} [Category.{v, u} C] {X₁ X₂ X₃ S : C} {f₁ : X₁ ⟶ S} {f₂ : X₂ ⟶ S} {f₃ : X₃ ⟶ S} {h₁₂ : ChosenPullback f₁ f₂} {h₂₃ : ChosenPullback f₂ f₃} {h₁₃ : ChosenPullback f₁ f₃} (h : ChosenPullback₃ h₁₂ h₂₃ h₁₃) : h.pullback ⟶ X₂

The projection from the wide pullback of (f₁, f₂, f₃) to X₂.

@[simp]

theorem CategoryTheory.Limits.ChosenPullback₃.p₁₂_p₁ {C : Type u} [Category.{v, u} C] {X₁ X₂ X₃ S : C} {f₁ : X₁ ⟶ S} {f₂ : X₂ ⟶ S} {f₃ : X₃ ⟶ S} {h₁₂ : ChosenPullback f₁ f₂} {h₂₃ : ChosenPullback f₂ f₃} {h₁₃ : ChosenPullback f₁ f₃} (h : ChosenPullback₃ h₁₂ h₂₃ h₁₃) : CategoryStruct.comp h.p₁₂ h₁₂.p₁ = h.p₁

@[simp]

theorem CategoryTheory.Limits.ChosenPullback₃.p₁₂_p₁_assoc {C : Type u} [Category.{v, u} C] {X₁ X₂ X₃ S : C} {f₁ : X₁ ⟶ S} {f₂ : X₂ ⟶ S} {f₃ : X₃ ⟶ S} {h₁₂ : ChosenPullback f₁ f₂} {h₂₃ : ChosenPullback f₂ f₃} {h₁₃ : ChosenPullback f₁ f₃} (h : ChosenPullback₃ h₁₂ h₂₃ h₁₃) {Z : C} (h✝ : X₁ ⟶ Z) : CategoryStruct.comp h.p₁₂ (CategoryStruct.comp h₁₂.p₁ h✝) = CategoryStruct.comp h.p₁ h✝

@[simp]

theorem CategoryTheory.Limits.ChosenPullback₃.p₁₂_p₂ {C : Type u} [Category.{v, u} C] {X₁ X₂ X₃ S : C} {f₁ : X₁ ⟶ S} {f₂ : X₂ ⟶ S} {f₃ : X₃ ⟶ S} {h₁₂ : ChosenPullback f₁ f₂} {h₂₃ : ChosenPullback f₂ f₃} {h₁₃ : ChosenPullback f₁ f₃} (h : ChosenPullback₃ h₁₂ h₂₃ h₁₃) : CategoryStruct.comp h.p₁₂ h₁₂.p₂ = h.p₂

@[simp]

theorem CategoryTheory.Limits.ChosenPullback₃.p₁₂_p₂_assoc {C : Type u} [Category.{v, u} C] {X₁ X₂ X₃ S : C} {f₁ : X₁ ⟶ S} {f₂ : X₂ ⟶ S} {f₃ : X₃ ⟶ S} {h₁₂ : ChosenPullback f₁ f₂} {h₂₃ : ChosenPullback f₂ f₃} {h₁₃ : ChosenPullback f₁ f₃} (h : ChosenPullback₃ h₁₂ h₂₃ h₁₃) {Z : C} (h✝ : X₂ ⟶ Z) : CategoryStruct.comp h.p₁₂ (CategoryStruct.comp h₁₂.p₂ h✝) = CategoryStruct.comp h.p₂ h✝

@[simp]

theorem CategoryTheory.Limits.ChosenPullback₃.p₂₃_p₂ {C : Type u} [Category.{v, u} C] {X₁ X₂ X₃ S : C} {f₁ : X₁ ⟶ S} {f₂ : X₂ ⟶ S} {f₃ : X₃ ⟶ S} {h₁₂ : ChosenPullback f₁ f₂} {h₂₃ : ChosenPullback f₂ f₃} {h₁₃ : ChosenPullback f₁ f₃} (h : ChosenPullback₃ h₁₂ h₂₃ h₁₃) : CategoryStruct.comp h.p₂₃ h₂₃.p₁ = h.p₂

@[simp]

theorem CategoryTheory.Limits.ChosenPullback₃.p₂₃_p₂_assoc {C : Type u} [Category.{v, u} C] {X₁ X₂ X₃ S : C} {f₁ : X₁ ⟶ S} {f₂ : X₂ ⟶ S} {f₃ : X₃ ⟶ S} {h₁₂ : ChosenPullback f₁ f₂} {h₂₃ : ChosenPullback f₂ f₃} {h₁₃ : ChosenPullback f₁ f₃} (h : ChosenPullback₃ h₁₂ h₂₃ h₁₃) {Z : C} (h✝ : X₂ ⟶ Z) : CategoryStruct.comp h.p₂₃ (CategoryStruct.comp h₂₃.p₁ h✝) = CategoryStruct.comp h.p₂ h✝

@[simp]

theorem CategoryTheory.Limits.ChosenPullback₃.p₂₃_p₃ {C : Type u} [Category.{v, u} C] {X₁ X₂ X₃ S : C} {f₁ : X₁ ⟶ S} {f₂ : X₂ ⟶ S} {f₃ : X₃ ⟶ S} {h₁₂ : ChosenPullback f₁ f₂} {h₂₃ : ChosenPullback f₂ f₃} {h₁₃ : ChosenPullback f₁ f₃} (h : ChosenPullback₃ h₁₂ h₂₃ h₁₃) : CategoryStruct.comp h.p₂₃ h₂₃.p₂ = h.p₃

@[simp]

theorem CategoryTheory.Limits.ChosenPullback₃.p₂₃_p₃_assoc {C : Type u} [Category.{v, u} C] {X₁ X₂ X₃ S : C} {f₁ : X₁ ⟶ S} {f₂ : X₂ ⟶ S} {f₃ : X₃ ⟶ S} {h₁₂ : ChosenPullback f₁ f₂} {h₂₃ : ChosenPullback f₂ f₃} {h₁₃ : ChosenPullback f₁ f₃} (h : ChosenPullback₃ h₁₂ h₂₃ h₁₃) {Z : C} (h✝ : X₃ ⟶ Z) : CategoryStruct.comp h.p₂₃ (CategoryStruct.comp h₂₃.p₂ h✝) = CategoryStruct.comp h.p₃ h✝

@[simp]

theorem CategoryTheory.Limits.ChosenPullback₃.p₁₃_p₁ {C : Type u} [Category.{v, u} C] {X₁ X₂ X₃ S : C} {f₁ : X₁ ⟶ S} {f₂ : X₂ ⟶ S} {f₃ : X₃ ⟶ S} {h₁₂ : ChosenPullback f₁ f₂} {h₂₃ : ChosenPullback f₂ f₃} {h₁₃ : ChosenPullback f₁ f₃} (h : ChosenPullback₃ h₁₂ h₂₃ h₁₃) : CategoryStruct.comp h.p₁₃ h₁₃.p₁ = h.p₁

@[simp]

theorem CategoryTheory.Limits.ChosenPullback₃.p₁₃_p₁_assoc {C : Type u} [Category.{v, u} C] {X₁ X₂ X₃ S : C} {f₁ : X₁ ⟶ S} {f₂ : X₂ ⟶ S} {f₃ : X₃ ⟶ S} {h₁₂ : ChosenPullback f₁ f₂} {h₂₃ : ChosenPullback f₂ f₃} {h₁₃ : ChosenPullback f₁ f₃} (h : ChosenPullback₃ h₁₂ h₂₃ h₁₃) {Z : C} (h✝ : X₁ ⟶ Z) : CategoryStruct.comp h.p₁₃ (CategoryStruct.comp h₁₃.p₁ h✝) = CategoryStruct.comp h.p₁ h✝

@[simp]

theorem CategoryTheory.Limits.ChosenPullback₃.p₁₃_p₃ {C : Type u} [Category.{v, u} C] {X₁ X₂ X₃ S : C} {f₁ : X₁ ⟶ S} {f₂ : X₂ ⟶ S} {f₃ : X₃ ⟶ S} {h₁₂ : ChosenPullback f₁ f₂} {h₂₃ : ChosenPullback f₂ f₃} {h₁₃ : ChosenPullback f₁ f₃} (h : ChosenPullback₃ h₁₂ h₂₃ h₁₃) : CategoryStruct.comp h.p₁₃ h₁₃.p₂ = h.p₃

@[simp]

theorem CategoryTheory.Limits.ChosenPullback₃.p₁₃_p₃_assoc {C : Type u} [Category.{v, u} C] {X₁ X₂ X₃ S : C} {f₁ : X₁ ⟶ S} {f₂ : X₂ ⟶ S} {f₃ : X₃ ⟶ S} {h₁₂ : ChosenPullback f₁ f₂} {h₂₃ : ChosenPullback f₂ f₃} {h₁₃ : ChosenPullback f₁ f₃} (h : ChosenPullback₃ h₁₂ h₂₃ h₁₃) {Z : C} (h✝ : X₃ ⟶ Z) : CategoryStruct.comp h.p₁₃ (CategoryStruct.comp h₁₃.p₂ h✝) = CategoryStruct.comp h.p₃ h✝

@[simp]

theorem CategoryTheory.Limits.ChosenPullback₃.w₁ {C : Type u} [Category.{v, u} C] {X₁ X₂ X₃ S : C} {f₁ : X₁ ⟶ S} {f₂ : X₂ ⟶ S} {f₃ : X₃ ⟶ S} {h₁₂ : ChosenPullback f₁ f₂} {h₂₃ : ChosenPullback f₂ f₃} {h₁₃ : ChosenPullback f₁ f₃} (h : ChosenPullback₃ h₁₂ h₂₃ h₁₃) : CategoryStruct.comp h.p₁ f₁ = h.p

@[simp]

theorem CategoryTheory.Limits.ChosenPullback₃.w₁_assoc {C : Type u} [Category.{v, u} C] {X₁ X₂ X₃ S : C} {f₁ : X₁ ⟶ S} {f₂ : X₂ ⟶ S} {f₃ : X₃ ⟶ S} {h₁₂ : ChosenPullback f₁ f₂} {h₂₃ : ChosenPullback f₂ f₃} {h₁₃ : ChosenPullback f₁ f₃} (h : ChosenPullback₃ h₁₂ h₂₃ h₁₃) {Z : C} (h✝ : S ⟶ Z) : CategoryStruct.comp h.p₁ (CategoryStruct.comp f₁ h✝) = CategoryStruct.comp h.p h✝

@[simp]

theorem CategoryTheory.Limits.ChosenPullback₃.w₃ {C : Type u} [Category.{v, u} C] {X₁ X₂ X₃ S : C} {f₁ : X₁ ⟶ S} {f₂ : X₂ ⟶ S} {f₃ : X₃ ⟶ S} {h₁₂ : ChosenPullback f₁ f₂} {h₂₃ : ChosenPullback f₂ f₃} {h₁₃ : ChosenPullback f₁ f₃} (h : ChosenPullback₃ h₁₂ h₂₃ h₁₃) : CategoryStruct.comp h.p₃ f₃ = h.p

@[simp]

theorem CategoryTheory.Limits.ChosenPullback₃.w₃_assoc {C : Type u} [Category.{v, u} C] {X₁ X₂ X₃ S : C} {f₁ : X₁ ⟶ S} {f₂ : X₂ ⟶ S} {f₃ : X₃ ⟶ S} {h₁₂ : ChosenPullback f₁ f₂} {h₂₃ : ChosenPullback f₂ f₃} {h₁₃ : ChosenPullback f₁ f₃} (h : ChosenPullback₃ h₁₂ h₂₃ h₁₃) {Z : C} (h✝ : S ⟶ Z) : CategoryStruct.comp h.p₃ (CategoryStruct.comp f₃ h✝) = CategoryStruct.comp h.p h✝

@[simp]

theorem CategoryTheory.Limits.ChosenPullback₃.w₂ {C : Type u} [Category.{v, u} C] {X₁ X₂ X₃ S : C} {f₁ : X₁ ⟶ S} {f₂ : X₂ ⟶ S} {f₃ : X₃ ⟶ S} {h₁₂ : ChosenPullback f₁ f₂} {h₂₃ : ChosenPullback f₂ f₃} {h₁₃ : ChosenPullback f₁ f₃} (h : ChosenPullback₃ h₁₂ h₂₃ h₁₃) : CategoryStruct.comp h.p₂ f₂ = h.p

@[simp]

theorem CategoryTheory.Limits.ChosenPullback₃.w₂_assoc {C : Type u} [Category.{v, u} C] {X₁ X₂ X₃ S : C} {f₁ : X₁ ⟶ S} {f₂ : X₂ ⟶ S} {f₃ : X₃ ⟶ S} {h₁₂ : ChosenPullback f₁ f₂} {h₂₃ : ChosenPullback f₂ f₃} {h₁₃ : ChosenPullback f₁ f₃} (h : ChosenPullback₃ h₁₂ h₂₃ h₁₃) {Z : C} (h✝ : S ⟶ Z) : CategoryStruct.comp h.p₂ (CategoryStruct.comp f₂ h✝) = CategoryStruct.comp h.p h✝

@[simp]

theorem CategoryTheory.Limits.ChosenPullback₃.p₁₂_p {C : Type u} [Category.{v, u} C] {X₁ X₂ X₃ S : C} {f₁ : X₁ ⟶ S} {f₂ : X₂ ⟶ S} {f₃ : X₃ ⟶ S} {h₁₂ : ChosenPullback f₁ f₂} {h₂₃ : ChosenPullback f₂ f₃} {h₁₃ : ChosenPullback f₁ f₃} (h : ChosenPullback₃ h₁₂ h₂₃ h₁₃) : CategoryStruct.comp h.p₁₂ h₁₂.p = h.p

@[simp]

theorem CategoryTheory.Limits.ChosenPullback₃.p₁₂_p_assoc {C : Type u} [Category.{v, u} C] {X₁ X₂ X₃ S : C} {f₁ : X₁ ⟶ S} {f₂ : X₂ ⟶ S} {f₃ : X₃ ⟶ S} {h₁₂ : ChosenPullback f₁ f₂} {h₂₃ : ChosenPullback f₂ f₃} {h₁₃ : ChosenPullback f₁ f₃} (h : ChosenPullback₃ h₁₂ h₂₃ h₁₃) {Z : C} (h✝ : S ⟶ Z) : CategoryStruct.comp h.p₁₂ (CategoryStruct.comp h₁₂.p h✝) = CategoryStruct.comp h.p h✝

@[simp]

theorem CategoryTheory.Limits.ChosenPullback₃.p₂₃_p {C : Type u} [Category.{v, u} C] {X₁ X₂ X₃ S : C} {f₁ : X₁ ⟶ S} {f₂ : X₂ ⟶ S} {f₃ : X₃ ⟶ S} {h₁₂ : ChosenPullback f₁ f₂} {h₂₃ : ChosenPullback f₂ f₃} {h₁₃ : ChosenPullback f₁ f₃} (h : ChosenPullback₃ h₁₂ h₂₃ h₁₃) : CategoryStruct.comp h.p₂₃ h₂₃.p = h.p

@[simp]

theorem CategoryTheory.Limits.ChosenPullback₃.p₂₃_p_assoc {C : Type u} [Category.{v, u} C] {X₁ X₂ X₃ S : C} {f₁ : X₁ ⟶ S} {f₂ : X₂ ⟶ S} {f₃ : X₃ ⟶ S} {h₁₂ : ChosenPullback f₁ f₂} {h₂₃ : ChosenPullback f₂ f₃} {h₁₃ : ChosenPullback f₁ f₃} (h : ChosenPullback₃ h₁₂ h₂₃ h₁₃) {Z : C} (h✝ : S ⟶ Z) : CategoryStruct.comp h.p₂₃ (CategoryStruct.comp h₂₃.p h✝) = CategoryStruct.comp h.p h✝

@[simp]

theorem CategoryTheory.Limits.ChosenPullback₃.p₁₃_p {C : Type u} [Category.{v, u} C] {X₁ X₂ X₃ S : C} {f₁ : X₁ ⟶ S} {f₂ : X₂ ⟶ S} {f₃ : X₃ ⟶ S} {h₁₂ : ChosenPullback f₁ f₂} {h₂₃ : ChosenPullback f₂ f₃} {h₁₃ : ChosenPullback f₁ f₃} (h : ChosenPullback₃ h₁₂ h₂₃ h₁₃) : CategoryStruct.comp h.p₁₃ h₁₃.p = h.p

@[simp]

theorem CategoryTheory.Limits.ChosenPullback₃.p₁₃_p_assoc {C : Type u} [Category.{v, u} C] {X₁ X₂ X₃ S : C} {f₁ : X₁ ⟶ S} {f₂ : X₂ ⟶ S} {f₃ : X₃ ⟶ S} {h₁₂ : ChosenPullback f₁ f₂} {h₂₃ : ChosenPullback f₂ f₃} {h₁₃ : ChosenPullback f₁ f₃} (h : ChosenPullback₃ h₁₂ h₂₃ h₁₃) {Z : C} (h✝ : S ⟶ Z) : CategoryStruct.comp h.p₁₃ (CategoryStruct.comp h₁₃.p h✝) = CategoryStruct.comp h.p h✝

theorem CategoryTheory.Limits.ChosenPullback₃.p₁₂_eq_lift {C : Type u} [Category.{v, u} C] {X₁ X₂ X₃ S : C} {f₁ : X₁ ⟶ S} {f₂ : X₂ ⟶ S} {f₃ : X₃ ⟶ S} {h₁₂ : ChosenPullback f₁ f₂} {h₂₃ : ChosenPullback f₂ f₃} {h₁₃ : ChosenPullback f₁ f₃} (h : ChosenPullback₃ h₁₂ h₂₃ h₁₃) : h.p₁₂ = ⋯.lift h.p₁ h.p₂ ⋯

theorem CategoryTheory.Limits.ChosenPullback₃.p₂₃_eq_lift {C : Type u} [Category.{v, u} C] {X₁ X₂ X₃ S : C} {f₁ : X₁ ⟶ S} {f₂ : X₂ ⟶ S} {f₃ : X₃ ⟶ S} {h₁₂ : ChosenPullback f₁ f₂} {h₂₃ : ChosenPullback f₂ f₃} {h₁₃ : ChosenPullback f₁ f₃} (h : ChosenPullback₃ h₁₂ h₂₃ h₁₃) : h.p₂₃ = ⋯.lift h.p₂ h.p₃ ⋯

theorem CategoryTheory.Limits.ChosenPullback₃.p₁₃_eq_lift {C : Type u} [Category.{v, u} C] {X₁ X₂ X₃ S : C} {f₁ : X₁ ⟶ S} {f₂ : X₂ ⟶ S} {f₃ : X₃ ⟶ S} {h₁₂ : ChosenPullback f₁ f₂} {h₂₃ : ChosenPullback f₂ f₃} {h₁₃ : ChosenPullback f₁ f₃} (h : ChosenPullback₃ h₁₂ h₂₃ h₁₃) : h.p₁₃ = ⋯.lift h.p₁ h.p₃ ⋯

theorem CategoryTheory.Limits.ChosenPullback₃.exists_lift {C : Type u} [Category.{v, u} C] {X₁ X₂ X₃ S : C} {f₁ : X₁ ⟶ S} {f₂ : X₂ ⟶ S} {f₃ : X₃ ⟶ S} {h₁₂ : ChosenPullback f₁ f₂} {h₂₃ : ChosenPullback f₂ f₃} {h₁₃ : ChosenPullback f₁ f₃} (h : ChosenPullback₃ h₁₂ h₂₃ h₁₃) {Y : C} (g₁ : Y ⟶ X₁) (g₂ : Y ⟶ X₂) (g₃ : Y ⟶ X₃) (b : Y ⟶ S) (hg₁ : CategoryStruct.comp g₁ f₁ = b) (hg₂ : CategoryStruct.comp g₂ f₂ = b) (hg₃ : CategoryStruct.comp g₃ f₃ = b) : ∃ (φ : Y ⟶ h.pullback), CategoryStruct.comp φ h.p₁ = g₁ ∧ CategoryStruct.comp φ h.p₂ = g₂ ∧ CategoryStruct.comp φ h.p₃ = g₃

theorem CategoryTheory.Limits.ChosenPullback₃.isPullback₂ {C : Type u} [Category.{v, u} C] {X₁ X₂ X₃ S : C} {f₁ : X₁ ⟶ S} {f₂ : X₂ ⟶ S} {f₃ : X₃ ⟶ S} {h₁₂ : ChosenPullback f₁ f₂} {h₂₃ : ChosenPullback f₂ f₃} {h₁₃ : ChosenPullback f₁ f₃} (h : ChosenPullback₃ h₁₂ h₂₃ h₁₃) : IsPullback h.p₁₂ h.p₂₃ h₁₂.p₂ h₂₃.p₁

theorem CategoryTheory.Limits.ChosenPullback₃.hom_ext {C : Type u} [Category.{v, u} C] {X₁ X₂ X₃ S : C} {f₁ : X₁ ⟶ S} {f₂ : X₂ ⟶ S} {f₃ : X₃ ⟶ S} {h₁₂ : ChosenPullback f₁ f₂} {h₂₃ : ChosenPullback f₂ f₃} {h₁₃ : ChosenPullback f₁ f₃} (h : ChosenPullback₃ h₁₂ h₂₃ h₁₃) {Y : C} {φ φ' : Y ⟶ h.pullback} (h₁ : CategoryStruct.comp φ h.p₁ = CategoryStruct.comp φ' h.p₁) (h₂ : CategoryStruct.comp φ h.p₂ = CategoryStruct.comp φ' h.p₂) (h₃ : CategoryStruct.comp φ h.p₃ = CategoryStruct.comp φ' h.p₃) : φ = φ'

theorem CategoryTheory.Limits.ChosenPullback₃.hom_ext_iff {C : Type u} [Category.{v, u} C] {X₁ X₂ X₃ S : C} {f₁ : X₁ ⟶ S} {f₂ : X₂ ⟶ S} {f₃ : X₃ ⟶ S} {h₁₂ : ChosenPullback f₁ f₂} {h₂₃ : ChosenPullback f₂ f₃} {h₁₃ : ChosenPullback f₁ f₃} {h : ChosenPullback₃ h₁₂ h₂₃ h₁₃} {Y : C} {φ φ' : Y ⟶ h.pullback} : φ = φ' ↔ CategoryStruct.comp φ h.p₁ = CategoryStruct.comp φ' h.p₁ ∧ CategoryStruct.comp φ h.p₂ = CategoryStruct.comp φ' h.p₂ ∧ CategoryStruct.comp φ h.p₃ = CategoryStruct.comp φ' h.p₃

theorem CategoryTheory.Limits.ChosenPullback₃.isPullback₁ {C : Type u} [Category.{v, u} C] {X₁ X₂ X₃ S : C} {f₁ : X₁ ⟶ S} {f₂ : X₂ ⟶ S} {f₃ : X₃ ⟶ S} {h₁₂ : ChosenPullback f₁ f₂} {h₂₃ : ChosenPullback f₂ f₃} {h₁₃ : ChosenPullback f₁ f₃} (h : ChosenPullback₃ h₁₂ h₂₃ h₁₃) : IsPullback h.p₁₂ h.p₁₃ h₁₂.p₁ h₁₃.p₁

theorem CategoryTheory.Limits.ChosenPullback₃.isPullback₃ {C : Type u} [Category.{v, u} C] {X₁ X₂ X₃ S : C} {f₁ : X₁ ⟶ S} {f₂ : X₂ ⟶ S} {f₃ : X₃ ⟶ S} {h₁₂ : ChosenPullback f₁ f₂} {h₂₃ : ChosenPullback f₂ f₃} {h₁₃ : ChosenPullback f₁ f₃} (h : ChosenPullback₃ h₁₂ h₂₃ h₁₃) : IsPullback h.p₁₃ h.p₂₃ h₁₃.p₂ h₂₃.p₂