relative_map_iff — Mathlib

English

With suitable hypotheses (faithful, full, preserves pullbacks, stability under base change), P.relative F (F.map f) is equivalent to P f.

Русский

При подходящих предпосылках (верность, полнота, сохранение вытяжек, устойчивость к базовым изменениям) свойство P.relative F (F.map f) эквивалентно P f.

LaTeX

$$$P.relative F (F.map f) \iff P f$$$

Lean4

theorem relative_map_iff [F.Faithful] [F.Full] [PreservesLimitsOfShape WalkingCospan F] [HasPullbacks C]
    [IsStableUnderBaseChange P] {X Y : C} {f : X ⟶ Y} : P.relative F (F.map f) ↔ P f :=
  ⟨fun hf ↦ of_relative_map hf, fun hf ↦ relative_map hf⟩

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