trW_isoClosure — Mathlib

English

For any P, the trW-closure and the ordinary trW coincide: P.isoClosure.trW = P.trW.

Русский

Для любого P верно, что замыкание по изоморфизмам сохраняет трW: P.isoClosure.trW = P.trW.

LaTeX

$$$P.isoClosure.trW = P.trW$$$

Lean4

theorem trW_isoClosure : P.isoClosure.trW = P.trW := by
  ext X Y f
  constructor
  · rintro ⟨Z, g, h, mem, ⟨Z', hZ', ⟨e⟩⟩⟩
    refine ⟨Z', g ≫ e.hom, e.inv ≫ h, isomorphic_distinguished _ mem _ ?_, hZ'⟩
    exact Triangle.isoMk _ _ (Iso.refl _) (Iso.refl _) e.symm
  · rintro ⟨Z, g, h, mem, hZ⟩
    exact ⟨Z, g, h, mem, ObjectProperty.le_isoClosure _ _ hZ⟩

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