map_isoClosure — Mathlib

English

For any P and functor F, P.isoClosure.map F equals P.map F.

Русский

Для любого P и функторa F, P.isoClosure.map F совпадает с P.map F.

LaTeX

$$$P.isoClosure.map F = P.map F$$$

Lean4

@[simp]
theorem map_isoClosure (P : MorphismProperty C) (F : C ⥤ D) : P.isoClosure.map F = P.map F :=
  by
  apply le_antisymm
  · rw [map_le_iff]
    intro X Y f ⟨X', Y', f', hf', ⟨e⟩⟩
    exact ⟨_, _, f', hf', ⟨F.mapArrow.mapIso e⟩⟩
  · exact monotone_map _ (le_isoClosure P)

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