incl — Mathlib

English

An isomorphism between formal coproducts is determined by an equivalence e of indices and a family of isomorphisms of components.

Русский

Изоморфизм между формальными копроизводами задаётся эквивалентностью индексов и семейством изоморфизмов компонент.

LaTeX

$$$X \\cong Y$ when $e: X.I \\simeq Y.I$ and $\\forall i, X_i \\cong Y_{e(i)}$$$

Lean4

/-- An object of the original category produces a formal coproduct on that object only, so indexed
by `PUnit`, the type with one element. -/
@[simps!]
def incl : C ⥤ FormalCoproduct.{w} C where
  obj X := ⟨PUnit, fun _ ↦ X⟩
  map f := ⟨fun _ ↦ PUnit.unit, fun _ ↦ f⟩

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