W_isoClosure — Mathlib

English

W is closed under taking iso-closures; equating to the iso-closure of W yields equality of the corresponding morphism properties.

Русский

W замкнуто относительно изоморфизмов; приравнивание к изоморфизму замкнутые свойства дают эквивалентность.

LaTeX

$$$W_{isoClosure} = W$$$

Lean4

theorem W_isoClosure : W P.isoClosure = W P := by
  ext X Y f
  constructor
  · intro hf Z hZ
    exact hf _ (P.le_isoClosure _ hZ)
  · rintro hf Z ⟨Z', hZ', ⟨e⟩⟩
    constructor
    · intro g₁ g₂ eq
      rw [← cancel_mono e.hom]
      apply (hf _ hZ').1
      simp only [reassoc_of% eq]
    · intro g
      obtain ⟨a, h⟩ := (hf _ hZ').2 (g ≫ e.hom)
      exact ⟨a ≫ e.inv, by simp only [reassoc_of% h, e.hom_inv_id, comp_id]⟩

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