π — Mathlib · SciLib

English

The fan of a product-triangle is the canonical cone to the product, i.e., a family of maps from a single object to each component, compatible with the product-triangle projections.

Русский

Фан произведения треугольников — это канонический конус к произведению, т.е. семья отображений из одного объекта в каждый компонент, совместимая с проекторами треугольника.

LaTeX

$$Fan.mk (productTriangle T) (productTriangle.π T)$$

Lean4

/-- A projection from the product of a family of triangles. -/
@[simps]
def π (j : J) : productTriangle T ⟶ T j where
  hom₁ := Pi.π _ j
  hom₂ := Pi.π _ j
  hom₃ := Pi.π _ j
  comm₃ := by
    dsimp
    rw [← piComparison_comp_π, assoc, IsIso.inv_hom_id_assoc]
    simp only [limMap_π, Discrete.natTrans_app]

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