homOfPiHom — Mathlib

English

A family of maps from f j to X yields a morphism in FormalCoproduct.

Русский

Семейство отображений f j → X образует Морфизм в FormalCoproduct.

LaTeX

$$$\\mathrm{homOfPiHom}(X,f,\\phi): \\mathrm{FormalCoproduct}(X) \\to \\mathrm{incl}(X)$$$

Lean4

/-- A family of maps with the same target can be turned into one arrow in the category of formal
coproducts. This is used in Čech cohomology. -/
@[simps!]
def homOfPiHom (X : C) {J : Type w} (f : (j : J) → C) (φ : (j : J) → f j ⟶ X) :
    FormalCoproduct.mk _ f ⟶ (incl C).obj X :=
  ⟨fun _ ↦ PUnit.unit, φ⟩

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