isoClosure_eq_iff — Mathlib

English

The iso-closure of a morphism property P equals P if and only if P respects isomorphisms.

Русский

Изоморфная закрывающая оболочка свойства морфизмов равна самому свойству тогда и только тогда, когда это свойство сохраняет изоморфизмы.

LaTeX

$$$P.\\mathrm{isoClosure} = P \\iff P.\\mathrm{RespectsIso}$$$

Lean4

theorem isoClosure_eq_iff (P : MorphismProperty C) : P.isoClosure = P ↔ P.RespectsIso :=
  by
  refine ⟨(· ▸ P.isoClosure_respectsIso), fun hP ↦ le_antisymm ?_ (P.le_isoClosure)⟩
  intro X Y f ⟨X', Y', f', hf', ⟨e⟩⟩
  exact (P.arrow_mk_iso_iff e).1 hf'

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