English
Let P be stable under base change and multiplicative, and Q stable under base change. The HasOfPostcompProperty P Q holds iff Q is contained in P.diagonal.
Русский
Пусть P устойчиво к изменению основания и мультипликативно, Q устойчиво к изменению основания. Свойство HasOfPostcompProperty P Q матожно эквиваленты тому, что Q ≤ P.diagonal.
LaTeX
$$$P.HasOfPostcompProperty Q \iff Q \le P.diagonal$$$
Lean4
/-- If `P` is multiplicative and stable under base change, having the of-postcomp property
w.r.t. `Q` is equivalent to `Q` implying `P` on the diagonal. -/
theorem hasOfPostcompProperty_iff_le_diagonal [P.IsStableUnderBaseChange] [P.IsMultiplicative] {Q : MorphismProperty C}
[Q.IsStableUnderBaseChange] : P.HasOfPostcompProperty Q ↔ Q ≤ P.diagonal :=
by
refine ⟨fun hP X Y f hf ↦ ?_, fun hP ↦ ⟨fun {Y X S} g f hf hcomp ↦ ?_⟩⟩
· exact hP.of_postcomp _ _ (Q.pullback_fst _ _ hf) (by simpa using P.id_mem X)
· set gr : Y ⟶ pullback (g ≫ f) f := pullback.lift (𝟙 Y) g (by simp)
have : g = gr ≫ pullback.snd _ _ := by simp [gr]
rw [this]
apply P.comp_mem
· exact P.of_isPullback (pullback_lift_diagonal_isPullback g f) (hP _ hf)
· exact P.pullback_snd _ _ hcomp
