isoOfComponents — Mathlib

English

A version of hom_ext_iff' specialized to formal coproducts.

Русский

Версия hom_ext_iff', специализирующаяся на формальных копропроизводах.

LaTeX

$$$\\text{Hom\_ext\_iff}'(X,Y,f,g) : (f=g) \\iff \\dots$$$

Lean4

/-- A way to create isomorphisms in the category of formal coproducts, by creating an `Equiv`
between the indexing sets, and then correspondingly isomorphisms of each component. -/
@[simps!]
def isoOfComponents {X Y : FormalCoproduct.{w} C} (e : X.I ≃ Y.I) (h : ∀ i, X.obj i ≅ Y.obj (e i)) : X ≅ Y
    where
  hom := { f := e, φ := fun i ↦ (h i).hom }
  inv := { f := e.symm, φ := fun i ↦ eqToHom (by simp) ≫ (h (e.symm i)).inv }
  hom_inv_id := by ext <;> aesop
  inv_hom_id := by ext <;> aesop

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