English
If W is stable under composition, and P is stable under base-change and under composition, then the source-local-closure (W, P) is stable under composition.
Русский
Если W стабильно по композиции, а P стабильно по базовому изменению и по композиции, то sourceLocalClosure(W, P) стабильно по композиции.
LaTeX
$$$ W.IsStableUnderComposition \land P.IsStableUnderBaseChange \land P.IsStableUnderComposition \Rightarrow (sourceLocalClosure\ W\ P).IsStableUnderComposition $$$
Lean4
instance [W.IsStableUnderComposition] [P.IsStableUnderBaseChange] [P.IsStableUnderComposition] :
(sourceLocalClosure W P).IsStableUnderComposition :=
by
refine ⟨fun {X Y Z} f g ⟨𝒰, hf⟩ ⟨𝒱, hg⟩ ↦ ?_⟩
refine ⟨𝒰.bind fun i ↦ (𝒱.pullback₁ (𝒰.f i ≫ f)), fun ⟨l, r⟩ ↦ ?_⟩
simpa [← pullbackRightPullbackFstIso_inv_snd_fst_assoc, pullback.condition_assoc] using
P.comp_mem _ _ (P.pullback_snd _ _ (hf _)) (hg r)
