English
For x on a presieve R with HasPairwisePullbacks, the compatibility notion is equivalent to the pullback-compatibility notion.
Русский
Для x на презиве R с свойствами HasPairwisePullbacks совместимость совпадает с понятием совместимости по вытягиванию (pullback-compatibility).
LaTeX
$$$x.\\text{Compatible} \\iff x.\\text{PullbackCompatible}$$$
Lean4
theorem pullbackCompatible_iff (x : FamilyOfElements P R) [R.HasPairwisePullbacks] :
x.Compatible ↔ x.PullbackCompatible := by
constructor
· intro t Y₁ Y₂ f₁ f₂ hf₁ hf₂
apply t
haveI := HasPairwisePullbacks.has_pullbacks hf₁ hf₂
apply pullback.condition
· intro t Y₁ Y₂ Z g₁ g₂ f₁ f₂ hf₁ hf₂ comm
haveI := HasPairwisePullbacks.has_pullbacks hf₁ hf₂
rw [← pullback.lift_fst _ _ comm, op_comp, FunctorToTypes.map_comp_apply, t hf₁ hf₂, ←
FunctorToTypes.map_comp_apply, ← op_comp, pullback.lift_snd]
