map — Mathlib

English

If f is an isomorphism, then F maps f to a relatively representable morphism.

Русский

Если f изоморфизм, то F отображает f как относительно представимый морфизм.

LaTeX

$$$$ \\text{of_isIso: } (IsIso\\, f) \\Rightarrow F.relativelyRepresentable f $$$$

Lean4

/-- When `C` has pullbacks, then `F.map f` is representable with respect to `F` for any
`f : a ⟶ b` in `C`. -/
theorem map [Full F] [HasPullbacks C] {a b : C} (f : a ⟶ b) [∀ c (g : c ⟶ b), PreservesLimit (cospan f g) F] :
    F.relativelyRepresentable (F.map f) := fun c g ↦
  by
  obtain ⟨g, rfl⟩ := F.map_surjective g
  refine ⟨Limits.pullback f g, Limits.pullback.snd f g, F.map (Limits.pullback.fst f g), ?_⟩
  apply F.map_isPullback <| IsPullback.of_hasPullback f g

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