iso_inv_π — Mathlib

English

The coimage projection after applying F maps to the mapped coimage projection via the inverse of the coimage iso.

Русский

Проекция кообраза после применения F переходит к проекции кообраза после отображения через F с помощью обратного кообразного изоморфизма.

LaTeX

$$$\operatorname{Abelian}.coimage.\pi (F.map f) \;\gg\; (\mathrm{PreservesCoimage.iso} F f).inv = F.map(\operatorname{Abelian}.coimage.\pi f)$$$

Lean4

@[reassoc (attr := simp)]
theorem iso_inv_π : Abelian.coimage.π (F.map f) ≫ (PreservesCoimage.iso F f).inv = F.map (Abelian.coimage.π f) := by
  simp [Iso.comp_inv_eq]

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