relative_of_snd — Mathlib

English

If F.relativelyRepresentable f holds and for every a there is P for hf.snd g, then P.relative F f holds.

Русский

Если F.relativelyRepresentable f выполняется и для каждого a свойства P выполняется для hf.snd g, тогда P.relative F f выполняется.

LaTeX

$$$ (F.relativelyRepresentable f) \Rightarrow (\forall a,g, P( hf.snd g)) \Rightarrow P.relative F f$$

Lean4

theorem relative_of_snd [F.Faithful] [F.Full] [P.RespectsIso] {f : X ⟶ Y} (hf : F.relativelyRepresentable f)
    (h : ∀ ⦃a : C⦄ (g : F.obj a ⟶ Y), P (hf.snd g)) : P.relative F f :=
  relative.of_exists (fun _ g ↦ ⟨hf.pullback g, hf.fst g, hf.snd g, hf.isPullback g, h g⟩)

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