English
The cokernel of biproduct.fromSubtype f p is canonically isomorphic to ⨁ Subtype.restrict pᶜ f in the finite setting.
Русский
Коконкурент biproduct.fromSubtype f p изоморфен канонически к ⨁ Subtype.restrict pᶜ f в конечной ситуации.
LaTeX
$$$\\text{cokernel}(\\text{biproduct.fromSubtype } f p) \\cong ⨁ \\text{Subtype.restrict } p^c f$$$
Lean4
/-- The limit cone exhibiting `⨁ Subtype.restrict pᶜ f` as the kernel of
`biproduct.toSubtype f p` -/
@[simps]
def kernelForkBiproductToSubtype (p : Set K) : LimitCone (parallelPair (biproduct.toSubtype f p) 0)
where
cone :=
KernelFork.ofι (biproduct.fromSubtype f pᶜ)
(by
classical
ext j k
simp only [Category.assoc, biproduct.ι_fromSubtype_assoc, biproduct.ι_toSubtype_assoc, comp_zero, zero_comp]
rw [dif_neg k.2]
simp only [zero_comp])
isLimit :=
KernelFork.IsLimit.ofι _ _ (fun {_} g _ => g ≫ biproduct.toSubtype f pᶜ)
(by
classical
intro W' g' w
ext j
simp only [Category.assoc, biproduct.toSubtype_fromSubtype, Pi.compl_apply, biproduct.map_π]
split_ifs with h
· simp
· replace w := w =≫ biproduct.π _ ⟨j, not_not.mp h⟩
simpa using w.symm)
(by cat_disch)
