English
If Q.IsStableUnderCobaseChange and P.HasOfPostcompProperty Q and P.RespectsLeft Q, then P.CodescendsAlong Q.
Русский
Если Q стабилен по кобазе и P имеет свойство HasOfPostcompProperty Q и P уважает левый фактор, то P спускается по Q.
LaTeX
$$$[Q.IsStableUnderCobaseChange] [P.HasOfPostcompProperty Q] [P.RespectsLeft Q] : P.CodescendsAlong Q$$$
Lean4
instance [Q.IsStableUnderCobaseChange] [P.HasOfPostcompProperty Q] [P.RespectsLeft Q] : P.CodescendsAlong Q where
of_isPushout {X Y Z A f g inl inr} h hf
hinl := by
apply P.of_postcomp (W' := Q) g inr (Q.of_isPushout h.flip hf)
rw [← h.1.1]
exact RespectsLeft.precomp _ hf _ hinl
