English
If, for every a and every morphism g: F.obj a → Y, there exist a pullback presentation with P-snd, then f is relative for F with respect to P.
Русский
Если для каждого a и каждого морфизма g: F.obj a → Y существует представление вытяжки с P snd, то f является относительным для F по P.
LaTeX
$$$\forall a:\;\exists b, fst, snd, BC, P snd \Rightarrow P.relative F f$$$
Lean4
/-- Given a morphism property `P` which respects isomorphisms, then to show that a morphism
`f : X ⟶ Y` satisfies `P.relative` it suffices to show that:
* The morphism is representable.
* For any morphism `g : F.obj a ⟶ G`, the property `P` holds for *some* represented pullback
of `f` by `g`. -/
theorem of_exists [F.Faithful] [F.Full] [P.RespectsIso] {f : X ⟶ Y}
(h₀ :
∀ ⦃a : C⦄ (g : F.obj a ⟶ Y),
∃ (b : C) (fst : F.obj b ⟶ X) (snd : b ⟶ a) (_ : IsPullback fst (F.map snd) f g), P snd) :
P.relative F f := by
refine ⟨fun a g ↦ ?_, fun a b g fst snd h ↦ ?_⟩
all_goals obtain ⟨c, g_fst, g_snd, BC, H⟩ := h₀ g
· refine ⟨c, g_snd, g_fst, BC⟩
· refine (P.arrow_mk_iso_iff ?_).2 H
exact Arrow.isoMk (F.preimageIso (h.isoIsPullback X (F.obj a) BC)) (Iso.refl _) (F.map_injective (by simp))
