iff_of_iso — Mathlib

English

For A,B presheaves and η: A → B with η an isomorphism, A is an Ind-object if and only if B is an Ind-object.

Русский

Для прешепафет A,B и изоморфизма η: A → B верно: A является Ind-объектом тогда и только тогда, когда B является Ind-объектом.

LaTeX

$$$\forall A,B\;\forall \eta\colon A\to B\;[\mathrm{IsIso}\;\eta],\; \mathrm{IsIndObject}(A) \iff \mathrm{IsIndObject}(B)$$$

Lean4

theorem iff_of_iso {A B : Cᵒᵖ ⥤ Type v} (η : A ⟶ B) [IsIso η] : IsIndObject A ↔ IsIndObject B :=
  ⟨.map η, .map (inv η)⟩

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