piIsoPi_inv_kernel_ι — Mathlib

English

The inverse of piIsoPi composed with the projection to Z_i is the canonical projection lof.

Русский

Обратный образ от piIsoPi, композиция с проекцией к Z_i дает канониальное отображение lof.

LaTeX

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

Lean4

@[simp, elementwise]
theorem piIsoPi_inv_kernel_ι (i : ι) :
    (piIsoPi Z).inv ≫ Pi.π Z i = ofHom (LinearMap.proj i : (∀ i : ι, Z i) →ₗ[R] Z i) :=
  limit.isoLimitCone_inv_π _ _

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