universally_mk' — Mathlib

English

If P respects iso and g: X → Y, and for every pullback along f with g we have P(pullback.fst f g), then universally P g.

Русский

Если P сохраняет изоморфизмы и для каждого f и f pullback имеет P(pullback.fst f g), тогда universally P g.

LaTeX

$$$Universally(P,g)$$$

Lean4

theorem universally_mk' (P : MorphismProperty C) [P.RespectsIso] {X Y : C} (g : X ⟶ Y)
    (H : ∀ {T : C} (f : T ⟶ Y) [HasPullback f g], P (pullback.fst f g)) : universally P g :=
  by
  introv X' h
  have := h.hasPullback
  rw [← h.isoPullback_hom_fst, P.cancel_left_of_respectsIso]
  exact H ..

Похожие утверждения