ι_unop — Mathlib

English

The morphism kernel.ι g.unop, taken in the opposite direction, corresponds to cokernel.π g via the kernelUnopOp isomorphism.

Русский

Морфизм kernel.ι g.unop, развёрнутый против, соответствует cokernel.π g через изоморфизм kernelUnopOp.

LaTeX

$$$ (kernel.ι g.unop).op = eqToHom( Opposite.op_unop _) \circ cokernel.π g \circ (kernelUnopOp g)^{-1} $$$

Lean4

theorem ι_unop : (kernel.ι g.unop).op = eqToHom (Opposite.op_unop _) ≫ cokernel.π g ≫ (kernelUnopOp g).inv := by simp

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