piIsoPi_hom_ker_subtype — Mathlib

English

The i-th component of piIsoPi.hom composed with the inclusion is the canonical projection to Z_i.

Русский

Компонента i из piIsoPi.hom после включения равна каноническому проекционному отображению в Z_i.

LaTeX

$$$ (piIsoPi Z).hom \; \circ \; ofHom(DirectSum.lof Z i) = \; Pi.π Z i $$$

Lean4

@[simp, elementwise]
theorem piIsoPi_hom_ker_subtype (i : ι) :
    (piIsoPi Z).hom ≫ ofHom (LinearMap.proj i : (∀ i : ι, Z i) →ₗ[R] Z i) = Pi.π Z i :=
  IsLimit.conePointUniqueUpToIso_inv_comp _ (limit.isLimit _) (Discrete.mk i)

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