ι_toSubtype_subtype — Mathlib

English

The toSubtype and fromSubtype compose to the identity on the biproduct over restricted f.

Русский

Сложение toSubtype и fromSubtype даёт тождественность на биопродукте, ограниченном f.

LaTeX

$$$\\text{toSubtype } f p \\circ \\text{fromSubtype } f p = \\mathrm{Id}_{⨁ f|_{p}}$$$

Lean4

@[reassoc]
theorem ι_toSubtype_subtype (j : Subtype p) :
    biproduct.ι f j ≫ biproduct.toSubtype f p = biproduct.ι (Subtype.restrict p f) j := by
  classical
  ext
  rw [biproduct.toSubtype, Category.assoc, biproduct.lift_π, biproduct.ι_π, biproduct.ι_π]
  split_ifs with h₁ h₂ h₂
  exacts [rfl, False.elim (h₂ (Subtype.ext h₁)), False.elim (h₁ (congr_arg Subtype.val h₂)), rfl]

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