relative_map — Mathlib

English

If P holds on f, then the mapped morphism F.map f satisfies P.relative.

Русский

Если P выполняется на f, то F.map f удовлетворяет P.relative.

LaTeX

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

Lean4

/-- If `P : MorphismProperty C` is stable under base change, `F` is fully faithful and preserves
pullbacks, and `C` has all pullbacks, then for any `f : a ⟶ b` in `C`, `F.map f` satisfies
`P.relative` if `f` satisfies `P`. -/
theorem relative_map [F.Faithful] [F.Full] [HasPullbacks C] [IsStableUnderBaseChange P] {a b : C} {f : a ⟶ b}
    [∀ c (g : c ⟶ b), PreservesLimit (cospan f g) F] (hf : P f) : P.relative F (F.map f) :=
  by
  apply relative.of_exists
  intro Y' g
  obtain ⟨g, rfl⟩ := F.map_surjective g
  exact ⟨_, _, _, (IsPullback.of_hasPullback f g).map F, P.pullback_snd _ _ hf⟩

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