range_mkQ_cokernelIsoRangeQuotient_inv

English

The inclusion of the range into H composed with the cokernel inverse map recovers the projection mkQ onto the quotient.

Русский

Включение диапазона в H, затем обратное отображение коканелла, восстанавливает проекцию mkQ на частичное.

LaTeX

$$$$ ofHom(\\operatorname{range}(f.hom).mkQ) \\circ (cokernelIsoRangeQuotient f).inv = cokernel.π f $$$$

Lean4

@[simp, elementwise]
theorem range_mkQ_cokernelIsoRangeQuotient_inv :
    ofHom (LinearMap.range f.hom).mkQ ≫ (cokernelIsoRangeQuotient f).inv = cokernel.π f :=
  colimit.isoColimitCocone_ι_inv ⟨_, cokernelIsColimit f⟩ WalkingParallelPair.one

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