isSeparatedFor_iso — Mathlib

English

Let X be an object in a category and R a presieve on X. If P is separated for R and there is an isomorphism of presheaves P ≅ P′, then P′ is also separated for R.

Русский

Пусть X — объект в некоторой категории и R — предраспелив на X. Пусть P отделён относительно R и существует изоморфизм предобраза P ≅ P′. Тогда P′ также отделён относительно R.

LaTeX

$$$ (P \cong P') \Rightarrow (\mathrm{IsSeparatedFor}(P,R) \Rightarrow \mathrm{IsSeparatedFor}(P',R)) $$$

Lean4

/-- The property of being separated for some presieve is preserved under isomorphisms. -/
theorem isSeparatedFor_iso {P' : Cᵒᵖ ⥤ Type w} (i : P ≅ P') (hP : IsSeparatedFor P R) : IsSeparatedFor P' R :=
  by
  intro x t₁ t₂ ht₁ ht₂
  simpa using congrArg (i.hom.app _) <| hP (x.map i.inv) _ _ (ht₁.map i.inv) (ht₂.map i.inv)

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